:: ORDINAL4 semantic presentation
begin
Lm1: {} in omega
by ORDINAL1:def_11;
Lm2: omega is limit_ordinal
by ORDINAL1:def_11;
Lm3: 1 = succ {}
;
registration
let L be Ordinal-Sequence;
cluster last L -> ordinal ;
coherence
last L is ordinal ;
end;
theorem :: ORDINAL4:1
for fi being Ordinal-Sequence
for A being Ordinal st dom fi = succ A holds
( last fi is_limes_of fi & lim fi = last fi )
proof
let fi be Ordinal-Sequence; ::_thesis: for A being Ordinal st dom fi = succ A holds
( last fi is_limes_of fi & lim fi = last fi )
let A be Ordinal; ::_thesis: ( dom fi = succ A implies ( last fi is_limes_of fi & lim fi = last fi ) )
assume A1: dom fi = succ A ; ::_thesis: ( last fi is_limes_of fi & lim fi = last fi )
then A2: last fi = fi . A by ORDINAL2:6;
thus last fi is_limes_of fi ::_thesis: lim fi = last fi
proof
percases ( last fi = {} or last fi <> {} ) ;
:: according to ORDINAL2:def_9
caseA3: last fi = {} ; ::_thesis: ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or fi . b2 = {} ) ) )
take A ; ::_thesis: ( A in dom fi & ( for b1 being set holds
( not A c= b1 or not b1 in dom fi or fi . b1 = {} ) ) )
thus A in dom fi by A1, ORDINAL1:6; ::_thesis: for b1 being set holds
( not A c= b1 or not b1 in dom fi or fi . b1 = {} )
let B be Ordinal; ::_thesis: ( not A c= B or not B in dom fi or fi . B = {} )
assume that
A4: A c= B and
A5: B in dom fi ; ::_thesis: fi . B = {}
B c= A by A1, A5, ORDINAL1:22;
hence fi . B = {} by A2, A3, A4, XBOOLE_0:def_10; ::_thesis: verum
end;
case last fi <> {} ; ::_thesis: for b1, b2 being set holds
( not b1 in last fi or not last fi in b2 or ex b3 being set st
( b3 in dom fi & ( for b4 being set holds
( not b3 c= b4 or not b4 in dom fi or ( b1 in fi . b4 & fi . b4 in b2 ) ) ) ) )
let B, C be Ordinal; ::_thesis: ( not B in last fi or not last fi in C or ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or ( B in fi . b2 & fi . b2 in C ) ) ) ) )
assume that
A6: B in last fi and
A7: last fi in C ; ::_thesis: ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or ( B in fi . b2 & fi . b2 in C ) ) ) )
take A ; ::_thesis: ( A in dom fi & ( for b1 being set holds
( not A c= b1 or not b1 in dom fi or ( B in fi . b1 & fi . b1 in C ) ) ) )
thus A in dom fi by A1, ORDINAL1:6; ::_thesis: for b1 being set holds
( not A c= b1 or not b1 in dom fi or ( B in fi . b1 & fi . b1 in C ) )
let D be Ordinal; ::_thesis: ( not A c= D or not D in dom fi or ( B in fi . D & fi . D in C ) )
assume that
A8: A c= D and
A9: D in dom fi ; ::_thesis: ( B in fi . D & fi . D in C )
D c= A by A1, A9, ORDINAL1:22;
hence ( B in fi . D & fi . D in C ) by A2, A6, A7, A8, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
end;
hence lim fi = last fi by ORDINAL2:def_10; ::_thesis: verum
end;
definition
let fi, psi be T-Sequence;
funcfi ^ psi -> T-Sequence means :Def1: :: ORDINAL4:def 1
( dom it = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
it . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
it . ((dom fi) +^ A) = psi . A ) );
existence
ex b1 being T-Sequence st
( dom b1 = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
b1 . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
b1 . ((dom fi) +^ A) = psi . A ) )
proof
defpred S1[ set ] means $1 in dom fi;
deffunc H1( Ordinal) -> set = psi . ($1 -^ (dom fi));
deffunc H2( set ) -> set = fi . $1;
consider f being Function such that
A1: dom f = (dom fi) +^ (dom psi) and
A2: for x being Ordinal st x in (dom fi) +^ (dom psi) holds
( ( S1[x] implies f . x = H2(x) ) & ( not S1[x] implies f . x = H1(x) ) ) from FINSET_1:sch_1();
reconsider f = f as T-Sequence by A1, ORDINAL1:def_7;
take f ; ::_thesis: ( dom f = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
f . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
f . ((dom fi) +^ A) = psi . A ) )
thus dom f = (dom fi) +^ (dom psi) by A1; ::_thesis: ( ( for A being Ordinal st A in dom fi holds
f . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
f . ((dom fi) +^ A) = psi . A ) )
thus for A being Ordinal st A in dom fi holds
f . A = fi . A ::_thesis: for A being Ordinal st A in dom psi holds
f . ((dom fi) +^ A) = psi . A
proof
A3: dom fi c= dom f by A1, ORDINAL3:24;
let A be Ordinal; ::_thesis: ( A in dom fi implies f . A = fi . A )
assume A in dom fi ; ::_thesis: f . A = fi . A
hence f . A = fi . A by A1, A2, A3; ::_thesis: verum
end;
let A be Ordinal; ::_thesis: ( A in dom psi implies f . ((dom fi) +^ A) = psi . A )
dom fi c= (dom fi) +^ A by ORDINAL3:24;
then A4: not (dom fi) +^ A in dom fi by ORDINAL1:5;
assume A in dom psi ; ::_thesis: f . ((dom fi) +^ A) = psi . A
then (dom fi) +^ A in dom f by A1, ORDINAL2:32;
then f . ((dom fi) +^ A) = psi . (((dom fi) +^ A) -^ (dom fi)) by A1, A2, A4;
hence f . ((dom fi) +^ A) = psi . A by ORDINAL3:52; ::_thesis: verum
end;
uniqueness
for b1, b2 being T-Sequence st dom b1 = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
b1 . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
b1 . ((dom fi) +^ A) = psi . A ) & dom b2 = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
b2 . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
b2 . ((dom fi) +^ A) = psi . A ) holds
b1 = b2
proof
let f1, f2 be T-Sequence; ::_thesis: ( dom f1 = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
f1 . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
f1 . ((dom fi) +^ A) = psi . A ) & dom f2 = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
f2 . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
f2 . ((dom fi) +^ A) = psi . A ) implies f1 = f2 )
assume that
A5: dom f1 = (dom fi) +^ (dom psi) and
A6: for A being Ordinal st A in dom fi holds
f1 . A = fi . A and
A7: for A being Ordinal st A in dom psi holds
f1 . ((dom fi) +^ A) = psi . A and
A8: dom f2 = (dom fi) +^ (dom psi) and
A9: for A being Ordinal st A in dom fi holds
f2 . A = fi . A and
A10: for A being Ordinal st A in dom psi holds
f2 . ((dom fi) +^ A) = psi . A ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_set_st_x_in_(dom_fi)_+^_(dom_psi)_holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in (dom fi) +^ (dom psi) implies f1 . x = f2 . x )
assume A11: x in (dom fi) +^ (dom psi) ; ::_thesis: f1 . x = f2 . x
then reconsider A = x as Ordinal ;
now__::_thesis:_f1_._x_=_f2_._x
percases ( x in dom fi or not x in dom fi ) ;
supposeA12: x in dom fi ; ::_thesis: f1 . x = f2 . x
then f1 . A = fi . A by A6;
hence f1 . x = f2 . x by A9, A12; ::_thesis: verum
end;
suppose not x in dom fi ; ::_thesis: f1 . x = f2 . x
then dom fi c= A by ORDINAL1:16;
then A13: (dom fi) +^ (A -^ (dom fi)) = A by ORDINAL3:def_5;
then f1 . A = psi . (A -^ (dom fi)) by A7, A11, ORDINAL3:22;
hence f1 . x = f2 . x by A10, A11, A13, ORDINAL3:22; ::_thesis: verum
end;
end;
end;
hence f1 . x = f2 . x ; ::_thesis: verum
end;
hence f1 = f2 by A5, A8, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines ^ ORDINAL4:def_1_:_
for fi, psi, b3 being T-Sequence holds
( b3 = fi ^ psi iff ( dom b3 = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
b3 . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
b3 . ((dom fi) +^ A) = psi . A ) ) );
theorem Th2: :: ORDINAL4:2
for fi, psi being Ordinal-Sequence holds rng (fi ^ psi) c= (rng fi) \/ (rng psi)
proof
let fi, psi be Ordinal-Sequence; ::_thesis: rng (fi ^ psi) c= (rng fi) \/ (rng psi)
set f = fi ^ psi;
set A1 = rng fi;
set A2 = rng psi;
A1: dom (fi ^ psi) = (dom fi) +^ (dom psi) by Def1;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (fi ^ psi) or y in (rng fi) \/ (rng psi) )
assume y in rng (fi ^ psi) ; ::_thesis: y in (rng fi) \/ (rng psi)
then consider x being set such that
A2: x in dom (fi ^ psi) and
A3: y = (fi ^ psi) . x by FUNCT_1:def_3;
reconsider x = x as Ordinal by A2;
percases ( x in dom fi or not x in dom fi ) ;
supposeA4: x in dom fi ; ::_thesis: y in (rng fi) \/ (rng psi)
then A5: fi . x in rng fi by FUNCT_1:def_3;
y = fi . x by A3, A4, Def1;
then y in rng fi by A5;
hence y in (rng fi) \/ (rng psi) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose not x in dom fi ; ::_thesis: y in (rng fi) \/ (rng psi)
then dom fi c= x by ORDINAL1:16;
then A6: (dom fi) +^ (x -^ (dom fi)) = x by ORDINAL3:def_5;
then A7: x -^ (dom fi) in dom psi by A1, A2, ORDINAL3:22;
then y = psi . (x -^ (dom fi)) by A3, A6, Def1;
then y in rng psi by A7, FUNCT_1:def_3;
then y in rng psi ;
hence y in (rng fi) \/ (rng psi) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
registration
let fi, psi be Ordinal-Sequence;
clusterfi ^ psi -> Ordinal-yielding ;
coherence
fi ^ psi is Ordinal-yielding
proof
set f = fi ^ psi;
consider A1 being Ordinal such that
A1: rng fi c= A1 by ORDINAL2:def_4;
consider A2 being Ordinal such that
A2: rng psi c= A2 by ORDINAL2:def_4;
A3: A2 c= A1 +^ A2 by ORDINAL3:24;
A1 c= A1 +^ A2 by ORDINAL3:24;
then A4: A1 \/ A2 c= A1 +^ A2 by A3, XBOOLE_1:8;
A5: rng (fi ^ psi) c= (rng fi) \/ (rng psi) by Th2;
(rng fi) \/ (rng psi) c= A1 \/ A2 by A1, A2, XBOOLE_1:13;
then rng (fi ^ psi) c= A1 \/ A2 by A5, XBOOLE_1:1;
then rng (fi ^ psi) c= A1 +^ A2 by A4, XBOOLE_1:1;
hence fi ^ psi is Ordinal-yielding by ORDINAL2:def_4; ::_thesis: verum
end;
end;
theorem Th3: :: ORDINAL4:3
for psi, fi being Ordinal-Sequence
for A being Ordinal st A is_limes_of psi holds
A is_limes_of fi ^ psi
proof
let psi, fi be Ordinal-Sequence; ::_thesis: for A being Ordinal st A is_limes_of psi holds
A is_limes_of fi ^ psi
let A be Ordinal; ::_thesis: ( A is_limes_of psi implies A is_limes_of fi ^ psi )
assume A1: ( ( A = {} & ex B being Ordinal st
( B in dom psi & ( for C being Ordinal st B c= C & C in dom psi holds
psi . C = {} ) ) ) or ( A <> {} & ( for B, C being Ordinal st B in A & A in C holds
ex D being Ordinal st
( D in dom psi & ( for E being Ordinal st D c= E & E in dom psi holds
( B in psi . E & psi . E in C ) ) ) ) ) ) ; :: according to ORDINAL2:def_9 ::_thesis: A is_limes_of fi ^ psi
A2: dom (fi ^ psi) = (dom fi) +^ (dom psi) by Def1;
percases ( A = {} or A <> {} ) ;
:: according to ORDINAL2:def_9
case A = {} ; ::_thesis: ex b1 being set st
( b1 in dom (fi ^ psi) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (fi ^ psi) or (fi ^ psi) . b2 = {} ) ) )
then consider B being Ordinal such that
A3: B in dom psi and
A4: for C being Ordinal st B c= C & C in dom psi holds
psi . C = {} by A1;
take B1 = (dom fi) +^ B; ::_thesis: ( B1 in dom (fi ^ psi) & ( for b1 being set holds
( not B1 c= b1 or not b1 in dom (fi ^ psi) or (fi ^ psi) . b1 = {} ) ) )
thus B1 in dom (fi ^ psi) by A2, A3, ORDINAL2:32; ::_thesis: for b1 being set holds
( not B1 c= b1 or not b1 in dom (fi ^ psi) or (fi ^ psi) . b1 = {} )
let C be Ordinal; ::_thesis: ( not B1 c= C or not C in dom (fi ^ psi) or (fi ^ psi) . C = {} )
assume that
A5: B1 c= C and
A6: C in dom (fi ^ psi) ; ::_thesis: (fi ^ psi) . C = {}
A7: C = B1 +^ (C -^ B1) by A5, ORDINAL3:def_5
.= (dom fi) +^ (B +^ (C -^ B1)) by ORDINAL3:30 ;
then A8: B +^ (C -^ B1) in dom psi by A2, A6, ORDINAL3:22;
B c= B +^ (C -^ B1) by ORDINAL3:24;
then psi . (B +^ (C -^ B1)) = {} by A2, A4, A6, A7, ORDINAL3:22;
hence (fi ^ psi) . C = {} by A7, A8, Def1; ::_thesis: verum
end;
case A <> {} ; ::_thesis: for b1, b2 being set holds
( not b1 in A or not A in b2 or ex b3 being set st
( b3 in dom (fi ^ psi) & ( for b4 being set holds
( not b3 c= b4 or not b4 in dom (fi ^ psi) or ( b1 in (fi ^ psi) . b4 & (fi ^ psi) . b4 in b2 ) ) ) ) )
let B, C be Ordinal; ::_thesis: ( not B in A or not A in C or ex b1 being set st
( b1 in dom (fi ^ psi) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (fi ^ psi) or ( B in (fi ^ psi) . b2 & (fi ^ psi) . b2 in C ) ) ) ) )
assume that
A9: B in A and
A10: A in C ; ::_thesis: ex b1 being set st
( b1 in dom (fi ^ psi) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (fi ^ psi) or ( B in (fi ^ psi) . b2 & (fi ^ psi) . b2 in C ) ) ) )
consider D being Ordinal such that
A11: D in dom psi and
A12: for E being Ordinal st D c= E & E in dom psi holds
( B in psi . E & psi . E in C ) by A1, A9, A10;
take D1 = (dom fi) +^ D; ::_thesis: ( D1 in dom (fi ^ psi) & ( for b1 being set holds
( not D1 c= b1 or not b1 in dom (fi ^ psi) or ( B in (fi ^ psi) . b1 & (fi ^ psi) . b1 in C ) ) ) )
thus D1 in dom (fi ^ psi) by A2, A11, ORDINAL2:32; ::_thesis: for b1 being set holds
( not D1 c= b1 or not b1 in dom (fi ^ psi) or ( B in (fi ^ psi) . b1 & (fi ^ psi) . b1 in C ) )
let E be Ordinal; ::_thesis: ( not D1 c= E or not E in dom (fi ^ psi) or ( B in (fi ^ psi) . E & (fi ^ psi) . E in C ) )
assume that
A13: D1 c= E and
A14: E in dom (fi ^ psi) ; ::_thesis: ( B in (fi ^ psi) . E & (fi ^ psi) . E in C )
A15: D c= D +^ (E -^ D1) by ORDINAL3:24;
A16: E = D1 +^ (E -^ D1) by A13, ORDINAL3:def_5
.= (dom fi) +^ (D +^ (E -^ D1)) by ORDINAL3:30 ;
then A17: D +^ (E -^ D1) in dom psi by A2, A14, ORDINAL3:22;
then (fi ^ psi) . E = psi . (D +^ (E -^ D1)) by A16, Def1;
hence ( B in (fi ^ psi) . E & (fi ^ psi) . E in C ) by A12, A15, A17; ::_thesis: verum
end;
end;
end;
theorem :: ORDINAL4:4
for fi being Ordinal-Sequence
for A, B being Ordinal st A is_limes_of fi holds
B +^ A is_limes_of B +^ fi
proof
let fi be Ordinal-Sequence; ::_thesis: for A, B being Ordinal st A is_limes_of fi holds
B +^ A is_limes_of B +^ fi
let A, B be Ordinal; ::_thesis: ( A is_limes_of fi implies B +^ A is_limes_of B +^ fi )
assume A1: ( ( A = {} & ex B being Ordinal st
( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = {} ) ) ) or ( A <> {} & ( for B, C being Ordinal st B in A & A in C holds
ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) ) ) ) ) ; :: according to ORDINAL2:def_9 ::_thesis: B +^ A is_limes_of B +^ fi
A2: dom fi = dom (B +^ fi) by ORDINAL3:def_1;
percases ( B +^ A = {} or B +^ A <> {} ) ;
:: according to ORDINAL2:def_9
caseA3: B +^ A = {} ; ::_thesis: ex b1 being set st
( b1 in dom (B +^ fi) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (B +^ fi) or (B +^ fi) . b2 = {} ) ) )
then consider A1 being Ordinal such that
A4: A1 in dom fi and
A5: for C being Ordinal st A1 c= C & C in dom fi holds
fi . C = {} by A1, ORDINAL3:26;
take A1 ; ::_thesis: ( A1 in dom (B +^ fi) & ( for b1 being set holds
( not A1 c= b1 or not b1 in dom (B +^ fi) or (B +^ fi) . b1 = {} ) ) )
thus A1 in dom (B +^ fi) by A4, ORDINAL3:def_1; ::_thesis: for b1 being set holds
( not A1 c= b1 or not b1 in dom (B +^ fi) or (B +^ fi) . b1 = {} )
let C be Ordinal; ::_thesis: ( not A1 c= C or not C in dom (B +^ fi) or (B +^ fi) . C = {} )
assume that
A6: A1 c= C and
A7: C in dom (B +^ fi) ; ::_thesis: (B +^ fi) . C = {}
A8: (B +^ fi) . C = B +^ (fi . C) by A2, A7, ORDINAL3:def_1;
fi . C = {} by A2, A5, A6, A7;
hence (B +^ fi) . C = {} by A3, A8, ORDINAL3:26; ::_thesis: verum
end;
case B +^ A <> {} ; ::_thesis: for b1, b2 being set holds
( not b1 in B +^ A or not B +^ A in b2 or ex b3 being set st
( b3 in dom (B +^ fi) & ( for b4 being set holds
( not b3 c= b4 or not b4 in dom (B +^ fi) or ( b1 in (B +^ fi) . b4 & (B +^ fi) . b4 in b2 ) ) ) ) )
now__::_thesis:_for_B1,_B2_being_Ordinal_st_B1_in_B_+^_A_&_B_+^_A_in_B2_holds_
ex_A1_being_Ordinal_st_
(_A1_in_dom_(B_+^_fi)_&_(_for_C_being_Ordinal_st_A1_c=_C_&_C_in_dom_(B_+^_fi)_holds_
(_B1_in_(B_+^_fi)_._C_&_(B_+^_fi)_._C_in_B2_)_)_)
percases ( A = {} or A <> {} ) ;
supposeA9: A = {} ; ::_thesis: for B1, B2 being Ordinal st B1 in B +^ A & B +^ A in B2 holds
ex A1 being Ordinal st
( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )
then consider A1 being Ordinal such that
A10: A1 in dom fi and
A11: for C being Ordinal st A1 c= C & C in dom fi holds
fi . C = {} by A1;
let B1, B2 be Ordinal; ::_thesis: ( B1 in B +^ A & B +^ A in B2 implies ex A1 being Ordinal st
( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) ) )
assume that
A12: B1 in B +^ A and
A13: B +^ A in B2 ; ::_thesis: ex A1 being Ordinal st
( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )
take A1 = A1; ::_thesis: ( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )
thus A1 in dom (B +^ fi) by A10, ORDINAL3:def_1; ::_thesis: for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 )
let C be Ordinal; ::_thesis: ( A1 c= C & C in dom (B +^ fi) implies ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) )
assume that
A14: A1 c= C and
A15: C in dom (B +^ fi) ; ::_thesis: ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 )
(B +^ fi) . C = B +^ (fi . C) by A2, A15, ORDINAL3:def_1;
hence ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) by A2, A9, A11, A12, A13, A14, A15; ::_thesis: verum
end;
supposeA16: A <> {} ; ::_thesis: for B1, B2 being Ordinal st B1 in B +^ A & B +^ A in B2 holds
ex A1 being Ordinal st
( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )
let B1, B2 be Ordinal; ::_thesis: ( B1 in B +^ A & B +^ A in B2 implies ex A1 being Ordinal st
( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) ) )
assume that
A17: B1 in B +^ A and
A18: B +^ A in B2 ; ::_thesis: ex A1 being Ordinal st
( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )
B1 -^ B in A by A16, A17, ORDINAL3:60;
then consider A1 being Ordinal such that
A19: A1 in dom fi and
A20: for C being Ordinal st A1 c= C & C in dom fi holds
( B1 -^ B in fi . C & fi . C in B2 -^ B ) by A1, A18, ORDINAL3:61;
A21: B1 c= B +^ (B1 -^ B) by ORDINAL3:62;
A22: B c= B +^ A by ORDINAL3:24;
B +^ A c= B2 by A18, ORDINAL1:def_2;
then B c= B2 by A22, XBOOLE_1:1;
then A23: B +^ (B2 -^ B) = B2 by ORDINAL3:def_5;
take A1 = A1; ::_thesis: ( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )
thus A1 in dom (B +^ fi) by A19, ORDINAL3:def_1; ::_thesis: for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 )
let C be Ordinal; ::_thesis: ( A1 c= C & C in dom (B +^ fi) implies ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) )
assume that
A24: A1 c= C and
A25: C in dom (B +^ fi) ; ::_thesis: ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 )
A26: (B +^ fi) . C = B +^ (fi . C) by A2, A25, ORDINAL3:def_1;
reconsider E = fi . C as Ordinal ;
B1 -^ B in E by A2, A20, A24, A25;
then A27: B +^ (B1 -^ B) in B +^ E by ORDINAL2:32;
E in B2 -^ B by A2, A20, A24, A25;
hence ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) by A21, A26, A23, A27, ORDINAL1:12, ORDINAL2:32; ::_thesis: verum
end;
end;
end;
hence for b1, b2 being set holds
( not b1 in B +^ A or not B +^ A in b2 or ex b3 being set st
( b3 in dom (B +^ fi) & ( for b4 being set holds
( not b3 c= b4 or not b4 in dom (B +^ fi) or ( b1 in (B +^ fi) . b4 & (B +^ fi) . b4 in b2 ) ) ) ) ) ; ::_thesis: verum
end;
end;
end;
Lm4: for fi being Ordinal-Sequence
for A being Ordinal st A is_limes_of fi holds
dom fi <> {}
proof
let fi be Ordinal-Sequence; ::_thesis: for A being Ordinal st A is_limes_of fi holds
dom fi <> {}
let A be Ordinal; ::_thesis: ( A is_limes_of fi implies dom fi <> {} )
assume A1: ( ( A = {} & ex B being Ordinal st
( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = {} ) ) ) or ( A <> {} & ( for B, C being Ordinal st B in A & A in C holds
ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) ) ) ) ) ; :: according to ORDINAL2:def_9 ::_thesis: dom fi <> {}
now__::_thesis:_dom_fi_<>_{}
percases ( A = {} or A <> {} ) ;
suppose A = {} ; ::_thesis: dom fi <> {}
hence dom fi <> {} by A1; ::_thesis: verum
end;
suppose A <> {} ; ::_thesis: dom fi <> {}
then {} in A by ORDINAL3:8;
then ex B being Ordinal st
( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
( {} in fi . C & fi . C in succ A ) ) ) by A1, ORDINAL1:6;
hence dom fi <> {} ; ::_thesis: verum
end;
end;
end;
hence dom fi <> {} ; ::_thesis: verum
end;
theorem Th5: :: ORDINAL4:5
for fi being Ordinal-Sequence
for A, B being Ordinal st A is_limes_of fi holds
A *^ B is_limes_of fi *^ B
proof
let fi be Ordinal-Sequence; ::_thesis: for A, B being Ordinal st A is_limes_of fi holds
A *^ B is_limes_of fi *^ B
let A, B be Ordinal; ::_thesis: ( A is_limes_of fi implies A *^ B is_limes_of fi *^ B )
A1: dom fi = dom (fi *^ B) by ORDINAL3:def_4;
assume A2: A is_limes_of fi ; ::_thesis: A *^ B is_limes_of fi *^ B
then A3: dom fi <> {} by Lm4;
percases ( A *^ B = {} or A *^ B <> {} ) ;
:: according to ORDINAL2:def_9
case A *^ B = {} ; ::_thesis: ex b1 being set st
( b1 in dom (fi *^ B) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (fi *^ B) or (fi *^ B) . b2 = {} ) ) )
then A4: ( B = {} or A = {} ) by ORDINAL3:31;
now__::_thesis:_ex_A1_being_Ordinal_st_
(_A1_in_dom_(fi_*^_B)_&_(_for_C_being_Ordinal_st_A1_c=_C_&_C_in_dom_(fi_*^_B)_holds_
(fi_*^_B)_._C_=_{}_)_)
percases ( B = {} or B <> {} ) ;
supposeA5: B = {} ; ::_thesis: ex A1 being Ordinal st
( A1 in dom (fi *^ B) & ( for C being Ordinal st A1 c= C & C in dom (fi *^ B) holds
(fi *^ B) . C = {} ) )
set x = the Element of dom fi;
reconsider x = the Element of dom fi as Ordinal ;
take A1 = x; ::_thesis: ( A1 in dom (fi *^ B) & ( for C being Ordinal st A1 c= C & C in dom (fi *^ B) holds
(fi *^ B) . C = {} ) )
thus A1 in dom (fi *^ B) by A1, A3; ::_thesis: for C being Ordinal st A1 c= C & C in dom (fi *^ B) holds
(fi *^ B) . C = {}
let C be Ordinal; ::_thesis: ( A1 c= C & C in dom (fi *^ B) implies (fi *^ B) . C = {} )
assume that
A1 c= C and
A6: C in dom (fi *^ B) ; ::_thesis: (fi *^ B) . C = {}
thus (fi *^ B) . C = (fi . C) *^ B by A1, A6, ORDINAL3:def_4
.= {} by A5, ORDINAL2:38 ; ::_thesis: verum
end;
suppose B <> {} ; ::_thesis: ex A1 being Ordinal st
( A1 in dom (fi *^ B) & ( for C being Ordinal st A1 c= C & C in dom (fi *^ B) holds
(fi *^ B) . C = {} ) )
then consider A1 being Ordinal such that
A7: A1 in dom fi and
A8: for C being Ordinal st A1 c= C & C in dom fi holds
fi . C = {} by A2, A4, ORDINAL2:def_9;
take A1 = A1; ::_thesis: ( A1 in dom (fi *^ B) & ( for C being Ordinal st A1 c= C & C in dom (fi *^ B) holds
(fi *^ B) . C = {} ) )
thus A1 in dom (fi *^ B) by A7, ORDINAL3:def_4; ::_thesis: for C being Ordinal st A1 c= C & C in dom (fi *^ B) holds
(fi *^ B) . C = {}
let C be Ordinal; ::_thesis: ( A1 c= C & C in dom (fi *^ B) implies (fi *^ B) . C = {} )
assume that
A9: A1 c= C and
A10: C in dom (fi *^ B) ; ::_thesis: (fi *^ B) . C = {}
A11: (fi *^ B) . C = (fi . C) *^ B by A1, A10, ORDINAL3:def_4;
fi . C = {} by A1, A8, A9, A10;
hence (fi *^ B) . C = {} by A11, ORDINAL2:35; ::_thesis: verum
end;
end;
end;
hence ex b1 being set st
( b1 in dom (fi *^ B) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (fi *^ B) or (fi *^ B) . b2 = {} ) ) ) ; ::_thesis: verum
end;
caseA12: A *^ B <> {} ; ::_thesis: for b1, b2 being set holds
( not b1 in A *^ B or not A *^ B in b2 or ex b3 being set st
( b3 in dom (fi *^ B) & ( for b4 being set holds
( not b3 c= b4 or not b4 in dom (fi *^ B) or ( b1 in (fi *^ B) . b4 & (fi *^ B) . b4 in b2 ) ) ) ) )
let B1, B2 be Ordinal; ::_thesis: ( not B1 in A *^ B or not A *^ B in B2 or ex b1 being set st
( b1 in dom (fi *^ B) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (fi *^ B) or ( B1 in (fi *^ B) . b2 & (fi *^ B) . b2 in B2 ) ) ) ) )
assume that
A13: B1 in A *^ B and
A14: A *^ B in B2 ; ::_thesis: ex b1 being set st
( b1 in dom (fi *^ B) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (fi *^ B) or ( B1 in (fi *^ B) . b2 & (fi *^ B) . b2 in B2 ) ) ) )
A15: B <> {} by A12, ORDINAL2:38;
A16: now__::_thesis:_(_(_for_A1_being_Ordinal_holds_not_A_=_succ_A1_)_implies_ex_D_being_Ordinal_st_
(_D_in_dom_(fi_*^_B)_&_(_for_A1_being_Ordinal_st_D_c=_A1_&_A1_in_dom_(fi_*^_B)_holds_
(_B1_in_(fi_*^_B)_._A1_&_(fi_*^_B)_._A1_in_B2_)_)_)_)
assume for A1 being Ordinal holds not A = succ A1 ; ::_thesis: ex D being Ordinal st
( D in dom (fi *^ B) & ( for A1 being Ordinal st D c= A1 & A1 in dom (fi *^ B) holds
( B1 in (fi *^ B) . A1 & (fi *^ B) . A1 in B2 ) ) )
then A is limit_ordinal by ORDINAL1:29;
then consider C being Ordinal such that
A17: C in A and
A18: B1 in C *^ B by A13, ORDINAL3:41;
A in succ A by ORDINAL1:6;
then consider D being Ordinal such that
A19: D in dom fi and
A20: for A1 being Ordinal st D c= A1 & A1 in dom fi holds
( C in fi . A1 & fi . A1 in succ A ) by A2, A17, ORDINAL2:def_9;
take D = D; ::_thesis: ( D in dom (fi *^ B) & ( for A1 being Ordinal st D c= A1 & A1 in dom (fi *^ B) holds
( B1 in (fi *^ B) . A1 & (fi *^ B) . A1 in B2 ) ) )
thus D in dom (fi *^ B) by A19, ORDINAL3:def_4; ::_thesis: for A1 being Ordinal st D c= A1 & A1 in dom (fi *^ B) holds
( B1 in (fi *^ B) . A1 & (fi *^ B) . A1 in B2 )
let A1 be Ordinal; ::_thesis: ( D c= A1 & A1 in dom (fi *^ B) implies ( B1 in (fi *^ B) . A1 & (fi *^ B) . A1 in B2 ) )
assume that
A21: D c= A1 and
A22: A1 in dom (fi *^ B) ; ::_thesis: ( B1 in (fi *^ B) . A1 & (fi *^ B) . A1 in B2 )
reconsider E = fi . A1 as Ordinal ;
fi . A1 in succ A by A1, A20, A21, A22;
then A23: E c= A by ORDINAL1:22;
C in fi . A1 by A1, A20, A21, A22;
then C *^ B in E *^ B by A15, ORDINAL2:40;
then A24: B1 in E *^ B by A18, ORDINAL1:10;
(fi *^ B) . A1 = (fi . A1) *^ B by A1, A22, ORDINAL3:def_4;
hence ( B1 in (fi *^ B) . A1 & (fi *^ B) . A1 in B2 ) by A14, A23, A24, ORDINAL1:12, ORDINAL2:41; ::_thesis: verum
end;
now__::_thesis:_(_ex_A1_being_Ordinal_st_A_=_succ_A1_implies_ex_D_being_Ordinal_st_
(_D_in_dom_(fi_*^_B)_&_(_for_C_being_Ordinal_st_D_c=_C_&_C_in_dom_(fi_*^_B)_holds_
(_B1_in_(fi_*^_B)_._C_&_(fi_*^_B)_._C_in_B2_)_)_)_)
A25: A in succ A by ORDINAL1:6;
given A1 being Ordinal such that A26: A = succ A1 ; ::_thesis: ex D being Ordinal st
( D in dom (fi *^ B) & ( for C being Ordinal st D c= C & C in dom (fi *^ B) holds
( B1 in (fi *^ B) . C & (fi *^ B) . C in B2 ) ) )
A1 in A by A26, ORDINAL1:6;
then consider D being Ordinal such that
A27: D in dom fi and
A28: for C being Ordinal st D c= C & C in dom fi holds
( A1 in fi . C & fi . C in succ A ) by A2, A25, ORDINAL2:def_9;
take D = D; ::_thesis: ( D in dom (fi *^ B) & ( for C being Ordinal st D c= C & C in dom (fi *^ B) holds
( B1 in (fi *^ B) . C & (fi *^ B) . C in B2 ) ) )
thus D in dom (fi *^ B) by A27, ORDINAL3:def_4; ::_thesis: for C being Ordinal st D c= C & C in dom (fi *^ B) holds
( B1 in (fi *^ B) . C & (fi *^ B) . C in B2 )
let C be Ordinal; ::_thesis: ( D c= C & C in dom (fi *^ B) implies ( B1 in (fi *^ B) . C & (fi *^ B) . C in B2 ) )
assume that
A29: D c= C and
A30: C in dom (fi *^ B) ; ::_thesis: ( B1 in (fi *^ B) . C & (fi *^ B) . C in B2 )
reconsider E = fi . C as Ordinal ;
A1 in E by A1, A28, A29, A30;
then A31: A c= E by A26, ORDINAL1:21;
E in succ A by A1, A28, A29, A30;
then A32: E c= A by ORDINAL1:22;
(fi *^ B) . C = E *^ B by A1, A30, ORDINAL3:def_4;
hence ( B1 in (fi *^ B) . C & (fi *^ B) . C in B2 ) by A13, A14, A31, A32, XBOOLE_0:def_10; ::_thesis: verum
end;
hence ex b1 being set st
( b1 in dom (fi *^ B) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (fi *^ B) or ( B1 in (fi *^ B) . b2 & (fi *^ B) . b2 in B2 ) ) ) ) by A16; ::_thesis: verum
end;
end;
end;
theorem Th6: :: ORDINAL4:6
for fi, psi being Ordinal-Sequence
for B, C being Ordinal st dom fi = dom psi & B is_limes_of fi & C is_limes_of psi & ( for A being Ordinal st A in dom fi holds
fi . A c= psi . A or for A being Ordinal st A in dom fi holds
fi . A in psi . A ) holds
B c= C
proof
let fi, psi be Ordinal-Sequence; ::_thesis: for B, C being Ordinal st dom fi = dom psi & B is_limes_of fi & C is_limes_of psi & ( for A being Ordinal st A in dom fi holds
fi . A c= psi . A or for A being Ordinal st A in dom fi holds
fi . A in psi . A ) holds
B c= C
let B, C be Ordinal; ::_thesis: ( dom fi = dom psi & B is_limes_of fi & C is_limes_of psi & ( for A being Ordinal st A in dom fi holds
fi . A c= psi . A or for A being Ordinal st A in dom fi holds
fi . A in psi . A ) implies B c= C )
assume that
A1: dom fi = dom psi and
A2: ( ( B = {} & ex A1 being Ordinal st
( A1 in dom fi & ( for C being Ordinal st A1 c= C & C in dom fi holds
fi . C = {} ) ) ) or ( B <> {} & ( for A1, C being Ordinal st A1 in B & B in C holds
ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( A1 in fi . E & fi . E in C ) ) ) ) ) ) and
A3: ( ( C = {} & ex B being Ordinal st
( B in dom psi & ( for A1 being Ordinal st B c= A1 & A1 in dom psi holds
psi . A1 = {} ) ) ) or ( C <> {} & ( for B, A1 being Ordinal st B in C & C in A1 holds
ex D being Ordinal st
( D in dom psi & ( for E being Ordinal st D c= E & E in dom psi holds
( B in psi . E & psi . E in A1 ) ) ) ) ) ) and
A4: ( for A being Ordinal st A in dom fi holds
fi . A c= psi . A or for A being Ordinal st A in dom fi holds
fi . A in psi . A ) ; :: according to ORDINAL2:def_9 ::_thesis: B c= C
A5: now__::_thesis:_for_A_being_Ordinal_st_A_in_dom_fi_holds_
fi_._A_c=_psi_._A
let A be Ordinal; ::_thesis: ( A in dom fi implies fi . A c= psi . A )
reconsider A1 = fi . A, A2 = psi . A as Ordinal ;
assume A in dom fi ; ::_thesis: fi . A c= psi . A
then ( A1 c= A2 or A1 in A2 ) by A4;
hence fi . A c= psi . A by ORDINAL1:def_2; ::_thesis: verum
end;
now__::_thesis:_B_c=_C
percases ( ( B = {} & C = {} ) or ( B = {} & C <> {} ) or ( B <> {} & C = {} ) or ( B <> {} & C <> {} ) ) ;
suppose ( B = {} & C = {} ) ; ::_thesis: B c= C
hence B c= C ; ::_thesis: verum
end;
suppose ( B = {} & C <> {} ) ; ::_thesis: B c= C
then B in C by ORDINAL3:8;
hence B c= C by ORDINAL1:def_2; ::_thesis: verum
end;
supposeA6: ( B <> {} & C = {} ) ; ::_thesis: B c= C
then {} in B by ORDINAL3:8;
then consider A2 being Ordinal such that
A7: A2 in dom fi and
A8: for A being Ordinal st A2 c= A & A in dom fi holds
( {} in fi . A & fi . A in succ B ) by A2, ORDINAL1:6;
consider A1 being Ordinal such that
A9: A1 in dom psi and
A10: for A being Ordinal st A1 c= A & A in dom psi holds
psi . A = {} by A3, A6;
A11: ( A1 \/ A2 = A1 or A1 \/ A2 = A2 ) by ORDINAL3:12;
then A12: fi . (A1 \/ A2) c= psi . (A1 \/ A2) by A1, A5, A9, A7;
A2 c= A1 \/ A2 by XBOOLE_1:7;
then {} in fi . (A1 \/ A2) by A1, A9, A7, A8, A11;
hence B c= C by A1, A9, A10, A7, A11, A12, XBOOLE_1:7; ::_thesis: verum
end;
supposeA13: ( B <> {} & C <> {} ) ; ::_thesis: B c= C
assume not B c= C ; ::_thesis: contradiction
then C in B by ORDINAL1:16;
then consider A1 being Ordinal such that
A14: A1 in dom fi and
A15: for A being Ordinal st A1 c= A & A in dom fi holds
( C in fi . A & fi . A in succ B ) by A2, ORDINAL1:6;
{} in C by A13, ORDINAL3:8;
then consider A2 being Ordinal such that
A16: A2 in dom psi and
A17: for A being Ordinal st A2 c= A & A in dom psi holds
( {} in psi . A & psi . A in succ C ) by A3, ORDINAL1:6;
A18: ( A1 \/ A2 = A1 or A1 \/ A2 = A2 ) by ORDINAL3:12;
reconsider A3 = psi . (A1 \/ A2) as Ordinal ;
A2 c= A1 \/ A2 by XBOOLE_1:7;
then psi . (A1 \/ A2) in succ C by A1, A14, A16, A17, A18;
then A19: A3 c= C by ORDINAL1:22;
A1 c= A1 \/ A2 by XBOOLE_1:7;
then A20: C in fi . (A1 \/ A2) by A1, A14, A15, A16, A18;
fi . (A1 \/ A2) c= psi . (A1 \/ A2) by A1, A5, A14, A16, A18;
hence contradiction by A20, A19, ORDINAL1:5; ::_thesis: verum
end;
end;
end;
hence B c= C ; ::_thesis: verum
end;
theorem :: ORDINAL4:7
for fi being Ordinal-Sequence
for A being Ordinal
for f1, f2 being Ordinal-Sequence st dom f1 = dom fi & dom fi = dom f2 & A is_limes_of f1 & A is_limes_of f2 & ( for A being Ordinal st A in dom fi holds
( f1 . A c= fi . A & fi . A c= f2 . A ) ) holds
A is_limes_of fi
proof
let fi be Ordinal-Sequence; ::_thesis: for A being Ordinal
for f1, f2 being Ordinal-Sequence st dom f1 = dom fi & dom fi = dom f2 & A is_limes_of f1 & A is_limes_of f2 & ( for A being Ordinal st A in dom fi holds
( f1 . A c= fi . A & fi . A c= f2 . A ) ) holds
A is_limes_of fi
let A be Ordinal; ::_thesis: for f1, f2 being Ordinal-Sequence st dom f1 = dom fi & dom fi = dom f2 & A is_limes_of f1 & A is_limes_of f2 & ( for A being Ordinal st A in dom fi holds
( f1 . A c= fi . A & fi . A c= f2 . A ) ) holds
A is_limes_of fi
let f1, f2 be Ordinal-Sequence; ::_thesis: ( dom f1 = dom fi & dom fi = dom f2 & A is_limes_of f1 & A is_limes_of f2 & ( for A being Ordinal st A in dom fi holds
( f1 . A c= fi . A & fi . A c= f2 . A ) ) implies A is_limes_of fi )
assume that
A1: dom f1 = dom fi and
A2: dom fi = dom f2 and
A3: ( ( A = {} & ex B being Ordinal st
( B in dom f1 & ( for C being Ordinal st B c= C & C in dom f1 holds
f1 . C = {} ) ) ) or ( A <> {} & ( for B, C being Ordinal st B in A & A in C holds
ex D being Ordinal st
( D in dom f1 & ( for E being Ordinal st D c= E & E in dom f1 holds
( B in f1 . E & f1 . E in C ) ) ) ) ) ) and
A4: ( ( A = {} & ex B being Ordinal st
( B in dom f2 & ( for C being Ordinal st B c= C & C in dom f2 holds
f2 . C = {} ) ) ) or ( A <> {} & ( for B, C being Ordinal st B in A & A in C holds
ex D being Ordinal st
( D in dom f2 & ( for E being Ordinal st D c= E & E in dom f2 holds
( B in f2 . E & f2 . E in C ) ) ) ) ) ) and
A5: for A being Ordinal st A in dom fi holds
( f1 . A c= fi . A & fi . A c= f2 . A ) ; :: according to ORDINAL2:def_9 ::_thesis: A is_limes_of fi
percases ( A = {} or A <> {} ) ;
:: according to ORDINAL2:def_9
case A = {} ; ::_thesis: ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or fi . b2 = {} ) ) )
then consider B being Ordinal such that
A6: B in dom f2 and
A7: for C being Ordinal st B c= C & C in dom f2 holds
f2 . C = {} by A4;
take B ; ::_thesis: ( B in dom fi & ( for b1 being set holds
( not B c= b1 or not b1 in dom fi or fi . b1 = {} ) ) )
thus B in dom fi by A2, A6; ::_thesis: for b1 being set holds
( not B c= b1 or not b1 in dom fi or fi . b1 = {} )
let C be Ordinal; ::_thesis: ( not B c= C or not C in dom fi or fi . C = {} )
assume that
A8: B c= C and
A9: C in dom fi ; ::_thesis: fi . C = {}
f2 . C = {} by A2, A7, A8, A9;
hence fi . C = {} by A5, A9, XBOOLE_1:3; ::_thesis: verum
end;
case A <> {} ; ::_thesis: for b1, b2 being set holds
( not b1 in A or not A in b2 or ex b3 being set st
( b3 in dom fi & ( for b4 being set holds
( not b3 c= b4 or not b4 in dom fi or ( b1 in fi . b4 & fi . b4 in b2 ) ) ) ) )
let B, C be Ordinal; ::_thesis: ( not B in A or not A in C or ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or ( B in fi . b2 & fi . b2 in C ) ) ) ) )
assume that
A10: B in A and
A11: A in C ; ::_thesis: ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or ( B in fi . b2 & fi . b2 in C ) ) ) )
consider D2 being Ordinal such that
A12: D2 in dom f2 and
A13: for A1 being Ordinal st D2 c= A1 & A1 in dom f2 holds
( B in f2 . A1 & f2 . A1 in C ) by A4, A10, A11;
consider D1 being Ordinal such that
A14: D1 in dom f1 and
A15: for A1 being Ordinal st D1 c= A1 & A1 in dom f1 holds
( B in f1 . A1 & f1 . A1 in C ) by A3, A10, A11;
take D = D1 \/ D2; ::_thesis: ( D in dom fi & ( for b1 being set holds
( not D c= b1 or not b1 in dom fi or ( B in fi . b1 & fi . b1 in C ) ) ) )
thus D in dom fi by A1, A2, A14, A12, ORDINAL3:12; ::_thesis: for b1 being set holds
( not D c= b1 or not b1 in dom fi or ( B in fi . b1 & fi . b1 in C ) )
let A1 be Ordinal; ::_thesis: ( not D c= A1 or not A1 in dom fi or ( B in fi . A1 & fi . A1 in C ) )
assume that
A16: D c= A1 and
A17: A1 in dom fi ; ::_thesis: ( B in fi . A1 & fi . A1 in C )
reconsider B1 = fi . A1, B2 = f2 . A1 as Ordinal ;
A18: B1 c= B2 by A5, A17;
D2 c= D by XBOOLE_1:7;
then D2 c= A1 by A16, XBOOLE_1:1;
then A19: B2 in C by A2, A13, A17;
D1 c= D by XBOOLE_1:7;
then D1 c= A1 by A16, XBOOLE_1:1;
then A20: B in f1 . A1 by A1, A15, A17;
f1 . A1 c= fi . A1 by A5, A17;
hence ( B in fi . A1 & fi . A1 in C ) by A20, A18, A19, ORDINAL1:12; ::_thesis: verum
end;
end;
end;
theorem Th8: :: ORDINAL4:8
for fi being Ordinal-Sequence st dom fi <> {} & dom fi is limit_ordinal & fi is increasing holds
( sup fi is_limes_of fi & lim fi = sup fi )
proof
let fi be Ordinal-Sequence; ::_thesis: ( dom fi <> {} & dom fi is limit_ordinal & fi is increasing implies ( sup fi is_limes_of fi & lim fi = sup fi ) )
assume that
A1: ( dom fi <> {} & dom fi is limit_ordinal ) and
A2: for A, B being Ordinal st A in B & B in dom fi holds
fi . A in fi . B ; :: according to ORDINAL2:def_12 ::_thesis: ( sup fi is_limes_of fi & lim fi = sup fi )
reconsider x = fi . {} as Ordinal ;
{} in dom fi by A1, ORDINAL3:8;
then A3: x in rng fi by FUNCT_1:def_3;
thus sup fi is_limes_of fi ::_thesis: lim fi = sup fi
proof
percases ( sup fi = {} or sup fi <> {} ) ;
:: according to ORDINAL2:def_9
case sup fi = {} ; ::_thesis: ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or fi . b2 = {} ) ) )
hence ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or fi . b2 = {} ) ) ) by A3, ORDINAL2:19; ::_thesis: verum
end;
case sup fi <> {} ; ::_thesis: for b1, b2 being set holds
( not b1 in sup fi or not sup fi in b2 or ex b3 being set st
( b3 in dom fi & ( for b4 being set holds
( not b3 c= b4 or not b4 in dom fi or ( b1 in fi . b4 & fi . b4 in b2 ) ) ) ) )
let A, B be Ordinal; ::_thesis: ( not A in sup fi or not sup fi in B or ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or ( A in fi . b2 & fi . b2 in B ) ) ) ) )
assume that
A4: A in sup fi and
A5: sup fi in B ; ::_thesis: ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or ( A in fi . b2 & fi . b2 in B ) ) ) )
consider C being Ordinal such that
A6: C in rng fi and
A7: A c= C by A4, ORDINAL2:21;
consider x being set such that
A8: x in dom fi and
A9: C = fi . x by A6, FUNCT_1:def_3;
reconsider x = x as Ordinal by A8;
take M = succ x; ::_thesis: ( M in dom fi & ( for b1 being set holds
( not M c= b1 or not b1 in dom fi or ( A in fi . b1 & fi . b1 in B ) ) ) )
thus M in dom fi by A1, A8, ORDINAL1:28; ::_thesis: for b1 being set holds
( not M c= b1 or not b1 in dom fi or ( A in fi . b1 & fi . b1 in B ) )
let D be Ordinal; ::_thesis: ( not M c= D or not D in dom fi or ( A in fi . D & fi . D in B ) )
assume that
A10: M c= D and
A11: D in dom fi ; ::_thesis: ( A in fi . D & fi . D in B )
reconsider E = fi . D as Ordinal ;
x in M by ORDINAL1:6;
then C in E by A2, A9, A10, A11;
hence A in fi . D by A7, ORDINAL1:12; ::_thesis: fi . D in B
fi . D in rng fi by A11, FUNCT_1:def_3;
then E in sup fi by ORDINAL2:19;
hence fi . D in B by A5, ORDINAL1:10; ::_thesis: verum
end;
end;
end;
hence lim fi = sup fi by ORDINAL2:def_10; ::_thesis: verum
end;
theorem Th9: :: ORDINAL4:9
for fi being Ordinal-Sequence
for A, B being Ordinal st fi is increasing & A c= B & B in dom fi holds
fi . A c= fi . B
proof
let fi be Ordinal-Sequence; ::_thesis: for A, B being Ordinal st fi is increasing & A c= B & B in dom fi holds
fi . A c= fi . B
let A, B be Ordinal; ::_thesis: ( fi is increasing & A c= B & B in dom fi implies fi . A c= fi . B )
assume that
A1: for A, B being Ordinal st A in B & B in dom fi holds
fi . A in fi . B and
A2: A c= B and
A3: B in dom fi ; :: according to ORDINAL2:def_12 ::_thesis: fi . A c= fi . B
reconsider C = fi . B as Ordinal ;
now__::_thesis:_fi_._A_c=_fi_._B
percases ( A = B or A <> B ) ;
suppose A = B ; ::_thesis: fi . A c= fi . B
hence fi . A c= fi . B ; ::_thesis: verum
end;
suppose A <> B ; ::_thesis: fi . A c= fi . B
then A c< B by A2, XBOOLE_0:def_8;
then A in B by ORDINAL1:11;
then fi . A in C by A1, A3;
hence fi . A c= fi . B by ORDINAL1:def_2; ::_thesis: verum
end;
end;
end;
hence fi . A c= fi . B ; ::_thesis: verum
end;
theorem Th10: :: ORDINAL4:10
for fi being Ordinal-Sequence
for A being Ordinal st fi is increasing & A in dom fi holds
A c= fi . A
proof
let fi be Ordinal-Sequence; ::_thesis: for A being Ordinal st fi is increasing & A in dom fi holds
A c= fi . A
let A be Ordinal; ::_thesis: ( fi is increasing & A in dom fi implies A c= fi . A )
assume that
A1: for A, B being Ordinal st A in B & B in dom fi holds
fi . A in fi . B and
A2: A in dom fi and
A3: not A c= fi . A ; :: according to ORDINAL2:def_12 ::_thesis: contradiction
defpred S1[ set ] means ( $1 in dom fi & not $1 c= fi . $1 );
A4: ex A being Ordinal st S1[A] by A2, A3;
consider A being Ordinal such that
A5: S1[A] and
A6: for B being Ordinal st S1[B] holds
A c= B from ORDINAL1:sch_1(A4);
reconsider B = fi . A as Ordinal ;
A7: B in A by A5, ORDINAL1:16;
then not B c= fi . B by A1, A5, ORDINAL1:5;
hence contradiction by A5, A6, A7, ORDINAL1:10; ::_thesis: verum
end;
theorem Th11: :: ORDINAL4:11
for phi being Ordinal-Sequence
for A being Ordinal st phi is increasing holds
phi " A is Ordinal
proof
let phi be Ordinal-Sequence; ::_thesis: for A being Ordinal st phi is increasing holds
phi " A is Ordinal
let A be Ordinal; ::_thesis: ( phi is increasing implies phi " A is Ordinal )
assume A1: for A, B being Ordinal st A in B & B in dom phi holds
phi . A in phi . B ; :: according to ORDINAL2:def_12 ::_thesis: phi " A is Ordinal
now__::_thesis:_for_X_being_set_st_X_in_phi_"_A_holds_
(_X_is_Ordinal_&_X_c=_phi_"_A_)
let X be set ; ::_thesis: ( X in phi " A implies ( X is Ordinal & X c= phi " A ) )
assume A2: X in phi " A ; ::_thesis: ( X is Ordinal & X c= phi " A )
then A3: X in dom phi by FUNCT_1:def_7;
hence X is Ordinal ; ::_thesis: X c= phi " A
reconsider B = X as Ordinal by A3;
A4: phi . X in A by A2, FUNCT_1:def_7;
thus X c= phi " A ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in phi " A )
assume A5: x in X ; ::_thesis: x in phi " A
then x in B ;
then reconsider C = x, D = phi . B as Ordinal ;
reconsider E = phi . C as Ordinal ;
E in D by A1, A3, A5;
then A6: phi . x in A by A4, ORDINAL1:10;
C in dom phi by A3, A5, ORDINAL1:10;
hence x in phi " A by A6, FUNCT_1:def_7; ::_thesis: verum
end;
end;
hence phi " A is Ordinal by ORDINAL1:19; ::_thesis: verum
end;
theorem Th12: :: ORDINAL4:12
for f1, f2 being Ordinal-Sequence st f1 is increasing holds
f2 * f1 is Ordinal-Sequence
proof
let f1, f2 be Ordinal-Sequence; ::_thesis: ( f1 is increasing implies f2 * f1 is Ordinal-Sequence )
A1: dom (f2 * f1) = f1 " (dom f2) by RELAT_1:147;
assume f1 is increasing ; ::_thesis: f2 * f1 is Ordinal-Sequence
then dom (f2 * f1) is Ordinal by A1, Th11;
then reconsider f = f2 * f1 as T-Sequence by ORDINAL1:def_7;
consider A being Ordinal such that
A2: rng f2 c= A by ORDINAL2:def_4;
rng f c= rng f2 by RELAT_1:26;
then rng f c= A by A2, XBOOLE_1:1;
hence f2 * f1 is Ordinal-Sequence by ORDINAL2:def_4; ::_thesis: verum
end;
theorem Th13: :: ORDINAL4:13
for f1, f2 being Ordinal-Sequence st f1 is increasing & f2 is increasing holds
ex phi being Ordinal-Sequence st
( phi = f1 * f2 & phi is increasing )
proof
let f1, f2 be Ordinal-Sequence; ::_thesis: ( f1 is increasing & f2 is increasing implies ex phi being Ordinal-Sequence st
( phi = f1 * f2 & phi is increasing ) )
assume that
A1: f1 is increasing and
A2: f2 is increasing ; ::_thesis: ex phi being Ordinal-Sequence st
( phi = f1 * f2 & phi is increasing )
reconsider f = f1 * f2 as Ordinal-Sequence by A2, Th12;
take f ; ::_thesis: ( f = f1 * f2 & f is increasing )
thus f = f1 * f2 ; ::_thesis: f is increasing
let A be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not A in b1 or not b1 in dom f or f . A in f . b1 )
let B be Ordinal; ::_thesis: ( not A in B or not B in dom f or f . A in f . B )
assume that
A3: A in B and
A4: B in dom f ; ::_thesis: f . A in f . B
reconsider A1 = f2 . A, B1 = f2 . B as Ordinal ;
A5: B1 in dom f1 by A4, FUNCT_1:11;
dom f c= dom f2 by RELAT_1:25;
then A6: A1 in B1 by A2, A3, A4, ORDINAL2:def_12;
A7: f . B = f1 . B1 by A4, FUNCT_1:12;
f . A = f1 . A1 by A3, A4, FUNCT_1:12, ORDINAL1:10;
hence f . A in f . B by A1, A6, A5, A7, ORDINAL2:def_12; ::_thesis: verum
end;
theorem Th14: :: ORDINAL4:14
for fi being Ordinal-Sequence
for A being Ordinal
for f1, f2 being Ordinal-Sequence st f1 is increasing & A is_limes_of f2 & sup (rng f1) = dom f2 & fi = f2 * f1 holds
A is_limes_of fi
proof
let fi be Ordinal-Sequence; ::_thesis: for A being Ordinal
for f1, f2 being Ordinal-Sequence st f1 is increasing & A is_limes_of f2 & sup (rng f1) = dom f2 & fi = f2 * f1 holds
A is_limes_of fi
let A be Ordinal; ::_thesis: for f1, f2 being Ordinal-Sequence st f1 is increasing & A is_limes_of f2 & sup (rng f1) = dom f2 & fi = f2 * f1 holds
A is_limes_of fi
let f1, f2 be Ordinal-Sequence; ::_thesis: ( f1 is increasing & A is_limes_of f2 & sup (rng f1) = dom f2 & fi = f2 * f1 implies A is_limes_of fi )
assume that
A1: f1 is increasing and
A2: ( ( A = {} & ex B being Ordinal st
( B in dom f2 & ( for C being Ordinal st B c= C & C in dom f2 holds
f2 . C = {} ) ) ) or ( A <> {} & ( for B, C being Ordinal st B in A & A in C holds
ex D being Ordinal st
( D in dom f2 & ( for E being Ordinal st D c= E & E in dom f2 holds
( B in f2 . E & f2 . E in C ) ) ) ) ) ) and
A3: sup (rng f1) = dom f2 and
A4: fi = f2 * f1 ; :: according to ORDINAL2:def_9 ::_thesis: A is_limes_of fi
percases ( A = {} or A <> {} ) ;
:: according to ORDINAL2:def_9
case A = {} ; ::_thesis: ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or fi . b2 = {} ) ) )
then consider B being Ordinal such that
A5: B in dom f2 and
A6: for C being Ordinal st B c= C & C in dom f2 holds
f2 . C = {} by A2;
consider B1 being Ordinal such that
A7: B1 in rng f1 and
A8: B c= B1 by A3, A5, ORDINAL2:21;
consider x being set such that
A9: x in dom f1 and
A10: B1 = f1 . x by A7, FUNCT_1:def_3;
reconsider x = x as Ordinal by A9;
take x ; ::_thesis: ( x in dom fi & ( for b1 being set holds
( not x c= b1 or not b1 in dom fi or fi . b1 = {} ) ) )
B1 in dom f2 by A3, A7, ORDINAL2:19;
hence x in dom fi by A4, A9, A10, FUNCT_1:11; ::_thesis: for b1 being set holds
( not x c= b1 or not b1 in dom fi or fi . b1 = {} )
let C be Ordinal; ::_thesis: ( not x c= C or not C in dom fi or fi . C = {} )
assume that
A11: x c= C and
A12: C in dom fi ; ::_thesis: fi . C = {}
reconsider C1 = f1 . C as Ordinal ;
A13: dom fi c= dom f1 by A4, RELAT_1:25;
then B1 c= C1 by A1, A10, A11, A12, Th9;
then A14: B c= C1 by A8, XBOOLE_1:1;
C1 in rng f1 by A12, A13, FUNCT_1:def_3;
then f2 . C1 = {} by A3, A6, A14, ORDINAL2:19;
hence fi . C = {} by A4, A12, FUNCT_1:12; ::_thesis: verum
end;
case A <> {} ; ::_thesis: for b1, b2 being set holds
( not b1 in A or not A in b2 or ex b3 being set st
( b3 in dom fi & ( for b4 being set holds
( not b3 c= b4 or not b4 in dom fi or ( b1 in fi . b4 & fi . b4 in b2 ) ) ) ) )
let B, C be Ordinal; ::_thesis: ( not B in A or not A in C or ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or ( B in fi . b2 & fi . b2 in C ) ) ) ) )
assume that
A15: B in A and
A16: A in C ; ::_thesis: ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or ( B in fi . b2 & fi . b2 in C ) ) ) )
consider D being Ordinal such that
A17: D in dom f2 and
A18: for A1 being Ordinal st D c= A1 & A1 in dom f2 holds
( B in f2 . A1 & f2 . A1 in C ) by A2, A15, A16;
consider B1 being Ordinal such that
A19: B1 in rng f1 and
A20: D c= B1 by A3, A17, ORDINAL2:21;
consider x being set such that
A21: x in dom f1 and
A22: B1 = f1 . x by A19, FUNCT_1:def_3;
reconsider x = x as Ordinal by A21;
take x ; ::_thesis: ( x in dom fi & ( for b1 being set holds
( not x c= b1 or not b1 in dom fi or ( B in fi . b1 & fi . b1 in C ) ) ) )
B1 in dom f2 by A3, A19, ORDINAL2:19;
hence x in dom fi by A4, A21, A22, FUNCT_1:11; ::_thesis: for b1 being set holds
( not x c= b1 or not b1 in dom fi or ( B in fi . b1 & fi . b1 in C ) )
let E be Ordinal; ::_thesis: ( not x c= E or not E in dom fi or ( B in fi . E & fi . E in C ) )
assume that
A23: x c= E and
A24: E in dom fi ; ::_thesis: ( B in fi . E & fi . E in C )
reconsider E1 = f1 . E as Ordinal ;
A25: dom fi c= dom f1 by A4, RELAT_1:25;
then E1 in rng f1 by A24, FUNCT_1:def_3;
then A26: E1 in dom f2 by A3, ORDINAL2:19;
B1 c= E1 by A1, A22, A23, A24, A25, Th9;
then A27: D c= E1 by A20, XBOOLE_1:1;
then A28: f2 . E1 in C by A18, A26;
B in f2 . E1 by A18, A27, A26;
hence ( B in fi . E & fi . E in C ) by A4, A24, A28, FUNCT_1:12; ::_thesis: verum
end;
end;
end;
theorem Th15: :: ORDINAL4:15
for phi being Ordinal-Sequence
for A being Ordinal st phi is increasing holds
phi | A is increasing
proof
let phi be Ordinal-Sequence; ::_thesis: for A being Ordinal st phi is increasing holds
phi | A is increasing
let A be Ordinal; ::_thesis: ( phi is increasing implies phi | A is increasing )
assume A1: for A, B being Ordinal st A in B & B in dom phi holds
phi . A in phi . B ; :: according to ORDINAL2:def_12 ::_thesis: phi | A is increasing
let B be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not B in b1 or not b1 in dom (phi | A) or (phi | A) . B in (phi | A) . b1 )
let C be Ordinal; ::_thesis: ( not B in C or not C in dom (phi | A) or (phi | A) . B in (phi | A) . C )
assume that
A2: B in C and
A3: C in dom (phi | A) ; ::_thesis: (phi | A) . B in (phi | A) . C
A4: phi . B = (phi | A) . B by A2, A3, FUNCT_1:47, ORDINAL1:10;
dom (phi | A) c= dom phi by RELAT_1:60;
then phi . B in phi . C by A1, A2, A3;
hence (phi | A) . B in (phi | A) . C by A3, A4, FUNCT_1:47; ::_thesis: verum
end;
theorem Th16: :: ORDINAL4:16
for phi being Ordinal-Sequence st phi is increasing & dom phi is limit_ordinal holds
sup phi is limit_ordinal
proof
let phi be Ordinal-Sequence; ::_thesis: ( phi is increasing & dom phi is limit_ordinal implies sup phi is limit_ordinal )
assume that
A1: phi is increasing and
A2: dom phi is limit_ordinal ; ::_thesis: sup phi is limit_ordinal
now__::_thesis:_for_A_being_Ordinal_st_A_in_sup_phi_holds_
succ_A_in_sup_phi
let A be Ordinal; ::_thesis: ( A in sup phi implies succ A in sup phi )
assume A in sup phi ; ::_thesis: succ A in sup phi
then consider B being Ordinal such that
A3: B in rng phi and
A4: A c= B by ORDINAL2:21;
consider x being set such that
A5: x in dom phi and
A6: B = phi . x by A3, FUNCT_1:def_3;
reconsider x = x as Ordinal by A5;
A7: succ x in dom phi by A2, A5, ORDINAL1:28;
reconsider C = phi . (succ x) as Ordinal ;
x in succ x by ORDINAL1:6;
then B in C by A1, A6, A7, ORDINAL2:def_12;
then A8: succ B c= C by ORDINAL1:21;
A9: succ A c= succ B by A4, ORDINAL2:1;
C in rng phi by A7, FUNCT_1:def_3;
then C in sup phi by ORDINAL2:19;
then succ B in sup phi by A8, ORDINAL1:12;
hence succ A in sup phi by A9, ORDINAL1:12; ::_thesis: verum
end;
hence sup phi is limit_ordinal by ORDINAL1:28; ::_thesis: verum
end;
Lm5: for f, g being Function
for X being set st rng f c= X holds
(g | X) * f = g * f
proof
let f, g be Function; ::_thesis: for X being set st rng f c= X holds
(g | X) * f = g * f
let X be set ; ::_thesis: ( rng f c= X implies (g | X) * f = g * f )
A1: f " (rng f) = dom f by RELAT_1:134;
assume rng f c= X ; ::_thesis: (g | X) * f = g * f
then A2: f " (rng f) c= f " X by RELAT_1:143;
f " X c= dom f by RELAT_1:132;
then A3: f " X = dom f by A2, A1, XBOOLE_0:def_10;
dom ((g | X) * f) = f " (dom (g | X)) by RELAT_1:147
.= f " ((dom g) /\ X) by RELAT_1:61
.= (f " (dom g)) /\ (f " X) by FUNCT_1:68
.= f " (dom g) by A3, RELAT_1:132, XBOOLE_1:28
.= dom (g * f) by RELAT_1:147 ;
hence (g | X) * f = g * f by GRFUNC_1:3, RELAT_1:64; ::_thesis: verum
end;
theorem :: ORDINAL4:17
for fi, psi, phi being Ordinal-Sequence st fi is increasing & fi is continuous & psi is continuous & phi = psi * fi holds
phi is continuous
proof
let fi, psi, phi be Ordinal-Sequence; ::_thesis: ( fi is increasing & fi is continuous & psi is continuous & phi = psi * fi implies phi is continuous )
assume that
A1: fi is increasing and
A2: for A, B being Ordinal st A in dom fi & A <> {} & A is limit_ordinal & B = fi . A holds
B is_limes_of fi | A and
A3: for A, B being Ordinal st A in dom psi & A <> {} & A is limit_ordinal & B = psi . A holds
B is_limes_of psi | A and
A4: phi = psi * fi ; :: according to ORDINAL2:def_13 ::_thesis: phi is continuous
let A be Ordinal; :: according to ORDINAL2:def_13 ::_thesis: for b1 being set holds
( not A in dom phi or A = {} or not A is limit_ordinal or not b1 = phi . A or b1 is_limes_of phi | A )
let B be Ordinal; ::_thesis: ( not A in dom phi or A = {} or not A is limit_ordinal or not B = phi . A or B is_limes_of phi | A )
assume that
A5: A in dom phi and
A6: A <> {} and
A7: A is limit_ordinal and
A8: B = phi . A ; ::_thesis: B is_limes_of phi | A
reconsider A1 = fi . A as Ordinal ;
A9: fi | A is increasing by A1, Th15;
A10: dom phi c= dom fi by A4, RELAT_1:25;
then A c= dom fi by A5, ORDINAL1:def_2;
then A11: dom (fi | A) = A by RELAT_1:62;
A1 is_limes_of fi | A by A2, A5, A6, A7, A10;
then lim (fi | A) = A1 by ORDINAL2:def_10;
then A12: sup (fi | A) = A1 by A6, A7, A11, A9, Th8;
A13: B = psi . A1 by A4, A5, A8, FUNCT_1:12;
A14: {} in A by A6, ORDINAL3:8;
A15: A1 in dom psi by A4, A5, FUNCT_1:11;
then A1 c= dom psi by ORDINAL1:def_2;
then A16: dom (psi | A1) = A1 by RELAT_1:62;
A17: rng (fi | A) c= sup (rng (fi | A))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (fi | A) or x in sup (rng (fi | A)) )
assume A18: x in rng (fi | A) ; ::_thesis: x in sup (rng (fi | A))
then ex y being set st
( y in dom (fi | A) & x = (fi | A) . y ) by FUNCT_1:def_3;
hence x in sup (rng (fi | A)) by A18, ORDINAL2:19; ::_thesis: verum
end;
phi | A = psi * (fi | A) by A4, RELAT_1:83;
then A19: phi | A = (psi | A1) * (fi | A) by A17, A12, Lm5;
A c= A1 by A1, A5, A10, Th10;
then B is_limes_of psi | A1 by A3, A7, A13, A15, A11, A14, A9, A12, Th16;
hence B is_limes_of phi | A by A9, A16, A12, A19, Th14; ::_thesis: verum
end;
theorem :: ORDINAL4:18
for fi being Ordinal-Sequence
for C being Ordinal st ( for A being Ordinal st A in dom fi holds
fi . A = C +^ A ) holds
fi is increasing
proof
let fi be Ordinal-Sequence; ::_thesis: for C being Ordinal st ( for A being Ordinal st A in dom fi holds
fi . A = C +^ A ) holds
fi is increasing
let C be Ordinal; ::_thesis: ( ( for A being Ordinal st A in dom fi holds
fi . A = C +^ A ) implies fi is increasing )
assume A1: for A being Ordinal st A in dom fi holds
fi . A = C +^ A ; ::_thesis: fi is increasing
let A be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not A in b1 or not b1 in dom fi or fi . A in fi . b1 )
let B be Ordinal; ::_thesis: ( not A in B or not B in dom fi or fi . A in fi . B )
assume that
A2: A in B and
A3: B in dom fi ; ::_thesis: fi . A in fi . B
A4: fi . B = C +^ B by A1, A3;
fi . A = C +^ A by A1, A2, A3, ORDINAL1:10;
hence fi . A in fi . B by A2, A4, ORDINAL2:32; ::_thesis: verum
end;
theorem Th19: :: ORDINAL4:19
for fi being Ordinal-Sequence
for C being Ordinal st C <> {} & ( for A being Ordinal st A in dom fi holds
fi . A = A *^ C ) holds
fi is increasing
proof
let fi be Ordinal-Sequence; ::_thesis: for C being Ordinal st C <> {} & ( for A being Ordinal st A in dom fi holds
fi . A = A *^ C ) holds
fi is increasing
let C be Ordinal; ::_thesis: ( C <> {} & ( for A being Ordinal st A in dom fi holds
fi . A = A *^ C ) implies fi is increasing )
assume that
A1: C <> {} and
A2: for A being Ordinal st A in dom fi holds
fi . A = A *^ C ; ::_thesis: fi is increasing
let A be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not A in b1 or not b1 in dom fi or fi . A in fi . b1 )
let B be Ordinal; ::_thesis: ( not A in B or not B in dom fi or fi . A in fi . B )
assume that
A3: A in B and
A4: B in dom fi ; ::_thesis: fi . A in fi . B
A5: fi . B = B *^ C by A2, A4;
fi . A = A *^ C by A2, A3, A4, ORDINAL1:10;
hence fi . A in fi . B by A1, A3, A5, ORDINAL2:40; ::_thesis: verum
end;
theorem Th20: :: ORDINAL4:20
for A being Ordinal st A <> {} holds
exp ({},A) = {}
proof
let A be Ordinal; ::_thesis: ( A <> {} implies exp ({},A) = {} )
defpred S1[ Ordinal] means ( $1 <> {} implies exp ({},$1) = {} );
A1: for B being Ordinal st S1[B] holds
S1[ succ B]
proof
let B be Ordinal; ::_thesis: ( S1[B] implies S1[ succ B] )
assume that
S1[B] and
succ B <> {} ; ::_thesis: exp ({},(succ B)) = {}
thus exp ({},(succ B)) = {} *^ (exp ({},B)) by ORDINAL2:44
.= {} by ORDINAL2:35 ; ::_thesis: verum
end;
A2: for B being Ordinal st B <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds
S1[C] ) holds
S1[B]
proof
deffunc H1( Ordinal) -> set = exp ({},$1);
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal & ( for C being Ordinal st C in A holds
S1[C] ) implies S1[A] )
assume that
A3: A <> {} and
A4: A is limit_ordinal and
A5: for C being Ordinal st C in A holds
S1[C] and
A <> {} ; ::_thesis: exp ({},A) = {}
consider fi being Ordinal-Sequence such that
A6: ( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = H1(B) ) ) from ORDINAL2:sch_3();
{} is_limes_of fi
proof
percases ( {} = {} or {} <> {} ) ;
:: according to ORDINAL2:def_9
case {} = {} ; ::_thesis: ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or fi . b2 = {} ) ) )
take B = 1; ::_thesis: ( B in dom fi & ( for b1 being set holds
( not B c= b1 or not b1 in dom fi or fi . b1 = {} ) ) )
{} in A by A3, ORDINAL3:8;
hence B in dom fi by A4, A6, Lm3, ORDINAL1:28; ::_thesis: for b1 being set holds
( not B c= b1 or not b1 in dom fi or fi . b1 = {} )
let D be Ordinal; ::_thesis: ( not B c= D or not D in dom fi or fi . D = {} )
assume A7: B c= D ; ::_thesis: ( not D in dom fi or fi . D = {} )
assume A8: D in dom fi ; ::_thesis: fi . D = {}
then S1[D] by A5, A6;
hence fi . D = {} by A6, A7, A8, Lm3, ORDINAL1:21; ::_thesis: verum
end;
case {} <> {} ; ::_thesis: for b1, b2 being set holds
( not b1 in {} or not {} in b2 or ex b3 being set st
( b3 in dom fi & ( for b4 being set holds
( not b3 c= b4 or not b4 in dom fi or ( b1 in fi . b4 & fi . b4 in b2 ) ) ) ) )
thus for b1, b2 being set holds
( not b1 in {} or not {} in b2 or ex b3 being set st
( b3 in dom fi & ( for b4 being set holds
( not b3 c= b4 or not b4 in dom fi or ( b1 in fi . b4 & fi . b4 in b2 ) ) ) ) ) ; ::_thesis: verum
end;
end;
end;
then lim fi = {} by ORDINAL2:def_10;
hence exp ({},A) = {} by A3, A4, A6, ORDINAL2:45; ::_thesis: verum
end;
A9: S1[ {} ] ;
for B being Ordinal holds S1[B] from ORDINAL2:sch_1(A9, A1, A2);
hence ( A <> {} implies exp ({},A) = {} ) ; ::_thesis: verum
end;
Lm6: for A being Ordinal st A <> {} & A is limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp ({},B) ) holds
{} is_limes_of fi
proof
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal implies for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp ({},B) ) holds
{} is_limes_of fi )
assume that
A1: A <> {} and
A2: A is limit_ordinal ; ::_thesis: for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp ({},B) ) holds
{} is_limes_of fi
let fi be Ordinal-Sequence; ::_thesis: ( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp ({},B) ) implies {} is_limes_of fi )
assume that
A3: dom fi = A and
A4: for B being Ordinal st B in A holds
fi . B = exp ({},B) ; ::_thesis: {} is_limes_of fi
percases ( {} = {} or {} <> {} ) ;
:: according to ORDINAL2:def_9
case {} = {} ; ::_thesis: ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or fi . b2 = {} ) ) )
take B = 1; ::_thesis: ( B in dom fi & ( for b1 being set holds
( not B c= b1 or not b1 in dom fi or fi . b1 = {} ) ) )
{} in A by A1, ORDINAL3:8;
hence B in dom fi by A2, A3, Lm3, ORDINAL1:28; ::_thesis: for b1 being set holds
( not B c= b1 or not b1 in dom fi or fi . b1 = {} )
let D be Ordinal; ::_thesis: ( not B c= D or not D in dom fi or fi . D = {} )
assume that
A5: B c= D and
A6: D in dom fi ; ::_thesis: fi . D = {}
A7: D <> {} by A5, Lm3, ORDINAL1:21;
exp ({},D) = fi . D by A3, A4, A6;
hence fi . D = {} by A7, Th20; ::_thesis: verum
end;
case {} <> {} ; ::_thesis: for b1, b2 being set holds
( not b1 in {} or not {} in b2 or ex b3 being set st
( b3 in dom fi & ( for b4 being set holds
( not b3 c= b4 or not b4 in dom fi or ( b1 in fi . b4 & fi . b4 in b2 ) ) ) ) )
thus for b1, b2 being set holds
( not b1 in {} or not {} in b2 or ex b3 being set st
( b3 in dom fi & ( for b4 being set holds
( not b3 c= b4 or not b4 in dom fi or ( b1 in fi . b4 & fi . b4 in b2 ) ) ) ) ) ; ::_thesis: verum
end;
end;
end;
Lm7: for A being Ordinal st A <> {} holds
for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp (1,B) ) holds
1 is_limes_of fi
proof
let A be Ordinal; ::_thesis: ( A <> {} implies for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp (1,B) ) holds
1 is_limes_of fi )
assume A1: A <> {} ; ::_thesis: for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp (1,B) ) holds
1 is_limes_of fi
let fi be Ordinal-Sequence; ::_thesis: ( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp (1,B) ) implies 1 is_limes_of fi )
assume that
A2: dom fi = A and
A3: for B being Ordinal st B in A holds
fi . B = exp (1,B) ; ::_thesis: 1 is_limes_of fi
percases ( 1 = {} or 1 <> {} ) ;
:: according to ORDINAL2:def_9
case 1 = {} ; ::_thesis: ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or fi . b2 = {} ) ) )
hence ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or fi . b2 = {} ) ) ) ; ::_thesis: verum
end;
case 1 <> {} ; ::_thesis: for b1, b2 being set holds
( not b1 in 1 or not 1 in b2 or ex b3 being set st
( b3 in dom fi & ( for b4 being set holds
( not b3 c= b4 or not b4 in dom fi or ( b1 in fi . b4 & fi . b4 in b2 ) ) ) ) )
let A1, A2 be Ordinal; ::_thesis: ( not A1 in 1 or not 1 in A2 or ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or ( A1 in fi . b2 & fi . b2 in A2 ) ) ) ) )
assume that
A4: A1 in 1 and
A5: 1 in A2 ; ::_thesis: ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or ( A1 in fi . b2 & fi . b2 in A2 ) ) ) )
take B = {} ; ::_thesis: ( B in dom fi & ( for b1 being set holds
( not B c= b1 or not b1 in dom fi or ( A1 in fi . b1 & fi . b1 in A2 ) ) ) )
thus B in dom fi by A1, A2, ORDINAL3:8; ::_thesis: for b1 being set holds
( not B c= b1 or not b1 in dom fi or ( A1 in fi . b1 & fi . b1 in A2 ) )
let D be Ordinal; ::_thesis: ( not B c= D or not D in dom fi or ( A1 in fi . D & fi . D in A2 ) )
assume that
B c= D and
A6: D in dom fi ; ::_thesis: ( A1 in fi . D & fi . D in A2 )
exp (1,D) = fi . D by A2, A3, A6;
hence ( A1 in fi . D & fi . D in A2 ) by A4, A5, ORDINAL2:46; ::_thesis: verum
end;
end;
end;
Lm8: for C, A being Ordinal st A <> {} & A is limit_ordinal holds
ex fi being Ordinal-Sequence st
( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp (C,B) ) & ex D being Ordinal st D is_limes_of fi )
proof
let C be Ordinal; ::_thesis: for A being Ordinal st A <> {} & A is limit_ordinal holds
ex fi being Ordinal-Sequence st
( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp (C,B) ) & ex D being Ordinal st D is_limes_of fi )
defpred S1[ Ordinal] means ( $1 <> {} & $1 is limit_ordinal & ( for fi being Ordinal-Sequence st dom fi = $1 & ( for B being Ordinal st B in $1 holds
fi . B = exp (C,B) ) holds
for D being Ordinal holds not D is_limes_of fi ) );
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal implies ex fi being Ordinal-Sequence st
( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp (C,B) ) & ex D being Ordinal st D is_limes_of fi ) )
assume that
A1: A <> {} and
A2: A is limit_ordinal and
A3: for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp (C,B) ) holds
for D being Ordinal holds not D is_limes_of fi ; ::_thesis: contradiction
deffunc H1( Ordinal) -> set = exp (C,$1);
A4: ex A being Ordinal st S1[A] by A1, A2, A3;
consider A being Ordinal such that
A5: S1[A] and
A6: for A1 being Ordinal st S1[A1] holds
A c= A1 from ORDINAL1:sch_1(A4);
consider fi being Ordinal-Sequence such that
A7: ( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = H1(B) ) ) from ORDINAL2:sch_3();
A8: now__::_thesis:_(_not_C_=_{}_&_not_C_=_1_)
assume ( C = {} or C = 1 ) ; ::_thesis: contradiction
then ( {} is_limes_of fi or 1 is_limes_of fi ) by A5, A7, Lm6, Lm7;
hence contradiction by A5, A7; ::_thesis: verum
end;
then {} in C by ORDINAL3:8;
then 1 c= C by Lm3, ORDINAL1:21;
then A9: 1 c< C by A8, XBOOLE_0:def_8;
A10: for B2, B1 being Ordinal st B1 in B2 & B2 in A holds
exp (C,B1) in exp (C,B2)
proof
defpred S2[ Ordinal] means for B1 being Ordinal st B1 in $1 & $1 in A holds
exp (C,B1) in exp (C,$1);
A11: for B being Ordinal st S2[B] holds
S2[ succ B]
proof
let B be Ordinal; ::_thesis: ( S2[B] implies S2[ succ B] )
assume A12: for B1 being Ordinal st B1 in B & B in A holds
exp (C,B1) in exp (C,B) ; ::_thesis: S2[ succ B]
let B1 be Ordinal; ::_thesis: ( B1 in succ B & succ B in A implies exp (C,B1) in exp (C,(succ B)) )
assume that
A13: B1 in succ B and
A14: succ B in A ; ::_thesis: exp (C,B1) in exp (C,(succ B))
A15: B1 c= B by A13, ORDINAL1:22;
B in succ B by ORDINAL1:6;
then A16: B in A by A14, ORDINAL1:10;
A17: 1 *^ (exp (C,B)) = exp (C,B) by ORDINAL2:39;
A18: exp (C,B) <> {}
proof
now__::_thesis:_exp_(C,B)_<>_{}
percases ( B = {} or B <> {} ) ;
suppose B = {} ; ::_thesis: exp (C,B) <> {}
hence exp (C,B) <> {} by ORDINAL2:43; ::_thesis: verum
end;
supposeA19: B <> {} ; ::_thesis: exp (C,B) <> {}
B in succ B by ORDINAL1:6;
then B in A by A14, ORDINAL1:10;
hence exp (C,B) <> {} by A12, A19, ORDINAL3:8; ::_thesis: verum
end;
end;
end;
hence exp (C,B) <> {} ; ::_thesis: verum
end;
A20: exp (C,(succ B)) = C *^ (exp (C,B)) by ORDINAL2:44;
then A21: exp (C,B) in exp (C,(succ B)) by A9, A18, A17, ORDINAL1:11, ORDINAL2:40;
now__::_thesis:_(_B1_<>_B_implies_exp_(C,B1)_in_exp_(C,(succ_B))_)
assume B1 <> B ; ::_thesis: exp (C,B1) in exp (C,(succ B))
then B1 c< B by A15, XBOOLE_0:def_8;
then B1 in B by ORDINAL1:11;
then exp (C,B1) in exp (C,B) by A12, A16;
hence exp (C,B1) in exp (C,(succ B)) by A21, ORDINAL1:10; ::_thesis: verum
end;
hence exp (C,B1) in exp (C,(succ B)) by A9, A18, A20, A17, ORDINAL1:11, ORDINAL2:40; ::_thesis: verum
end;
A22: for B being Ordinal st B <> {} & B is limit_ordinal & ( for D being Ordinal st D in B holds
S2[D] ) holds
S2[B]
proof
let B be Ordinal; ::_thesis: ( B <> {} & B is limit_ordinal & ( for D being Ordinal st D in B holds
S2[D] ) implies S2[B] )
assume that
A23: B <> {} and
A24: B is limit_ordinal and
A25: for D being Ordinal st D in B holds
S2[D] ; ::_thesis: S2[B]
let B1 be Ordinal; ::_thesis: ( B1 in B & B in A implies exp (C,B1) in exp (C,B) )
assume that
A26: B1 in B and
A27: B in A ; ::_thesis: exp (C,B1) in exp (C,B)
consider psi being Ordinal-Sequence such that
A28: dom psi = B and
A29: for D being Ordinal st D in B holds
psi . D = exp (C,D) and
ex D being Ordinal st D is_limes_of psi by A6, A24, A26, A27, ORDINAL1:5;
psi . B1 = exp (C,B1) by A26, A29;
then A30: exp (C,B1) in rng psi by A26, A28, FUNCT_1:def_3;
psi is increasing
proof
let B1, B2 be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: ( not B1 in B2 or not B2 in dom psi or psi . B1 in psi . B2 )
assume that
A31: B1 in B2 and
A32: B2 in dom psi ; ::_thesis: psi . B1 in psi . B2
B2 in A by A27, A28, A32, ORDINAL1:10;
then A33: exp (C,B1) in exp (C,B2) by A25, A28, A31, A32;
psi . B1 = exp (C,B1) by A28, A29, A31, A32, ORDINAL1:10;
hence psi . B1 in psi . B2 by A28, A29, A32, A33; ::_thesis: verum
end;
then A34: lim psi = sup psi by A23, A24, A28, Th8;
exp (C,B) = lim psi by A23, A24, A28, A29, ORDINAL2:45;
hence exp (C,B1) in exp (C,B) by A34, A30, ORDINAL2:19; ::_thesis: verum
end;
A35: S2[ {} ] ;
thus for B being Ordinal holds S2[B] from ORDINAL2:sch_1(A35, A11, A22); ::_thesis: verum
end;
fi is increasing
proof
let B1, B2 be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: ( not B1 in B2 or not B2 in dom fi or fi . B1 in fi . B2 )
assume that
A36: B1 in B2 and
A37: B2 in dom fi ; ::_thesis: fi . B1 in fi . B2
A38: fi . B1 = exp (C,B1) by A7, A36, A37, ORDINAL1:10;
exp (C,B1) in exp (C,B2) by A7, A10, A36, A37;
hence fi . B1 in fi . B2 by A7, A37, A38; ::_thesis: verum
end;
then sup fi is_limes_of fi by A5, A7, Th8;
hence contradiction by A5, A7; ::_thesis: verum
end;
theorem Th21: :: ORDINAL4:21
for A, C being Ordinal st A <> {} & A is limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp (C,B) ) holds
exp (C,A) is_limes_of fi
proof
let A, C be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal implies for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp (C,B) ) holds
exp (C,A) is_limes_of fi )
assume that
A1: A <> {} and
A2: A is limit_ordinal ; ::_thesis: for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp (C,B) ) holds
exp (C,A) is_limes_of fi
consider psi being Ordinal-Sequence such that
A3: dom psi = A and
A4: for B being Ordinal st B in A holds
psi . B = exp (C,B) and
A5: ex D being Ordinal st D is_limes_of psi by A1, A2, Lm8;
let fi be Ordinal-Sequence; ::_thesis: ( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp (C,B) ) implies exp (C,A) is_limes_of fi )
assume that
A6: dom fi = A and
A7: for B being Ordinal st B in A holds
fi . B = exp (C,B) ; ::_thesis: exp (C,A) is_limes_of fi
now__::_thesis:_for_x_being_set_st_x_in_A_holds_
fi_._x_=_psi_._x
let x be set ; ::_thesis: ( x in A implies fi . x = psi . x )
assume A8: x in A ; ::_thesis: fi . x = psi . x
then reconsider B = x as Ordinal ;
thus fi . x = exp (C,B) by A7, A8
.= psi . x by A4, A8 ; ::_thesis: verum
end;
then fi = psi by A6, A3, FUNCT_1:2;
then consider D being Ordinal such that
A9: D is_limes_of fi by A5;
D = lim fi by A9, ORDINAL2:def_10
.= exp (C,A) by A1, A2, A6, A7, ORDINAL2:45 ;
hence exp (C,A) is_limes_of fi by A9; ::_thesis: verum
end;
theorem Th22: :: ORDINAL4:22
for C, A being Ordinal st C <> {} holds
exp (C,A) <> {}
proof
let C, A be Ordinal; ::_thesis: ( C <> {} implies exp (C,A) <> {} )
defpred S1[ Ordinal] means exp (C,$1) <> {} ;
assume A1: C <> {} ; ::_thesis: exp (C,A) <> {}
A2: for A being Ordinal st S1[A] holds
S1[ succ A]
proof
let A be Ordinal; ::_thesis: ( S1[A] implies S1[ succ A] )
assume A3: exp (C,A) <> {} ; ::_thesis: S1[ succ A]
exp (C,(succ A)) = C *^ (exp (C,A)) by ORDINAL2:44;
hence S1[ succ A] by A1, A3, ORDINAL3:31; ::_thesis: verum
end;
A4: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume that
A5: A <> {} and
A6: A is limit_ordinal and
A7: for B being Ordinal st B in A holds
exp (C,B) <> {} ; ::_thesis: S1[A]
consider fi being Ordinal-Sequence such that
A8: dom fi = A and
A9: for B being Ordinal st B in A holds
fi . B = exp (C,B) and
A10: ex D being Ordinal st D is_limes_of fi by A5, A6, Lm8;
A11: exp (C,A) = lim fi by A5, A6, A8, A9, ORDINAL2:45;
assume A12: exp (C,A) = {} ; ::_thesis: contradiction
consider D being Ordinal such that
A13: D is_limes_of fi by A10;
lim fi = D by A13, ORDINAL2:def_10;
then consider B being Ordinal such that
A14: B in dom fi and
A15: for D being Ordinal st B c= D & D in dom fi holds
fi . D = {} by A11, A13, A12, ORDINAL2:def_9;
fi . B = exp (C,B) by A8, A9, A14;
hence contradiction by A7, A8, A14, A15; ::_thesis: verum
end;
A16: S1[ {} ] by ORDINAL2:43;
for A being Ordinal holds S1[A] from ORDINAL2:sch_1(A16, A2, A4);
hence exp (C,A) <> {} ; ::_thesis: verum
end;
theorem Th23: :: ORDINAL4:23
for C, A being Ordinal st 1 in C holds
exp (C,A) in exp (C,(succ A))
proof
let C, A be Ordinal; ::_thesis: ( 1 in C implies exp (C,A) in exp (C,(succ A)) )
A1: 1 *^ (exp (C,A)) = exp (C,A) by ORDINAL2:39;
assume 1 in C ; ::_thesis: exp (C,A) in exp (C,(succ A))
then exp (C,A) in C *^ (exp (C,A)) by A1, Th22, ORDINAL2:40;
hence exp (C,A) in exp (C,(succ A)) by ORDINAL2:44; ::_thesis: verum
end;
theorem Th24: :: ORDINAL4:24
for C, A, B being Ordinal st 1 in C & A in B holds
exp (C,A) in exp (C,B)
proof
let C, A, B be Ordinal; ::_thesis: ( 1 in C & A in B implies exp (C,A) in exp (C,B) )
defpred S1[ Ordinal] means for A being Ordinal st A in $1 holds
exp (C,A) in exp (C,$1);
A1: for B being Ordinal st B <> {} & B is limit_ordinal & ( for D being Ordinal st D in B holds
S1[D] ) holds
S1[B]
proof
deffunc H1( Ordinal) -> set = exp (C,$1);
let B be Ordinal; ::_thesis: ( B <> {} & B is limit_ordinal & ( for D being Ordinal st D in B holds
S1[D] ) implies S1[B] )
assume that
A2: B <> {} and
A3: B is limit_ordinal and
A4: for D being Ordinal st D in B holds
S1[D] ; ::_thesis: S1[B]
consider fi being Ordinal-Sequence such that
A5: ( dom fi = B & ( for D being Ordinal st D in B holds
fi . D = H1(D) ) ) from ORDINAL2:sch_3();
fi is increasing
proof
let B1, B2 be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: ( not B1 in B2 or not B2 in dom fi or fi . B1 in fi . B2 )
assume that
A6: B1 in B2 and
A7: B2 in dom fi ; ::_thesis: fi . B1 in fi . B2
A8: fi . B1 = exp (C,B1) by A5, A6, A7, ORDINAL1:10;
exp (C,B1) in exp (C,B2) by A4, A5, A6, A7;
hence fi . B1 in fi . B2 by A5, A7, A8; ::_thesis: verum
end;
then A9: sup fi = lim fi by A2, A3, A5, Th8;
let A be Ordinal; ::_thesis: ( A in B implies exp (C,A) in exp (C,B) )
assume A10: A in B ; ::_thesis: exp (C,A) in exp (C,B)
fi . A = exp (C,A) by A10, A5;
then A11: exp (C,A) in rng fi by A10, A5, FUNCT_1:def_3;
exp (C,B) = lim fi by A2, A3, A5, ORDINAL2:45;
hence exp (C,A) in exp (C,B) by A9, A11, ORDINAL2:19; ::_thesis: verum
end;
assume A12: 1 in C ; ::_thesis: ( not A in B or exp (C,A) in exp (C,B) )
A13: for B being Ordinal st S1[B] holds
S1[ succ B]
proof
let B be Ordinal; ::_thesis: ( S1[B] implies S1[ succ B] )
assume A14: for A being Ordinal st A in B holds
exp (C,A) in exp (C,B) ; ::_thesis: S1[ succ B]
let A be Ordinal; ::_thesis: ( A in succ B implies exp (C,A) in exp (C,(succ B)) )
assume A in succ B ; ::_thesis: exp (C,A) in exp (C,(succ B))
then A15: A c= B by ORDINAL1:22;
A16: now__::_thesis:_(_A_<>_B_implies_exp_(C,A)_in_exp_(C,B)_)
assume A <> B ; ::_thesis: exp (C,A) in exp (C,B)
then A c< B by A15, XBOOLE_0:def_8;
hence exp (C,A) in exp (C,B) by A14, ORDINAL1:11; ::_thesis: verum
end;
exp (C,B) in exp (C,(succ B)) by A12, Th23;
hence exp (C,A) in exp (C,(succ B)) by A16, ORDINAL1:10; ::_thesis: verum
end;
A17: S1[ {} ] ;
for B being Ordinal holds S1[B] from ORDINAL2:sch_1(A17, A13, A1);
hence ( not A in B or exp (C,A) in exp (C,B) ) ; ::_thesis: verum
end;
theorem Th25: :: ORDINAL4:25
for fi being Ordinal-Sequence
for C being Ordinal st 1 in C & ( for A being Ordinal st A in dom fi holds
fi . A = exp (C,A) ) holds
fi is increasing
proof
let fi be Ordinal-Sequence; ::_thesis: for C being Ordinal st 1 in C & ( for A being Ordinal st A in dom fi holds
fi . A = exp (C,A) ) holds
fi is increasing
let C be Ordinal; ::_thesis: ( 1 in C & ( for A being Ordinal st A in dom fi holds
fi . A = exp (C,A) ) implies fi is increasing )
assume that
A1: 1 in C and
A2: for A being Ordinal st A in dom fi holds
fi . A = exp (C,A) ; ::_thesis: fi is increasing
let A be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not A in b1 or not b1 in dom fi or fi . A in fi . b1 )
let B be Ordinal; ::_thesis: ( not A in B or not B in dom fi or fi . A in fi . B )
assume that
A3: A in B and
A4: B in dom fi ; ::_thesis: fi . A in fi . B
A5: fi . B = exp (C,B) by A2, A4;
fi . A = exp (C,A) by A2, A3, A4, ORDINAL1:10;
hence fi . A in fi . B by A1, A3, A5, Th24; ::_thesis: verum
end;
theorem :: ORDINAL4:26
for C, A being Ordinal st 1 in C & A <> {} & A is limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp (C,B) ) holds
exp (C,A) = sup fi
proof
let C, A be Ordinal; ::_thesis: ( 1 in C & A <> {} & A is limit_ordinal implies for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp (C,B) ) holds
exp (C,A) = sup fi )
assume that
A1: 1 in C and
A2: A <> {} and
A3: A is limit_ordinal ; ::_thesis: for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp (C,B) ) holds
exp (C,A) = sup fi
let fi be Ordinal-Sequence; ::_thesis: ( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp (C,B) ) implies exp (C,A) = sup fi )
assume that
A4: dom fi = A and
A5: for B being Ordinal st B in A holds
fi . B = exp (C,B) ; ::_thesis: exp (C,A) = sup fi
fi is increasing by A1, A4, A5, Th25;
then lim fi = sup fi by A2, A3, A4, Th8;
hence exp (C,A) = sup fi by A2, A3, A4, A5, ORDINAL2:45; ::_thesis: verum
end;
theorem :: ORDINAL4:27
for C, A, B being Ordinal st C <> {} & A c= B holds
exp (C,A) c= exp (C,B)
proof
let C, A, B be Ordinal; ::_thesis: ( C <> {} & A c= B implies exp (C,A) c= exp (C,B) )
A1: ( A c< B iff ( A c= B & A <> B ) ) by XBOOLE_0:def_8;
assume C <> {} ; ::_thesis: ( not A c= B or exp (C,A) c= exp (C,B) )
then {} in C by ORDINAL3:8;
then A2: 1 c= C by Lm3, ORDINAL1:21;
assume A c= B ; ::_thesis: exp (C,A) c= exp (C,B)
then A3: ( A in B or A = B ) by A1, ORDINAL1:11;
now__::_thesis:_exp_(C,A)_c=_exp_(C,B)
percases ( C = 1 or C <> 1 ) ;
supposeA4: C = 1 ; ::_thesis: exp (C,A) c= exp (C,B)
then exp (C,A) = 1 by ORDINAL2:46;
hence exp (C,A) c= exp (C,B) by A4, ORDINAL2:46; ::_thesis: verum
end;
suppose C <> 1 ; ::_thesis: exp (C,A) c= exp (C,B)
then 1 c< C by A2, XBOOLE_0:def_8;
then 1 in C by ORDINAL1:11;
then ( exp (C,A) in exp (C,B) or exp (C,A) = exp (C,B) ) by A3, Th24;
hence exp (C,A) c= exp (C,B) by ORDINAL1:def_2; ::_thesis: verum
end;
end;
end;
hence exp (C,A) c= exp (C,B) ; ::_thesis: verum
end;
theorem :: ORDINAL4:28
for A, B, C being Ordinal st A c= B holds
exp (A,C) c= exp (B,C)
proof
let A, B, C be Ordinal; ::_thesis: ( A c= B implies exp (A,C) c= exp (B,C) )
defpred S1[ Ordinal] means exp (A,$1) c= exp (B,$1);
assume A1: A c= B ; ::_thesis: exp (A,C) c= exp (B,C)
A2: for C being Ordinal st S1[C] holds
S1[ succ C]
proof
let C be Ordinal; ::_thesis: ( S1[C] implies S1[ succ C] )
A3: exp (B,(succ C)) = B *^ (exp (B,C)) by ORDINAL2:44;
exp (A,(succ C)) = A *^ (exp (A,C)) by ORDINAL2:44;
hence ( S1[C] implies S1[ succ C] ) by A1, A3, ORDINAL3:20; ::_thesis: verum
end;
A4: for C being Ordinal st C <> {} & C is limit_ordinal & ( for D being Ordinal st D in C holds
S1[D] ) holds
S1[C]
proof
deffunc H1( Ordinal) -> set = exp (A,$1);
let C be Ordinal; ::_thesis: ( C <> {} & C is limit_ordinal & ( for D being Ordinal st D in C holds
S1[D] ) implies S1[C] )
assume that
A5: C <> {} and
A6: C is limit_ordinal and
A7: for D being Ordinal st D in C holds
exp (A,D) c= exp (B,D) ; ::_thesis: S1[C]
consider f1 being Ordinal-Sequence such that
A8: ( dom f1 = C & ( for D being Ordinal st D in C holds
f1 . D = H1(D) ) ) from ORDINAL2:sch_3();
deffunc H2( Ordinal) -> set = exp (B,$1);
consider f2 being Ordinal-Sequence such that
A9: ( dom f2 = C & ( for D being Ordinal st D in C holds
f2 . D = H2(D) ) ) from ORDINAL2:sch_3();
A10: now__::_thesis:_for_D_being_Ordinal_st_D_in_dom_f1_holds_
f1_._D_c=_f2_._D
let D be Ordinal; ::_thesis: ( D in dom f1 implies f1 . D c= f2 . D )
assume A11: D in dom f1 ; ::_thesis: f1 . D c= f2 . D
then A12: f1 . D = exp (A,D) by A8;
f2 . D = exp (B,D) by A8, A9, A11;
hence f1 . D c= f2 . D by A7, A8, A11, A12; ::_thesis: verum
end;
A13: exp (A,C) is_limes_of f1 by A5, A6, A8, Th21;
exp (B,C) is_limes_of f2 by A5, A6, A9, Th21;
hence S1[C] by A8, A9, A13, A10, Th6; ::_thesis: verum
end;
exp (A,{}) = 1 by ORDINAL2:43;
then A14: S1[ {} ] by ORDINAL2:43;
for C being Ordinal holds S1[C] from ORDINAL2:sch_1(A14, A2, A4);
hence exp (A,C) c= exp (B,C) ; ::_thesis: verum
end;
theorem :: ORDINAL4:29
for C, A being Ordinal st 1 in C & A <> {} holds
1 in exp (C,A)
proof
let C, A be Ordinal; ::_thesis: ( 1 in C & A <> {} implies 1 in exp (C,A) )
assume that
A1: 1 in C and
A2: A <> {} ; ::_thesis: 1 in exp (C,A)
exp (C,{}) = 1 by ORDINAL2:43;
hence 1 in exp (C,A) by A1, A2, Th24, ORDINAL3:8; ::_thesis: verum
end;
theorem Th30: :: ORDINAL4:30
for C, A, B being Ordinal holds exp (C,(A +^ B)) = (exp (C,B)) *^ (exp (C,A))
proof
let C, A, B be Ordinal; ::_thesis: exp (C,(A +^ B)) = (exp (C,B)) *^ (exp (C,A))
defpred S1[ Ordinal] means exp (C,(A +^ $1)) = (exp (C,$1)) *^ (exp (C,A));
A1: 1 = exp (C,{}) by ORDINAL2:43;
A2: for B being Ordinal st S1[B] holds
S1[ succ B]
proof
let B be Ordinal; ::_thesis: ( S1[B] implies S1[ succ B] )
assume A3: exp (C,(A +^ B)) = (exp (C,B)) *^ (exp (C,A)) ; ::_thesis: S1[ succ B]
thus exp (C,(A +^ (succ B))) = exp (C,(succ (A +^ B))) by ORDINAL2:28
.= C *^ (exp (C,(A +^ B))) by ORDINAL2:44
.= (C *^ (exp (C,B))) *^ (exp (C,A)) by A3, ORDINAL3:50
.= (exp (C,(succ B))) *^ (exp (C,A)) by ORDINAL2:44 ; ::_thesis: verum
end;
A4: for B being Ordinal st B <> {} & B is limit_ordinal & ( for D being Ordinal st D in B holds
S1[D] ) holds
S1[B]
proof
deffunc H1( Ordinal) -> set = exp (C,$1);
let B be Ordinal; ::_thesis: ( B <> {} & B is limit_ordinal & ( for D being Ordinal st D in B holds
S1[D] ) implies S1[B] )
assume that
A5: B <> {} and
A6: B is limit_ordinal and
A7: for D being Ordinal st D in B holds
exp (C,(A +^ D)) = (exp (C,D)) *^ (exp (C,A)) ; ::_thesis: S1[B]
consider fi being Ordinal-Sequence such that
A8: ( dom fi = B & ( for D being Ordinal st D in B holds
fi . D = H1(D) ) ) from ORDINAL2:sch_3();
consider psi being Ordinal-Sequence such that
A9: ( dom psi = A +^ B & ( for D being Ordinal st D in A +^ B holds
psi . D = H1(D) ) ) from ORDINAL2:sch_3();
deffunc H2( Ordinal) -> set = exp (C,$1);
consider f1 being Ordinal-Sequence such that
A10: ( dom f1 = A & ( for D being Ordinal st D in A holds
f1 . D = H2(D) ) ) from ORDINAL2:sch_3();
A11: now__::_thesis:_for_D_being_Ordinal_st_D_in_dom_(fi_*^_(exp_(C,A)))_holds_
psi_._((dom_f1)_+^_D)_=_(fi_*^_(exp_(C,A)))_._D
let D be Ordinal; ::_thesis: ( D in dom (fi *^ (exp (C,A))) implies psi . ((dom f1) +^ D) = (fi *^ (exp (C,A))) . D )
assume D in dom (fi *^ (exp (C,A))) ; ::_thesis: psi . ((dom f1) +^ D) = (fi *^ (exp (C,A))) . D
then A12: D in dom fi by ORDINAL3:def_4;
hence psi . ((dom f1) +^ D) = exp (C,(A +^ D)) by A8, A9, A10, ORDINAL2:32
.= (exp (C,D)) *^ (exp (C,A)) by A7, A8, A12
.= (fi . D) *^ (exp (C,A)) by A8, A12
.= (fi *^ (exp (C,A))) . D by A12, ORDINAL3:def_4 ;
::_thesis: verum
end;
A13: now__::_thesis:_for_D_being_Ordinal_st_D_in_dom_f1_holds_
psi_._D_=_f1_._D
let D be Ordinal; ::_thesis: ( D in dom f1 implies psi . D = f1 . D )
assume A14: D in dom f1 ; ::_thesis: psi . D = f1 . D
A c= A +^ B by ORDINAL3:24;
hence psi . D = exp (C,D) by A9, A10, A14
.= f1 . D by A10, A14 ;
::_thesis: verum
end;
dom psi = (dom f1) +^ (dom (fi *^ (exp (C,A)))) by A8, A9, A10, ORDINAL3:def_4;
then A15: psi = f1 ^ (fi *^ (exp (C,A))) by A13, A11, Def1;
(exp (C,B)) *^ (exp (C,A)) is_limes_of fi *^ (exp (C,A)) by A5, A6, A8, Th5, Th21;
then A16: (exp (C,B)) *^ (exp (C,A)) is_limes_of psi by A15, Th3;
A17: A +^ B <> {} by A5, ORDINAL3:26;
A +^ B is limit_ordinal by A5, A6, ORDINAL3:29;
then lim psi = exp (C,(A +^ B)) by A9, A17, ORDINAL2:45;
hence S1[B] by A16, ORDINAL2:def_10; ::_thesis: verum
end;
exp (C,A) = 1 *^ (exp (C,A)) by ORDINAL2:39;
then A18: S1[ {} ] by A1, ORDINAL2:27;
for B being Ordinal holds S1[B] from ORDINAL2:sch_1(A18, A2, A4);
hence exp (C,(A +^ B)) = (exp (C,B)) *^ (exp (C,A)) ; ::_thesis: verum
end;
theorem :: ORDINAL4:31
for C, A, B being Ordinal holds exp ((exp (C,A)),B) = exp (C,(B *^ A))
proof
let C, A, B be Ordinal; ::_thesis: exp ((exp (C,A)),B) = exp (C,(B *^ A))
defpred S1[ Ordinal] means exp ((exp (C,A)),$1) = exp (C,($1 *^ A));
A1: exp (C,{}) = 1 by ORDINAL2:43;
A2: for B being Ordinal st S1[B] holds
S1[ succ B]
proof
let B be Ordinal; ::_thesis: ( S1[B] implies S1[ succ B] )
assume exp ((exp (C,A)),B) = exp (C,(B *^ A)) ; ::_thesis: S1[ succ B]
hence exp ((exp (C,A)),(succ B)) = (exp (C,A)) *^ (exp (C,(B *^ A))) by ORDINAL2:44
.= exp (C,((B *^ A) +^ A)) by Th30
.= exp (C,((succ B) *^ A)) by ORDINAL2:36 ;
::_thesis: verum
end;
A3: for B being Ordinal st B <> {} & B is limit_ordinal & ( for D being Ordinal st D in B holds
S1[D] ) holds
S1[B]
proof
deffunc H1( Ordinal) -> set = exp ((exp (C,A)),$1);
let B be Ordinal; ::_thesis: ( B <> {} & B is limit_ordinal & ( for D being Ordinal st D in B holds
S1[D] ) implies S1[B] )
assume that
A4: B <> {} and
A5: B is limit_ordinal and
A6: for D being Ordinal st D in B holds
exp ((exp (C,A)),D) = exp (C,(D *^ A)) ; ::_thesis: S1[B]
consider fi being Ordinal-Sequence such that
A7: ( dom fi = B & ( for D being Ordinal st D in B holds
fi . D = H1(D) ) ) from ORDINAL2:sch_3();
deffunc H2( Ordinal) -> set = $1 *^ A;
consider f1 being Ordinal-Sequence such that
A8: ( dom f1 = B & ( for D being Ordinal st D in B holds
f1 . D = H2(D) ) ) from ORDINAL2:sch_3();
deffunc H3( Ordinal) -> set = exp (C,$1);
consider f2 being Ordinal-Sequence such that
A9: ( dom f2 = B *^ A & ( for D being Ordinal st D in B *^ A holds
f2 . D = H3(D) ) ) from ORDINAL2:sch_3();
A10: now__::_thesis:_(_A_<>_{}_implies_S1[B]_)
assume A11: A <> {} ; ::_thesis: S1[B]
then B *^ A <> {} by A4, ORDINAL3:31;
then A12: exp (C,(B *^ A)) is_limes_of f2 by A5, A9, Th21, ORDINAL3:40;
A13: rng f1 c= dom f2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f1 or x in dom f2 )
assume x in rng f1 ; ::_thesis: x in dom f2
then consider y being set such that
A14: y in dom f1 and
A15: x = f1 . y by FUNCT_1:def_3;
reconsider y = y as Ordinal by A14;
x = y *^ A by A8, A14, A15;
hence x in dom f2 by A8, A9, A11, A14, ORDINAL2:40; ::_thesis: verum
end;
A16: sup (rng f1) = dom f2
proof
sup (rng f1) c= sup (dom f2) by A13, ORDINAL2:22;
hence sup (rng f1) c= dom f2 by ORDINAL2:18; :: according to XBOOLE_0:def_10 ::_thesis: dom f2 c= sup (rng f1)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f2 or x in sup (rng f1) )
assume A17: x in dom f2 ; ::_thesis: x in sup (rng f1)
then reconsider D = x as Ordinal ;
consider A1 being Ordinal such that
A18: A1 in B and
A19: D in A1 *^ A by A5, A9, A17, ORDINAL3:41;
f1 . A1 = A1 *^ A by A8, A18;
then A1 *^ A in rng f1 by A8, A18, FUNCT_1:def_3;
then A1 *^ A in sup (rng f1) by ORDINAL2:19;
hence x in sup (rng f1) by A19, ORDINAL1:10; ::_thesis: verum
end;
A20: dom (f2 * f1) = B
proof
thus dom (f2 * f1) c= B by A8, RELAT_1:25; :: according to XBOOLE_0:def_10 ::_thesis: B c= dom (f2 * f1)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in dom (f2 * f1) )
assume A21: x in B ; ::_thesis: x in dom (f2 * f1)
then reconsider E = x as Ordinal ;
A22: f1 . E = E *^ A by A8, A21;
E *^ A in B *^ A by A11, A21, ORDINAL2:40;
hence x in dom (f2 * f1) by A8, A9, A21, A22, FUNCT_1:11; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_B_holds_
fi_._x_=_(f2_*_f1)_._x
let x be set ; ::_thesis: ( x in B implies fi . x = (f2 * f1) . x )
assume A23: x in B ; ::_thesis: fi . x = (f2 * f1) . x
then reconsider D = x as Ordinal ;
A24: f1 . D = D *^ A by A8, A23;
thus fi . x = exp ((exp (C,A)),D) by A7, A23
.= exp (C,(D *^ A)) by A6, A23
.= f2 . (f1 . D) by A9, A11, A23, A24, ORDINAL2:40
.= (f2 * f1) . x by A8, A23, FUNCT_1:13 ; ::_thesis: verum
end;
then fi = f2 * f1 by A7, A20, FUNCT_1:2;
then exp (C,(B *^ A)) is_limes_of fi by A8, A11, A12, A16, Th14, Th19;
then exp (C,(B *^ A)) = lim fi by ORDINAL2:def_10;
hence S1[B] by A4, A5, A7, ORDINAL2:45; ::_thesis: verum
end;
A25: B *^ {} = {} by ORDINAL2:38;
exp (C,{}) = 1 by ORDINAL2:43;
hence S1[B] by A25, A10, ORDINAL2:46; ::_thesis: verum
end;
exp ((exp (C,A)),{}) = 1 by ORDINAL2:43;
then A26: S1[ {} ] by A1, ORDINAL2:35;
for B being Ordinal holds S1[B] from ORDINAL2:sch_1(A26, A2, A3);
hence exp ((exp (C,A)),B) = exp (C,(B *^ A)) ; ::_thesis: verum
end;
theorem :: ORDINAL4:32
for C, A being Ordinal st 1 in C holds
A c= exp (C,A)
proof
let C, A be Ordinal; ::_thesis: ( 1 in C implies A c= exp (C,A) )
defpred S1[ Ordinal] means $1 c= exp (C,$1);
assume A1: 1 in C ; ::_thesis: A c= exp (C,A)
A2: for B being Ordinal st S1[B] holds
S1[ succ B]
proof
let B be Ordinal; ::_thesis: ( S1[B] implies S1[ succ B] )
assume A3: B c= exp (C,B) ; ::_thesis: S1[ succ B]
A4: exp (C,B) = 1 *^ (exp (C,B)) by ORDINAL2:39;
exp (C,(succ B)) = C *^ (exp (C,B)) by ORDINAL2:44;
then exp (C,B) in exp (C,(succ B)) by A1, A4, Th22, ORDINAL2:40;
then B in exp (C,(succ B)) by A3, ORDINAL1:12;
hence S1[ succ B] by ORDINAL1:21; ::_thesis: verum
end;
A5: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
deffunc H1( Ordinal) -> set = exp (C,$1);
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume that
A6: A <> {} and
A7: A is limit_ordinal and
A8: for B being Ordinal st B in A holds
B c= exp (C,B) ; ::_thesis: S1[A]
consider fi being Ordinal-Sequence such that
A9: ( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = H1(B) ) ) from ORDINAL2:sch_3();
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in exp (C,A) )
assume A10: x in A ; ::_thesis: x in exp (C,A)
then reconsider B = x as Ordinal ;
fi . B = exp (C,B) by A9, A10;
then exp (C,B) in rng fi by A9, A10, FUNCT_1:def_3;
then A11: exp (C,B) in sup fi by ORDINAL2:19;
fi is increasing by A1, A9, Th25;
then A12: sup fi = lim fi by A6, A7, A9, Th8
.= exp (C,A) by A6, A7, A9, ORDINAL2:45 ;
B c= exp (C,B) by A8, A10;
hence x in exp (C,A) by A12, A11, ORDINAL1:12; ::_thesis: verum
end;
A13: S1[ {} ] by XBOOLE_1:2;
for B being Ordinal holds S1[B] from ORDINAL2:sch_1(A13, A2, A5);
hence A c= exp (C,A) ; ::_thesis: verum
end;
scheme :: ORDINAL4:sch 1
CriticalNumber{ F1( Ordinal) -> Ordinal } :
ex A being Ordinal st F1(A) = A
provided
A1: for A, B being Ordinal st A in B holds
F1(A) in F1(B) and
A2: for A being Ordinal st A <> {} & A is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = A & ( for B being Ordinal st B in A holds
phi . B = F1(B) ) holds
F1(A) is_limes_of phi
proof
A3: now__::_thesis:_for_A_being_Ordinal_holds_not_S1[A]
defpred S1[ Ordinal] means not $1 c= F1($1);
assume A4: ex A being Ordinal st S1[A] ; ::_thesis: contradiction
consider A being Ordinal such that
A5: S1[A] and
A6: for B being Ordinal st S1[B] holds
A c= B from ORDINAL1:sch_1(A4);
F1(F1(A)) in F1(A) by A1, A5, ORDINAL1:16;
then not F1(A) c= F1(F1(A)) by ORDINAL1:5;
hence contradiction by A5, A6; ::_thesis: verum
end;
deffunc H1( Ordinal, T-Sequence) -> set = {} ;
deffunc H2( Ordinal, Ordinal) -> Ordinal = F1($2);
consider phi being Ordinal-Sequence such that
A7: dom phi = omega and
A8: ( {} in omega implies phi . {} = F1({}) ) and
A9: for A being Ordinal st succ A in omega holds
phi . (succ A) = H2(A,phi . A) and
for A being Ordinal st A in omega & A <> {} & A is limit_ordinal holds
phi . A = H1(A,phi | A) from ORDINAL2:sch_11();
assume A10: for A being Ordinal holds not F1(A) = A ; ::_thesis: contradiction
A11: now__::_thesis:_for_A_being_Ordinal_holds_A_in_F1(A)
let A be Ordinal; ::_thesis: A in F1(A)
A12: A <> F1(A) by A10;
A c= F1(A) by A3;
then A c< F1(A) by A12, XBOOLE_0:def_8;
hence A in F1(A) by ORDINAL1:11; ::_thesis: verum
end;
A13: phi is increasing
proof
let A be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not A in b1 or not b1 in dom phi or phi . A in phi . b1 )
let B be Ordinal; ::_thesis: ( not A in B or not B in dom phi or phi . A in phi . B )
assume that
A14: A in B and
A15: B in dom phi ; ::_thesis: phi . A in phi . B
defpred S1[ Ordinal] means ( A +^ $1 in omega & $1 <> {} implies phi . A in phi . (A +^ $1) );
A16: for B being Ordinal st B <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds
S1[C] ) holds
S1[B]
proof
let B be Ordinal; ::_thesis: ( B <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds
S1[C] ) implies S1[B] )
assume that
A17: B <> {} and
A18: B is limit_ordinal and
for C being Ordinal st C in B & A +^ C in omega & C <> {} holds
phi . A in phi . (A +^ C) and
A19: A +^ B in omega and
A20: B <> {} ; ::_thesis: phi . A in phi . (A +^ B)
A +^ B <> {} by A20, ORDINAL3:26;
then A21: {} in A +^ B by ORDINAL3:8;
A +^ B is limit_ordinal by A17, A18, ORDINAL3:29;
then omega c= A +^ B by A21, ORDINAL1:def_11;
hence phi . A in phi . (A +^ B) by A19, ORDINAL1:5; ::_thesis: verum
end;
A22: for C being Ordinal st S1[C] holds
S1[ succ C]
proof
let C be Ordinal; ::_thesis: ( S1[C] implies S1[ succ C] )
assume that
A23: ( A +^ C in omega & C <> {} implies phi . A in phi . (A +^ C) ) and
A24: A +^ (succ C) in omega and
succ C <> {} ; ::_thesis: phi . A in phi . (A +^ (succ C))
reconsider D = phi . (A +^ C) as Ordinal ;
A25: A +^ C in succ (A +^ C) by ORDINAL1:6;
A26: D in F1(D) by A11;
A27: A +^ (succ C) = succ (A +^ C) by ORDINAL2:28;
then phi . (A +^ (succ C)) = F1(D) by A9, A24;
hence phi . A in phi . (A +^ (succ C)) by A23, A24, A25, A27, A26, ORDINAL1:10, ORDINAL2:27; ::_thesis: verum
end;
A28: S1[ {} ] ;
A29: for C being Ordinal holds S1[C] from ORDINAL2:sch_1(A28, A22, A16);
ex C being Ordinal st
( B = A +^ C & C <> {} ) by A14, ORDINAL3:28;
hence phi . A in phi . B by A7, A15, A29; ::_thesis: verum
end;
deffunc H3( Ordinal) -> Ordinal = F1($1);
consider fi being Ordinal-Sequence such that
A30: ( dom fi = sup phi & ( for A being Ordinal st A in sup phi holds
fi . A = H3(A) ) ) from ORDINAL2:sch_3();
H3( {} ) in rng phi by A7, A8, Lm1, FUNCT_1:def_3;
then A31: sup phi <> {} by ORDINAL2:19;
then A32: H3( sup phi) is_limes_of fi by A2, A7, A13, A30, Lm2, Th16;
A33: sup fi c= sup phi
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in sup fi or x in sup phi )
assume A34: x in sup fi ; ::_thesis: x in sup phi
then reconsider A = x as Ordinal ;
consider B being Ordinal such that
A35: B in rng fi and
A36: A c= B by A34, ORDINAL2:21;
consider y being set such that
A37: y in dom fi and
A38: B = fi . y by A35, FUNCT_1:def_3;
reconsider y = y as Ordinal by A37;
consider C being Ordinal such that
A39: C in rng phi and
A40: y c= C by A30, A37, ORDINAL2:21;
( y c< C iff ( y <> C & y c= C ) ) by XBOOLE_0:def_8;
then A41: ( H3(y) in H3(C) or y = C ) by A1, A40, ORDINAL1:11;
B = H3(y) by A30, A37, A38;
then A42: B c= H3(C) by A41, ORDINAL1:def_2;
consider z being set such that
A43: z in dom phi and
A44: C = phi . z by A39, FUNCT_1:def_3;
reconsider z = z as Ordinal by A43;
A45: succ z in omega by A7, A43, Lm2, ORDINAL1:28;
then A46: phi . (succ z) in rng phi by A7, FUNCT_1:def_3;
phi . (succ z) = H3(C) by A9, A44, A45;
then H3(C) in sup phi by A46, ORDINAL2:19;
then B in sup phi by A42, ORDINAL1:12;
hence x in sup phi by A36, ORDINAL1:12; ::_thesis: verum
end;
A47: fi is increasing
proof
let A be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not A in b1 or not b1 in dom fi or fi . A in fi . b1 )
let B be Ordinal; ::_thesis: ( not A in B or not B in dom fi or fi . A in fi . B )
assume that
A48: A in B and
A49: B in dom fi ; ::_thesis: fi . A in fi . B
A50: fi . B = H3(B) by A30, A49;
fi . A = H3(A) by A30, A48, A49, ORDINAL1:10;
hence fi . A in fi . B by A1, A48, A50; ::_thesis: verum
end;
sup phi is limit_ordinal by A7, A13, Lm2, Th16;
then sup fi = lim fi by A30, A31, A47, Th8
.= H3( sup phi) by A32, ORDINAL2:def_10 ;
hence contradiction by A11, A33, ORDINAL1:5; ::_thesis: verum
end;
registration
let W be Universe;
cluster ordinal for Element of W;
existence
ex b1 being Element of W st b1 is ordinal
proof
A1: On W c= W by ORDINAL2:7;
{} in On W by CLASSES2:51, ORDINAL3:8;
hence ex b1 being Element of W st b1 is ordinal by A1; ::_thesis: verum
end;
end;
definition
let W be Universe;
mode Ordinal of W is ordinal Element of W;
mode Ordinal-Sequence of W is Function of (On W),(On W);
end;
registration
let W be Universe;
cluster epsilon-transitive epsilon-connected ordinal non empty for Element of W;
existence
not for b1 being Ordinal of W holds b1 is empty
proof
A1: On W c= W by ORDINAL2:7;
{} in On W by CLASSES2:51, ORDINAL3:8;
then 1 in W by A1, Lm3, CLASSES2:5;
hence not for b1 being Ordinal of W holds b1 is empty ; ::_thesis: verum
end;
end;
registration
let W be Universe;
cluster On W -> non empty ;
coherence
not On W is empty by CLASSES2:51;
end;
registration
let W be Universe;
cluster Function-like V25( On W, On W) -> T-Sequence-like Ordinal-yielding for Element of bool [:(On W),(On W):];
coherence
for b1 being Ordinal-Sequence of W holds
( b1 is T-Sequence-like & b1 is Ordinal-yielding )
proof
let s be Ordinal-Sequence of W; ::_thesis: ( s is T-Sequence-like & s is Ordinal-yielding )
thus dom s is ordinal by FUNCT_2:def_1; :: according to ORDINAL1:def_7 ::_thesis: s is Ordinal-yielding
take On W ; :: according to ORDINAL2:def_4 ::_thesis: rng s c= On W
thus rng s c= On W by RELAT_1:def_19; ::_thesis: verum
end;
end;
scheme :: ORDINAL4:sch 2
UOSLambda{ F1() -> Universe, F2( set ) -> Ordinal of F1() } :
ex phi being Ordinal-Sequence of F1() st
for a being Ordinal of F1() holds phi . a = F2(a)
proof
consider psi being Ordinal-Sequence such that
A1: ( dom psi = On F1() & ( for A being Ordinal st A in On F1() holds
psi . A = F2(A) ) ) from ORDINAL2:sch_3();
rng psi c= On F1()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng psi or x in On F1() )
assume x in rng psi ; ::_thesis: x in On F1()
then consider y being set such that
A2: y in dom psi and
A3: x = psi . y by FUNCT_1:def_3;
reconsider y = y as Ordinal by A2;
x = F2(y) by A1, A2, A3;
hence x in On F1() by ORDINAL1:def_9; ::_thesis: verum
end;
then reconsider psi = psi as Ordinal-Sequence of F1() by A1, FUNCT_2:def_1, RELSET_1:4;
take psi ; ::_thesis: for a being Ordinal of F1() holds psi . a = F2(a)
let a be Ordinal of F1(); ::_thesis: psi . a = F2(a)
a in On F1() by ORDINAL1:def_9;
hence psi . a = F2(a) by A1; ::_thesis: verum
end;
definition
let W be Universe;
func 0-element_of W -> Ordinal of W equals :: ORDINAL4:def 2
{} ;
correctness
coherence
{} is Ordinal of W;
proof
A1: On W c= W by ORDINAL2:7;
{} in On W by ORDINAL3:8;
then reconsider A = {} as Ordinal of W by A1;
A = {} ;
hence {} is Ordinal of W ; ::_thesis: verum
end;
func 1-element_of W -> non empty Ordinal of W equals :: ORDINAL4:def 3
1;
correctness
coherence
1 is non empty Ordinal of W;
proof
A2: On W c= W by ORDINAL2:7;
{} in On W by ORDINAL3:8;
then reconsider A = 1 as Ordinal of W by A2, Lm3, CLASSES2:5;
A = 1 ;
hence 1 is non empty Ordinal of W ; ::_thesis: verum
end;
let phi be Ordinal-Sequence of W;
let A1 be Ordinal of W;
:: original: .
redefine funcphi . A1 -> Ordinal of W;
coherence
phi . A1 is Ordinal of W
proof
reconsider B = phi . A1 as Ordinal ;
A3: dom phi = On W by FUNCT_2:def_1;
A4: rng phi c= On W by RELAT_1:def_19;
A1 in On W by ORDINAL1:def_9;
then B in rng phi by A3, FUNCT_1:def_3;
then A5: B in On W by A4;
On W c= W by ORDINAL2:7;
hence phi . A1 is Ordinal of W by A5; ::_thesis: verum
end;
end;
:: deftheorem defines 0-element_of ORDINAL4:def_2_:_
for W being Universe holds 0-element_of W = {} ;
:: deftheorem defines 1-element_of ORDINAL4:def_3_:_
for W being Universe holds 1-element_of W = 1;
definition
let W be Universe;
let p2, p1 be Ordinal-Sequence of W;
:: original: *
redefine funcp1 * p2 -> Ordinal-Sequence of W;
coherence
p2 * p1 is Ordinal-Sequence of W
proof
A1: rng p2 c= On W by RELAT_1:def_19;
A2: dom p2 = On W by FUNCT_2:def_1;
dom p1 = On W by FUNCT_2:def_1;
then A3: dom (p1 * p2) = On W by A2, A1, RELAT_1:27;
then reconsider f = p1 * p2 as T-Sequence by ORDINAL1:def_7;
A4: rng p1 c= On W by RELAT_1:def_19;
rng (p1 * p2) c= rng p1 by RELAT_1:26;
then rng f c= On W by A4, XBOOLE_1:1;
hence p2 * p1 is Ordinal-Sequence of W by A3, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
end;
theorem :: ORDINAL4:33
for W being Universe holds
( 0-element_of W = {} & 1-element_of W = 1 ) ;
definition
let W be Universe;
let A1 be Ordinal of W;
:: original: succ
redefine func succ A1 -> non empty Ordinal of W;
coherence
succ A1 is non empty Ordinal of W by CLASSES2:5;
let B1 be Ordinal of W;
:: original: +^
redefine funcA1 +^ B1 -> Ordinal of W;
coherence
A1 +^ B1 is Ordinal of W
proof
defpred S1[ Ordinal] means ( $1 in W implies A1 +^ $1 in W );
A1: for B being Ordinal st ( for C being Ordinal st C in B holds
S1[C] ) holds
S1[B]
proof
let B be Ordinal; ::_thesis: ( ( for C being Ordinal st C in B holds
S1[C] ) implies S1[B] )
assume that
A2: for C being Ordinal st C in B & C in W holds
A1 +^ C in W and
A3: B in W ; ::_thesis: A1 +^ B in W
[:B,{(1-element_of W)}:] in W by A3, CLASSES2:61;
then [:A1,{(0-element_of W)}:] \/ [:B,{(1-element_of W)}:] in W by CLASSES2:60;
then A4: card ([:A1,{(0-element_of W)}:] \/ [:B,{(1-element_of W)}:]) in card W by CLASSES2:1;
A5: A1 +^ B c= W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A1 +^ B or x in W )
assume A6: x in A1 +^ B ; ::_thesis: x in W
then reconsider A = x as Ordinal ;
A7: now__::_thesis:_(_A1_c=_A_implies_x_in_W_)
A8: B c= W by A3, ORDINAL1:def_2;
assume A1 c= A ; ::_thesis: x in W
then consider C being Ordinal such that
A9: A = A1 +^ C by ORDINAL3:27;
C in B by A6, A9, ORDINAL3:22;
hence x in W by A2, A9, A8; ::_thesis: verum
end;
A10: ( A in A1 or A1 c= A ) by ORDINAL1:16;
A1 c= W by ORDINAL1:def_2;
hence x in W by A10, A7; ::_thesis: verum
end;
card (A1 +^ B) = card ([:A1,{(0-element_of W)}:] \/ [:B,{(1-element_of W)}:]) by CARD_2:9;
hence A1 +^ B in W by A4, A5, CLASSES1:1; ::_thesis: verum
end;
for B being Ordinal holds S1[B] from ORDINAL1:sch_2(A1);
hence A1 +^ B1 is Ordinal of W ; ::_thesis: verum
end;
end;
definition
let W be Universe;
let A1, B1 be Ordinal of W;
:: original: *^
redefine funcA1 *^ B1 -> Ordinal of W;
coherence
A1 *^ B1 is Ordinal of W
proof
defpred S1[ Ordinal] means ( $1 in W implies $1 *^ B1 in W );
A1: for A being Ordinal st ( for C being Ordinal st C in A holds
S1[C] ) holds
S1[A]
proof
let A be Ordinal; ::_thesis: ( ( for C being Ordinal st C in A holds
S1[C] ) implies S1[A] )
assume that
A2: for C being Ordinal st C in A & C in W holds
C *^ B1 in W and
A3: A in W ; ::_thesis: A *^ B1 in W
[:A,B1:] in W by A3, CLASSES2:61;
then A4: card [:A,B1:] in card W by CLASSES2:1;
A5: A *^ B1 c= W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A *^ B1 or x in W )
A6: B1 c= W by ORDINAL1:def_2;
assume A7: x in A *^ B1 ; ::_thesis: x in W
then reconsider B = x as Ordinal ;
B1 <> {} by A7, ORDINAL2:38;
then consider C, D being Ordinal such that
A8: B = (C *^ B1) +^ D and
A9: D in B1 by ORDINAL3:47;
C *^ B1 c= B by A8, ORDINAL3:24;
then C *^ B1 in A *^ B1 by A7, ORDINAL1:12;
then A10: C in A by ORDINAL3:34;
A c= W by A3, ORDINAL1:def_2;
then reconsider CB = C *^ B1, D = D as Ordinal of W by A2, A9, A6, A10;
x = CB +^ D by A8;
hence x in W ; ::_thesis: verum
end;
card (A *^ B1) = card [:A,B1:] by CARD_2:11;
hence A *^ B1 in W by A4, A5, CLASSES1:1; ::_thesis: verum
end;
for A being Ordinal holds S1[A] from ORDINAL1:sch_2(A1);
hence A1 *^ B1 is Ordinal of W ; ::_thesis: verum
end;
end;
theorem Th34: :: ORDINAL4:34
for W being Universe
for A1 being Ordinal of W
for phi being Ordinal-Sequence of W holds A1 in dom phi
proof
let W be Universe; ::_thesis: for A1 being Ordinal of W
for phi being Ordinal-Sequence of W holds A1 in dom phi
let A1 be Ordinal of W; ::_thesis: for phi being Ordinal-Sequence of W holds A1 in dom phi
let phi be Ordinal-Sequence of W; ::_thesis: A1 in dom phi
dom phi = On W by FUNCT_2:def_1;
hence A1 in dom phi by ORDINAL1:def_9; ::_thesis: verum
end;
theorem Th35: :: ORDINAL4:35
for fi being Ordinal-Sequence
for W being Universe st dom fi in W & rng fi c= W holds
sup fi in W
proof
let fi be Ordinal-Sequence; ::_thesis: for W being Universe st dom fi in W & rng fi c= W holds
sup fi in W
let W be Universe; ::_thesis: ( dom fi in W & rng fi c= W implies sup fi in W )
assume that
A1: dom fi in W and
A2: rng fi c= W ; ::_thesis: sup fi in W
ex A being Ordinal st rng fi c= A by ORDINAL2:def_4;
then for x being set st x in rng fi holds
x is Ordinal ;
then reconsider B = union (rng fi) as Ordinal by ORDINAL1:23;
A3: rng fi = fi .: (dom fi) by RELAT_1:113;
A4: sup fi c= succ B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in sup fi or x in succ B )
assume A5: x in sup fi ; ::_thesis: x in succ B
then reconsider A = x as Ordinal ;
consider C being Ordinal such that
A6: C in rng fi and
A7: A c= C by A5, ORDINAL2:21;
C c= union (rng fi) by A6, ZFMISC_1:74;
then A c= B by A7, XBOOLE_1:1;
hence x in succ B by ORDINAL1:22; ::_thesis: verum
end;
card (dom fi) in card W by A1, CLASSES2:1;
then card (rng fi) in card W by A3, CARD_1:67, ORDINAL1:12;
then rng fi in W by A2, CLASSES1:1;
then union (rng fi) in W by CLASSES2:59;
then succ B in W by CLASSES2:5;
hence sup fi in W by A4, CLASSES1:def_1; ::_thesis: verum
end;
theorem :: ORDINAL4:36
for W being Universe
for phi being Ordinal-Sequence of W st phi is increasing & phi is continuous & omega in W holds
ex A being Ordinal st
( A in dom phi & phi . A = A )
proof
let W be Universe; ::_thesis: for phi being Ordinal-Sequence of W st phi is increasing & phi is continuous & omega in W holds
ex A being Ordinal st
( A in dom phi & phi . A = A )
let phi be Ordinal-Sequence of W; ::_thesis: ( phi is increasing & phi is continuous & omega in W implies ex A being Ordinal st
( A in dom phi & phi . A = A ) )
deffunc H1( set , set ) -> set = {} ;
assume that
A1: phi is increasing and
A2: phi is continuous and
A3: omega in W ; ::_thesis: ex A being Ordinal st
( A in dom phi & phi . A = A )
deffunc H2( set , set ) -> set = phi . $2;
reconsider N = phi . (0-element_of W) as Ordinal ;
consider L being T-Sequence such that
A4: dom L = omega and
A5: ( {} in omega implies L . {} = N ) and
A6: for A being Ordinal st succ A in omega holds
L . (succ A) = H2(A,L . A) and
for A being Ordinal st A in omega & A <> {} & A is limit_ordinal holds
L . A = H1(A,L | A) from ORDINAL2:sch_5();
defpred S1[ Ordinal] means ( $1 in dom L implies L . $1 is Ordinal of W );
A7: for A being Ordinal st S1[A] holds
S1[ succ A]
proof
let A be Ordinal; ::_thesis: ( S1[A] implies S1[ succ A] )
assume that
A8: ( A in dom L implies L . A is Ordinal of W ) and
A9: succ A in dom L ; ::_thesis: L . (succ A) is Ordinal of W
A in succ A by ORDINAL1:6;
then reconsider x = L . A as Ordinal of W by A8, A9, ORDINAL1:10;
L . (succ A) = phi . x by A4, A6, A9;
hence L . (succ A) is Ordinal of W ; ::_thesis: verum
end;
A10: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume that
A11: A <> {} and
A12: A is limit_ordinal and
for B being Ordinal st B in A & B in dom L holds
L . B is Ordinal of W and
A13: A in dom L ; ::_thesis: L . A is Ordinal of W
{} in A by A11, ORDINAL3:8;
then omega c= A by A12, ORDINAL1:def_11;
hence L . A is Ordinal of W by A4, A13, ORDINAL1:5; ::_thesis: verum
end;
A14: S1[ {} ] by A4, A5;
A15: for A being Ordinal holds S1[A] from ORDINAL2:sch_1(A14, A7, A10);
rng L c= sup (rng L)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng L or x in sup (rng L) )
assume A16: x in rng L ; ::_thesis: x in sup (rng L)
then consider y being set such that
A17: y in dom L and
A18: x = L . y by FUNCT_1:def_3;
reconsider y = y as Ordinal by A17;
reconsider A = L . y as Ordinal of W by A15, A17;
A in sup (rng L) by A16, A18, ORDINAL2:19;
hence x in sup (rng L) by A18; ::_thesis: verum
end;
then reconsider L = L as Ordinal-Sequence by ORDINAL2:def_4;
A19: dom phi = On W by FUNCT_2:def_1;
assume A20: for A being Ordinal holds
( not A in dom phi or not phi . A = A ) ; ::_thesis: contradiction
A21: now__::_thesis:_for_A1_being_Ordinal_of_W_holds_A1_in_phi_._A1
let A1 be Ordinal of W; ::_thesis: A1 in phi . A1
A1 in dom phi by Th34;
then A22: A1 c= phi . A1 by A1, Th10;
A1 <> phi . A1 by A20, Th34;
then A1 c< phi . A1 by A22, XBOOLE_0:def_8;
hence A1 in phi . A1 by ORDINAL1:11; ::_thesis: verum
end;
L is increasing
proof
let A be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not A in b1 or not b1 in dom L or L . A in L . b1 )
let B be Ordinal; ::_thesis: ( not A in B or not B in dom L or L . A in L . B )
assume that
A23: A in B and
A24: B in dom L ; ::_thesis: L . A in L . B
defpred S2[ Ordinal] means ( A +^ $1 in omega & $1 <> {} implies L . A in L . (A +^ $1) );
A25: for B being Ordinal st B <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds
S2[C] ) holds
S2[B]
proof
let B be Ordinal; ::_thesis: ( B <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds
S2[C] ) implies S2[B] )
assume that
A26: B <> {} and
A27: B is limit_ordinal and
for C being Ordinal st C in B & A +^ C in omega & C <> {} holds
L . A in L . (A +^ C) and
A28: A +^ B in omega and
A29: B <> {} ; ::_thesis: L . A in L . (A +^ B)
A +^ B <> {} by A29, ORDINAL3:26;
then A30: {} in A +^ B by ORDINAL3:8;
A +^ B is limit_ordinal by A26, A27, ORDINAL3:29;
then omega c= A +^ B by A30, ORDINAL1:def_11;
hence L . A in L . (A +^ B) by A28, ORDINAL1:5; ::_thesis: verum
end;
A31: for C being Ordinal st S2[C] holds
S2[ succ C]
proof
let C be Ordinal; ::_thesis: ( S2[C] implies S2[ succ C] )
assume that
A32: ( A +^ C in omega & C <> {} implies L . A in L . (A +^ C) ) and
A33: A +^ (succ C) in omega and
succ C <> {} ; ::_thesis: L . A in L . (A +^ (succ C))
A34: A +^ (succ C) = succ (A +^ C) by ORDINAL2:28;
A35: A +^ C in succ (A +^ C) by ORDINAL1:6;
then reconsider D = L . (A +^ C) as Ordinal of W by A4, A15, A33, A34, ORDINAL1:10;
A36: D in phi . D by A21;
L . (A +^ (succ C)) = phi . D by A6, A33, A34;
hence L . A in L . (A +^ (succ C)) by A32, A33, A35, A34, A36, ORDINAL1:10, ORDINAL2:27; ::_thesis: verum
end;
A37: S2[ {} ] ;
A38: for C being Ordinal holds S2[C] from ORDINAL2:sch_1(A37, A31, A25);
ex C being Ordinal st
( B = A +^ C & C <> {} ) by A23, ORDINAL3:28;
hence L . A in L . B by A4, A24, A38; ::_thesis: verum
end;
then A39: sup L is limit_ordinal by A4, Lm2, Th16;
A40: rng L c= W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng L or x in W )
assume x in rng L ; ::_thesis: x in W
then consider y being set such that
A41: y in dom L and
A42: x = L . y by FUNCT_1:def_3;
reconsider y = y as Ordinal by A41;
L . y is Ordinal of W by A15, A41;
hence x in W by A42; ::_thesis: verum
end;
then reconsider S = sup L as Ordinal of W by A3, A4, Th35;
set fi = phi | (sup L);
N in rng L by A4, A5, Lm1, FUNCT_1:def_3;
then A43: sup L <> {} by ORDINAL2:19;
A44: S in On W by ORDINAL1:def_9;
then A45: phi . S is_limes_of phi | (sup L) by A2, A43, A39, A19, ORDINAL2:def_13;
S c= dom phi by A44, A19, ORDINAL1:def_2;
then A46: dom (phi | (sup L)) = S by RELAT_1:62;
A47: sup (phi | (sup L)) c= sup L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in sup (phi | (sup L)) or x in sup L )
assume A48: x in sup (phi | (sup L)) ; ::_thesis: x in sup L
then reconsider A = x as Ordinal ;
consider B being Ordinal such that
A49: B in rng (phi | (sup L)) and
A50: A c= B by A48, ORDINAL2:21;
consider y being set such that
A51: y in dom (phi | (sup L)) and
A52: B = (phi | (sup L)) . y by A49, FUNCT_1:def_3;
reconsider y = y as Ordinal by A51;
consider C being Ordinal such that
A53: C in rng L and
A54: y c= C by A46, A51, ORDINAL2:21;
reconsider C1 = C as Ordinal of W by A40, A53;
( y c< C1 iff ( y c= C1 & y <> C1 ) ) by XBOOLE_0:def_8;
then ( ( y in C1 & C1 in dom phi ) or y = C ) by A19, A54, ORDINAL1:11, ORDINAL1:def_9;
then A55: ( phi . y in phi . C1 or y = C1 ) by A1, ORDINAL2:def_12;
B = phi . y by A51, A52, FUNCT_1:47;
then A56: B c= phi . C1 by A55, ORDINAL1:def_2;
consider z being set such that
A57: z in dom L and
A58: C = L . z by A53, FUNCT_1:def_3;
reconsider z = z as Ordinal by A57;
A59: succ z in omega by A4, A57, Lm2, ORDINAL1:28;
then A60: L . (succ z) in rng L by A4, FUNCT_1:def_3;
L . (succ z) = phi . C by A6, A58, A59;
then phi . C1 in sup L by A60, ORDINAL2:19;
then B in sup L by A56, ORDINAL1:12;
hence x in sup L by A50, ORDINAL1:12; ::_thesis: verum
end;
phi | (sup L) is increasing
proof
A61: dom (phi | (sup L)) c= dom phi by RELAT_1:60;
let A be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not A in b1 or not b1 in dom (phi | (sup L)) or (phi | (sup L)) . A in (phi | (sup L)) . b1 )
let B be Ordinal; ::_thesis: ( not A in B or not B in dom (phi | (sup L)) or (phi | (sup L)) . A in (phi | (sup L)) . B )
assume that
A62: A in B and
A63: B in dom (phi | (sup L)) ; ::_thesis: (phi | (sup L)) . A in (phi | (sup L)) . B
A64: (phi | (sup L)) . B = phi . B by A63, FUNCT_1:47;
(phi | (sup L)) . A = phi . A by A62, A63, FUNCT_1:47, ORDINAL1:10;
hence (phi | (sup L)) . A in (phi | (sup L)) . B by A1, A62, A63, A61, A64, ORDINAL2:def_12; ::_thesis: verum
end;
then sup (phi | (sup L)) = lim (phi | (sup L)) by A43, A39, A46, Th8
.= phi . (sup L) by A45, ORDINAL2:def_10 ;
then not S in phi . S by A47, ORDINAL1:5;
hence contradiction by A21; ::_thesis: verum
end;
begin
theorem :: ORDINAL4:37
for A, B, C being Ordinal st A is_cofinal_with B & B is_cofinal_with C holds
A is_cofinal_with C
proof
let A, B, C be Ordinal; ::_thesis: ( A is_cofinal_with B & B is_cofinal_with C implies A is_cofinal_with C )
given xi1 being Ordinal-Sequence such that A1: dom xi1 = B and
A2: rng xi1 c= A and
A3: xi1 is increasing and
A4: A = sup xi1 ; :: according to ORDINAL2:def_17 ::_thesis: ( not B is_cofinal_with C or A is_cofinal_with C )
given xi2 being Ordinal-Sequence such that A5: dom xi2 = C and
A6: rng xi2 c= B and
A7: xi2 is increasing and
A8: B = sup xi2 ; :: according to ORDINAL2:def_17 ::_thesis: A is_cofinal_with C
consider xi being Ordinal-Sequence such that
A9: xi = xi1 * xi2 and
A10: xi is increasing by A3, A7, Th13;
take xi ; :: according to ORDINAL2:def_17 ::_thesis: ( dom xi = C & rng xi c= A & xi is increasing & A = sup xi )
thus A11: dom xi = C by A1, A5, A6, A9, RELAT_1:27; ::_thesis: ( rng xi c= A & xi is increasing & A = sup xi )
rng xi c= rng xi1 by A9, RELAT_1:26;
hence A12: ( rng xi c= A & xi is increasing ) by A2, A10, XBOOLE_1:1; ::_thesis: A = sup xi
thus A c= sup xi :: according to XBOOLE_0:def_10 ::_thesis: sup xi c= A
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A or a in sup xi )
assume A13: a in A ; ::_thesis: a in sup xi
then reconsider a = a as Ordinal ;
consider b being Ordinal such that
A14: b in rng xi1 and
A15: a c= b by A4, A13, ORDINAL2:21;
consider e being set such that
A16: e in B and
A17: b = xi1 . e by A1, A14, FUNCT_1:def_3;
reconsider e = e as Ordinal by A16;
consider c being Ordinal such that
A18: c in rng xi2 and
A19: e c= c by A8, A16, ORDINAL2:21;
consider u being set such that
A20: u in C and
A21: c = xi2 . u by A5, A18, FUNCT_1:def_3;
reconsider u = u as Ordinal by A20;
A22: xi1 . c = xi . u by A9, A11, A20, A21, FUNCT_1:12;
xi . u in rng xi by A11, A20, FUNCT_1:def_3;
then A23: xi . u in sup xi by ORDINAL2:19;
xi1 . e c= xi1 . c by A1, A3, A6, A18, A19, Th9;
hence a in sup xi by A15, A17, A22, A23, ORDINAL1:12, XBOOLE_1:1; ::_thesis: verum
end;
sup (rng xi) c= sup A by A12, ORDINAL2:22;
hence sup xi c= A by ORDINAL2:18; ::_thesis: verum
end;
theorem :: ORDINAL4:38
for A, B being Ordinal st A is_cofinal_with B holds
( A is limit_ordinal iff B is limit_ordinal )
proof
let A, B be Ordinal; ::_thesis: ( A is_cofinal_with B implies ( A is limit_ordinal iff B is limit_ordinal ) )
given psi being Ordinal-Sequence such that A1: dom psi = B and
A2: rng psi c= A and
A3: psi is increasing and
A4: A = sup psi ; :: according to ORDINAL2:def_17 ::_thesis: ( A is limit_ordinal iff B is limit_ordinal )
thus ( A is limit_ordinal implies B is limit_ordinal ) ::_thesis: ( B is limit_ordinal implies A is limit_ordinal )
proof
assume A5: A is limit_ordinal ; ::_thesis: B is limit_ordinal
now__::_thesis:_for_C_being_Ordinal_st_C_in_B_holds_
succ_C_in_B
let C be Ordinal; ::_thesis: ( C in B implies succ C in B )
reconsider c = psi . C as Ordinal ;
assume A6: C in B ; ::_thesis: succ C in B
then psi . C in rng psi by A1, FUNCT_1:def_3;
then succ c in A by A2, A5, ORDINAL1:28;
then consider b being Ordinal such that
A7: b in rng psi and
A8: succ c c= b by A4, ORDINAL2:21;
consider e being set such that
A9: e in B and
A10: b = psi . e by A1, A7, FUNCT_1:def_3;
reconsider e = e as Ordinal by A9;
c in succ c by ORDINAL1:6;
then not e c= C by A1, A3, A6, A8, A10, Th9, ORDINAL1:5;
then C in e by ORDINAL1:16;
then succ C c= e by ORDINAL1:21;
hence succ C in B by A9, ORDINAL1:12; ::_thesis: verum
end;
hence B is limit_ordinal by ORDINAL1:28; ::_thesis: verum
end;
thus ( B is limit_ordinal implies A is limit_ordinal ) by A1, A3, A4, Th16; ::_thesis: verum
end;
registration
let D be Ordinal;
let f, g be T-Sequence of D;
clusterf ^ g -> D -valued ;
coherence
f ^ g is D -valued
proof
( rng f c= D & rng g c= D ) by RELAT_1:def_19;
then A1: (rng f) \/ (rng g) c= D by XBOOLE_1:8;
rng (f ^ g) c= (rng f) \/ (rng g) by Th2;
hence rng (f ^ g) c= D by A1, XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum
end;
end;