:: Sequences of Ordinal Numbers. Beginnings of Ordinal Arithmetics :: by Grzegorz Bancerek :: :: Received July 18, 1989 :: Copyright (c) 1990-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies ORDINAL1, FUNCT_1, XBOOLE_0, TARSKI, ZFMISC_1, RELAT_1, SETFAM_1, SUBSET_1, FUNCOP_1, ORDINAL2, NAT_1, CARD_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, SETFAM_1, FUNCOP_1; constructors SETFAM_1, ORDINAL1, FUNCOP_1; registrations SUBSET_1, FUNCT_1, ORDINAL1, FUNCOP_1; requirements SUBSET, BOOLE, NUMERALS; definitions ORDINAL1, TARSKI, XBOOLE_0; equalities ORDINAL1, XBOOLE_0; expansions ORDINAL1, TARSKI, XBOOLE_0; theorems TARSKI, ORDINAL1, SETFAM_1, ZFMISC_1, FUNCT_1, RELAT_1, XBOOLE_1, FUNCOP_1, XTUPLE_0; schemes XBOOLE_0, FUNCT_1, ORDINAL1; begin reserve A,A1,A2,B,C,D for Ordinal, X,Y for set, x,y,a,b,c for object, L,L1,L2,L3 for Sequence, f for Function; scheme OrdinalInd { P[Ordinal] } : for A holds P[A] provided A1: P[0] and A2: for A st P[A] holds P[succ A] and A3: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B] holds P[A] proof A4: for A st for B st B in A holds P[B] holds P[A] proof let A such that A5: for B st B in A holds P[B]; A6: A <> 0 & (for B holds A <> succ B) implies thesis by A3,A5,ORDINAL1:29; now given B such that A7: A = succ B; B in A by A7,ORDINAL1:6; hence thesis by A2,A5,A7; end; hence thesis by A1,A6; end; thus for A holds P[A] from ORDINAL1:sch 2(A4); end; theorem Th1: A c= B iff succ A c= succ B proof A c= B iff A in succ B by ORDINAL1:22; hence thesis by ORDINAL1:21; end; theorem Th2: union succ A = A proof thus union succ A c= A proof let x be object; assume x in union succ A; then consider X such that A1: x in X and A2: X in succ A by TARSKI:def 4; reconsider X as Ordinal by A2; X c= A by A2,ORDINAL1:22; hence thesis by A1; end; thus thesis by ORDINAL1:6,ZFMISC_1:74; end; theorem succ A c= bool A proof let x be object; assume A1: x in succ A; then reconsider B = x as Ordinal; x in A or x = A by A1,ORDINAL1:8; then B c= A by ORDINAL1:def 2; hence thesis; end; theorem 0 is limit_ordinal by ZFMISC_1:2; theorem Th5: union A c= A proof let x be object; assume x in union A; then consider Y such that A1: x in Y and A2: Y in A by TARSKI:def 4; Y c= A by A2,ORDINAL1:def 2; hence thesis by A1; end; definition let L; func last L -> set equals L.(union dom L); coherence; end; theorem dom L = succ A implies last L = L.A by Th2; theorem On X c= X by ORDINAL1:def 9; theorem Th8: On A = A proof for x being object holds x in A iff x in A & x is Ordinal; hence thesis by ORDINAL1:def 9; end; theorem Th9: X c= Y implies On X c= On Y proof assume A1: X c= Y; let x be object; assume x in On X; then x in X & x is Ordinal by ORDINAL1:def 9; hence thesis by A1,ORDINAL1:def 9; end; theorem Lim X c= X by ORDINAL1:def 10; theorem X c= Y implies Lim X c= Lim Y proof assume A1: X c= Y; let x be object; assume x in Lim X; then x in X & ex A st x = A & A is limit_ordinal by ORDINAL1:def 10; hence thesis by A1,ORDINAL1:def 10; end; theorem Lim X c= On X proof let x be object; assume x in Lim X; then x in X & ex A st x = A & A is limit_ordinal by ORDINAL1:def 10; hence thesis by ORDINAL1:def 9; end; theorem Th13: (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 defpred P[Ordinal] means \$1 in X; set x = the Element of X; assume A2: X <> 0; then x is Ordinal by A1; 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 ORDINAL1:sch 1(A3); for x being object holds x in A iff for Y st Y in X holds x in Y proof let x be object; 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 thesis by A5; end; assume for Y st Y in X holds x in Y; hence thesis by A4; end; hence thesis by A2,SETFAM_1:def 1; end; hence thesis by SETFAM_1:def 1; end; registration cluster limit_ordinal for Ordinal; existence proof take omega; thus thesis by ORDINAL1:def 11; end; end; definition let X; func inf X -> Ordinal equals meet On X; coherence proof x in On X implies x is Ordinal by ORDINAL1:def 9; hence thesis by Th13; end; func sup X -> Ordinal means :Def3: On X c= it & for A st On X c= A holds it c= A; existence proof defpred P[Ordinal] means On X c= \$1; x in On X implies x is Ordinal by ORDINAL1:def 9; then reconsider A = union On X as epsilon-transitive epsilon-connected set by ORDINAL1:23; On X c= succ A proof let x be object; assume A1: x in On X; then reconsider B = x as Ordinal by ORDINAL1:def 9; B c= A by A1,ZFMISC_1:74; hence thesis by ORDINAL1:22; 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 ORDINAL1 :sch 1(A2); end; uniqueness; end; theorem A in X implies inf X c= A proof assume A in X; then A in On X by ORDINAL1:def 9; hence thesis by SETFAM_1:3; end; theorem On X <> 0 & (for A st A in X holds D c= A) implies D c= inf X proof assume that A1: On X <> 0 and A2: for A st A in X holds D c= A; let x be object such that A3: x in D; for Y st Y in On X holds x in Y proof let Y; assume A4: Y in On X; then reconsider A = Y as Ordinal by ORDINAL1:def 9; A in X by A4,ORDINAL1:def 9; then D c= A by A2; hence thesis by A3; end; hence thesis by A1,SETFAM_1:def 1; end; theorem A in X & X c= Y implies inf Y c= inf X proof assume A in X; then A1: On X <> 0 by ORDINAL1:def 9; assume X c= Y; then On X c= On Y by Th9; hence thesis by A1,SETFAM_1:6; 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 ORDINAL1:sch 1(A1); A3: A in On X by A2,ORDINAL1:def 9; A4: now let x be object; 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 reconsider B = Y as Ordinal by ORDINAL1:def 9; Y in X by A6,ORDINAL1:def 9; then A c= B by A2; hence thesis by A5; end; assume for Y st Y in On X holds x in Y; hence x in A by A3; end; On X <> 0 by A2,ORDINAL1:def 9; hence thesis by A2,A4,SETFAM_1:def 1; end; theorem Th18: sup A = A proof On A = A & for B st On A c= B holds A c= B by Th8; hence thesis by Def3; end; theorem Th19: A in X implies A in sup X proof assume A in X; then A1: A in On X by ORDINAL1:def 9; On X c= sup X by Def3; hence thesis by A1; end; theorem Th20: (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 be object; assume A2: x in On X; then reconsider A = x as Ordinal by ORDINAL1:def 9; A in X by A2,ORDINAL1:def 9; hence thesis by A1; end; hence thesis by Def3; end; theorem A in sup X implies ex B st B in X & A c= B proof assume that A1: A in sup X and A2: for B st B in X holds not A c= B; for B st B in X holds B in A by A2,ORDINAL1:16; then sup X c= A by Th20; hence contradiction by A1,ORDINAL1:5; end; theorem X c= Y implies sup X c= sup Y proof assume X c= Y; then A1: On X c= On Y by Th9; On Y c= sup Y by Def3; then On X c= sup Y by A1; hence thesis by Def3; end; theorem sup { A } = succ A proof A1: On { A } c= succ A proof let x be object; assume x in On { A }; then x in { A } by ORDINAL1:def 9; then x = A by TARSKI:def 1; hence thesis by ORDINAL1:6; end; now A in { A } by TARSKI:def 1; then A2: A in On { A } by ORDINAL1:def 9; let B; assume On { A } c= B; hence succ A c= B by A2,ORDINAL1:21; end; hence thesis by A1,Def3; end; theorem inf X c= sup X proof let x be object; set y = the Element of On X; assume A1: x in inf X; then reconsider y as Ordinal by ORDINAL1:def 9,SETFAM_1:1; On X c= sup X by Def3; then y in sup X by A1,SETFAM_1:1; then A2: y c= sup X by ORDINAL1:def 2; x in y by A1,SETFAM_1:1,def 1; hence thesis by A2; end; scheme TSLambda { 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(object) = F(sup union { \$1 }); consider f such that A1: dom f = A() & for x being object st x in A() holds f.x = G(x) from FUNCT_1:sch 3; reconsider f as 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:25 .= F(A) by Th18; end; definition let f; attr f is Ordinal-yielding means :Def4: ex A st rng f c= A; end; registration cluster Ordinal-yielding for Sequence; existence proof set A = the Ordinal; set L = the Sequence of A; take L,A; thus thesis by RELAT_1:def 19; end; end; definition mode Ordinal-Sequence is Ordinal-yielding Sequence; end; registration let A; cluster -> Ordinal-yielding for Sequence of A; coherence by RELAT_1:def 19; end; registration let L be Ordinal-Sequence; let A; cluster L|A -> Ordinal-yielding; coherence proof consider B such that A1: rng L c= B by Def4; L|A is Ordinal-yielding proof take B; rng(L|A) c= rng L by RELAT_1:70; hence thesis by A1; end; hence thesis; end; end; reserve fi,psi for Ordinal-Sequence; theorem Th25: 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 3; ex B st rng fi c= B by Def4; hence thesis by A1; end; registration let f be Ordinal-Sequence, a be object; cluster f.a -> ordinal; coherence proof a in dom f or not a in dom f; hence thesis by Th25,FUNCT_1:def 2; end; end; scheme OSLambda { A()->Ordinal, F(Ordinal)->Ordinal } : ex fi st dom fi = A() & for A st A in A() holds fi.A = F(A) proof consider L such that A1: dom L = A() & for A st A in A() holds L.A = F(A) from TSLambda; L is Ordinal-yielding proof take sup rng L; let x be object; assume A2: x in rng L; then consider y being object such that A3: y in dom L and A4: x = L.y by FUNCT_1:def 3; reconsider y as Ordinal by A3; L.y = F(y) by A1,A3; then A5: x in On rng L by A2,A4,ORDINAL1:def 9; On rng L c= sup rng L by Def3; hence thesis by A5; end; then reconsider L as Ordinal-Sequence; take fi = L; thus dom fi = A() by A1; let A; assume A in A(); hence thesis by A1; end; scheme TSUniq1 { A()->Ordinal, B()->object, C(Ordinal,set)->object, D(Ordinal,Sequence)->object, L1()->Sequence, L2()->Sequence } : L1() = L2() provided A1: dom L1() = A() and A2: 0 in A() implies L1().0 = 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 <> 0 & A is limit_ordinal holds L1().A = D(A, L1()|A) and A5: dom L2() = A() and A6: 0 in A() implies L2().0 = 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 <> 0 & A is limit_ordinal holds L2().A = D(A, L2()|A) proof defpred P[object] means L1().\$1 <> L2().\$1; consider X such that A9: for Y being object holds Y in X iff Y in A() & P[Y] from XBOOLE_0:sch 1; for b being object holds b in X implies b in A() by A9; then A10: X c= A(); assume L1() <> L2(); then ex a being object st a in A() & L1().a <> L2().a by A1,A5,FUNCT_1:2; then X <> 0 by A9; then consider B such that A11: B in X and A12: for C st C in X holds B c= C by A10,ORDINAL1:20; A13: B in A() by A9,A11; then A14: B c= A() by ORDINAL1:def 2; then A15: dom(L1()|B) = B & dom(L2()|B) = B by A1,A5,RELAT_1:62; A16: now let C; assume A17: C in B; then not C in X by A12,ORDINAL1:5; hence L1().C = L2().C by A9,A14,A17; end; A18: now let a be object; assume A19: a in B; L1()|B.a = L1().a & L2()|B.a = L2().a by A15,A19,FUNCT_1:47; hence L1()|B.a = L2()|B.a by A16,A19; end; A20: now given C such that A21: B = succ C; A22: L1().C = L1()|B.C & L2().C = L2()|B.C by A21,FUNCT_1:49,ORDINAL1:6; L1().B = C(C,L1().C) & L2().B = C(C,L2().C) by A3,A7,A13,A21; hence L1().B = L2().B by A18,A21,A22,ORDINAL1:6; end; now assume that A23: B <> 0 and A24: for C holds B <> succ C; B is limit_ordinal by A24,ORDINAL1:29; then L1().B = D(B,L1()|B) & L2().B = D(B,L2()|B) by A4,A8,A13,A23; hence L1().B = L2().B by A15,A18,FUNCT_1:2; end; hence contradiction by A2,A6,A9,A11,A20; end; scheme TSExist1 { A()->Ordinal, B()->object, C(Ordinal,set)->object, D(Ordinal,Sequence)->object } : ex L st dom L = A() & (0 in A() implies L.0 = B() ) & (for A st succ A in A() holds L.(succ A) = C(A,L.A) ) & for A st A in A() & A <> 0 & A is limit_ordinal holds L.A = D(A,L|A); defpred P[Ordinal,Sequence] means dom \$2 = \$1 & (0 in \$1 implies \$2.0 = B() ) & (for A st succ A in \$1 holds \$2.(succ A) = C(A,\$2.A) ) & for A st A in \$1 & A <> 0 & A is limit_ordinal holds \$2.A = D(A,\$2|A); defpred R[Ordinal] means ex L st P[\$1,L]; A1: for B st for C st C in B holds R[C] holds R[B] proof defpred R[object,object] means \$1 is Ordinal & \$2 is Sequence & for A,L st A = \$1 & L = \$2 holds P[A,L]; let B such that A2: for C st C in B ex L st P[C,L]; A3: for a,b,c being object st R[a,b] & R[a,c] holds b = c proof let a,b,c be object; assume that A4: a is Ordinal and A5: b is Sequence and A6: for A,L st A = a & L = b holds P[A,L] and a is Ordinal and A7: c is Sequence and A8: for A,L st A = a & L = c holds P[ A,L]; reconsider a as Ordinal by A4; reconsider c as Sequence by A7; A9: dom c = a by A8; A10: for A st A in a & A <> 0 & A is limit_ordinal holds c.A = D(A,c|A) by A8; A11: for A st succ A in a holds c.(succ A) = C(A,c.A) by A8; A12: 0 in a implies c.0 = B() by A8; reconsider b as Sequence by A5; A13: 0 in a implies b.0 = B() by A6; A14: for A st succ A in a holds b.(succ A) = C(A,b.A) by A6; A15: for A st A in a & A <> 0 & A is limit_ordinal holds b.A = D(A,b|A) by A6; A16: dom b = a by A6; b = c from TSUniq1(A16,A13,A14,A15,A9,A12,A11,A10); hence thesis; end; consider G being Function such that A17: for a,b being object holds [a,b] in G iff a in B & R[a,b] from FUNCT_1:sch 1(A3); defpred Q[object,object] means ex A,L st A = \$1 & L = G.\$1 & (A = 0 & \$2 = B() or (ex B st A = succ B & \$2 = C(B,L.B)) or A <> 0 & A is limit_ordinal & \$2 = D(A,L)); A18: dom G = B proof thus for a being object holds a in dom G implies a in B proof let a be object; assume a in dom G; then ex b being object st [a,b] in G by XTUPLE_0:def 12; hence thesis by A17; end; let a be object; assume A19: a in B; then reconsider a9 = a as Ordinal; consider L such that A20: P[a9,L] by A2,A19; for A holds for K be Sequence holds A = a9 & K = L implies P[A,K] by A20; then [a9,L] in G by A17,A19; hence thesis by XTUPLE_0:def 12; end; A21: for a being object st a in B ex b being object st Q[a,b] proof let a be object; assume A22: a in B; then reconsider A = a as Ordinal; consider c being object such that A23: [a,c] in G by A18,A22,XTUPLE_0:def 12; reconsider L = c as Sequence by A17,A23; A24: now given C such that A25: A = succ C; thus ex b being object st Q[a,b] proof take C(C,L.C), A, L; thus A = a & L = G.a by A23,FUNCT_1:1; thus thesis by A25; end; end; A26: now assume A27: A <> 0 & for C holds A <> succ C; thus Q[a,D(A,L)] proof take A,L; thus A = a & L = G.a by A23,FUNCT_1:1; thus thesis by A27,ORDINAL1:29; end; end; now assume A28: A = 0; thus Q[a,B()] proof take A,L; thus A = a & L = G.a by A23,FUNCT_1:1; thus thesis by A28; end; end; hence thesis by A24,A26; end; A29: for a,b,c being object st a in B & Q[a,b] & Q[a,c] holds b = c proof let a,b,c being object such that a in B; given Ab being Ordinal,Lb being Sequence such that A30: Ab = a and A31: Lb = G.a and A32: Ab = 0 & b = B() or (ex B st Ab = succ B & b = C(B,Lb.B)) or Ab <> 0 & Ab is limit_ordinal & b = D(Ab,Lb); given Ac being Ordinal,Lc being Sequence such that A33: Ac = a and A34: Lc = G.a and A35: Ac = 0 & c = B() or (ex B st Ac = succ B & c = C(B,Lc.B)) or Ac <> 0 & Ac is limit_ordinal & c = D(Ac,Lc); now given C such that A36: Ab = succ C; consider A such that A37: Ab = succ A and A38: b = C(A,Lb.A) by A32,A36,ORDINAL1:29; consider D such that A39: Ac = succ D and A40: c = C(D,Lc.D) by A30,A33,A35,A36,ORDINAL1:29; A = D by A30,A33,A37,A39,ORDINAL1:7; hence thesis by A31,A34,A38,A40; end; hence thesis by A30,A31,A32,A33,A34,A35; end; consider F being Function such that A41: dom F = B & for a being object st a in B holds Q[a,F.a] from FUNCT_1:sch 2(A29 ,A21); reconsider L = F as Sequence by A41,ORDINAL1:def 7; take L; thus dom L = B by A41; thus 0 in B implies L.0 = B() proof assume 0 in B; then ex A being Ordinal, K being Sequence st A = 0 & K = G.0 & (A = 0 & F.0 = B() or (ex B st A = succ B & F.0 = C(B,K.B)) or A <> 0 & A is limit_ordinal & F.0 = D(A,K)) by A41; hence thesis; end; A42: 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; A43: for A st for C st C in A holds P[C] holds P[A] proof let A such that for C st C in A for L1 st C in B & L1 = G.C holds L|C = L1; let L1; assume that A44: A in B and A45: L1 = G.A; A46: [A,L1] in G by A18,A44,A45,FUNCT_1:1; then A47: P[A,L1] by A17; A48: now let x be object; assume A49: x in A; then reconsider x9 = x as Ordinal; A50: x9 in B by A44,A49,ORDINAL1:10; then consider A1,L2 such that A51: A1 = x9 and A52: L2 = G.x9 and A53: A1 = 0 & L.x9 = B() or (ex B st A1 = succ B & L.x9 = C(B, L2.B)) or A1 <> 0 & A1 is limit_ordinal & L.x9 = D(A1,L2) by A41; for D,L3 st D = x9 & L3 = L1|x9 holds P[D,L3] proof let D,L3 such that A54: D = x9 and A55: L3 = L1|x9; x9 c= A by A49,ORDINAL1:def 2; hence dom L3 = D by A47,A54,A55,RELAT_1:62; thus 0 in D implies L3.0 = B() by A47,A49,A54,A55,FUNCT_1:49 ,ORDINAL1:10; thus succ C in D implies L3.(succ C) = C(C,L3.C) proof assume A56: succ C in D; C in succ C by ORDINAL1:6; then A57: L1|x9.C = L1.C by A54,A56,FUNCT_1:49,ORDINAL1:10; succ C in A & L1|x9.succ C = L1.succ C by A49,A54,A56,FUNCT_1:49 ,ORDINAL1:10; hence thesis by A17,A46,A55,A57; end; let C; assume that A58: C in D and A59: C <> 0 & C is limit_ordinal; C c= x9 by A54,A58,ORDINAL1:def 2; then A60: L1|C = L3|C by A55,FUNCT_1:51; C in A by A49,A54,A58,ORDINAL1:10; then L1.C = D(C,L3|C) by A17,A46,A59,A60; hence thesis by A54,A55,A58,FUNCT_1:49; end; then [x9,L1|x9] in G by A17,A50; then A61: L1|x9 = L2 by A52,FUNCT_1:1; A62: L|A.x = L.x by A49,FUNCT_1:49; now given D such that A63: x9 = succ D; A64: L1.x = C(D,L1.D) by A17,A46,A49,A63; consider C such that A65: A1 = succ C and A66: L.x9 = C(C,L2.C) by A51,A53,A63,ORDINAL1:29; C = D by A51,A63,A65,ORDINAL1:7; hence L1.x = L|A.x by A62,A61,A63,A66,A64,FUNCT_1:49,ORDINAL1:6; end; hence L1.x = L|A.x by A17,A46,A49,A51,A53,A62,A61; end; A c= dom L by A41,A44,ORDINAL1:def 2; then dom(L|A) = A by RELAT_1:62; hence thesis by A47,A48,FUNCT_1:2; end; thus for A holds P[A] from ORDINAL1:sch 2(A43); end; thus succ A in B implies L.(succ A) = C(A,L.A) proof assume A67: succ A in B; then consider C being Ordinal, K being Sequence such that A68: C = succ A and A69: K = G.succ A and A70: C = 0 & F.succ A = B() or (ex B st C = succ B & F.succ A = C(B ,K.B)) or C <> 0 & C is limit_ordinal & F.succ A = D(C,K) by A41; A71: K = L|succ A by A42,A67,A69; consider D such that A72: C = succ D and A73: F.succ A = C(D,K.D) by A68,A70,ORDINAL1:29; A = D by A68,A72,ORDINAL1:7; hence thesis by A73,A71,FUNCT_1:49,ORDINAL1:6; end; let D; assume that A74: D in B and A75: D <> 0 & D is limit_ordinal; ex A being Ordinal, K being Sequence st A = D & K = G.D & (A = 0 & F.D = B() or (ex B st A = succ B & F.D = C(B,K.B)) or A <> 0 & A is limit_ordinal & F.D = D(A,K)) by A41,A74; hence thesis by A42,A74,A75,ORDINAL1:29; end; for A holds R[A] from ORDINAL1:sch 2(A1); hence thesis; end; scheme TSResult { L()->Sequence, F(Ordinal)->set, A()->Ordinal, B()->set, C( Ordinal,set)->set, D(Ordinal,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. 0 = 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 <> 0 & C is limit_ordinal holds L.C = D(C,L|C) and A2: dom L() = A() and A3: 0 in A() implies L().0 = 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 <> 0 & 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() by ORDINAL1:21; A7: for C st succ C in succ A holds L.succ C = C(C,L.C) proof let C such that A8: succ C in succ A; C in succ C by ORDINAL1:6; then A9: L.C = L().C by A8,FUNCT_1:49,ORDINAL1:10; L.succ C = L().succ C by A8,FUNCT_1:49; hence thesis by A2,A4,A6,A8,A9; end; A10: for C st C in succ A & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C ) proof let C; assume that A11: C in succ A and A12: C <> 0 & C is limit_ordinal; C c= succ A by A11,ORDINAL1:def 2; then A13: L|C = L()|C by FUNCT_1:51; L.C = L().C by A11,FUNCT_1:49; hence thesis by A2,A5,A6,A11,A12,A13; end; 0 c= succ A; then 0 c< succ A; then A14: 0 in succ A & L.0 = L().0 by FUNCT_1:49,ORDINAL1:11; A15: dom L = succ A by A6,RELAT_1:62; then A in succ A & last L = L.A by Th2,ORDINAL1:21; then last L = L().A by FUNCT_1:49; hence thesis by A1,A2,A3,A6,A15,A14,A7,A10; end; scheme TSDef { A()->Ordinal, B()->set, C(Ordinal,set)->set, D(Ordinal,Sequence)-> set } : (ex x,L st x = last L & dom L = succ A() & L.0 = 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 <> 0 & 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.0 = 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 <> 0 & C is limit_ordinal holds L.C = D(C,L|C) ) & (ex L st x2 = last L & dom L = succ A() & L.0 = 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 <> 0 & C is limit_ordinal holds L.C = D(C,L|C) ) holds x1 = x2 proof consider L such that A1: dom L = succ A() & (0 in succ A() implies L.0 = 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 <> 0 & C is limit_ordinal holds L.C = D(C,L|C) from TSExist1; thus ex x,L st x = last L & dom L = succ A() & L.0 = 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 <> 0 & 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; 0 c= succ A(); then 0 c< succ A(); hence thesis by A1,ORDINAL1:11; end; let x1,x2 be set; given L1 such that A2: x1 = last L1 and A3: dom L1 = succ A() and A4: L1.0 = 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 <> 0 & C is limit_ordinal holds L1.C = D (C,L1|C); A7: 0 in succ A() implies L1.0 = B() by A4; given L2 such that A8: x2 = last L2 and A9: dom L2 = succ A() and A10: L2.0 = B() and A11: for C st succ C in succ A() holds L2.succ C = C(C,L2.C) and A12: for C st C in succ A() & C <> 0 & C is limit_ordinal holds L2.C = D(C,L2|C); A13: 0 in succ A() implies L2.0 = B() by A10; L1 = L2 from TSUniq1(A3,A7,A5,A6,A9,A13,A11,A12); hence thesis by A2,A8; end; scheme TSResult0 { F(Ordinal)->set, B()->set, C(Ordinal,set)->set, D(Ordinal, Sequence)->set } : F(0) = B() provided A1: for A,x holds x = F(A) iff ex L st x = last L & dom L = succ A & L. 0 = 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 <> 0 & C is limit_ordinal holds L.C = D(C,L|C) proof consider L such that A2: dom L = succ 0 & (0 in succ 0 implies L.0 = B() ) & (for A st succ A in succ 0 holds L.(succ A) = C(A,L.A) ) & for A st A in succ 0 & A <> 0 & A is limit_ordinal holds L.A = D(A,L|A) from TSExist1; B() = last L by A2,Th2,ORDINAL1:6; hence thesis by A1,A2,ORDINAL1:6; end; scheme TSResultS { B()->set, C(Ordinal,set)->set, D(Ordinal,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. 0 = 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 <> 0 & C is limit_ordinal holds L.C = D(C,L|C) proof let A; consider L such that A2: dom L = succ succ A and A3: 0 in succ succ A implies L.0 = B() and A4: for C st succ C in succ succ A holds L.(succ C) = C(C,L.C) and A5: for C st C in succ succ A & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C) from TSExist1; A6: for A,x holds x = F(A) iff ex L st x = last L & dom L = succ A & L.0 = 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 <> 0 & C is limit_ordinal holds L.C = D(C,L|C) by A1; A7: for B st B in dom L holds L.B = F(B) from TSResult(A6,A2,A3,A4, A5); then A8: L.succ A = F(succ A) by A2,ORDINAL1:6; A in succ A & succ A in succ succ A by ORDINAL1:6; then L.A = F(A) by A2,A7,ORDINAL1:10; hence thesis by A4,A8,ORDINAL1:6; end; scheme TSResultL { L()->Sequence, A()->Ordinal, F(Ordinal)->set, B()->set, C( Ordinal,set)->set, D(Ordinal,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. 0 = 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 <> 0 & C is limit_ordinal holds L.C = D(C,L|C) and A2: A() <> 0 & A() is limit_ordinal and A3: dom L() = A() and A4: for A st A in A() holds L().A = F(A) proof A5: A() in succ A() by ORDINAL1:6; consider L such that A6: dom L = succ A() and A7: 0 in succ A() implies L.0 = B() and A8: for C st succ C in succ A() holds L.(succ C) = C(C,L.C) and A9: for C st C in succ A() & C <> 0 & C is limit_ordinal holds L.C = D( C,L|C) from TSExist1; set L1 = L|A(); A10: for A,x holds x = F(A) iff ex L st x = last L & dom L = succ A & L.0 = 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 <> 0 & C is limit_ordinal holds L.C = D(C,L|C) by A1; A11: for B st B in dom L holds L.B = F(B) from TSResult(A10,A6,A7,A8, A9); A12: now let x be object; assume A13: x in A(); then reconsider x9 = x as Ordinal; thus L1.x = L.x9 by A13,FUNCT_1:49 .= F(x9) by A6,A11,A5,A13,ORDINAL1:10 .= L().x by A4,A13; end; A() c= dom L by A6,A5,ORDINAL1:def 2; then dom L1 = A() by RELAT_1:62; then L1 = L() by A3,A12,FUNCT_1:2; then L.A() = D(A(),L()) by A2,A9,ORDINAL1:6; hence thesis by A6,A11,ORDINAL1:6; end; scheme OSExist { A()->Ordinal, B()->Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal ,Sequence)->Ordinal } : ex fi st dom fi = A() & (0 in A() implies fi.0 = B( ) ) & (for A st succ A in A() holds fi.(succ A) = C(A,fi.A) ) & for A st A in A () & A <> 0 & A is limit_ordinal holds fi.A = D(A,fi|A) proof deffunc CC(Ordinal,set) = C(\$1,sup union {\$2}); consider L such that A1: dom L = A() and A2: 0 in A() implies L.0 = 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 <> 0 & A is limit_ordinal holds L.A = D(A,L|A ) from TSExist1; L is Ordinal-yielding proof take sup rng L; let x be object; assume A5: x in rng L; then consider y being object such that A6: y in dom L and A7: x = L.y by FUNCT_1:def 3; reconsider y as Ordinal by A6; A8: now assume that A9: y <> 0 and A10: for B holds y <> succ B; y is limit_ordinal by A10,ORDINAL1:29; then L.y = D(y,L|y) by A1,A4,A6,A9; hence x is Ordinal by A7; end; A11: On rng L c= sup rng L by Def3; now given B such that A12: y = succ B; L.y = C(B,sup union {L.B}) by A1,A3,A6,A12; hence x is Ordinal by A7; end; then x in On rng L by A1,A2,A5,A6,A7,A8,ORDINAL1:def 9; hence thesis by A11; end; then reconsider L as Ordinal-Sequence; take fi = L; thus dom fi = A() & (0 in A() implies fi.0 = 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:25 .= B by Th18; hence thesis by A3; end; thus thesis by A4; end; scheme OSResult { fi()->Ordinal-Sequence, F(Ordinal)->Ordinal, A()->Ordinal, B()-> Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal,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.0 = 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 <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) and A2: dom fi() = A() and A3: 0 in A() implies fi().0 = 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 <> 0 & 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() by ORDINAL1:21; A7: for C st succ C in succ A holds fi.succ C = C(C,fi.C) proof let C such that A8: succ C in succ A; C in succ C by ORDINAL1:6; then A9: fi.C = fi().C by A8,FUNCT_1:49,ORDINAL1:10; fi.succ C = fi().succ C by A8,FUNCT_1:49; hence thesis by A2,A4,A6,A8,A9; end; A10: for C st C in succ A & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi |C) proof let C; assume that A11: C in succ A and A12: C <> 0 & C is limit_ordinal; C c= succ A by A11,ORDINAL1:def 2; then A13: fi|C = fi()|C by FUNCT_1:51; fi.C = fi().C by A11,FUNCT_1:49; hence thesis by A2,A5,A6,A11,A12,A13; end; 0 c= succ A; then 0 c< succ A; then A14: 0 in succ A & fi.0 = fi().0 by FUNCT_1:49,ORDINAL1:11; A15: dom fi = succ A by A6,RELAT_1:62; then A in succ A & last fi = fi.A by Th2,ORDINAL1:21; then last fi = fi().A by FUNCT_1:49; hence thesis by A1,A2,A3,A6,A15,A14,A7,A10; end; scheme OSDef { A()->Ordinal, B()->Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal, Sequence)->Ordinal } : (ex A,fi st A = last fi & dom fi = succ A() & fi.0 = 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 <> 0 & 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.0 = 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 <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) & (ex fi st A2 = last fi & dom fi = succ A() & fi.0 = 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 <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) holds A1 = A2 proof consider fi such that A1: dom fi = succ A() & (0 in succ A() implies fi.0 = 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 <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) from OSExist; reconsider A = last fi as Ordinal; thus ex A,fi st A = last fi & dom fi = succ A() & fi.0 = 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 <> 0 & 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; 0 c= succ A(); then 0 c< succ A(); hence thesis by A1,ORDINAL1:11; end; deffunc CD(Ordinal,Ordinal) = C(\$1,sup union { \$2 }); 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.0 = 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 <> 0 & C is limit_ordinal holds L1.C = D (C,L1|C); A7: 0 in succ A() implies L1.0 = B() by A4; A8: for C st succ C in succ A() holds L1.(succ C) = CD(C,L1.C) proof let C such that A9: succ C in succ A(); reconsider x9 = L1.C as Ordinal; sup union { L1.C } = sup x9 by ZFMISC_1:25 .= x9 by Th18; hence thesis by A5,A9; end; given L2 being Ordinal-Sequence such that A10: A2 = last L2 and A11: dom L2 = succ A() and A12: L2.0 = B() and A13: for C st succ C in succ A() holds L2.succ C = C(C,L2.C) and A14: for C st C in succ A() & C <> 0 & C is limit_ordinal holds L2.C = D(C,L2|C); A15: for C st C in succ A() & C <> 0 & C is limit_ordinal holds L2.C = D(C, L2|C) by A14; A16: for C st C in succ A() & C <> 0 & C is limit_ordinal holds L1.C = D(C, L1|C) by A6; A17: for C st succ C in succ A() holds L2.(succ C) = CD(C,L2.C) proof let C such that A18: succ C in succ A(); reconsider x9 = L2.C as Ordinal; sup union { L2.C } = sup x9 by ZFMISC_1:25 .= x9 by Th18; hence thesis by A13,A18; end; A19: 0 in succ A() implies L2.0 = B() by A12; L1 = L2 from TSUniq1(A3,A7,A8,A16,A11,A19,A17,A15); hence thesis by A2,A10; end; scheme OSResult0 { F(Ordinal)->Ordinal, B()->Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal,Sequence)->Ordinal } : F(0) = B() provided A1: for A,B holds B = F(A) iff ex fi st B = last fi & dom fi = succ A & fi.0 = 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 <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) proof consider fi such that A2: dom fi = succ 0 & (0 in succ 0 implies fi.0 = B() ) & (for A st succ A in succ 0 holds fi.(succ A) = C(A,fi.A) ) & for A st A in succ 0 & A <> 0 & A is limit_ordinal holds fi.A = D(A,fi|A) from OSExist; B() = last fi by A2,Th2,ORDINAL1:6; hence thesis by A1,A2,ORDINAL1:6; end; scheme OSResultS { B()->Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal,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.0 = 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 <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) proof let A; consider fi such that A2: dom fi = succ succ A and A3: 0 in succ succ A implies fi.0 = B() and A4: for C st succ C in succ succ A holds fi.(succ C) = C(C,fi.C) and A5: for C st C in succ succ A & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) from OSExist; A6: for A,B holds B = F(A) iff ex fi st B = last fi & dom fi = succ A & fi. 0 = 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 <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by A1; A7: for B st B in dom fi holds fi.B = F(B) from OSResult(A6,A2,A3,A4, A5); then A8: fi.succ A = F(succ A) by A2,ORDINAL1:6; A in succ A & succ A in succ succ A by ORDINAL1:6; then fi.A = F(A) by A2,A7,ORDINAL1:10; hence thesis by A4,A8,ORDINAL1:6; end; scheme OSResultL { fi()->Ordinal-Sequence, A()->Ordinal, F(Ordinal)->Ordinal, B()-> Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal,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.0 = 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 <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) and A2: A() <> 0 & A() is limit_ordinal and A3: dom fi() = A() and A4: for A st A in A() holds fi().A = F(A) proof A5: A() in succ A() by ORDINAL1:6; consider fi such that A6: dom fi = succ A() and A7: 0 in succ A() implies fi.0 = B() and A8: for C st succ C in succ A() holds fi.(succ C) = C(C,fi.C) and A9: for C st C in succ A() & C <> 0 & C is limit_ordinal holds fi.C = D (C,fi|C) from OSExist; set psi = fi|A(); A10: for A,B holds B = F(A) iff ex fi st B = last fi & dom fi = succ A & fi. 0 = 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 <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by A1; A11: for B st B in dom fi holds fi.B = F(B) from OSResult(A10,A6,A7,A8, A9); A12: now let x be object; assume A13: x in A(); then reconsider x9 = x as Ordinal; thus psi.x = fi.x9 by A13,FUNCT_1:49 .= F(x9) by A6,A11,A5,A13,ORDINAL1:10 .= fi().x by A4,A13; end; A() c= dom fi by A6,A5,ORDINAL1:def 2; then dom psi = A() by RELAT_1:62; then psi = fi() by A3,A12,FUNCT_1:2; then fi.A() = D(A(),fi()) by A2,A9,ORDINAL1:6; hence thesis by A6,A11,ORDINAL1:6; end; definition let L; func sup L -> Ordinal equals sup rng L; correctness; func inf L -> Ordinal equals inf rng L; correctness; end; theorem sup L = sup rng L & inf L = inf rng L; 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 OSLambda; take inf fi, fi; thus thesis by A1; end; uniqueness proof let A1,A2 be Ordinal; given fi such that A2: A1 = inf fi & dom fi = dom L and A3: for A st A in dom L holds fi.A = sup rng (L|(dom L \ A)); given psi such that A4: A2 = inf psi & dom psi = dom L and A5: for A st A in dom L holds psi.A = sup rng (L|(dom L \ A)); now let x be object; assume A6: x in dom L; then reconsider A = x as Ordinal; fi.A = sup rng (L|(dom L \ A)) by A3,A6; hence fi.x = psi.x by A5,A6; end; hence thesis by A2,A4,FUNCT_1:2; 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 OSLambda; take sup fi, fi; thus thesis by A7; end; uniqueness proof let A1,A2 be Ordinal; given fi such that A8: A1 = sup fi & dom fi = dom L and A9: for A st A in dom L holds fi.A = inf rng (L|(dom L \ A)); given psi such that A10: A2 = sup psi & dom psi = dom L and A11: for A st A in dom L holds psi.A = inf rng (L|(dom L \ A)); now let x be object; assume A12: x in dom L; then reconsider A = x as Ordinal; fi.A = inf rng (L|(dom L \ A)) by A9,A12; hence fi.x = psi.x by A11,A12; end; hence thesis by A8,A10,FUNCT_1:2; end; end; definition let A,fi; pred A is_limes_of fi means :Def9: ex B st B in dom fi & for C st B c= C & C in dom fi holds fi.C = 0 if A = 0 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 :Def10: it is_limes_of fi; existence by A1; uniqueness proof let A1,A2 be Ordinal such that A2: (A1 = 0 & ex B st B in dom fi & for C st B c= C & C in dom fi holds fi.C = 0) or (A1 <> 0 & 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 = 0 & ex B st B in dom fi & for C st B c= C & C in dom fi holds fi.C = 0) or (A2 <> 0 & 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); A4: now set x = the Element of A1; reconsider x as Ordinal; assume A1 in A2; then consider D such that A5: D in dom fi and A6: for A st D c= A & A in dom fi holds A1 in fi.A & fi.A in succ A2 by A3,ORDINAL1:6; now assume A1 = 0; then consider B such that A7: B in dom fi and A8: for C st B c= C & C in dom fi holds fi.C = 0 by A2; B c= D or D c= B; then consider E being Ordinal such that A9: E = D & B c= D or E = B & D c= B; fi.E = 0 by A5,A7,A8,A9; hence contradiction by A5,A6,A7,A9; end; then consider C such that A10: C in dom fi and A11: for A st C c= A & A in dom fi holds x in fi.A & fi.A in succ A1 by A2,ORDINAL1:6; C c= D or D c= C; then consider E being Ordinal such that A12: E = D & C c= D or E = C & D c= C; fi.E in succ A1 by A5,A10,A11,A12; then A13: fi.E in A1 or fi.E = A1 by ORDINAL1:8; A1 in fi.E by A5,A6,A10,A12; hence contradiction by A13; end; set x = the Element of A2; reconsider x as Ordinal; assume A1 <> A2; then A1 in A2 or A2 in A1 by ORDINAL1:14; then consider D such that A14: D in dom fi and A15: for A st D c= A & A in dom fi holds A2 in fi.A & fi.A in succ A1 by A2,A4,ORDINAL1:6; now assume A2 = 0; then consider B such that A16: B in dom fi and A17: for C st B c= C & C in dom fi holds fi.C = 0 by A3; B c= D or D c= B; then consider E being Ordinal such that A18: E = D & B c= D or E = B & D c= B; fi.E = 0 by A14,A16,A17,A18; hence contradiction by A14,A15,A16,A18; end; then consider C such that A19: C in dom fi and A20: for A st C c= A & A in dom fi holds x in fi.A & fi.A in succ A2 by A3,ORDINAL1:6; C c= D or D c= C; then consider E being Ordinal such that A21: E = D & C c= D or E = C & D c= C; fi.E in succ A2 by A14,A19,A20,A21; then A22: fi.E in A2 or fi.E = A2 by ORDINAL1:8; A2 in fi.E by A14,A15,A19,A21; hence contradiction by A22; 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 <> 0 & A is limit_ordinal & B = L.A holds B is_limes_of L|A; end; definition let A,B be Ordinal; func A +^ B -> Ordinal means :Def14: ex fi st it = last fi & dom fi = succ B & fi.0 = A & (for C st succ C in succ B holds fi.succ C = succ(fi.C)) & for C st C in succ B & C <> 0 & C is limit_ordinal holds fi.C = sup(fi|C); correctness proof deffunc D(Ordinal,Sequence) = sup \$2; deffunc C(Ordinal,Ordinal) = succ \$2; (ex F being Ordinal,fi st F = last fi & dom fi = succ B & fi.0 = 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 <> 0 & 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.0 = 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 <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) & (ex fi st A2 = last fi & dom fi = succ B & fi.0 = 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 <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) holds A1 = A2 from OSDef; hence thesis; end; end; definition let A,B; func A *^ B -> Ordinal means :Def15: ex fi st it = last fi & dom fi = succ A & fi.0 = 0 & (for C st succ C in succ A holds fi.succ C = (fi.C)+^B) & for C st C in succ A & C <> 0 & C is limit_ordinal holds fi.C = union sup(fi|C); correctness proof deffunc D(Ordinal,Ordinal-Sequence) = union sup \$2; deffunc C(Ordinal,Ordinal) = \$2+^B; (ex F being Ordinal,fi st F = last fi & dom fi = succ A & fi.0 = 0 & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C st C in succ A & C <> 0 & 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.0 = 0 & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C st C in succ A & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) & (ex fi st A2 = last fi & dom fi = succ A & fi.0 = 0 & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C st C in succ A & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) holds A1 = A2 from OSDef; hence thesis; end; end; registration let O be Ordinal; cluster -> ordinal for Element of O; coherence; end; definition let A,B; func exp(A,B) -> Ordinal means :Def16: ex fi st it = last fi & dom fi = succ B & fi.0 = 1 & (for C st succ C in succ B holds fi.succ C = A*^(fi.C)) & for C st C in succ B & C <> 0 & C is limit_ordinal holds fi.C = lim(fi|C); correctness proof deffunc D(Ordinal,Ordinal-Sequence) = lim \$2; deffunc C(Ordinal,Ordinal) = A*^\$2; (ex F being Ordinal,fi st F = last fi & dom fi = succ B & fi.0 = 1 & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> 0 & 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.0 = 1 & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) & (ex fi st A2 = last fi & dom fi = succ B & fi.0 = 1 & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) holds A1 = A2 from OSDef; hence thesis; end; end; theorem Th27: A+^0 = A proof deffunc C(Ordinal,Ordinal) = succ \$2; deffunc D(Ordinal,Sequence) = sup \$2; deffunc F(Ordinal) = A+^\$1; A1: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi. 0 = 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 <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def14; thus F(0) = A from OSResult0(A1); end; theorem Th28: A+^succ B = succ(A+^B) proof deffunc C(Ordinal,Ordinal) = succ \$2; deffunc D(Ordinal,Sequence) = sup \$2; deffunc F(Ordinal) = A+^\$1; A1: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi. 0 = 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 <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def14; for B holds F(succ B) = C(B,F(B)) from OSResultS(A1); hence thesis; end; theorem Th29: B <> 0 & 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 deffunc C(Ordinal,Ordinal) = succ \$2; deffunc D(Ordinal,Ordinal-Sequence) = sup \$2; assume A1: B <> 0 & B is limit_ordinal; deffunc F(Ordinal) = A+^\$1; 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. 0 = 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 <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def14; thus F(B) = D(B,fi) from OSResultL(A4,A1,A2,A3); end; theorem Th30: 0+^A = A proof defpred P[Ordinal] means 0+^\$1 = \$1; A1: for A holds P[A] implies P[succ A] by Th28; A2: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B] holds P[A] proof deffunc F(Ordinal) = 0+^\$1; let A; assume that A3: A <> 0 & A is limit_ordinal and A4: for B st B in A holds 0+^B = B; consider fi such that A5: dom fi = A & for B st B in A holds fi.B = F(B) from OSLambda; A6: rng fi = A proof thus for x being object holds x in rng fi implies x in A proof let x be object; assume x in rng fi; then consider y being object such that A7: y in dom fi and A8: x = fi.y by FUNCT_1:def 3; reconsider y as Ordinal by A7; x = 0+^y by A5,A7,A8 .= y by A4,A5,A7; hence thesis by A5,A7; end; let x be object; assume A9: x in A; then reconsider B = x as Ordinal; 0+^B = B & fi.B = 0+^B by A4,A5,A9; hence thesis by A5,A9,FUNCT_1:def 3; end; 0+^A = sup fi by A3,A5,Th29 .= sup rng fi; hence thesis by A6,Th18; end; A10: P[0] by Th27; for A holds P[A] from OrdinalInd(A10,A1,A2); hence thesis; end; Lm1: 1 = succ 0; theorem A+^1 = succ A proof thus A+^1 = succ(A+^0) by Lm1,Th28 .= succ A by Th27; end; theorem Th32: 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: now assume A in D; then A7: C +^ A in C +^ D by A2,A5,ORDINAL1:6; succ(C +^ D) = C +^ succ D & C +^ D in succ(C +^ D) by Th28,ORDINAL1:6; hence thesis by A5,A7,ORDINAL1:10; end; now assume A8: not A in D; A c< D iff A c= D & A <> D; then C +^ A in succ(C +^ D) by A3,A5,A8,ORDINAL1:11,22; hence thesis by A5,Th28; end; hence thesis by A6; end; now deffunc F(Ordinal) = C+^\$1; consider fi such that A9: dom fi = B & for D st D in B holds fi.D = F(D) from OSLambda; fi.A = C+^A by A3,A9; then A10: C+^A in rng fi by A3,A9,FUNCT_1:def 3; assume for D holds B <> succ D; then B is limit_ordinal by ORDINAL1:29; then C+^B = sup fi by A3,A9,Th29 .= sup rng fi; hence thesis by A10,Th19; end; hence thesis by A4; end; for B holds P[B] from ORDINAL1:sch 2(A1); hence thesis; end; theorem Th33: 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; then C +^ A in C +^ B by Th32,ORDINAL1:11; hence thesis by ORDINAL1:def 2; end; hence thesis; end; theorem Th34: A c= B implies A +^ C c= B +^ C proof defpred P[Ordinal] means A +^ \$1 c= B +^ \$1; assume A1: A c= B; 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 given D such that A5: C = succ D; A6: B +^ C = succ(B +^ D) by A5,Th28; A +^ D c= B +^ D & A +^ C = succ(A +^ D) by A3,A5,Th28,ORDINAL1:6; hence thesis by A6,Th1; end; A7: now deffunc F(Ordinal) = A+^\$1; assume that A8: C <> 0 and A9: for D holds C <> succ D; consider fi such that A10: dom fi = C & for D st D in C holds fi.D = F(D) from OSLambda; A11: now let D; assume D in rng fi; then consider x being object such that A12: x in dom fi and A13: D = fi.x by FUNCT_1:def 3; reconsider x as Ordinal by A12; A14: B +^ x in B +^ C by A10,A12,Th32; D = A+^x & A +^ x c= B +^ x by A3,A10,A12,A13; hence D in B +^ C by A14,ORDINAL1:12; end; C is limit_ordinal by A9,ORDINAL1:29; then A+^C = sup fi by A8,A10,Th29 .= sup rng fi; hence thesis by A11,Th20; end; now assume A15: C = 0; then A +^ C = A by Th27; hence thesis by A1,A15,Th27; end; hence thesis by A4,A7; end; for C holds P[C] from ORDINAL1:sch 2(A2); hence thesis; end; theorem Th35: 0*^A = 0 proof deffunc D(Ordinal,Sequence) = union sup \$2; deffunc F(Ordinal) = \$1*^A; 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. 0 = 0 & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def15; thus F(0) = 0 from OSResult0(A1); end; theorem Th36: (succ B)*^A = B*^A +^ A proof deffunc D(Ordinal,Sequence) = union sup \$2; deffunc F(Ordinal) = \$1*^A; 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. 0 = 0 & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def15; for B holds F(succ B) = C(B,F(B)) from OSResultS(A1); hence thesis; end; theorem Th37: B <> 0 & 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 deffunc D(Ordinal,Ordinal-Sequence) = union sup \$2; assume A1: B <> 0 & B is limit_ordinal; deffunc C(Ordinal,Ordinal) = \$2+^A; deffunc F(Ordinal) = \$1*^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. 0 = 0 & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def15; thus F(B) = D(B,fi) from OSResultL(A4,A1,A2,A3); end; theorem Th38: A*^0 = 0 proof defpred P[Ordinal] means \$1*^0 = 0; A1: for A st P[A] holds P[succ A] proof let A; assume A*^0 = 0; hence (succ A)*^0 = 0+^0 by Th36 .= 0 by Th27; end; A2: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B] holds P[A] proof deffunc F(Ordinal) = \$1*^0; let A; assume that A3: A <> 0 and A4: A is limit_ordinal and A5: for B st B in A holds B*^0 = 0; consider fi such that A6: dom fi = A & for B st B in A holds fi.B = F(B) from OSLambda; rng fi = succ 0 proof thus for x being object holds x in rng fi implies x in succ 0 proof let x be object; assume x in rng fi; then consider y being object such that A7: y in dom fi and A8: x = fi.y by FUNCT_1:def 3; reconsider y as Ordinal by A7; x = y*^0 by A6,A7,A8 .= 0 by A5,A6,A7; hence thesis by TARSKI:def 1; end; let x be object; assume x in succ 0; then A9: x = 0 by TARSKI:def 1; 0 c= A; then A10: 0 c< A by A3; then A11: 0 in A by ORDINAL1:11; 0 *^ 0 = 0 by Th35; then fi.x = x by A6,A10,A9,ORDINAL1:11; hence thesis by A6,A11,A9,FUNCT_1:def 3; end; then A12: sup rng fi = succ 0 by Th18; A*^0 = union sup fi by A3,A4,A6,Th37 .= union sup rng fi; hence thesis by A12,Th2; end; A13: P[0] by Th35; for A holds P[A] from OrdinalInd(A13,A1,A2); hence thesis; end; theorem Th39: 1*^A = A & A*^1 = A proof defpred P[Ordinal] means \$1*^succ 0 = \$1; thus 1*^A = 0*^A +^ A by Lm1,Th36 .= 0 +^ A by Th35 .= A by Th30; 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 0) = B; A3: now deffunc F(Ordinal) = \$1*^succ 0; assume that A4: A <> 0 and A5: for B holds A <> succ B; consider fi such that A6: dom fi = A & for D st D in A holds fi.D = F(D) from OSLambda; A7: A = rng fi proof thus A c= rng fi proof let x be object; assume A8: x in A; then reconsider B = x as Ordinal; x = B*^succ 0 by A2,A8 .= fi.x by A6,A8; hence thesis by A6,A8,FUNCT_1:def 3; end; let x be object; assume x in rng fi; then consider y being object such that A9: y in dom fi and A10: x = fi.y by FUNCT_1:def 3; reconsider y as Ordinal by A9; fi.y = y*^succ 0 by A6,A9 .= y by A2,A6,A9; hence thesis by A6,A9,A10; end; A11: A is limit_ordinal by A5,ORDINAL1:29; then A*^succ 0 = union sup fi by A4,A6,Th37 .= union sup rng fi; hence A*^succ 0 = union A by A7,Th18 .= A by A11; end; now given B such that A12: A = succ B; thus A*^(succ 0) = B*^(succ 0) +^ succ 0 by A12,Th36 .= B +^ succ 0 by A2,A12,ORDINAL1:6 .= succ(B +^ 0) by Th28 .= A by A12,Th27; end; hence thesis by A3,Th35; end; for A holds P[A] from ORDINAL1:sch 2(A1); hence thesis; end; theorem Th40: C <> 0 & A in B implies A*^C in B*^C proof A1: 0 c= C; defpred P[Ordinal] means A in \$1 implies A*^C in \$1*^C; assume C <> 0; then A2: 0 c< C by A1; then A3: 0 in C by ORDINAL1:11; A4: for B st for D st D in B holds P[D] holds P[B] proof let B such that A5: for D st D in B holds A in D implies A *^ C in D *^ C and A6: A in B; A7: now given D such that A8: B = succ D; A9: now assume A in D; then A10: A*^C in D*^C by A5,A8,ORDINAL1:6; A11: D*^C +^ 0 in D*^C +^ C by A2,Th32,ORDINAL1:11; D*^C +^ C = (succ D)*^C & D*^C +^ 0 = D*^C by Th27,Th36; hence thesis by A8,A10,A11,ORDINAL1:10; end; now A12: A*^C +^ 0 = A*^C by Th27; assume A13: not A in D; A c< D iff A c= D & A <> D; then A*^C +^ 0 in D*^C +^ C by A3,A6,A8,A13,Th32,ORDINAL1:11,22; hence thesis by A8,A12,Th36; end; hence thesis by A9; end; now A14: A*^C +^ 0 = A*^C & A*^C +^ 0 in A*^C +^ C by A2,Th27,Th32,ORDINAL1:11; A15: (succ A)*^C = A*^C +^ C by Th36; deffunc F(Ordinal) = \$1*^C; consider fi such that A16: dom fi = B & for D st D in B holds fi.D = F(D) from OSLambda; assume for D holds B <> succ D; then A17: B is limit_ordinal by ORDINAL1:29; then A18: succ A in B by A6,ORDINAL1:28; then fi.(succ A) = (succ A)*^C by A16; then (succ A)*^C in rng fi by A16,A18,FUNCT_1:def 3; then A19: (succ A)*^C c= union sup rng fi by Th19,ZFMISC_1:74; B*^C = union sup fi by A6,A17,A16,Th37 .= union sup rng fi; hence thesis by A19,A14,A15; end; hence thesis by A7; end; for B holds P[B] from ORDINAL1:sch 2(A4); hence thesis; end; theorem A c= B implies A*^C c= B*^C proof assume A1: A c= B; A2: now assume A3: C <> 0; now assume A <> B; then A c< B by A1; then A*^C in B*^C by A3,Th40,ORDINAL1:11; hence thesis by ORDINAL1:def 2; end; hence thesis; end; C = 0 implies thesis by Th38; hence thesis by A2; end; theorem A c= B implies C*^A c= C*^B proof assume A1: A c= B; now defpred P[Ordinal] means \$1*^A c= \$1*^B; assume A2: B <> 0; 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 given D such that A6: C = succ D; D*^A c= D*^B by A4,A6,ORDINAL1:6; then A7: D*^A +^ A c= D*^B +^ A by Th34; A8: C*^A = D*^A +^ A & C*^B = D*^B +^ B by A6,Th36; D*^B +^ A c= D*^B +^ B by A1,Th33; hence thesis by A7,A8,XBOOLE_1:1; end; A9: now deffunc F(Ordinal) = \$1*^A; assume that A10: C <> 0 and A11: for D holds C <> succ D; consider fi such that A12: dom fi = C & for D st D in C holds fi.D = F(D) from OSLambda; now let D; assume D in rng fi; then consider x being object such that A13: x in dom fi and A14: D = fi.x by FUNCT_1:def 3; reconsider x as Ordinal by A13; A15: x*^B in C*^B by A2,A12,A13,Th40; D = x*^A & x*^A c= x*^B by A4,A12,A13,A14; hence D in C*^B by A15,ORDINAL1:12; end; then A16: sup rng fi c= C*^B by Th20; C is limit_ordinal by A11,ORDINAL1:29; then A17: C*^A = union sup fi by A10,A12,Th37 .= union sup rng fi; union sup rng fi c= sup rng fi by Th5; hence thesis by A17,A16,XBOOLE_1:1; end; now assume C = 0; then C*^A = 0 by Th35; hence thesis; end; hence thesis by A5,A9; end; for C holds P[C] from ORDINAL1:sch 2(A3); hence thesis; end; hence thesis by A1; end; theorem Th43: exp(A,0) = 1 proof deffunc D(Ordinal,Ordinal-Sequence) = lim \$2; deffunc F(Ordinal) = exp(A,\$1); 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. 0 = 1 & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def16; thus F(0) = 1 from OSResult0(A1); end; theorem Th44: exp(A,succ B) = A*^exp(A,B) proof deffunc D(Ordinal,Ordinal-Sequence) = lim \$2; deffunc F(Ordinal) = exp(A,\$1); 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. 0 = 1 & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def16; for B holds F(succ B) = C(B,F(B)) from OSResultS(A1); hence thesis; end; theorem Th45: B <> 0 & 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 deffunc D(Ordinal,Ordinal-Sequence) = lim \$2; assume A1: B <> 0 & B is limit_ordinal; deffunc C(Ordinal,Ordinal) = A*^\$2; deffunc F(Ordinal) = exp(A,\$1); 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. 0 = 1 & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def16; thus F(B) = D(B,fi) from OSResultL(A4,A1,A2,A3); end; theorem exp(A,1) = A & exp(1,A) = 1 proof defpred P[Ordinal] means exp(1,\$1) = 1; A1: for A st P[A] holds P[succ A] proof let A; assume exp(1,A) = 1; hence exp(1,succ A) = 1*^1 by Th44 .= 1 by Th39; end; thus exp(A,1) = A*^exp(A,0) by Lm1,Th44 .= A*^1 by Th43 .= A by Th39; A2: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B] holds P[A] proof deffunc F(Ordinal) = exp(1,\$1); let A such that A3: A <> 0 and A4: A is limit_ordinal and A5: for B st B in A holds exp(1,B) = 1; consider fi such that A6: dom fi = A & for B st B in A holds fi.B = F(B) from OSLambda; A7: rng fi c= { 1 } proof let x be object; assume x in rng fi; then consider y being object such that A8: y in dom fi and A9: x = fi.y by FUNCT_1:def 3; reconsider y as Ordinal by A8; x = exp(1,y) by A6,A8,A9 .= 1 by A5,A6,A8; hence thesis by TARSKI:def 1; end; now set x = the Element of A; thus 0 <> 1; let B,C such that A10: B in 1 & 1 in C; reconsider x as Ordinal; take D = x; thus D in dom fi by A3,A6; let E be Ordinal; assume that D c= E and A11: E in dom fi; fi.E in rng fi by A11,FUNCT_1:def 3; hence B in fi.E & fi.E in C by A7,A10,TARSKI:def 1; end; then A12: 1 is_limes_of fi by Def9; exp(1,A) = lim fi by A3,A4,A6,Th45; hence thesis by A12,Def10; end; A13: P[0] by Th43; for A holds P[A] from OrdinalInd(A13,A1,A2); hence thesis; end; 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: (ex B st A = succ B) implies Th[A] proof given B such that A4: A = succ B; consider C,D such that A5: C is limit_ordinal and A6: D is natural and A7: B = C +^ D by A2,A4,ORDINAL1:6; take C, E = succ D; thus C is limit_ordinal by A5; thus E in omega by A6,ORDINAL1:def 12; thus thesis by A4,A7,Th28; end; (for B holds A <> succ B) implies Th[A] proof assume A8: for D holds A <> succ D; take B = A, C = 0; thus B is limit_ordinal by A8,ORDINAL1:29; thus C in omega by ORDINAL1:def 11; thus thesis by Th27; end; hence thesis by A3; end; thus for A holds Th[A] from ORDINAL1:sch 2(A1); end; :: 2005.05.04, A.T. registration let X be set, o be Ordinal; cluster X --> o -> Ordinal-yielding; coherence proof rng(X --> o) c= {o} & {o} c= succ o by FUNCOP_1:13,XBOOLE_1:7; then rng(X --> o) c= succ o; hence thesis; end; end; registration let O be Ordinal, x be object; cluster O --> x -> Sequence-like; coherence by FUNCOP_1:13; end; :: from ZFREFLE1, 2007.03.14, A.T. definition let A,B be Ordinal; pred A is_cofinal_with B means ex xi being Ordinal-Sequence st dom xi = B & rng xi c= A & xi is increasing & A = sup xi; reflexivity proof let A; A1: dom id A = A by RELAT_1:45; then reconsider xi = id A as Sequence by ORDINAL1:def 7; A2: rng id A = A by RELAT_1:45; then reconsider xi as Ordinal-Sequence by Def4; take xi; thus dom xi = A & rng xi c= A by RELAT_1:45; thus xi is increasing proof let B,C; assume that A3: B in C and A4: C in dom xi; xi.C = C by A1,A4,FUNCT_1:18; hence thesis by A1,A3,A4,FUNCT_1:18,ORDINAL1:10; end; thus thesis by A2,Th18; end; end; reserve e,u for set; theorem Th48: e in rng psi implies e is Ordinal proof assume e in rng psi; then ex u being object st u in dom psi & e = psi.u by FUNCT_1:def 3; hence thesis; end; theorem rng psi c= sup psi proof let e be object; assume A1: e in rng psi; then e is Ordinal by Th48; hence thesis by A1,Th19; end; theorem A is_cofinal_with 0 implies A = 0 proof given psi such that A1: dom psi = 0 and rng psi c= A and psi is increasing and A2: A = sup psi; thus A = sup 0 by A1,A2,RELAT_1:42 .= 0 by Th18; end; :: from ARYTM_3, 2007.10.23, A.T. scheme OmegaInd {a()-> Nat, P[object]}: P[a()] provided A1: P[0] and A2: for a being Nat st P[a] holds P[succ a] proof defpred P[Ordinal] means \$1 is natural implies P[\$1]; A3: now let A; assume A4: P[A]; now assume succ A is natural; then A5: succ A in omega; A in succ A by ORDINAL1:6; then A is Element of omega by A5,ORDINAL1:10; hence P[succ A] by A2,A4; end; hence P[succ A]; end; A6: now let A; assume A7: A <> 0; 0 c= A; then 0 c< A by A7; then A8: 0 in A by ORDINAL1:11; A9: not A in A; assume A is limit_ordinal; then omega c= A by A8,ORDINAL1:def 11; then not A in omega by A9; hence (for B st B in A holds P[B]) implies P[A] by ORDINAL1:def 12; end; A10: P[0] by A1; for A holds P[A] from OrdinalInd(A10,A3,A6); hence thesis; end; registration let a, b be Nat; cluster a +^ b -> natural; coherence proof defpred P[Nat] means a+^\$1 is natural; A1: now let b be Nat; assume P[b]; then reconsider c = a+^b as Nat; a+^succ b = succ c by Th28; hence P[succ b]; end; A2: P[0] by Th27; thus P[b] from OmegaInd(A2,A1); end; end; :: from AMI_2, 2008.02.14, A.T. registration let x,y be set, a,b be Nat; cluster IFEQ(x,y,a,b) -> natural; coherence proof per cases; suppose x = y; hence thesis by FUNCOP_1:def 8; end; suppose x <> y; hence thesis by FUNCOP_1:def 8; end; end; end; :: 2010.03.16, A.T. scheme LambdaRecEx{A() -> set,G(set,set) -> set}: ex f being Function st dom f = omega & f.0 = A() & for n being Nat holds f.succ n = G(n,f.n) proof deffunc D(set,set) = 0; consider L being Sequence such that A1: dom L = omega and A2: 0 in omega implies L.0 = A() and A3: for A being Ordinal st succ A in omega holds L.(succ A) = G(A,L.A) and for A being Ordinal st A in omega & A <> 0 & A is limit_ordinal holds L.A = D(A,L|A) from TSExist1; take L; thus dom L = omega by A1; 0 in omega by ORDINAL1:def 12; hence L.0 = A() by A2; let n be Nat; succ n in omega by ORDINAL1:def 12; hence thesis by A3; end; reserve n for Nat; scheme RecUn{A() -> set, F, G() -> Function, P[set,set,set]}: F() = G() provided A1: dom F() = omega and A2: F().0 = A() and A3: for n holds P[n,F().n,F().(succ n)] and A4: dom G() = omega and A5: G().0 = A() and A6: for n holds P[n,G().n,G().(succ n)] and A7: for n for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1 = y2 proof defpred P[Nat] means F().\$1 = G().\$1; A8: for n st P[n] holds P[succ n] proof let n; assume F().n = G().n; then A9: P[n,F().n,G().(succ n)] by A6; P[n,F().n,F().(succ n)] by A3; hence thesis by A7,A9; end; A10: P[0] by A2,A5; for n holds P[n] proof let n; thus thesis from OmegaInd(A10,A8); end; then for x being object st x in omega holds F().x = G().x; hence thesis by A1,A4,FUNCT_1:2; end; scheme LambdaRecUn{A() -> set, F(set,set) -> set, F, G() -> Function}: F() = G() provided A1: dom F() = omega and A2: F().0 = A() and A3: for n holds F().(succ n) = F(n,F().n) and A4: dom G() = omega and A5: G().0 = A() and A6: for n holds G().(succ n) = F(n,G().n) proof defpred P[Nat,set,set] means \$3=F(\$1,\$2); A7: for n holds P[n,G().n,G().(succ n)] by A6; A8: for n being Nat,x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1=y2; A9: for n holds P[n,F().n,F().(succ n)] by A3; thus F() = G() from RecUn(A1,A2,A9,A4,A5,A7,A8); end;