:: 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;