### The Mizar article:

### Sequences of Ordinal Numbers

**by****Grzegorz Bancerek**

- Received July 18, 1989
Copyright (c) 1989 Association of Mizar Users

- MML identifier: ORDINAL2
- [ MML identifier index ]

environ vocabulary ORDINAL1, FUNCT_1, BOOLE, SETFAM_1, TARSKI, RELAT_1, ORDINAL2; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, SETFAM_1; constructors ORDINAL1, SETFAM_1, XBOOLE_0; clusters FUNCT_1, SUBSET_1, ORDINAL1, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; definitions TARSKI, XBOOLE_0, ORDINAL1; theorems TARSKI, XBOOLE_0, ORDINAL1, SETFAM_1, ZFMISC_1, FUNCT_1, RELAT_1, XBOOLE_1; schemes XBOOLE_0, FUNCT_1, ORDINAL1; begin reserve A,A1,A2,B,C,D for Ordinal, X,Y,Z for set, x,y,a,b,c for set, L,L1,L2,L3 for T-Sequence, f for Function; scheme Ordinal_Ind { P[Ordinal] } : for A holds P[A] provided A1: P[{}] and A2: for A st P[A] holds P[succ A] and A3: for A st A <> {} & A is_limit_ordinal & for B st B in A holds P[B] holds P[A] proof defpred PP[Ordinal] means P[$1]; A4:for A st for B st B in A holds PP[B] holds PP[A] proof let A such that A5: for B st B in A holds P[B]; A6: now given B such that A7: A = succ B; B in A by A7,ORDINAL1:10; then P[B] by A5; hence thesis by A2,A7; end; now assume A8: A <> {} & for B holds A <> succ B; then A is_limit_ordinal by ORDINAL1:42; hence thesis by A3,A5,A8; end; hence thesis by A1,A6; end; thus for A holds PP[A] from Transfinite_Ind(A4); end; theorem Th1: A c= B iff succ A c= succ B proof (A c= B iff A in succ B) & (A in succ B iff succ A c= succ B) by ORDINAL1:33,34; hence thesis; end; Lm1: succ {} = { {} } proof thus succ {} = {} \/ { {} } by ORDINAL1:def 1 .= { {} }; end; theorem Th2: union succ A = A proof A1: A in succ A by ORDINAL1:10; thus union succ A c= A proof let x; assume x in union succ A; then consider X such that A2: x in X & X in succ A by TARSKI:def 4; reconsider X as Ordinal by A2,ORDINAL1:23; X c= A by A2,ORDINAL1:34; hence x in A by A2; end; thus thesis by A1,ZFMISC_1:92; end; theorem succ A c= bool A proof let x; assume A1: x in succ A; then A2: x in A or x = A by ORDINAL1:13; reconsider B = x as Ordinal by A1,ORDINAL1:23; B c= A by A2,ORDINAL1:def 2; hence x in bool A; end; theorem {} is_limit_ordinal proof thus {} = union {} by ZFMISC_1:2; end; theorem Th5: union A c= A proof let x; assume x in union A; then consider Y such that A1: x in Y & Y in A by TARSKI:def 4; Y c= A by A1,ORDINAL1:def 2; hence thesis by A1; end; definition let L; func last L -> set equals :Def1: L.(union dom L); coherence; end; canceled; theorem Th7: dom L = succ A implies last L = L.A proof union succ A = A by Th2; hence thesis by Def1; end; definition let X; func On X -> set means :Def2: x in it iff x in X & x is Ordinal; existence proof defpred P[set] means $1 is Ordinal; thus ex Y being set st for x being set holds x in Y iff x in X & P[x] from Separation; end; uniqueness proof defpred P[set] means $1 in X & $1 is Ordinal; let Y,Z such that A1: x in Y iff P[x] and A2: x in Z iff P[x]; thus Y = Z from Extensionality(A1,A2); end; func Lim X -> set means :Def3: x in it iff x in X & ex A st x = A & A is_limit_ordinal; existence proof defpred P[set] means ex A st $1 = A & A is_limit_ordinal; thus ex Y being set st for x being set holds x in Y iff x in X & P[x] from Separation; end; uniqueness proof defpred P[set] means $1 in X & ex A st $1 = A & A is_limit_ordinal; let Y,Z such that A3: x in Y iff P[x] and A4: x in Z iff P[x]; thus Y = Z from Extensionality(A3,A4); end; end; canceled; theorem On X c= X proof thus x in On X implies x in X by Def2; end; theorem Th10: On A = A proof x in A iff x in A & x is Ordinal by ORDINAL1:23; hence thesis by Def2; end; theorem Th11: X c= Y implies On X c= On Y proof assume A1: X c= Y; let x; assume x in On X; then x in X & x is Ordinal by Def2; hence x in On Y by A1,Def2; end; canceled; theorem Lim X c= X proof thus x in Lim X implies x in X by Def3; end; theorem X c= Y implies Lim X c= Lim Y proof assume A1: X c= Y; let x; assume x in Lim X; then x in X & ex A st x = A & A is_limit_ordinal by Def3; hence x in Lim Y by A1,Def3; end; theorem Lim X c= On X proof let x; assume x in Lim X; then x in X & ex A st x = A & A is_limit_ordinal by Def3; hence x in On X by Def2; end; theorem Th16: for D ex A st D in A & A is_limit_ordinal proof let D; consider Field being set such that A1: D in Field & (for X,Y holds X in Field & Y c= X implies Y in Field) & (for X holds X in Field implies bool X in Field) & (for X holds X c= Field implies X,Field are_equipotent or X in Field) by ZFMISC_1:136; for X st X in On Field holds X is Ordinal & X c= On Field proof let X; assume A2: X in On Field; hence X is Ordinal by Def2; reconsider A = X as Ordinal by A2,Def2; let y; assume A3: y in X; then y in A; then reconsider B = y as Ordinal by ORDINAL1:23; B c= A & A in Field by A2,A3,Def2,ORDINAL1:def 2; then B in Field by A1; hence thesis by Def2; end; then reconsider ON = On Field as Ordinal by ORDINAL1:31; take ON; thus D in ON by A1,Def2; A in ON implies succ A in ON proof assume A in ON; then A in Field by Def2; then A4: bool A in Field by A1; succ A c= bool A proof let x; assume x in succ A; then x in A or x = A by ORDINAL1:13; then x c= A by ORDINAL1:def 2; hence x in bool A; end; then succ A in Field by A1,A4; hence thesis by Def2; end; hence thesis by ORDINAL1:41; end; theorem Th17: (for x st x in X holds x is Ordinal) implies meet X is Ordinal proof assume A1: for x st x in X holds x is Ordinal; now assume A2: X <> {}; consider x being Element of X; defpred P[Ordinal] means $1 in X; x is Ordinal by A1,A2; then A3: ex A st P[A] by A2; consider A such that A4: P[A] & for B st P[B] holds A c= B from Ordinal_Min(A3); for x holds x in A iff for Y st Y in X holds x in Y proof let x; thus x in A implies for Y st Y in X holds x in Y proof assume A5: x in A; let Y; assume A6: Y in X; then reconsider B = Y as Ordinal by A1; A c= B by A4,A6; hence x in Y by A5; end; assume for Y st Y in X holds x in Y; hence x in A by A4; end; hence thesis by A2,SETFAM_1:def 1; end; hence thesis by SETFAM_1:def 1; end; definition func one -> non empty Ordinal equals :Def4: succ {}; correctness; end; definition func omega -> set means :Def5: {} in it & it is_limit_ordinal & it is ordinal & for A st {} in A & A is_limit_ordinal holds it c= A; existence proof defpred P[Ordinal] means {} in $1 & $1 is_limit_ordinal; A1: ex A st P[A] by Th16; ex C st P[C] & for A st P[A] holds C c= A from Ordinal_Min(A1); hence thesis; end; uniqueness proof let B,C be set such that A2: {} in B & B is_limit_ordinal & B is ordinal & for A st {} in A & A is_limit_ordinal holds B c= A and A3: {} in C & C is_limit_ordinal & C is ordinal & for A st {} in A & A is_limit_ordinal holds C c= A; thus B c= C & C c= B by A2,A3; end; end; definition cluster omega -> non empty ordinal; coherence by Def5; end; definition let X; func inf X -> Ordinal equals :Def6: meet On X; coherence proof x in On X implies x is Ordinal by Def2; hence thesis by Th17; end; func sup X -> Ordinal means :Def7: On X c= it & for A st On X c= A holds it c= A; existence proof x in On X implies x is Ordinal by Def2; then reconsider A = union On X as Ordinal by ORDINAL1:35; defpred P[Ordinal] means On X c= $1; On X c= succ A proof let x; assume A1: x in On X; then reconsider B = x as Ordinal by Def2; B c= A by A1,ZFMISC_1:92; hence x in succ A by ORDINAL1:34; end; then A2: ex A st P[A]; thus ex F being Ordinal st P[F] & for A st P[A] holds F c= A from Ordinal_Min(A2); end; uniqueness proof let B,C such that A3: On X c= B & for A st On X c= A holds B c= A and A4: On X c= C & for A st On X c= A holds C c= A; thus B c= C & C c= B by A3,A4; end; end; canceled; theorem {} in omega & omega is_limit_ordinal & for A st {} in A & A is_limit_ordinal holds omega c= A by Def5; canceled 2; theorem A in X implies inf X c= A proof assume A in X; then A in On X by Def2; then meet On X c= A by SETFAM_1:4; hence thesis by Def6; end; theorem On X <> {} & (for A st A in X holds D c= A) implies D c= inf X proof assume A1: On X <> {} & for A st A in X holds D c= A; let x such that A2: x in D; for Y st Y in On X holds x in Y proof let Y; assume A3: Y in On X; then reconsider A = Y as Ordinal by Def2; A in X by A3,Def2; then D c= A by A1; hence x in Y by A2; end; then x in meet On X by A1,SETFAM_1:def 1; hence x in inf X by Def6; end; theorem A in X & X c= Y implies inf Y c= inf X proof assume A in X; then A1: On X <> {} by Def2; assume X c= Y; then On X c= On Y & inf X = meet On X & inf Y = meet On Y by Def6,Th11; hence thesis by A1,SETFAM_1:7; end; theorem A in X implies inf X in X proof defpred P[Ordinal] means $1 in X; assume A in X; then A1: ex A st P[A]; consider A such that A2: P[A] & for B st P[B] holds A c= B from Ordinal_Min(A1); A3: A in On X by A2,Def2; A4: On X <> {} by A2,Def2; now let x; thus x in A implies for Y st Y in On X holds x in Y proof assume A5: x in A; let Y; assume A6: Y in On X; then A7: Y in X & Y is Ordinal by Def2; reconsider B = Y as Ordinal by A6,Def2; A c= B by A2,A7; hence x in Y by A5; end; assume for Y st Y in On X holds x in Y; hence x in A by A3; end; then A = meet On X by A4,SETFAM_1:def 1 .= inf X by Def6; hence thesis by A2; end; theorem Th26: sup A = A proof A1: On A = A by Th10; for B st On A c= B holds A c= B by Th10; hence thesis by A1,Def7; end; theorem Th27: A in X implies A in sup X proof assume A in X; then A in On X & On X c= sup X by Def2,Def7; hence thesis; end; theorem Th28: (for A st A in X holds A in D) implies sup X c= D proof assume A1: for A st A in X holds A in D; On X c= D proof let x; assume A2: x in On X; then reconsider A = x as Ordinal by Def2; A in X by A2,Def2; hence x in D by A1; end; hence thesis by Def7; end; theorem A in sup X implies ex B st B in X & A c= B proof assume A1: A in sup X & for B st B in X holds not A c= B; now let B; assume B in X; then not A c= B by A1; hence B in A by ORDINAL1:26; end; then sup X c= A by Th28; hence contradiction by A1,ORDINAL1:7; end; theorem X c= Y implies sup X c= sup Y proof assume X c= Y; then On X c= On Y & On Y c= sup Y by Def7,Th11; then On X c= sup Y & for A st On X c= A holds sup X c= A by Def7,XBOOLE_1:1 ; hence thesis; end; theorem sup { A } = succ A proof A1: On { A } c= succ A proof let x; assume x in On { A }; then x in { A } by Def2; then x = A by TARSKI:def 1; hence thesis by ORDINAL1:10; end; now let B such that A2: On { A } c= B; A in { A } by TARSKI:def 1; then A in On { A } by Def2; hence succ A c= B by A2,ORDINAL1:33; end; hence thesis by A1,Def7; end; theorem inf X c= sup X proof let x; assume x in inf X; then A1: x in meet On X by Def6; consider y being Element of On X; reconsider y as Ordinal by A1,Def2,SETFAM_1:2; On X c= sup X by Def7; then y in sup X by A1,SETFAM_1:2,TARSKI:def 3; then y c= sup X & x in y by A1,ORDINAL1:def 2,SETFAM_1:2,def 1; hence thesis; end; scheme TS_Lambda { A()->Ordinal, F(Ordinal)->set } : ex L st dom L = A() & for A st A in A() holds L.A = F(A) proof deffunc G(set) = F(sup union { $1 }); consider f such that A1: dom f = A() & for x st x in A() holds f.x = G(x) from Lambda; reconsider f as T-Sequence by A1,ORDINAL1:def 7; take L = f; thus dom L = A() by A1; let A; assume A in A(); hence L.A = F(sup union { A }) by A1 .= F(sup A) by ZFMISC_1:31 .= F(A) by Th26; end; definition let f; attr f is Ordinal-yielding means :Def8: ex A st rng f c= A; end; definition cluster Ordinal-yielding T-Sequence; existence proof consider A; consider L being T-Sequence of A; reconsider K = L as T-Sequence; take K,A; thus thesis by ORDINAL1:def 8; end; end; definition mode Ordinal-Sequence is Ordinal-yielding T-Sequence; end; definition let A; cluster -> Ordinal-yielding T-Sequence of A; coherence proof let L be T-Sequence of A; take A; thus rng L c= A by ORDINAL1:def 8; end; end; definition let L be Ordinal-Sequence; let A; cluster L|A -> Ordinal-yielding; coherence proof consider B such that A1: rng L c= B by Def8; L|A is Ordinal-yielding proof take B; rng(L|A) c= rng L by FUNCT_1:76; hence thesis by A1,XBOOLE_1:1; end; hence thesis; end; end; reserve fi,psi for Ordinal-Sequence; canceled; theorem Th34: A in dom fi implies fi.A is Ordinal proof assume A in dom fi; then A1: fi.A in rng fi by FUNCT_1:def 5; consider B such that A2: rng fi c= B by Def8; thus thesis by A1,A2,ORDINAL1:23; end; definition let f be Ordinal-Sequence, a be Ordinal; cluster f.a -> ordinal; coherence proof a in dom f or not a in dom f; hence thesis by FUNCT_1:def 4,Th34; end; end; scheme OS_Lambda { A()->Ordinal, F(Ordinal)->Ordinal } : ex fi st dom fi = A() & for A st A in A() holds fi.A = F(A) proof deffunc FF(Ordinal) = F($1); consider L such that A1: dom L = A() & for A st A in A() holds L.A = FF(A) from TS_Lambda; L is Ordinal-yielding proof take A = sup rng L; let x; assume A2: x in rng L; then consider y such that A3: y in dom L & x = L.y by FUNCT_1:def 5; reconsider y as Ordinal by A3,ORDINAL1:23; L.y = F(y) by A1,A3; then x in On rng L & On rng L c= sup rng L by A2,A3,Def2,Def7; hence x in A; end; then reconsider L as Ordinal-Sequence; take fi = L; thus dom fi = A() by A1; let A; assume A in A(); hence fi.A = F(A) by A1; end; scheme TS_Uniq1 { A()->Ordinal, B()->set, C(Ordinal,set)->set, D(Ordinal,T-Sequence)->set, L1()->T-Sequence, L2()->T-Sequence } : L1() = L2() provided A1: dom L1() = A() and A2: {} in A() implies L1().{} = B() and A3: for A st succ A in A() holds L1().(succ A) = C(A,L1().A) and A4: for A st A in A() & A <> {} & A is_limit_ordinal holds L1().A = D(A,L1()|A) and A5: dom L2() = A() and A6: {} in A() implies L2().{} = B() and A7: for A st succ A in A() holds L2().(succ A) = C(A,L2().A) and A8: for A st A in A() & A <> {} & A is_limit_ordinal holds L2().A = D(A,L2()|A) proof assume L1() <> L2(); then consider a such that A9: a in A() & L1().a <> L2().a by A1,A5,FUNCT_1:9; defpred P[set] means L1().$1 <> L2().$1; consider X such that A10: Y in X iff Y in A() & P[Y] from Separation; A11: X <> {} by A9,A10; for b holds b in X implies b in A() by A10; then X c= A() by TARSKI:def 3; then consider B such that A12: B in X & for C st C in X holds B c= C by A11,ORDINAL1:32; A13: B in A() & L1().B <> L2().B by A10,A12; then A14: B c= A() by ORDINAL1:def 2; A15: now let C; assume A16: C in B; then not B c= C by ORDINAL1:7; then not C in X by A12; hence L1().C = L2().C by A10,A14,A16; end; A17: dom(L1()|B) = B & dom(L2()|B) = B by A1,A5,A14,RELAT_1:91; A18: now let a; assume A19: a in B; then reconsider a' = a as Ordinal by ORDINAL1:23; A20: L1().a' = L2().a' by A15,A19; L1()|B.a = L1().a & L2()|B.a = L2().a by A17,A19,FUNCT_1:70; hence L1()|B.a = L2()|B.a by A20; end; A21: now given C such that A22: B = succ C; A23: L1().B = C(C,L1().C) & L2().B = C(C,L2().C) & C in B by A3,A7,A13,A22,ORDINAL1:10; then L1().C = L1()|B.C & L2().C = L2()|B.C by FUNCT_1:72; hence L1().B = L2().B by A18,A23; end; now assume A24: B <> {} & for C holds B <> succ C; then B is_limit_ordinal by ORDINAL1:42; then L1().B = D(B,L1()|B) & L2().B = D(B,L2()|B) by A4,A8,A13,A24; hence L1().B = L2().B by A17,A18,FUNCT_1:9; end; hence contradiction by A2,A6,A10,A12,A21; end; scheme TS_Exist1 { A()->Ordinal, B()->set, C(Ordinal,set)->set, D(Ordinal,T-Sequence)->set } : ex L st dom L = A() & ({} in A() implies L.{} = B() ) & (for A st succ A in A() holds L.(succ A) = C(A,L.A) ) & (for A st A in A() & A <> {} & A is_limit_ordinal holds L.A = D(A,L|A) ) proof defpred P[Ordinal,T-Sequence] means dom $2 = $1 & ({} in $1 implies $2.{} = B() ) & (for A st succ A in $1 holds $2.(succ A) = C(A,$2.A) ) & for A st A in $1 & A <> {} & A is_limit_ordinal holds $2.A = D(A,$2|A); defpred R[Ordinal] means ex L st P[$1,L]; deffunc CC(Ordinal,set) = C($1,$2); deffunc DD(Ordinal,set) = D($1,$2); A1: for B st for C st C in B holds R[C] holds R[B] proof let B such that A2: for C st C in B ex L st P[C,L]; defpred R[set,set] means $1 is Ordinal & $2 is T-Sequence & for A,L st A = $1 & L = $2 holds P[A,L]; A3: for a,b,c st R[a,b] & R[a,c] holds b = c proof let a,b,c; assume A4: ( a is Ordinal & b is T-Sequence & for A,L st A = a & L = b holds P[A,L] ) & ( a is Ordinal & c is T-Sequence & for A,L st A = a & L = c holds P[A,L] ); then reconsider a as Ordinal; reconsider b as T-Sequence by A4; reconsider c as T-Sequence by A4; A5: dom b = a by A4; A6: {} in a implies b.{} = B() by A4; A7: for A st succ A in a holds b.(succ A) = CC(A,b.A) by A4; A8: for A st A in a & A <> {} & A is_limit_ordinal holds b.A = DD(A,b|A) by A4; A9: dom c = a by A4; A10: {} in a implies c.{} = B() by A4; A11: for A st succ A in a holds c.(succ A) = CC(A,c.A) by A4; A12: for A st A in a & A <> {} & A is_limit_ordinal holds c.A = DD(A,c|A) by A4; b = c from TS_Uniq1(A5,A6,A7,A8,A9,A10,A11,A12); hence thesis; end; consider G being Function such that A13: [a,b] in G iff a in B & R[a,b] from GraphFunc(A3); A14: dom G = B proof thus a in dom G implies a in B proof assume a in dom G; then ex b st [a,b] in G by RELAT_1:def 4; hence a in B by A13; end; let a; assume A15: a in B; then reconsider a' = a as Ordinal by ORDINAL1:23; consider L such that A16: P[a',L] by A2,A15; for A holds for K be T-Sequence holds A = a' & K = L implies P[A,K] by A16; then [a',L] in G by A13,A15; hence a in dom G by RELAT_1:def 4; end; defpred Q[set,set] means ex A,L st A = $1 & L = G.$1 & (A = {} & $2 = B() or (ex B st A = succ B & $2 = C(B,L.B)) or A <> {} & A is_limit_ordinal & $2 = D(A,L)); A17: for a,b,c st a in B & Q[a,b] & Q[a,c] holds b = c proof let a,b,c such that a in B; given Ab being Ordinal,Lb being T-Sequence such that A18: Ab = a & Lb = G.a and A19: Ab = {} & b = B() or (ex B st Ab = succ B & b = C(B,Lb.B)) or Ab <> {} & Ab is_limit_ordinal & b = D(Ab,Lb); given Ac being Ordinal,Lc being T-Sequence such that A20: Ac = a & Lc = G.a and A21: Ac = {} & c = B() or (ex B st Ac = succ B & c = C(B,Lc.B)) or Ac <> {} & Ac is_limit_ordinal & c = D(Ac,Lc); now given C such that A22: Ab = succ C; consider A such that A23: Ab = succ A & b = C(A,Lb.A) by A19,A22,ORDINAL1:42; consider D such that A24: Ac = succ D & c = C(D,Lc.D) by A18,A20,A21,A22,ORDINAL1:42; A = D by A18,A20,A23,A24,ORDINAL1:12; hence thesis by A18,A20,A23,A24; end; hence thesis by A18,A19,A20,A21; end; A25: for a st a in B ex b st Q[a,b] proof let a; assume A26: a in B; then consider c such that A27: [a,c] in G by A14,RELAT_1:def 4; reconsider L = c as T-Sequence by A13,A27; reconsider A = a as Ordinal by A26,ORDINAL1:23; A28: now assume A29: A = {}; thus Q[a,B()] proof take A,L; thus A = a & L = G.a by A27,FUNCT_1:8; thus thesis by A29; end; end; A30: now given C such that A31: A = succ C; thus ex b st Q[a,b] proof take C(C,L.C), A, L; thus A = a & L = G.a by A27,FUNCT_1:8; thus thesis by A31; end; end; now assume A32: A <> {} & for C holds A <> succ C; thus Q[a,D(A,L)] proof take A,L; thus A = a & L = G.a by A27,FUNCT_1:8; thus thesis by A32,ORDINAL1:42; end; end; hence thesis by A28,A30; end; consider F being Function such that A33: dom F = B & for a st a in B holds Q[a,F.a] from FuncEx(A17,A25); reconsider L = F as T-Sequence by A33,ORDINAL1:def 7; take L; thus dom L = B by A33; thus {} in B implies L.{} = B() proof assume {} in B; then ex A being Ordinal, K being T-Sequence st A = {} & K = G.{} & (A = {} & F.{} = B() or (ex B st A = succ B & F.{} = C(B,K.B)) or A <> {} & A is_limit_ordinal & F.{} = D(A,K)) by A33; hence thesis; end; A34: for A,L1 st A in B & L1 = G.A holds L|A = L1 proof defpred P[Ordinal] means for L1 st $1 in B & L1 = G.$1 holds L|$1 = L1; A35: for A st for C st C in A holds P[C] holds P[A] proof let A such that A36: for C st C in A for L1 st C in B & L1 = G.C holds L|C = L1; let L1; assume A37: A in B & L1 = G.A; then A38: [A,L1] in G by A14,FUNCT_1:8; then A39: P[A,L1] & A c= dom L by A13,A33,A37,ORDINAL1:def 2; then A40: dom L1 = A & dom(L|A) = A & ({} in A implies L1.{} = B() ) & (for B,x st succ B in A & x = L1.B holds L1.(succ B) = C(B,x) ) & (for B,L2 st B in A & B <> {} & B is_limit_ordinal & L2 = L1|B holds L1.B = D(B,L2) ) by RELAT_1:91; now let x; assume A41: x in A; then reconsider x' = x as Ordinal by ORDINAL1:23; A42: x' in B by A37,A41,ORDINAL1:19; then consider A1,L2 such that A43: A1 = x' & L2 = G.x' and A44: A1 = {} & L.x' = B() or (ex B st A1 = succ B & L.x' = C(B,L2.B)) or A1 <> {} & A1 is_limit_ordinal & L.x' = D(A1,L2) by A33; A45: L|x' = L2 & L|A.x = L.x by A36,A41,A42,A43,FUNCT_1:72; for D,L3 st D = x' & L3 = L1|x' holds P[D,L3] proof let D,L3 such that A46: D = x' & L3 = L1|x'; x' c= A by A41,ORDINAL1:def 2; hence dom L3 = D by A39,A46,RELAT_1:91; thus {} in D implies L3.{} = B() by A39,A41,A46,FUNCT_1:72, ORDINAL1:19; thus succ C in D implies L3.(succ C) = C(C,L3.C) proof assume A47: succ C in D; C in succ C by ORDINAL1:10; then A48: C in D by A47,ORDINAL1:19; then A49: succ C in A & succ C in x' & C in A & C in x' by A41,A46,A47,ORDINAL1:19; L1|x'.succ C = L1.succ C & L1|x'.C = L1.C by A46,A47,A48,FUNCT_1:72; hence L3.(succ C) = C(C,L3.C) by A13,A38,A46,A49; end; let C; assume A50: C in D & C <> {} & C is_limit_ordinal; then C c= x' by A46,ORDINAL1:def 2; then L1|C = L3|C & C in A by A41,A46,A50,FUNCT_1:82,ORDINAL1:19; then L1.C = D(C,L3|C) & L1|x'.C = L1.C by A13,A38,A46,A50, FUNCT_1:72; hence L3.C = D(C,L3|C) by A46; end; then [x',L1|x'] in G by A13,A42; then A51: L1|x' = L2 by A43,FUNCT_1:8; now given D such that A52: x' = succ D; A53: D in x' by A52,ORDINAL1:10; consider C such that A54: A1 = succ C & L.x' = C(C,L2.C) by A43,A44,A52,ORDINAL1:42; C = D & L1.x = C(D,L1.D) by A13,A38,A41,A43,A52,A54,ORDINAL1:12 ; hence L1.x = L|A.x by A45,A51,A53,A54,FUNCT_1:72; end; hence L1.x = L|A.x by A13,A38,A41,A43,A44,A45,A51; end; hence thesis by A40,FUNCT_1:9; end; thus for A holds P[A] from Transfinite_Ind(A35); end; thus succ A in B implies L.(succ A) = C(A,L.A) proof assume A55: succ A in B; then consider C being Ordinal, K being T-Sequence such that A56: C = succ A & K = G.succ A and A57: C = {} & F.succ A = B() or (ex B st C = succ B & F.succ A = C(B,K.B)) or C <> {} & C is_limit_ordinal & F.succ A = D(C,K) by A33; consider D such that A58: C = succ D & F.succ A = C(D,K.D) by A56,A57,ORDINAL1:42; A = D & K = L|succ A & A in succ A by A34,A55,A56,A58,ORDINAL1:10,12; hence L.succ A = C(A,L.A) by A58,FUNCT_1:72; end; let D; assume A59: D in B & D <> {} & D is_limit_ordinal; then ex A being Ordinal, K being T-Sequence st A = D & K = G.D & (A = {} & F.D = B() or (ex B st A = succ B & F.D = C(B,K.B)) or A <> {} & A is_limit_ordinal & F.D = D(A,K)) by A33; hence L.D = D(D,L|D) by A34,A59,ORDINAL1:42; end; for A holds R[A] from Transfinite_Ind(A1); hence ex L st P[A(),L]; end; scheme TS_Result { L()->T-Sequence, F(Ordinal)->set, A()->Ordinal, B()->set, C(Ordinal,set)->set, D(Ordinal,T-Sequence)->set } : for A st A in dom L() holds L().A = F(A) provided A1: for A,x holds x = F(A) iff ex L st x = last L & dom L = succ A & L.{} = B() & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds L.C = D(C,L|C) and A2: dom L() = A() and A3: {} in A() implies L().{} = B() and A4: for A st succ A in A() holds L().(succ A) = C(A,L().A) and A5: for A st A in A() & A <> {} & A is_limit_ordinal holds L().A = D(A,L()|A) proof let A; set L = L()|succ A; assume A in dom L(); then A6: succ A c= dom L() & A in succ A by ORDINAL1:33; then A7: dom L = succ A by RELAT_1:91; then last L = L.A by Th7; then A8: last L = L().A by A6,FUNCT_1:72; succ A <> {} & {} c= succ A by XBOOLE_1:2; then {} c< succ A by XBOOLE_0:def 8; then {} in succ A by ORDINAL1:21; then A9: L().{} = B() & L.{} = L().{} by A2,A3,A6,FUNCT_1:72; A10: for C st succ C in succ A holds L.succ C = C(C,L.C) proof let C such that A11: succ C in succ A; C in succ C by ORDINAL1:10; then C in succ A by A11,ORDINAL1:19; then L.C = L().C & L.succ C = L().succ C by A11,FUNCT_1:72; hence L.succ C = C(C,L.C) by A2,A4,A6,A11; end; for C st C in succ A & C <> {} & C is_limit_ordinal holds L.C = D(C,L|C) proof let C; assume A12: C in succ A & C <> {} & C is_limit_ordinal; then C in A() & C c= succ A by A2,A6,ORDINAL1:def 2; then L.C = L().C & L|C = L()|C by A12,FUNCT_1:72,82; hence L.C = D(C,L|C) by A2,A5,A6,A12; end; hence thesis by A1,A7,A8,A9,A10; end; scheme TS_Def { A()->Ordinal, B()->set, C(Ordinal,set)->set, D(Ordinal,T-Sequence)->set } : (ex x,L st x = last L & dom L = succ A() & L.{} = B() & (for C st succ C in succ A() holds L.succ C = C(C,L.C)) & for C st C in succ A() & C <> {} & C is_limit_ordinal holds L.C = D(C,L|C) ) & for x1,x2 being set st (ex L st x1 = last L & dom L = succ A() & L.{} = B() & (for C st succ C in succ A() holds L.succ C = C(C,L.C)) & for C st C in succ A() & C <> {} & C is_limit_ordinal holds L.C = D(C,L|C) ) & (ex L st x2 = last L & dom L = succ A() & L.{} = B() & (for C st succ C in succ A() holds L.succ C = C(C,L.C)) & for C st C in succ A() & C <> {} & C is_limit_ordinal holds L.C = D(C,L|C) ) holds x1 = x2 proof deffunc DD(Ordinal,T-Sequence) = D($1,$2); deffunc CC(Ordinal,set) = C($1,$2); consider L such that A1: dom L = succ A() & ({} in succ A() implies L.{} = B() ) & (for C st succ C in succ A() holds L.(succ C) = CC(C,L.C)) & for C st C in succ A() & C <> {} & C is_limit_ordinal holds L.C = DD(C,L|C) from TS_Exist1; thus ex x,L st x = last L & dom L = succ A() & L.{} = B() & (for C st succ C in succ A() holds L.succ C = C(C,L.C)) & for C st C in succ A() & C <> {} & C is_limit_ordinal holds L.C = D(C,L|C) proof take x = last L, L; thus x = last L & dom L = succ A() by A1; succ A() <> {} & {} c= succ A() by XBOOLE_1:2; then {} c< succ A() by XBOOLE_0:def 8; hence thesis by A1,ORDINAL1:21; end; let x1,x2 be set; given L1 such that A2: x1 = last L1 and A3: dom L1 = succ A() and A4: L1.{} = B() and A5: for C st succ C in succ A() holds L1.succ C = CC(C,L1.C) and A6: for C st C in succ A() & C <> {} & C is_limit_ordinal holds L1.C = DD(C,L1|C); given L2 such that A7: x2 = last L2 and A8: dom L2 = succ A() and A9: L2.{} = B() and A10: for C st succ C in succ A() holds L2.succ C = CC(C,L2.C) and A11: for C st C in succ A() & C <> {} & C is_limit_ordinal holds L2.C = DD(C,L2|C); A12: {} in succ A() implies L1.{} = B() by A4; A13: {} in succ A() implies L2.{} = B() by A9; L1 = L2 from TS_Uniq1(A3,A12,A5,A6,A8,A13,A10,A11); hence thesis by A2,A7; end; scheme TS_Result0 { F(Ordinal)->set, B()->set, C(Ordinal,set)->set, D(Ordinal,T-Sequence)->set } : F({}) = B() provided A1: for A,x holds x = F(A) iff ex L st x = last L & dom L = succ A & L.{} = B() & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds L.C = D(C,L|C) proof deffunc DD(Ordinal,T-Sequence) = D($1,$2); deffunc CC(Ordinal,set) = C($1,$2); consider L such that A2: dom L = succ {} & ({} in succ {} implies L.{} = B() ) & (for A st succ A in succ {} holds L.(succ A) = CC(A,L.A) ) & for A st A in succ {} & A <> {} & A is_limit_ordinal holds L.A = DD(A,L|A) from TS_Exist1; B() = last L & L.{} = B() by A2,Th7,ORDINAL1:10; hence thesis by A1,A2; end; scheme TS_ResultS { B()->set, C(Ordinal,set)->set, D(Ordinal,T-Sequence)->set, F(Ordinal)->set } : for A holds F(succ A) = C(A,F(A)) provided A1: for A,x holds x = F(A) iff ex L st x = last L & dom L = succ A & L.{} = B() & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds L.C = D(C,L|C) proof deffunc DD(Ordinal,T-Sequence) = D($1,$2); deffunc CC(Ordinal,set) = C($1,$2); deffunc FF(Ordinal) = F($1); let A; A2: for A,x holds x = FF(A) iff ex L st x = last L & dom L = succ A & L.{} = B() & (for C st succ C in succ A holds L.succ C = CC(C,L.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds L.C = DD(C,L|C) by A1; consider L such that A3: dom L = succ succ A and A4: {} in succ succ A implies L.{} = B() and A5: for C st succ C in succ succ A holds L.(succ C) = CC(C,L.C) and A6: for C st C in succ succ A & C <> {} & C is_limit_ordinal holds L.C = DD(C,L|C) from TS_Exist1; A7: for B st B in dom L holds L.B = FF(B) from TS_Result(A2,A3,A4,A5,A6); A8: A in succ A & succ A in succ succ A by ORDINAL1:10; then A in succ succ A by ORDINAL1:19; then L.A = F(A) & L.succ A = F(succ A) by A3,A7,A8; hence thesis by A5,A8; end; scheme TS_ResultL { L()->T-Sequence, A()->Ordinal, F(Ordinal)->set, B()->set, C(Ordinal,set)->set, D(Ordinal,T-Sequence)->set } : F(A()) = D(A(),L()) provided A1: for A,x holds x = F(A) iff ex L st x = last L & dom L = succ A & L.{} = B() & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds L.C = D(C,L|C) and A2: A() <> {} & A() is_limit_ordinal and A3: dom L() = A() and A4: for A st A in A() holds L().A = F(A) proof deffunc DD(Ordinal,T-Sequence) = D($1,$2); deffunc CC(Ordinal,set) = C($1,$2); deffunc FF(Ordinal) = F($1); A5: for A,x holds x = FF(A) iff ex L st x = last L & dom L = succ A & L.{} = B() & (for C st succ C in succ A holds L.succ C = CC(C,L.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds L.C = DD(C,L|C) by A1; consider L such that A6: dom L = succ A() and A7: {} in succ A() implies L.{} = B() and A8: for C st succ C in succ A() holds L.(succ C) = CC(C,L.C) and A9: for C st C in succ A() & C <> {} & C is_limit_ordinal holds L.C = DD(C,L|C) from TS_Exist1; A10: for B st B in dom L holds L.B = FF(B) from TS_Result(A5,A6,A7,A8,A9); set L1 = L|A(); A11: A() in succ A() by ORDINAL1:10; then A() c= dom L by A6,ORDINAL1:def 2; then A12: dom L1 = A() by RELAT_1:91; now let x; assume A13: x in A(); then reconsider x' = x as Ordinal by ORDINAL1:23; A14: x' in succ A() by A11,A13,ORDINAL1:19; thus L1.x = L.x' by A13,FUNCT_1:72 .= F(x') by A6,A10,A14 .= L().x by A4, A13; end; then L1 = L() by A3,A12,FUNCT_1:9; then L.A() = D(A(),L()) by A2,A9,A11; hence thesis by A6,A10,A11; end; scheme OS_Exist { A()->Ordinal, B()->Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal,T-Sequence)->Ordinal } : ex fi st dom fi = A() & ({} in A() implies fi.{} = B() ) & (for A st succ A in A() holds fi.(succ A) = C(A,fi.A) ) & (for A st A in A() & A <> {} & A is_limit_ordinal holds fi.A = D(A,fi|A) ) proof deffunc DD(Ordinal,T-Sequence) = D($1,$2); deffunc CC(Ordinal,set) = C($1,sup union {$2}); consider L such that A1: dom L = A() and A2: {} in A() implies L.{} = B() and A3: for A st succ A in A() holds L.(succ A) = CC(A,L.A) and A4: for A st A in A() & A <> {} & A is_limit_ordinal holds L.A = DD(A,L|A) from TS_Exist1; L is Ordinal-yielding proof take A = sup rng L; let x; assume A5: x in rng L; then consider y such that A6: y in dom L & x = L.y by FUNCT_1:def 5; reconsider y as Ordinal by A6,ORDINAL1:23; A7: now given B such that A8: y = succ B; L.y = C(B,sup union {L.B}) by A1,A3,A6,A8; hence x is Ordinal by A6; end; now assume A9: y <> {} & for B holds y <> succ B; then y is_limit_ordinal by ORDINAL1:42; then L.y = D(y,L|y) by A1,A4,A6,A9; hence x is Ordinal by A6; end; then x in On rng L & On rng L c= sup rng L by A1,A2,A5,A6,A7,Def2,Def7; hence x in A; end; then reconsider L as Ordinal-Sequence; take fi = L; thus dom fi = A() & ({} in A() implies fi.{} = B() ) by A1,A2; thus for A st succ A in A() holds fi.(succ A) = C(A,fi.A) proof let A; reconsider B = fi.A as Ordinal; sup union {B} = sup B by ZFMISC_1:31 .= B by Th26; hence thesis by A3; end; thus thesis by A4; end; scheme OS_Result { fi()->Ordinal-Sequence, F(Ordinal)->Ordinal, A()->Ordinal, B()->Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal,T-Sequence)->Ordinal } : for A st A in dom fi() holds fi().A = F(A) provided A1: for A,B holds B = F(A) iff ex fi st B = last fi & dom fi = succ A & fi.{} = B() & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) and A2: dom fi() = A() and A3: {} in A() implies fi().{} = B() and A4: for A st succ A in A() holds fi().(succ A) = C(A,fi().A) and A5: for A st A in A() & A <> {} & A is_limit_ordinal holds fi().A = D(A,fi()|A) proof let A; set fi = fi()|succ A; assume A in dom fi(); then A6: succ A c= dom fi() & A in succ A by ORDINAL1:33; then A7: dom fi = succ A by RELAT_1:91; then A8: last fi = fi.A by Th7; then reconsider B = last fi as Ordinal; A9: last fi = fi().A by A6,A8,FUNCT_1:72; succ A <> {} & {} c= succ A by XBOOLE_1:2; then {} c< succ A by XBOOLE_0:def 8; then {} in succ A by ORDINAL1:21; then A10: fi().{} = B() & fi.{} = fi().{} by A2,A3,A6,FUNCT_1:72; A11: for C st succ C in succ A holds fi.succ C = C(C,fi.C) proof let C such that A12: succ C in succ A; C in succ C by ORDINAL1:10; then C in succ A by A12,ORDINAL1:19; then fi.C = fi().C & fi.succ C = fi().succ C by A12,FUNCT_1:72; hence fi.succ C = C(C,fi.C) by A2,A4,A6,A12; end; for C st C in succ A & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) proof let C; assume A13: C in succ A & C <> {} & C is_limit_ordinal; then C in A() & C c= succ A by A2,A6,ORDINAL1:def 2; then fi.C = fi().C & fi|C = fi()|C by A13,FUNCT_1:72,82; hence fi.C = D(C,fi|C) by A2,A5,A6,A13; end; then ex fi st B = last fi & dom fi = succ A & fi.{} = B() & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) by A7,A10,A11; hence thesis by A1,A9; end; scheme OS_Def { A()->Ordinal, B()->Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal,T-Sequence)->Ordinal } : (ex A,fi st A = last fi & dom fi = succ A() & fi.{} = B() & (for C st succ C in succ A() holds fi.succ C = C(C,fi.C)) & for C st C in succ A() & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) ) & for A1,A2 st (ex fi st A1 = last fi & dom fi = succ A() & fi.{} = B() & (for C st succ C in succ A() holds fi.succ C = C(C,fi.C)) & for C st C in succ A() & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) ) & (ex fi st A2 = last fi & dom fi = succ A() & fi.{} = B() & (for C st succ C in succ A() holds fi.succ C = C(C,fi.C)) & for C st C in succ A() & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) ) holds A1 = A2 proof deffunc DD(Ordinal,T-Sequence) = D($1,$2); deffunc CC(Ordinal,set) = C($1,$2); consider fi such that A1: dom fi = succ A() & ({} in succ A() implies fi.{} = B() ) & (for C st succ C in succ A() holds fi.(succ C) = CC(C,fi.C)) & for C st C in succ A() & C <> {} & C is_limit_ordinal holds fi.C = DD(C,fi|C) from OS_Exist; last fi = fi.A() & A() in dom fi by A1,Th7,ORDINAL1:10; then reconsider A = last fi as Ordinal; thus ex A,fi st A = last fi & dom fi = succ A() & fi.{} = B() & (for C st succ C in succ A() holds fi.succ C = C(C,fi.C)) & for C st C in succ A() & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) proof take A, fi; thus A = last fi & dom fi = succ A() by A1; succ A() <> {} & {} c= succ A() by XBOOLE_1:2; then {} c< succ A() by XBOOLE_0:def 8; hence thesis by A1,ORDINAL1:21; end; let A1,A2 be Ordinal; given L1 being Ordinal-Sequence such that A2: A1 = last L1 and A3: dom L1 = succ A() and A4: L1.{} = B() and A5: for C st succ C in succ A() holds L1.succ C = C(C,L1.C) and A6: for C st C in succ A() & C <> {} & C is_limit_ordinal holds L1.C = D(C,L1|C); given L2 being Ordinal-Sequence such that A7: A2 = last L2 and A8: dom L2 = succ A() and A9: L2.{} = B() and A10: for C st succ C in succ A() holds L2.succ C = CC(C,L2.C) and A11: for C st C in succ A() & C <> {} & C is_limit_ordinal holds L2.C = DD(C,L2|C); A12: {} in succ A() implies L1.{} = B() by A4; A13: {} in succ A() implies L2.{} = B() by A9; deffunc CD(Ordinal,Ordinal) = CC($1,sup union { $2 }); A14: for C st succ C in succ A() holds L1.(succ C) = CD(C,L1.C) proof let C such that A15: succ C in succ A(); reconsider x' = L1.C as Ordinal; sup union { L1.C } = sup x' by ZFMISC_1:31 .= x' by Th26; hence thesis by A5,A15; end; A16: for C st succ C in succ A() holds L2.(succ C) = CD(C,L2.C) proof let C such that A17: succ C in succ A(); reconsider x' = L2.C as Ordinal; sup union { L2.C } = sup x' by ZFMISC_1:31 .= x' by Th26; hence thesis by A10,A17; end; A18: for C st C in succ A() & C <> {} & C is_limit_ordinal holds L1.C = DD(C,L1|C) by A6; A19: for C st C in succ A() & C <> {} & C is_limit_ordinal holds L2.C = DD(C,L2|C) by A11; L1 = L2 from TS_Uniq1(A3,A12,A14,A18,A8,A13,A16,A19); hence thesis by A2,A7; end; scheme OS_Result0 { F(Ordinal)->Ordinal, B()->Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal,T-Sequence)->Ordinal } : F({}) = B() provided A1: for A,B holds B = F(A) iff ex fi st B = last fi & dom fi = succ A & fi.{} = B() & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) proof deffunc CC(Ordinal,Ordinal) = C($1,$2); deffunc DD(Ordinal,Ordinal) = D($1,$2); consider fi such that A2: dom fi = succ {} & ({} in succ {} implies fi.{} = B() ) & (for A st succ A in succ {} holds fi.(succ A) = CC(A,fi.A) ) & for A st A in succ {} & A <> {} & A is_limit_ordinal holds fi.A = DD(A,fi|A) from OS_Exist; B() = last fi & fi.{} = B() by A2,Th7,ORDINAL1:10; hence thesis by A1,A2; end; scheme OS_ResultS { B()->Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal,T-Sequence)->Ordinal, F(Ordinal)->Ordinal } : for A holds F(succ A) = C(A,F(A)) provided A1: for A,B holds B = F(A) iff ex fi st B = last fi & dom fi = succ A & fi.{} = B() & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) proof let A; deffunc CC(Ordinal,Ordinal) = C($1,$2); deffunc DD(Ordinal,Ordinal) = D($1,$2); deffunc FF(Ordinal) = F($1); A2: for A,B holds B = FF(A) iff ex fi st B = last fi & dom fi = succ A & fi.{} = B() & (for C st succ C in succ A holds fi.succ C = CC(C,fi.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds fi.C = DD(C,fi|C) by A1; consider fi such that A3: dom fi = succ succ A and A4: {} in succ succ A implies fi.{} = B() and A5: for C st succ C in succ succ A holds fi.(succ C) = CC(C,fi.C) and A6: for C st C in succ succ A & C <> {} & C is_limit_ordinal holds fi.C = DD(C,fi|C) from OS_Exist; A7: for B st B in dom fi holds fi.B = FF(B) from OS_Result(A2,A3,A4,A5,A6); A8: A in succ A & succ A in succ succ A by ORDINAL1:10; then A in succ succ A by ORDINAL1:19; then fi.A = F(A) & fi.succ A = F(succ A) by A3,A7,A8; hence thesis by A5,A8; end; scheme OS_ResultL { fi()->Ordinal-Sequence, A()->Ordinal, F(Ordinal)->Ordinal, B()->Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal,T-Sequence)->Ordinal } : F(A()) = D(A(),fi()) provided A1: for A,B holds B = F(A) iff ex fi st B = last fi & dom fi = succ A & fi.{} = B() & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) and A2: A() <> {} & A() is_limit_ordinal and A3: dom fi() = A() and A4: for A st A in A() holds fi().A = F(A) proof deffunc CC(Ordinal,Ordinal) = C($1,$2); deffunc DD(Ordinal,Ordinal) = D($1,$2); deffunc FF(Ordinal) = F($1); A5: for A,B holds B = FF(A) iff ex fi st B = last fi & dom fi = succ A & fi.{} = B() & (for C st succ C in succ A holds fi.succ C = CC(C,fi.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds fi.C = DD(C,fi|C) by A1; consider fi such that A6: dom fi = succ A() and A7: {} in succ A() implies fi.{} = B() and A8: for C st succ C in succ A() holds fi.(succ C) = CC(C,fi.C) and A9: for C st C in succ A() & C <> {} & C is_limit_ordinal holds fi.C = DD(C,fi|C) from OS_Exist; A10: for B st B in dom fi holds fi.B = FF(B) from OS_Result(A5,A6,A7,A8,A9); set psi = fi|A(); A11: A() in succ A() by ORDINAL1:10; then A() c= dom fi by A6,ORDINAL1:def 2; then A12: dom psi = A() by RELAT_1:91; now let x; assume A13: x in A(); then reconsider x' = x as Ordinal by ORDINAL1:23; A14: x' in succ A() by A11,A13,ORDINAL1:19; thus psi.x = fi.x' by A13,FUNCT_1:72 .= F(x') by A6,A10,A14 .= fi().x by A4,A13; end; then psi = fi() by A3,A12,FUNCT_1:9; then fi.A() = D(A(),fi()) by A2,A9,A11; hence thesis by A6,A10,A11; end; definition let L; func sup L -> Ordinal equals :Def9: sup rng L; correctness; func inf L -> Ordinal equals :Def10: inf rng L; correctness; end; theorem sup L = sup rng L & inf L = inf rng L by Def9,Def10; definition let L; func lim_sup L -> Ordinal means ex fi st it = inf fi & dom fi = dom L & for A st A in dom L holds fi.A = sup rng (L|(dom L \ A)); existence proof deffunc F(Ordinal) = sup rng (L|(dom L \ $1)); consider fi such that A1: dom fi = dom L & for A st A in dom L holds fi.A = F(A) from OS_Lambda; take inf fi, fi; thus thesis by A1; end; uniqueness proof let A1,A2 be Ordinal; given fi such that A2: A1 = inf fi and A3: dom fi = dom L & for A st A in dom L holds fi.A = sup rng (L|(dom L \ A)); given psi such that A4: A2 = inf psi and A5: dom psi = dom L & for A st A in dom L holds psi.A = sup rng (L|(dom L \ A)); now let x; assume A6: x in dom L; then reconsider A = x as Ordinal by ORDINAL1:23; fi.A = sup rng (L|(dom L \ A)) & psi.A = sup rng (L|(dom L \ A)) by A3,A5,A6; hence fi.x = psi.x; end; hence thesis by A2,A3,A4,A5,FUNCT_1:9; end; func lim_inf L -> Ordinal means ex fi st it = sup fi & dom fi = dom L & for A st A in dom L holds fi.A = inf rng (L|(dom L \ A)); existence proof deffunc F(Ordinal) = inf rng (L|(dom L \ $1)); consider fi such that A7: dom fi = dom L & for A st A in dom L holds fi.A = F(A) from OS_Lambda; take sup fi, fi; thus thesis by A7; end; uniqueness proof let A1,A2 be Ordinal; given fi such that A8: A1 = sup fi and A9: dom fi = dom L & for A st A in dom L holds fi.A = inf rng (L|(dom L \ A)); given psi such that A10: A2 = sup psi and A11: dom psi = dom L & for A st A in dom L holds psi.A = inf rng (L|(dom L \ A)); now let x; assume A12: x in dom L; then reconsider A = x as Ordinal by ORDINAL1:23; fi.A = inf rng (L|(dom L \ A)) & psi.A = inf rng (L|(dom L \ A)) by A9,A11,A12; hence fi.x = psi.x; end; hence thesis by A8,A9,A10,A11,FUNCT_1:9; end; end; definition let A,fi; pred A is_limes_of fi means :Def13: ex B st B in dom fi & for C st B c= C & C in dom fi holds fi.C = {} if A = {} otherwise for B,C st B in A & A in C ex D 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; consistency; end; definition let fi; given A such that A1: A is_limes_of fi; func lim fi -> Ordinal means :Def14: it is_limes_of fi; existence by A1; uniqueness proof let A1,A2 be Ordinal such that A2: (A1 = {} & ex B st B in dom fi & for C st B c= C & C in dom fi holds fi.C = {}) or (A1 <> {} & for B,C st B in A1 & A1 in C ex D 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) and A3: (A2 = {} & ex B st B in dom fi & for C st B c= C & C in dom fi holds fi.C = {}) or (A2 <> {} & for B,C st B in A2 & A2 in C ex D 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); assume A4: A1 <> A2; then A5: A1 in A2 or A2 in A1 by ORDINAL1:24; A6: now assume A7: A1 in A2; then A2 in succ A2 & A2 <> {} by ORDINAL1:10; then consider D such that A8: D in dom fi and A9: for A st D c= A & A in dom fi holds A1 in fi.A & fi.A in succ A2 by A3,A7; A10: now assume A11: A1 = {}; then consider B such that A12: B in dom fi & for C st B c= C & C in dom fi holds fi.C = {} by A2; B c= D or D c= B; then consider E being Ordinal such that A13: E = D & B c= D or E = B & D c= B; fi.E = {} & {} in fi.E by A8,A9,A11,A12,A13; hence contradiction; end; consider x being Element of A1; reconsider x as Ordinal by A10,ORDINAL1:23; A1 in succ A1 by ORDINAL1:10; then consider C such that A14: C in dom fi and A15: for A st C c= A & A in dom fi holds x in fi.A & fi.A in succ A1 by A2, A10; C c= D or D c= C; then consider E being Ordinal such that A16: E = D & C c= D or E = C & D c= C; A17: fi.E in succ A1 & A1 in fi.E by A8,A9,A14,A15,A16; then fi.E in A1 or fi.E = A1 by ORDINAL1:13; hence contradiction by A17; end; then A1 in succ A1 & A1 <> {} by A4,ORDINAL1:10,24; then consider D such that A18: D in dom fi and A19: for A st D c= A & A in dom fi holds A2 in fi.A & fi.A in succ A1 by A2,A5,A6; A20: now assume A21: A2 = {}; then consider B such that A22: B in dom fi & for C st B c= C & C in dom fi holds fi.C = {} by A3; B c= D or D c= B; then consider E being Ordinal such that A23: E = D & B c= D or E = B & D c= B; fi.E = {} & {} in fi.E by A18,A19,A21,A22,A23; hence contradiction; end; consider x being Element of A2; reconsider x as Ordinal by A20,ORDINAL1:23; A2 in succ A2 by ORDINAL1:10; then consider C such that A24: C in dom fi and A25: for A st C c= A & A in dom fi holds x in fi.A & fi.A in succ A2 by A3,A20; C c= D or D c= C; then consider E being Ordinal such that A26: E = D & C c= D or E = C & D c= C; A27: fi.E in succ A2 & A2 in fi.E by A18,A19,A24,A25,A26; then fi.E in A2 or fi.E = A2 by ORDINAL1:13; hence contradiction by A27; end; end; definition let A,fi; func lim(A,fi) -> Ordinal equals lim(fi|A); correctness; end; definition let L be Ordinal-Sequence; attr L is increasing means for A,B st A in B & B in dom L holds L.A in L.B; attr L is continuous means for A,B st A in dom L & A <> {} & A is_limit_ordinal & B = L.A holds B is_limes_of L|A; end; definition let A,B; func A +^ B -> Ordinal means :Def18: ex fi st it = last fi & dom fi = succ B & fi.{} = A & (for C st succ C in succ B holds fi.succ C = succ(fi.C)) & for C st C in succ B & C <> {} & C is_limit_ordinal holds fi.C = sup(fi|C); correctness proof deffunc C(Ordinal,Ordinal) = succ $2; deffunc D(Ordinal,T-Sequence) = sup $2; (ex F being Ordinal,fi st F = last fi & dom fi = succ B & fi.{} = A & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) ) & for A1,A2 st (ex fi st A1 = last fi & dom fi = succ B & fi.{} = A & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) ) & (ex fi st A2 = last fi & dom fi = succ B & fi.{} = A & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) ) holds A1 = A2 from OS_Def; hence thesis; end; end; definition let A,B; func A *^ B -> Ordinal means :Def19: ex fi st it = last fi & dom fi = succ A & fi.{} = {} & (for C st succ C in succ A holds fi.succ C = (fi.C)+^B) & for C st C in succ A & C <> {} & C is_limit_ordinal holds fi.C = union sup(fi|C); correctness proof deffunc C(Ordinal,Ordinal) = $2+^B; deffunc D(Ordinal,Ordinal-Sequence) = union sup $2; (ex F being Ordinal,fi st F = last fi & dom fi = succ A & fi.{} = {} & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) ) & for A1,A2 st (ex fi st A1 = last fi & dom fi = succ A & fi.{} = {} & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) ) & (ex fi st A2 = last fi & dom fi = succ A & fi.{} = {} & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) ) holds A1 = A2 from OS_Def; hence thesis; end; end; definition let A,B; func exp(A,B) -> Ordinal means :Def20: ex fi st it = last fi & dom fi = succ B & fi.{} = one & (for C st succ C in succ B holds fi.succ C = A*^(fi.C)) & for C st C in succ B & C <> {} & C is_limit_ordinal holds fi.C = lim(fi|C); correctness proof deffunc C(Ordinal,Ordinal) = A*^$2; deffunc D(Ordinal,Ordinal-Sequence) = lim $2; (ex F being Ordinal,fi st F = last fi & dom fi = succ B & fi.{} = one & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) ) & for A1,A2 st (ex fi st A1 = last fi & dom fi = succ B & fi.{} = one & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) ) & (ex fi st A2 = last fi & dom fi = succ B & fi.{} = one & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) ) holds A1 = A2 from OS_Def; hence thesis; end; end; canceled 8; theorem Th44: A+^{} = A proof deffunc F(Ordinal) = A+^$1; deffunc D(Ordinal,T-Sequence) = sup $2; deffunc C(Ordinal,Ordinal) = succ $2; A1: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.{} = A & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) by Def18; thus F({}) = A from OS_Result0(A1); end; theorem Th45: A+^succ B = succ(A+^B) proof deffunc F(Ordinal) = A+^$1; deffunc D(Ordinal,T-Sequence) = sup $2; deffunc C(Ordinal,Ordinal) = succ $2; A1: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.{} = A & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) by Def18; for B holds F(succ B) = C(B,F(B)) from OS_ResultS(A1); hence thesis; end; theorem Th46: B <> {} & B is_limit_ordinal implies for fi st dom fi = B & for C st C in B holds fi.C = A+^C holds A+^B = sup fi proof assume A1: B <> {} & B is_limit_ordinal; deffunc F(Ordinal) = A+^$1; deffunc D(Ordinal,Ordinal-Sequence) = sup $2; deffunc C(Ordinal,Ordinal) = succ $2; let fi such that A2: dom fi = B and A3: for C st C in B holds fi.C = F(C); A4: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.{} = A & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) by Def18; thus F(B) = D(B,fi) from OS_ResultL(A4,A1,A2,A3); end; theorem Th47: {}+^A = A proof defpred P[Ordinal] means {}+^$1 = $1; A1: P[{}] by Th44; A2: for A holds P[A] implies P[succ A] by Th45; A3: for A st A <> {} & A is_limit_ordinal & for B st B in A holds P[B] holds P[A] proof let A; assume that A4: A <> {} & A is_limit_ordinal and A5: for B st B in A holds {}+^B = B; deffunc F(Ordinal) = {}+^$1; consider fi such that A6: dom fi = A & for B st B in A holds fi.B = F(B) from OS_Lambda; A7: {}+^A = sup fi by A4,A6,Th46 .= sup rng fi by Def9; rng fi = A proof thus x in rng fi implies x in A proof assume x in rng fi; then consider y such that A8: y in dom fi & x = fi.y by FUNCT_1:def 5; reconsider y as Ordinal by A8,ORDINAL1:23; x = {}+^y by A6,A8 .= y by A5,A6,A8; hence thesis by A6,A8; end; let x; assume A9: x in A; then reconsider B = x as Ordinal by ORDINAL1:23; {}+^B = B & fi.B = {}+^B by A5,A6,A9; hence x in rng fi by A6,A9,FUNCT_1:def 5; end; hence {}+^A = A by A7,Th26; end; for A holds P[A] from Ordinal_Ind(A1,A2,A3); hence thesis; end; theorem A+^one = succ A proof thus A+^one = succ(A+^{}) by Def4,Th45 .= succ A by Th44; end; theorem Th49: A in B implies C +^ A in C +^ B proof defpred P[Ordinal] means A in $1 implies C +^ A in C +^ $1; A1: for B st for D st D in B holds P[D] holds P[B] proof let B such that A2: for D st D in B holds A in D implies C +^ A in C +^ D and A3: A in B; A4: now given D such that A5: B = succ D; A6: D in B by A5,ORDINAL1:10; A7: now A8: A c< D iff A c= D & A <> D by XBOOLE_0:def 8; assume not A in D; then C +^ A in succ(C +^ D) & succ(C +^ D) = C +^ succ D by A3,A5,A8,Th45,ORDINAL1:21,34; hence thesis by A5; end; now assume A in D; then C +^ A in C +^ D & succ(C +^ D) = C +^ succ D & C +^ D in succ(C +^ D) by A2,A6,Th45,ORDINAL1:10; hence thesis by A5,ORDINAL1:19; end; hence thesis by A7; end; now assume for D holds B <> succ D; then A9: B is_limit_ordinal by ORDINAL1:42; deffunc F(Ordinal) = C+^$1; consider fi such that A10: dom fi = B & for D st D in B holds fi.D = F(D) from OS_Lambda; A11: C+^B = sup fi by A3,A9,A10,Th46 .= sup rng fi by Def9; fi.A = C+^A by A3,A10; then C+^A in rng fi by A3,A10,FUNCT_1:def 5; hence thesis by A11,Th27; end; hence thesis by A4; end; for B holds P[B] from Transfinite_Ind(A1); hence thesis; end; theorem Th50: A c= B implies C +^ A c= C +^ B proof assume A1: A c= B; now assume A <> B; then A c< B by A1,XBOOLE_0:def 8; then A in B by ORDINAL1:21; then C +^ A in C +^ B by Th49; hence thesis by ORDINAL1:def 2; end; hence thesis; end; theorem Th51: A c= B implies A +^ C c= B +^ C proof assume A1: A c= B; defpred P[Ordinal] means A +^ $1 c= B +^ $1; A2:for C st for D st D in C holds P[D] holds P[C] proof let C such that A3: for D st D in C holds A +^ D c= B +^ D; A4: now assume C = {}; then A +^ C = A & B +^ C = B by Th44; hence thesis by A1; end; A5: now given D such that A6: C = succ D; D in C by A6,ORDINAL1:10; then A7: A +^ D c= B +^ D by A3; A +^ C = succ(A +^ D) & B +^ C = succ(B +^ D) by A6,Th45; hence thesis by A7,Th1; end; now assume A8: C <> {} & for D holds C <> succ D; then A9: C is_limit_ordinal by ORDINAL1:42; deffunc F(Ordinal) = A+^$1; consider fi such that A10: dom fi = C & for D st D in C holds fi.D = F(D) from OS_Lambda; A11: A+^C = sup fi by A8,A9,A10,Th46 .= sup rng fi by Def9; now let D; assume D in rng fi; then consider x such that A12: x in dom fi & D = fi.x by FUNCT_1:def 5; reconsider x as Ordinal by A12,ORDINAL1:23; A13: D = A+^x by A10,A12; A +^ x c= B +^ x & B +^ x in B +^ C by A3,A10,A12,Th49; hence D in B +^ C by A13,ORDINAL1:22; end; hence thesis by A11,Th28; end; hence thesis by A4,A5; end; for C holds P[C] from Transfinite_Ind(A2); hence thesis; end; theorem Th52: {}*^A = {} proof deffunc F(Ordinal) = $1*^A; deffunc D(Ordinal,T-Sequence) = union sup $2; deffunc C(Ordinal,Ordinal) = $2+^A; A1: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.{} = {} & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) by Def19; thus F({}) = {} from OS_Result0(A1); end; theorem Th53: (succ B)*^A = B*^A +^ A proof deffunc F(Ordinal) = $1*^A; deffunc D(Ordinal,T-Sequence) = union sup $2; deffunc C(Ordinal,Ordinal) = $2 +^ A; A1: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.{} = {} & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) by Def19; for B holds F(succ B) = C(B,F(B)) from OS_ResultS(A1); hence thesis; end; theorem Th54: B <> {} & B is_limit_ordinal implies for fi st dom fi = B & for C st C in B holds fi.C = C*^A holds B*^A = union sup fi proof assume A1: B <> {} & B is_limit_ordinal; deffunc F(Ordinal) = $1*^A; deffunc D(Ordinal,Ordinal-Sequence) = union sup $2; deffunc C(Ordinal,Ordinal) = $2+^A; let fi such that A2: dom fi = B and A3: for C st C in B holds fi.C = F(C); A4: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.{} = {} & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) by Def19; thus F(B) = D(B,fi) from OS_ResultL(A4,A1,A2,A3); end; theorem Th55: A*^{} = {} proof defpred P[Ordinal] means $1*^{} = {}; A1: P[{}] by Th52; A2: for A st P[A] holds P[succ A] proof let A; assume A*^{} = {}; hence (succ A)*^{} = {}+^{} by Th53 .= {} by Th44; end; A3: for A st A <> {} & A is_limit_ordinal & for B st B in A holds P[B] holds P[A] proof let A; assume that A4: A <> {} & A is_limit_ordinal and A5: for B st B in A holds B*^{} = {}; deffunc F(Ordinal) = $1*^{}; consider fi such that A6: dom fi = A & for B st B in A holds fi.B = F(B) from OS_Lambda; A7: A*^{} = union sup fi by A4,A6,Th54 .= union sup rng fi by Def9; rng fi = succ {} proof {} c= A by XBOOLE_1:2; then {} c< A by A4,XBOOLE_0:def 8; then A8: {} in A by ORDINAL1:21; thus x in rng fi implies x in succ {} proof assume x in rng fi; then consider y such that A9: y in dom fi & x = fi.y by FUNCT_1:def 5; reconsider y as Ordinal by A9,ORDINAL1:23; x = y*^{} by A6,A9 .= {} by A5,A6,A9; hence x in succ {} by Lm1,TARSKI:def 1; end; let x; assume x in succ {}; then A10: x = {} & {} *^ {} = {} by Lm1,Th52,TARSKI:def 1; then fi.x = x by A6,A8; hence x in rng fi by A6,A8,A10,FUNCT_1:def 5; end; then sup rng fi = succ {} by Th26; hence A*^{} = {} by A7,Th2; end; for A holds P[A] from Ordinal_Ind(A1,A2,A3); hence thesis; end; theorem Th56: one*^A = A & A*^one = A proof thus one*^A = {}*^A +^ A by Def4,Th53 .= {} +^ A by Th52 .= A by Th47; defpred P[Ordinal] means $1*^succ {} = $1; A1:for A st for B st B in A holds P[B] holds P[A] proof let A such that A2: for B st B in A holds B*^(succ {}) = B; A3: now given B such that A4: A = succ B; A5: B in A by A4,ORDINAL1:10; thus A*^(succ {}) = B*^(succ {}) +^ succ {} by A4,Th53 .= B +^ succ {} by A2,A5 .= succ(B +^ {}) by Th45 .= A by A4,Th44; end; now assume A6: A <> {} & for B holds A <> succ B; then A7: A is_limit_ordinal by ORDINAL1:42; deffunc F(Ordinal) = $1*^succ {}; consider fi such that A8: dom fi = A & for D st D in A holds fi.D = F(D) from OS_Lambda; A9: A*^succ {} = union sup fi by A6,A7,A8,Th54 .= union sup rng fi by Def9; A = rng fi proof thus A c= rng fi proof let x; assume A10: x in A; then reconsider B = x as Ordinal by ORDINAL1:23; x = B*^succ {} by A2,A10 .= fi.x by A8,A10; hence x in rng fi by A8,A10,FUNCT_1:def 5; end; let x; assume x in rng fi; then consider y such that A11: y in dom fi & x = fi.y by FUNCT_1:def 5; reconsider y as Ordinal by A11,ORDINAL1:23; fi.y = y*^succ {} by A8,A11 .= y by A2,A8,A11; hence x in A by A8,A11; end; hence A*^succ {} = union A by A9,Th26 .= A by A7,ORDINAL1:def 6; end; hence thesis by A3,Th52; end; for A holds P[A] from Transfinite_Ind(A1); hence thesis by Def4; end; theorem Th57: C <> {} & A in B implies A*^C in B*^C proof assume A1: C <> {}; {} c= C by XBOOLE_1:2; then {} c< C by A1,XBOOLE_0:def 8; then A2: {} in C by ORDINAL1:21; defpred P[Ordinal] means A in $1 implies A*^C in $1*^C; A3:for B st for D st D in B holds P[D] holds P[B] proof let B such that A4: for D st D in B holds A in D implies A *^ C in D *^ C and A5: A in B; A6: now given D such that A7: B = succ D; A8: D in B by A7,ORDINAL1:10; A9: now A10: A c< D iff A c= D & A <> D by XBOOLE_0:def 8; assume not A in D; then A*^C +^ {} = A*^C & A*^C +^ {} in D*^C +^ C & D*^C +^ C = (succ D) *^ C by A2,A5,A7,A10,Th44,Th49,Th53,ORDINAL1:21 ,34; hence thesis by A7; end; now assume A in D; then A*^C in D*^C & D*^C +^ C = (succ D)*^C & D*^C +^ {} = D*^C & D*^C +^ {} in D*^C +^ C by A2,A4,A8,Th44,Th49,Th53; hence thesis by A7,ORDINAL1:19; end; hence thesis by A9; end; now assume for D holds B <> succ D; then A11: B is_limit_ordinal by ORDINAL1:42; deffunc F(Ordinal) = $1*^C; consider fi such that A12: dom fi = B & for D st D in B holds fi.D = F(D) from OS_Lambda; A13: B*^C = union sup fi by A5,A11,A12,Th54 .= union sup rng fi by Def9; A14: succ A in B by A5,A11,ORDINAL1:41; then fi.(succ A) = (succ A)*^C by A12; then (succ A)*^C in rng fi by A12,A14,FUNCT_1:def 5; then (succ A)*^C in sup rng fi by Th27; then A15: (succ A)*^C c= union sup rng fi by ZFMISC_1:92; A*^C +^ {} = A*^C & A*^C +^ {} in A*^C +^ C & (succ A)*^C = A*^C +^ C by A2,Th44,Th49,Th53; hence thesis by A13,A15; end; hence thesis by A6; end; for B holds P[B] from Transfinite_Ind(A3); hence thesis; end; theorem A c= B implies A*^C c= B*^C proof assume A1: A c= B; A2: now assume C = {}; then A*^C = {} & B*^C = {} by Th55; hence thesis; end; now assume A3: C <> {}; now assume A <> B; then A c< B by A1,XBOOLE_0:def 8; then A in B by ORDINAL1:21; then A*^C in B*^C by A3,Th57; hence thesis by ORDINAL1:def 2; end; hence thesis; end; hence thesis by A2; end; theorem A c= B implies C*^A c= C*^B proof assume A1: A c= B; now assume A2: B <> {}; defpred P[Ordinal] means $1*^A c= $1*^B; A3: for C st for D st D in C holds P[D] holds P[C] proof let C such that A4: for D st D in C holds D*^A c= D*^B; A5: now assume C = {}; then C*^A = {} & C*^B = {} by Th52; hence thesis; end; A6: now given D such that A7: C = succ D; D in C by A7,ORDINAL1:10; then D*^A c= D*^B by A4; then D*^A +^ A c= D*^B +^ A & D*^B +^ A c= D*^B +^ B & C*^A = D*^A +^ A & C*^B = D*^B +^ B by A1,A7,Th50,Th51,Th53; hence thesis by XBOOLE_1:1; end; now assume A8: C <> {} & for D holds C <> succ D; then A9: C is_limit_ordinal by ORDINAL1:42; deffunc F(Ordinal) = $1*^A; consider fi such that A10: dom fi = C & for D st D in C holds fi.D = F(D) from OS_Lambda; A11: C*^A = union sup fi by A8,A9,A10,Th54 .= union sup rng fi by Def9; now let D; assume D in rng fi; then consider x such that A12: x in dom fi & D = fi.x by FUNCT_1:def 5; reconsider x as Ordinal by A12,ORDINAL1:23; A13: D = x*^A by A10,A12; x*^A c= x*^B & x*^B in C*^B by A2,A4,A10,A12,Th57; hence D in C*^B by A13,ORDINAL1:22; end; then sup rng fi c= C*^B & union sup rng fi c= sup rng fi by Th5,Th28 ; hence thesis by A11,XBOOLE_1:1; end; hence thesis by A5,A6; end; for C holds P[C] from Transfinite_Ind(A3); hence thesis; end; hence thesis by A1,XBOOLE_1:3; end; theorem Th60: exp(A,{}) = one proof deffunc F(Ordinal) = exp(A,$1); deffunc D(Ordinal,Ordinal-Sequence) = lim $2; deffunc C(Ordinal,Ordinal) = A*^$2; A1: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.{} = one & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) by Def20; thus F({}) = one from OS_Result0(A1); end; theorem Th61: exp(A,succ B) = A*^exp(A,B) proof deffunc F(Ordinal) = exp(A,$1); deffunc D(Ordinal,Ordinal-Sequence) = lim $2; deffunc C(Ordinal,Ordinal) = A *^ $2; A1: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.{} = one & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) by Def20; for B holds F(succ B) = C(B,F(B)) from OS_ResultS(A1); hence thesis; end; theorem Th62: B <> {} & B is_limit_ordinal implies for fi st dom fi = B & for C st C in B holds fi.C = exp(A,C) holds exp(A,B) = lim fi proof assume A1: B <> {} & B is_limit_ordinal; deffunc F(Ordinal) = exp(A,$1); deffunc D(Ordinal,Ordinal-Sequence) = lim $2; deffunc C(Ordinal,Ordinal) = A*^$2; let fi such that A2: dom fi = B and A3: for C st C in B holds fi.C = F(C); A4: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.{} = one & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> {} & C is_limit_ordinal holds fi.C = D(C,fi|C) by Def20; thus F(B) = D(B,fi) from OS_ResultL(A4,A1,A2,A3); end; theorem exp(A,one) = A & exp(one,A) = one proof thus exp(A,one) = A*^exp(A,{}) by Def4,Th61 .= A*^one by Th60 .= A by Th56; defpred P[Ordinal] means exp(one,$1) = one; A1: P[{}] by Th60; A2: for A st P[A] holds P[succ A] proof let A; assume exp(one,A) = one; hence exp(one,succ A) = one*^one by Th61 .= one by Th56; end; A3: for A st A <> {} & A is_limit_ordinal & for B st B in A holds P[B] holds P[A] proof let A such that A4: A <> {} & A is_limit_ordinal and A5: for B st B in A holds exp(one,B) = one; deffunc F(Ordinal) = exp(one,$1); consider fi such that A6: dom fi = A & for B st B in A holds fi.B = F(B) from OS_Lambda; A7: exp(one,A) = lim fi by A4,A6,Th62; A8: rng fi c= { one } proof let x; assume x in rng fi; then consider y such that A9: y in dom fi & x = fi.y by FUNCT_1:def 5; reconsider y as Ordinal by A9,ORDINAL1:23; x = exp(one,y) by A6,A9 .= one by A5,A6,A9; hence x in { one } by TARSKI:def 1; end; now thus {} <> one; let B,C such that A10: B in one & one in C; consider x being Element of A; reconsider x as Ordinal by A4,ORDINAL1:23; take D = x; thus D in dom fi by A4,A6; let E be Ordinal; assume D c= E & E in dom fi; then fi.E in rng fi by FUNCT_1:def 5; hence B in fi.E & fi.E in C by A8,A10,TARSKI:def 1; end; then one is_limes_of fi by Def13; hence exp(one,A) = one by A7,Def14; end; for A holds P[A] from Ordinal_Ind(A1,A2,A3); hence thesis; end; definition let A be set; attr A is natural means :Def21: A in omega; end; canceled; theorem for A ex B,C st B is_limit_ordinal & C is natural & A = B +^ C proof defpred Th[Ordinal] means ex B,C st B is_limit_ordinal & C is natural & $1 = B +^ C; A1:for A st for B st B in A holds Th[B] holds Th[A] proof let A such that A2: for B st B in A holds Th[B]; A3: (for B holds A <> succ B) implies Th[A] proof assume A4: for D holds A <> succ D; take B = A, C = {}; thus B is_limit_ordinal by A4,ORDINAL1:42; thus C in omega by Def5; thus A = B +^ C by Th44; end; (ex B st A = succ B) implies Th[A] proof given B such that A5: A = succ B; B in A by A5,ORDINAL1:10; then consider C,D such that A6: C is_limit_ordinal & D is natural & B = C +^ D by A2; take C, E = succ D; thus C is_limit_ordinal by A6; D in omega & omega is_limit_ordinal by A6,Def5,Def21; hence E in omega by ORDINAL1:41; thus A = C +^ E by A5,A6,Th45; end; hence thesis by A3; end; thus for A holds Th[A] from Transfinite_Ind(A1); end;

Back to top