### The Mizar article:

### The Ordinal Numbers

**by****Grzegorz Bancerek**

- Received March 20, 1989
Copyright (c) 1989 Association of Mizar Users

- MML identifier: ORDINAL1
- [ MML identifier index ]

environ vocabulary BOOLE, ZFMISC_1, TARSKI, FUNCT_1, RELAT_1, ORDINAL1, HAHNBAN, ARYTM; notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, RELAT_1, FUNCT_1; constructors TARSKI, ENUMSET1, FUNCT_1, SUBSET_1, XBOOLE_0; clusters FUNCT_1, RELAT_1, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1; theorems TARSKI, XBOOLE_0, FUNCT_1, ZFMISC_1, ENUMSET1, RELAT_1, XBOOLE_1; schemes XBOOLE_0, FUNCT_1; begin :: :: 1. Some consequences of regularity axiom (TARSKI:7) :: reserve X,Y,Z,X1,X2,X3,X4,X5,X6,x,y for set; canceled 2; theorem Th3: not ( X in Y & Y in Z & Z in X) proof A1: X in { X,Y,Z } & Y in { X,Y,Z } & Z in { X,Y,Z } by ENUMSET1:14; then consider T being set such that A2: T in { X,Y,Z } and A3: not ex x st x in { X,Y,Z } & x in T by TARSKI:7; T = X or T = Y or T = Z by A2,ENUMSET1:13; hence thesis by A1,A3; end; theorem not ( X1 in X2 & X2 in X3 & X3 in X4 & X4 in X1) proof A1: X1 in { X1,X2,X3,X4 } & X2 in { X1,X2,X3,X4 } & X3 in { X1,X2,X3,X4 } & X4 in { X1,X2,X3,X4 } by ENUMSET1:19; then consider T being set such that A2: T in { X1,X2,X3,X4 } and A3: not ex x st x in { X1,X2,X3,X4 } & x in T by TARSKI:7; T = X1 or T = X2 or T = X3 or T = X4 by A2,ENUMSET1:18; hence thesis by A1,A3; end; theorem not ( X1 in X2 & X2 in X3 & X3 in X4 & X4 in X5 & X5 in X1) proof assume A1: X1 in X2 & X2 in X3 & X3 in X4 & X4 in X5 & X5 in X1; set Z = { X1,X2,X3,X4,X5 }; A2: X1 in { X1,X2,X3,X4,X5 } by ENUMSET1:24; for Y st Y in Z ex y st y in Z & y in Y proof let Y such that A3: Y in Z; A4: Y in { X1,X2,X3,X4,X5 } implies Y = X1 or Y = X2 or Y = X3 or Y = X4 or Y = X5 by ENUMSET1:23; now per cases by A3,A4; suppose A5: Y = X1; take y = X5; thus y in Z & y in Y by A1,A5,ENUMSET1:24; suppose A6: Y = X2; take y = X1; thus y in Z & y in Y by A1,A6,ENUMSET1:24; suppose A7: Y = X3; take y = X2; thus y in Z & y in Y by A1,A7,ENUMSET1:24; suppose A8: Y = X4; take y = X3; thus y in Z & y in Y by A1,A8,ENUMSET1:24; suppose A9: Y = X5; take y = X4; thus y in Z & y in Y by A1,A9,ENUMSET1:24; end; hence thesis; end; hence contradiction by A2,TARSKI:7; end; theorem not ( X1 in X2 & X2 in X3 & X3 in X4 & X4 in X5 & X5 in X6 & X6 in X1) proof assume A1: X1 in X2 & X2 in X3 & X3 in X4 & X4 in X5 & X5 in X6 & X6 in X1; set Z = { X1,X2,X3,X4,X5,X6 }; A2: X1 in { X1,X2,X3,X4,X5,X6 } by ENUMSET1:29; for Y st Y in Z ex y st y in Z & y in Y proof let Y such that A3: Y in Z; A4: Y in { X1,X2,X3,X4,X5,X6 } implies Y = X1 or Y = X2 or Y = X3 or Y = X4 or Y = X5 or Y = X6 by ENUMSET1:28; now per cases by A3,A4; suppose A5: Y = X1; take y = X6; thus y in Z & y in Y by A1,A5,ENUMSET1:29; suppose A6: Y = X2; take y = X1; thus y in Z & y in Y by A1,A6,ENUMSET1:29; suppose A7: Y = X3; take y = X2; thus y in Z & y in Y by A1,A7,ENUMSET1:29; suppose A8: Y = X4; take y = X3; thus y in Z & y in Y by A1,A8,ENUMSET1:29; suppose A9: Y = X5; take y = X4; thus y in Z & y in Y by A1,A9,ENUMSET1:29; suppose A10: Y = X6; take y = X5; thus y in Z & y in Y by A1,A10,ENUMSET1:29; end; hence thesis; end; hence contradiction by A2,TARSKI:7; end; theorem Th7: Y in X implies not X c= Y proof assume A1: Y in X; assume X c= Y; then Y in Y by A1; hence contradiction; end; definition let X; func succ X -> set equals :Def1: X \/ { X }; coherence; end; definition let X; cluster succ X -> non empty; coherence proof succ X = X \/ { X } & X in { X } by Def1,TARSKI:def 1; hence thesis by XBOOLE_0:def 2; end; end; canceled 2; theorem Th10: X in succ X proof X in { X } by TARSKI:def 1; then X in X \/ { X } by XBOOLE_0:def 2; hence X in succ X by Def1; end; canceled; theorem succ X = succ Y implies X = Y proof assume that A1: succ X = succ Y and A2: X <> Y; X in succ X by Th10; then X in Y \/ { Y } by A1,Def1; then A3: X in Y or X in { Y } by XBOOLE_0:def 2; Y in succ Y by Th10; then Y in X \/ { X } by A1,Def1; then Y in X or Y in { X } by XBOOLE_0:def 2; hence contradiction by A2,A3,TARSKI:def 1; end; theorem x in succ X iff x in X or x = X proof thus x in succ X implies x in X or x = X proof assume x in succ X; then x in X \/ { X } by Def1; then x in X or x in { X } by XBOOLE_0:def 2; hence thesis by TARSKI:def 1; end; assume x in X or x = X; then x in X or x in { X } by TARSKI:def 1; then x in X \/ { X } by XBOOLE_0:def 2; hence thesis by Def1; end; theorem Th14: X <> succ X proof assume A1: X = succ X; X in succ X by Th10; hence contradiction by A1; end; :: :: 3. epsilon-transitivity & epsilon-connectedness :: reserve a,b,c,X,Y,Z,x,y,z for set; definition let X; attr X is epsilon-transitive means :Def2: for x st x in X holds x c= X; attr X is epsilon-connected means :Def3: for x,y st x in X & y in X holds x in y or x = y or y in x; end; Lm1: {} is epsilon-transitive & {} is epsilon-connected proof thus x in {} implies x c= {}; thus x in {} & y in {} implies x in y or x = y or y in x; end; :: :: 4. Definition of ordinal numbers - Ordinal :: definition let IT be set; attr IT is ordinal means :Def4: IT is epsilon-transitive epsilon-connected; end; definition cluster ordinal -> epsilon-transitive epsilon-connected set; coherence by Def4; cluster epsilon-transitive epsilon-connected -> ordinal set; coherence by Def4; end; definition redefine mode set; synonym number; end; definition cluster ordinal number; existence proof take {}; thus thesis by Def4,Lm1; end; end; definition mode Ordinal is ordinal number; end; reserve A,B,C,D for Ordinal; canceled 4; theorem Th19: for A being epsilon-transitive set st A in B & B in C holds A in C proof let A be epsilon-transitive set; assume A1: A in B & B in C; then B c= C by Def2; hence A in C by A1; end; canceled; theorem Th21: for x being epsilon-transitive set, A being Ordinal st x c< A holds x in A proof let x be epsilon-transitive set, A be Ordinal; assume A1: x c< A; then A2: x c= A by XBOOLE_0:def 8; consider a being Element of A \ x; A \ x <> {} proof assume A \ x = {}; then A c= x by XBOOLE_1:37; hence contradiction by A1,XBOOLE_1:60; end; then a in A \ x; then consider y such that A3: y in A \ x and A4: not ex a st a in A \ x & a in y by TARSKI:7; A5: y in A & not y in x by A3,XBOOLE_0:def 4; then A6: y c= A by Def2; now let a; assume A7: a in y; then not a in A \ x by A4; hence a in x by A6,A7,XBOOLE_0:def 4; end; then A8: y c= x by TARSKI:def 3; now let a; assume a in x; then consider z such that A9: z = a & z in x; z c= x by A9,Def2; then not y in z by A3,XBOOLE_0:def 4; hence a in y by A2,A5,A9,Def3; end; then x c= y by TARSKI:def 3; hence thesis by A5,A8,XBOOLE_0:def 10; end; theorem for A being epsilon-transitive set, B, C being Ordinal st A c= B & B in C holds A in C proof let A be epsilon-transitive set, B, C be Ordinal; assume A1: A c= B & B in C; then B c= C by Def2; then A c= C & A <> C by A1,Th7,XBOOLE_1:1; then A c< C by XBOOLE_0:def 8; hence thesis by Th21; end; theorem Th23: a in A implies a is Ordinal proof assume A1: a in A; then A2: a c= A by Def2; then for y,z st y in a & z in a holds y in z or y = z or z in y by Def3; then A3: a is epsilon-connected by Def3; now let y; assume A4: y in a; assume not y c= a; then consider b such that A5: b in y & not b in a by TARSKI:def 3; b in y \ a by A5,XBOOLE_0:def 4; then consider z such that A6: z in y \ a & not ex c st c in y \ a & c in z by TARSKI:7; A7: z in y & not z in a by A6,XBOOLE_0:def 4; y c= A by A2,A4,Def2; then z in a or z = a or a in z by A1,A7,Def3; hence contradiction by A4,A7,Th3; end; then a is epsilon-transitive by Def2; hence thesis by A3,Def4; end; theorem Th24: A in B or A = B or B in A proof assume A1: not A in B & A <> B; then not A c< B by Th21; then not A c= B by A1,XBOOLE_0:def 8; then consider a such that A2: a in A & not a in B by TARSKI:def 3; a in A \ B by A2,XBOOLE_0:def 4; then consider X such that A3: X in A \ B & not ex a st a in A \ B & a in X by TARSKI:7; A4: X in A & not X in B by A3,XBOOLE_0:def 4; then A5: X c= A by Def2; A6: X is Ordinal by A4,Th23; now let b; assume A7: b in X; then not b in A \ B by A3; hence b in B by A5,A7,XBOOLE_0:def 4; end; then X c= B by TARSKI:def 3; then X c< B or X = B by XBOOLE_0:def 8; hence thesis by A4,A6,Th21; end; definition let A,B; redefine pred A c= B; connectedness proof let A,B; A in B or A = B or B in A by Th24; hence thesis by Def2; end; end; theorem A,B are_c=-comparable proof A c= B or B c= A; hence thesis by XBOOLE_0:def 9; end; theorem Th26: A c= B or B in A proof A in B or A = B or B in A by Th24; hence thesis by Def2; end; theorem Th27: {} is Ordinal by Def4,Lm1; definition cluster empty Ordinal; existence by Th27; end; definition cluster empty -> ordinal number; coherence by Def4,Lm1; end; definition cluster {} -> ordinal; coherence; end; canceled; theorem Th29: x is Ordinal implies succ x is Ordinal proof assume A1: x is Ordinal; A2: succ x = x \/ { x } by Def1; A3: now let y; assume A4: y in succ x; y in { x } implies y = x by TARSKI:def 1; hence y in x or y = x by A2,A4,XBOOLE_0:def 2; end; now let y; assume A5: y in succ x; A6: now assume y in x; then A7: y c= x by A1,Def2; x c= x \/ { x } by XBOOLE_1:7; hence y c= succ x by A2,A7,XBOOLE_1:1; end; y = x implies y c= succ x by A2,XBOOLE_1:7; hence y c= succ x by A3,A5,A6; end; then A8: succ x is epsilon-transitive by Def2; now let y,z; assume A9: y in succ x & z in succ x; then A10: y in x or y = x by A3; z in x or z = x by A3,A9; hence y in z or y = z or z in y by A1,A10,Def3; end; then succ x is epsilon-connected by Def3; hence thesis by A8,Def4; end; theorem Th30: x is ordinal implies union x is ordinal proof assume x is epsilon-transitive & x is epsilon-connected; then reconsider A = x as Ordinal by Def4; thus y in union x implies y c= union x proof assume y in union x; then consider z such that A1: y in z & z in x by TARSKI:def 4; z in A by A1; then reconsider z as Ordinal by Th23; z c= A by A1,Def2; hence thesis by A1,ZFMISC_1:92; end; let y,z; assume A2: y in union x & z in union x; then consider X such that A3: y in X & X in x by TARSKI:def 4; consider Y such that A4: z in Y & Y in x by A2,TARSKI:def 4; X in A & Y in A by A3,A4; then reconsider X,Y as Ordinal by Th23; y in X & z in Y by A3,A4; then y is Ordinal & z is Ordinal by Th23; hence thesis by Th24; end; definition cluster non empty Ordinal; existence proof reconsider A = succ {} as Ordinal by Th29; take A; thus thesis; end; end; definition let A; cluster succ A -> non empty ordinal; coherence by Th29; cluster union A -> ordinal; coherence by Th30; end; theorem (for x st x in X holds x is Ordinal & x c= X) implies X is ordinal proof assume A1: for x st x in X holds x is Ordinal & x c= X; thus X is epsilon-transitive proof let x; assume x in X; hence x c= X by A1; end; let x,y; assume x in X & y in X; then x is Ordinal & y is Ordinal by A1; hence x in y or x = y or y in x by Th24; end; theorem Th32: X c= A & X <> {} implies ex C st C in X & for B st B in X holds C c= B proof consider a being Element of X; assume A1: X c= A & X <> {}; then a in X; then consider Y such that A2: Y in X & not ex a st a in X & a in Y by TARSKI:7; Y is Ordinal by A1,A2,Th23; then consider C such that A3: C = Y; take C; thus C in X by A2,A3; let B; assume B in X; then not B in C by A2,A3; then B = C or C in B by Th24; hence C c= B by Def2; end; theorem Th33: A in B iff succ A c= B proof thus A in B implies succ A c= B proof assume A1: A in B; then A2: A c= B by Def2; a in { A } implies a in B by A1,TARSKI:def 1; then { A } c= B by TARSKI:def 3; then A \/ { A } c= B by A2,XBOOLE_1:8; hence thesis by Def1; end; assume A3: succ A c= B; A in succ A by Th10; hence thesis by A3; end; theorem Th34: A in succ C iff A c= C proof thus A in succ C implies A c= C proof assume A in succ C; then A in C \/ { C } by Def1; then A in C or A in { C } by XBOOLE_0:def 2; hence thesis by Def2,TARSKI:def 1; end; assume A1: A c= C; assume not A in succ C; then A2: A = succ C or succ C in A by Th24; C in succ C by Th10; then A3: C c= succ C by Def2; succ C c= C by A1,A2,Def2; then succ C = C by A3,XBOOLE_0:def 10; hence contradiction by Th14; end; :: :: 6. Transfinite induction and principle of minimum of ordinals :: scheme Ordinal_Min { P[Ordinal] } : ex A st P[A] & for B st P[B] holds A c= B provided A1: ex A st P[A] proof consider A such that A2: P[A] by A1; defpred R[set] means ex B st $1 = B & P[B]; consider X such that A3: x in X iff x in succ A & R[x] from Separation; A in succ A by Th10; then A4: X <> {} by A2,A3; for a holds a in X implies a in succ A by A3; then X c= succ A by TARSKI:def 3; then consider C such that A5: C in X & for B st B in X holds C c= B by A4,Th32; take C; ex B st C = B & P[B] by A3,A5; hence P[C]; let B; assume A6: P[B]; assume A7: not C c= B; then B c= C & B <> C; then B c< C by XBOOLE_0:def 8; then A8: B in C by Th21; C in succ A by A3,A5; then C c= succ A by Def2; then B in X by A3,A6,A8; hence contradiction by A5,A7; end; scheme Transfinite_Ind { P[Ordinal] } : for A holds P[A] provided A1: for A st for C st C in A holds P[C] holds P[A] proof let A; set Y = succ A; defpred R[set] means ex B st $1 = B & P[B]; consider Z such that A2: x in Z iff x in Y & R[x] from Separation; A3: Y \ Z c= Y by XBOOLE_1:36; now assume Y \ Z <> {}; then consider C such that A4: C in Y \ Z & for B st B in Y \ Z holds C c= B by A3,Th32; A5: C in Y & not C in Z by A4,XBOOLE_0:def 4; now let B such that A6: B in C; A7: C c= Y by A5,Def2; now assume not B in Z; then B in Y \ Z by A6,A7,XBOOLE_0:def 4; then A8: C c= B by A4; C <> B by A6; then C c< B by A8,XBOOLE_0:def 8; hence contradiction by A6,Th21; end; then ex B' being Ordinal st B = B' & P[B'] by A2; hence P[B]; end; then P[C] by A1; hence contradiction by A2,A5; end; then not A in Y or A in Z by XBOOLE_0:def 4; then ex B st A = B & P[B] by A2,Th10; hence thesis; end; :: :: 7. Properties of sets of ordinals :: theorem Th35: for X st for a st a in X holds a is Ordinal holds union X is ordinal proof let X such that A1: for a st a in X holds a is Ordinal; thus union X is epsilon-transitive proof let x; assume x in union X; then consider Y such that A2: x in Y & Y in X by TARSKI:def 4; Y is Ordinal by A1,A2; then A3: x c= Y by A2,Def2; let a; assume a in x; hence a in union X by A2,A3,TARSKI:def 4; end; let x,y; assume A4: x in union X & y in union X; then consider Y such that A5: x in Y & Y in X by TARSKI:def 4; consider Z such that A6: y in Z & Z in X by A4,TARSKI:def 4; Y is Ordinal & Z is Ordinal by A1,A5,A6; then x is Ordinal & y is Ordinal by A5,A6,Th23; hence thesis by Th24; end; theorem Th36: for X st for a st a in X holds a is Ordinal ex A st X c= A proof let X; assume A1: for a st a in X holds a is Ordinal; then A2: union X is Ordinal by Th35; then reconsider A = succ(union X) as Ordinal by Th29; take A; let a; assume A3: a in X; then reconsider B = a as Ordinal by A1; b in B implies b in union X by A3,TARSKI:def 4; then B c= union X by TARSKI:def 3; hence thesis by A2,Th34; end; theorem Th37: not ex X st for x holds x in X iff x is Ordinal proof given X such that A1: for x holds x in X iff x is Ordinal; A2: X is epsilon-transitive proof let x; assume x in X; then A3: x is Ordinal by A1; thus thesis proof let a; assume a in x; then a is Ordinal by A3,Th23; hence thesis by A1; end; end; X is epsilon-connected proof let x,y; assume x in X & y in X; then x is Ordinal & y is Ordinal by A1; hence thesis by Th24; end; then X is Ordinal by A2,Def4; then X in X by A1; hence contradiction; end; theorem Th38: not ex X st for A holds A in X proof given X such that A1: A in X; defpred P[set] means $1 is Ordinal; consider Y such that A2: a in Y iff a in X & P[a] from Separation; now let x; assume A3: x is Ordinal; then x in X by A1; hence x in Y by A2,A3; end; then x in Y iff x is Ordinal by A2; hence contradiction by Th37; end; theorem for X ex A st not A in X & for B st not B in X holds A c= B proof let X; consider B such that A1: not B in X by Th38; defpred P[set] means not $1 in X; consider Y such that A2: a in Y iff a in succ B & P[a] from Separation; for a holds a in Y implies a in succ B by A2; then A3: Y c= succ B by TARSKI:def 3; B in succ B by Th10; then Y <> {} by A1,A2; then consider A such that A4: A in Y & for B st B in Y holds A c= B by A3,Th32; take A; thus not A in X by A2,A4; let C; assume A5: not C in X; assume A6: not A c= C; then not A in C by Def2; then A7: C in A by A6,Th24; A in succ B by A2,A4; then A c= succ B by Def2; then C in Y by A2,A5,A7; hence contradiction by A4,A6; end; :: :: 8. Limit ordinals :: definition let A be set; canceled; attr A is being_limit_ordinal means :Def6: A = union A; synonym A is_limit_ordinal; end; canceled; theorem Th41: for A holds A is_limit_ordinal iff for C st C in A holds succ C in A proof let A; thus A is_limit_ordinal implies for C st C in A holds succ C in A proof assume A is_limit_ordinal; then A1: A = union A by Def6; let C; assume C in A; then consider z such that A2: C in z & z in A by A1,TARSKI:def 4; for b holds b in { C } implies b in z by A2,TARSKI:def 1; then A3: { C } c= z by TARSKI:def 3; A4: z is Ordinal by A2,Th23; then C c= z by A2,Def2; then C \/ { C } c= z by A3,XBOOLE_1:8; then succ C c= z by Def1; then succ C = z or succ C c< z by XBOOLE_0:def 8; then A5: succ C = z or succ C in z by A4,Th21; z c= A by A2,Def2; hence thesis by A2,A5; end; assume A6: for C st C in A holds succ C in A; now let a; assume A7: a in A; then a is Ordinal by Th23; then A8: succ a in A by A6,A7; a in succ a by Th10; hence a in union A by A8,TARSKI:def 4; end; then A9: A c= union A by TARSKI:def 3; now let a; assume a in union A; then consider z such that A10: a in z & z in A by TARSKI:def 4; z c= A by A10,Def2; hence a in A by A10; end; then union A c= A by TARSKI:def 3; then A = union A by A9,XBOOLE_0:def 10; hence thesis by Def6; end; theorem not A is_limit_ordinal iff ex B st A = succ B proof thus not A is_limit_ordinal implies ex B st A = succ B proof assume not A is_limit_ordinal; then consider B such that A1: B in A & not succ B in A by Th41; take B; assume A2: A <> succ B; succ B c= A by A1,Th33; then succ B c< A by A2,XBOOLE_0:def 8; hence contradiction by A1,Th21; end; given B such that A3: A = succ B; A4: B in A by A3,Th10; not succ B in A by A3; hence not A is_limit_ordinal by A4,Th41; end; reserve F,G for Function; :: :: 9. Transfinite sequences :: definition let IT be Function; attr IT is T-Sequence-like means :Def7: dom IT is ordinal; end; definition cluster T-Sequence-like Function; existence proof reconsider E = {} as empty Function; take E; dom E = E; hence thesis by Def7; end; end; definition mode T-Sequence is T-Sequence-like Function; end; definition let Z; mode T-Sequence of Z -> T-Sequence means :Def8: rng it c= Z; existence proof dom {} = {}; then reconsider L = {} as T-Sequence by Def7; take L; rng {} = {}; hence rng L c= Z by XBOOLE_1:2; end; end; canceled 2; theorem {} is T-Sequence of Z proof reconsider F = {} as Function; A1: now consider a being Element of dom F; assume dom F <> {}; then ex b st [a,b] in F by RELAT_1:def 4; hence contradiction; end; then reconsider L = F as T-Sequence by Def7; rng L = {} by A1,RELAT_1:65; then rng L c= Z by XBOOLE_1:2; hence {} is T-Sequence of Z by Def8; end; reserve L,L1 for T-Sequence; theorem dom F is Ordinal implies F is T-Sequence of rng F proof assume dom F is Ordinal; then F is T-Sequence by Def7; hence thesis by Def8; end; definition let L; cluster dom L -> ordinal; coherence by Def7; end; theorem Th47: X c= Y implies for L being T-Sequence of X holds L is T-Sequence of Y proof assume A1: X c= Y; let L be T-Sequence of X; rng L c= X by Def8; hence rng L c= Y by A1,XBOOLE_1:1; end; definition let L,A; redefine func L|A -> T-Sequence of rng L; coherence proof A1: A c= dom L implies dom(L|A) = A by RELAT_1:91; dom L c= A implies dom(L|A) = dom L by RELAT_1:97; then L|A is T-Sequence & rng(L|A) c= rng L by A1,Def7,FUNCT_1:76; hence thesis by Def8; end; end; theorem for L being T-Sequence of X for A holds L|A is T-Sequence of X proof let L be T-Sequence of X; let A; rng L c= X by Def8; hence L|A is T-Sequence of X by Th47; end; definition let IT be set; attr IT is c=-linear means :Def9: for x,y being set st x in IT & y in IT holds x,y are_c=-comparable; end; theorem (for a st a in X holds a is T-Sequence) & X is c=-linear implies union X is T-Sequence proof assume that A1: for a st a in X holds a is T-Sequence and A2: X is c=-linear; union X is Relation-like Function-like proof thus a in union X implies ex b,c st [b,c] = a proof assume a in union X; then consider x such that A3: a in x & x in X by TARSKI:def 4; reconsider x as T-Sequence by A1,A3; x = x & for a st a in x holds ex b,c st [b,c] = a by RELAT_1:def 1; hence ex b,c st [b,c] = a by A3; end; let a,b,c; assume A4: [a,b] in union X & [a,c] in union X; then consider x such that A5: [a,b] in x & x in X by TARSKI:def 4; consider y such that A6: [a,c] in y & y in X by A4,TARSKI:def 4; reconsider x as T-Sequence by A1,A5; reconsider y as T-Sequence by A1,A6; x,y are_c=-comparable by A2,A5,A6,Def9; then x c= y or y c= x by XBOOLE_0:def 9; hence b = c by A5,A6,FUNCT_1:def 1; end; then reconsider F = union X as Function; defpred P[set,set] means $1 in X & for L st L = $1 holds dom L = $2; A7: for a,b,c st P[a,b] & P[a,c] holds b = c proof let a,b,c; assume A8: ( a in X & for L st L = a holds dom L = b ) & a in X & for L st L = a holds dom L = c; then reconsider a as T-Sequence by A1; dom a = b & dom a = c by A8; hence b = c; end; consider G such that A9: [a,b] in G iff a in X & P[a,b] from GraphFunc(A7); A10: [a,b] in G implies b is Ordinal proof assume A11: [a,b] in G; then a in X & for L st L = a holds dom L = b by A9; then reconsider a as T-Sequence by A1; dom a = b by A9,A11; hence b is Ordinal; end; a in rng G implies a is Ordinal proof assume a in rng G; then consider b such that A12: b in dom G & a = G.b by FUNCT_1:def 5; [b,a] in G by A12,FUNCT_1:8; hence thesis by A10; end; then consider A such that A13: rng G c= A by Th36; defpred P[Ordinal] means for B st B in rng G holds B c= $1; for B st B in rng G holds B c= A by A13,Def2; then A14: ex A st P[A]; consider A such that A15: P[A] & for C st P[C] holds A c= C from Ordinal_Min(A14); F is T-Sequence-like proof dom F = A proof thus a in dom F implies a in A proof assume a in dom F; then consider b such that A16: [a,b] in F by RELAT_1:def 4; consider x such that A17: [a,b] in x & x in X by A16,TARSKI:def 4; reconsider x as T-Sequence by A1,A17; A18: a in dom x by A17,RELAT_1:def 4; for L st L = x holds dom L = dom x; then [x,dom x] in G by A9,A17; then x in dom G & dom x = G.x by FUNCT_1:8; then dom x in rng G by FUNCT_1:def 5; then dom x c= A by A15; hence a in A by A18; end; let a; assume A19: a in A; then reconsider a' = a as Ordinal by Th23; now assume A20: for L st L in X holds not a' in dom L; A21: now let L; assume L in X; then not a' in dom L by A20; hence dom L c= a' by Th26; end; now let B; assume B in rng G; then consider c such that A22: c in dom G & B = G.c by FUNCT_1:def 5; A23: [c,B] in G by A22,FUNCT_1:8; then c in X by A9; then reconsider c as T-Sequence by A1; c in X & dom c = B by A9,A23; hence B c= a' by A21; end; then A24: A c= a' by A15; a' c= A by A19,Def2; then A = a by A24,XBOOLE_0:def 10; hence contradiction by A19; end; then consider L such that A25: L in X & a in dom L; A26: L c= F by A25,ZFMISC_1:92; consider b such that A27: [a,b] in L by A25,RELAT_1:def 4; thus a in dom F by A26,A27,RELAT_1:def 4; end; hence dom F is ordinal; end; hence thesis; end; :: :: 10. Schemes of definability by transfinite induction :: scheme TS_Uniq { A()->Ordinal, H(T-Sequence)->set, L1, L2() -> T-Sequence } : L1() = L2() provided A1: dom L1() = A() & for B,L st B in A() & L = L1()|B holds L1().B = H(L) and A2: dom L2() = A() & for B,L st B in A() & L = L2()|B holds L2().B = H(L) proof assume L1() <> L2(); then consider a such that A3: a in A() & L1().a <> L2().a by A1,A2,FUNCT_1:9; defpred P[set] means L1().$1 <> L2().$1; consider X such that A4: x in X iff x in A() & P[x] from Separation; A5: X <> {} by A3,A4; for b holds b in X implies b in A() by A4; then X c= A() by TARSKI:def 3; then consider B such that A6: B in X & for C st C in X holds B c= C by A5,Th32; A7: B in A() & L1().B <> L2().B by A4,A6; then A8: B c= A() by Def2; A9: now let C; assume A10: C in B; then not B c= C by Th7; then not C in X by A6; hence L1().C = L2().C by A4,A8,A10; end; A11: dom(L1()|B) = B & dom(L2()|B) = B by A1,A2,A8,RELAT_1:91; now let a; assume A12: a in B; then reconsider a' = a as Ordinal by Th23; A13: L1().a' = L2().a' by A9,A12; L1()|B.a = L1().a & L2()|B.a = L2().a by A11,A12,FUNCT_1:70; hence L1()|B.a = L2()|B.a by A13; end; then A14: L1()|B = L2()|B by A11,FUNCT_1:9; L1().B = H(L1()|B) & L2().B = H(L2()|B) by A1,A2,A7; hence contradiction by A4,A6,A14; end; scheme TS_Exist { A()->Ordinal,H(T-Sequence)->set } : ex L st dom L = A() & for B,L1 st B in A() & L1 = L|B holds L.B = H(L1) proof defpred S[Ordinal] means ex L st dom L = $1 & for B st B in $1 holds L.B = H(L|B); A1: for B st for C st C in B holds S[C] holds S[B] proof let B such that A2: for C st C in B ex L st dom L = C & for D st D in C holds L.D = H(L|D); defpred P[set,set] means $1 is Ordinal & $2 is T-Sequence & for A,L st A = $1 & L = $2 holds dom L = A & for B st B in A holds L.B = H(L|B); A3: for a,b,c st P[a,b] & P[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 dom L = A & for B st B in A holds L.B = H(L|B) ) & ( a is Ordinal & c is T-Sequence & for A,L st A = a & L = c holds dom L = A & for B st B in A holds L.B = H(L|B) ); then reconsider a as Ordinal; reconsider b as T-Sequence by A4; reconsider c as T-Sequence by A4; deffunc HH(Ordinal) = H($1); A5: dom b = a & for B,L st B in a & L=b|B holds b.B = HH(L) by A4; A6: dom c = a & for B,L st B in a & L=c|B holds c.B = HH(L) by A4; b = c from TS_Uniq(A5,A6); hence thesis; end; consider G such that A7: [a,b] in G iff a in B & P[a,b] from GraphFunc(A3); A8: 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 A7; end; let a; assume A9: a in B; then reconsider a' = a as Ordinal by Th23; consider L such that A10: dom L = a' & for D st D in a' holds L.D = H(L|D) by A2,A9; for A holds for K be T-Sequence holds A = a' & K = L implies dom K = A & for B holds B in A implies K.B = H(K|B) by A10; then [a',L] in G by A7,A9; hence a in dom G by RELAT_1:def 4; end; defpred R[Ordinal,Ordinal] means ex L st L = G.$1 & $2 = H(L); A11: for a,b,c st a in B & R[a,b] & R[a,c] holds b = c; A12: for a st a in B ex b st R[a,b] proof let a; assume a in B; then consider c such that A13: [a,c] in G by A8,RELAT_1:def 4; reconsider L = c as T-Sequence by A7,A13; take b = H(L), L; thus L = G.a by A13,FUNCT_1:8; thus b = H(L); end; consider F such that A14: dom F = B & for a st a in B holds R[a,F.a] from FuncEx(A11,A12); reconsider L = F as T-Sequence by A14,Def7; take L; thus dom L = B by A14; let D; assume A15: D in B; then consider K being T-Sequence such that A16: K = G.D & F.D = H(K) by A14; D c= dom L by A14,A15,Def2; then A17: dom(L|D) = D by RELAT_1:91; A18: [D,K] in G by A8,A15,A16,FUNCT_1:8; then A19: dom K = D & for B st B in D holds K.B = H(K|B) by A7; A20: now let C; assume A21: C in D; then A22: C in B by A15,Th19; now let A,L such that A23: A = C & L = K|C; A24: C c= D by A21,Def2; hence A25: dom L = A by A19,A23,RELAT_1:91; let B; assume A26: B in A; then B in D & B c= A by A23,A24,Def2; then K.B = H(K|B) & K|B = L|B by A7,A18,A23,FUNCT_1:82; hence L.B = H(L|B) by A23,A25,A26,FUNCT_1:70; end; then [C,K|C] in G by A7,A22; hence G.C = K|C by FUNCT_1:8; end; now let a; assume A27: a in D; then reconsider A = a as Ordinal by Th23; A28: G.A = K|A by A20,A27; A29: A in B by A15,A27,Th19; A30: L|D.A = L.A by A27,FUNCT_1:72; ex J being T-Sequence st J = G.A & F.A = H(J) by A14,A29; hence L|D.a = K.a by A7,A18,A27,A28,A30; end; hence L.D = H(L|D) by A16,A17,A19,FUNCT_1:9; end; for A holds S[A] from Transfinite_Ind(A1); then consider L such that A31: dom L = A() & for B st B in A() holds L.B = H(L|B); take L; thus dom L = A() by A31; let B,L1; assume B in A() & L1 = L|B; hence thesis by A31; end; scheme Func_TS { L() -> T-Sequence, F(Ordinal)->set, H(T-Sequence)->set } : for B st B in dom L() holds L().B = H(L()|B) provided A1: for A,a holds a = F(A) iff ex L st a = H(L) & dom L = A & for B st B in A holds L.B = H(L|B) and A2: for A st A in dom L() holds L().A = F(A) proof consider L such that F(dom L()) = H(L) and A3: dom L = dom L() and A4: for B st B in dom L() holds L.B = H(L|B) by A1; now let b; assume A5: b in dom L; then reconsider B = b as Ordinal by Th23; now take K = L|B; thus H(L|B) = H(K); A6: B c= dom L by A5,Def2; hence dom K = B by RELAT_1:91; let C; assume A7: C in B; then C in dom L() & C c= B by A3,A6,Def2; then K.C = L.C & L|C = K|C by A7,FUNCT_1:72,82; hence K.C = H(K|C) by A3,A4,A6,A7; end; then F(B) = H(L|B) by A1 .= L.B by A3,A4,A5; hence L().b = L.b by A2,A3,A5; end; then L() = L by A3,FUNCT_1:9; hence thesis by A4; end; theorem A c< B or A = B or B c< A proof assume not(A c< B or A = B or B c< A); then not(A c= B or B c= A) by XBOOLE_0:def 8; hence contradiction; end;

Back to top