Copyright (c) 1990 Association of Mizar Users
environ vocabulary CARD_1, ORDINAL1, FUNCT_1, CLASSES1, TARSKI, BOOLE, RELAT_1, ORDINAL2, CARD_3, FUNCT_2, PROB_1, RLVECT_1, ZF_LANG, ZFMISC_1, SETFAM_1, FINSET_1, CLASSES2, HAHNBAN; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NAT_1, WELLORD2, FINSET_1, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, ORDINAL1, ORDINAL2, CARD_1, CLASSES1, PROB_1, CARD_3; constructors WELLORD2, PROB_1, CLASSES1, CARD_3, XCMPLX_0, MEMBERED, PARTFUN1, RELAT_2, XBOOLE_0; clusters ORDINAL1, CARD_1, CLASSES1, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, FUNCT_2, PARTFUN1, XBOOLE_0, ORDINAL2; requirements SUBSET, BOOLE; definitions TARSKI, ORDINAL1, CLASSES1, XBOOLE_0; theorems TARSKI, ZFMISC_1, SETFAM_1, ORDINAL1, WELLORD2, ORDINAL2, ORDINAL3, FUNCT_1, FUNCT_2, CARD_1, CLASSES1, CARD_2, FRAENKEL, CARD_3, RELAT_1, PROB_1, XBOOLE_0, XBOOLE_1; schemes FUNCT_1, PARTFUN1, CARD_3, ORDINAL1, ORDINAL2, XBOOLE_0; begin reserve m for Cardinal, n for Nat, A,B,C for Ordinal, x,y,z,X,Y,Z,W for set, f for Function; Lm1: Tarski-Class X is_Tarski-Class proof Tarski-Class X is_Tarski-Class_of X by CLASSES1:def 4; hence thesis by CLASSES1:def 3; end; definition cluster being_Tarski-Class -> subset-closed set; coherence by CLASSES1:def 2; end; definition let X be set; cluster Tarski-Class X -> being_Tarski-Class; coherence by Lm1; end; theorem Th1: W is subset-closed & X in W implies not X,W are_equipotent & Card X <` Card W proof assume A1: W is subset-closed; assume A2: X in W; bool X c= W proof let x; assume x in bool X; hence x in W by A1,A2,CLASSES1:def 1; end; then A3: Card X <` Card bool X & Card bool X <=` Card W by CARD_1:27,30; then Card X <` Card W; then Card X <> Card W; hence thesis by A3,CARD_1:21; end; canceled; theorem Th3: W is_Tarski-Class & x in W & y in W implies {x} in W & {x,y} in W proof assume that A1: W is_Tarski-Class and A2: x in W & y in W; A3: W is subset-closed by A1,CLASSES1:def 2; bool x in W & {x} c= bool x by A1,A2,CLASSES1:def 2,ZFMISC_1:80; hence {x} in W by A3,CLASSES1:def 1; then bool {x} in W & bool {x} = {{},{x}} by A1,CLASSES1:def 2,ZFMISC_1:30; then A4: Card {{},{x}} <` Card W by A3,Th1; defpred C[set] means $1 = {}; deffunc f(set) = y; deffunc g(set) = x; consider f such that A5: dom f = {{},{x}} & for z st z in {{},{x}} holds (C[z] implies f.z = f(z)) & (not C[z] implies f.z = g(z)) from LambdaC; {x,y} c= rng f proof let z; assume z in {x,y}; then A6: (z = x or z = y) & {} in {{},{x}} & {x} in {{},{x}} & {x} <> {} by TARSKI:def 2; then f.{} = z or f.{x} = z by A5; hence z in rng f by A5,A6,FUNCT_1:def 5; end; then Card {x,y} <=` Card {{},{x}} by A5,CARD_1:28; then A7: Card {x,y} <` Card W by A4,ORDINAL1:22; {x,y} c= W proof let z; assume z in {x,y}; hence thesis by A2,TARSKI:def 2; end; hence {x,y} in W by A1,A7,CLASSES1:2; end; theorem Th4: W is_Tarski-Class & x in W & y in W implies [x,y] in W proof assume A1: W is_Tarski-Class; assume x in W & y in W; then {x} in W & {x,y} in W & [x,y] = {{x,y},{x}} by A1,Th3,TARSKI:def 5; hence [x,y] in W by A1,Th3; end; theorem Th5: W is_Tarski-Class & X in W implies Tarski-Class X c= W proof assume A1: W is_Tarski-Class & X in W; then reconsider D = W as non empty set; D is_Tarski-Class_of X by A1,CLASSES1:def 3; hence thesis by CLASSES1:def 4; end; scheme TC {P[set]}: for X holds P[Tarski-Class X] provided A1: for X st X is_Tarski-Class holds P[X] by A1; theorem Th6: W is_Tarski-Class & A in W implies succ A in W & A c= W proof assume that A1: for X,Y st X in W & Y c= X holds Y in W and A2: for X st X in W holds bool X in W and for X st X c= W holds X,W are_equipotent or X in W and A3: A in W; bool A in W & succ A c= bool A by A2,A3,ORDINAL2:3; hence succ A in W by A1; let x; assume A4: x in A; then reconsider B = x as Ordinal by ORDINAL1:23; B c= A by A4,ORDINAL1:def 2; hence thesis by A1,A3; end; theorem A in Tarski-Class W implies succ A in Tarski-Class W & A c= Tarski-Class W by Th6; theorem Th8: W is subset-closed & X is epsilon-transitive & X in W implies X c= W proof assume that A1: for X,Y st X in W & Y c= X holds Y in W and A2: Y in X implies Y c= X and A3: X in W; let x; assume x in X; then x c= X by A2; hence thesis by A1,A3; end; theorem X is epsilon-transitive & X in Tarski-Class W implies X c= Tarski-Class W by Th8; theorem Th10: W is_Tarski-Class implies On W = Card W proof assume A1: W is_Tarski-Class; then A2: W is subset-closed by CLASSES1:def 2; now let X; assume A3: X in On W; then A4: X in W & X is Ordinal by ORDINAL2:def 2; thus X is Ordinal by A3,ORDINAL2:def 2; reconsider A = X as Ordinal by A3,ORDINAL2:def 2; thus X c= On W proof let x; assume A5: x in X; then x in A; then reconsider B = x as Ordinal by ORDINAL1:23; B c= A by A5,ORDINAL1:def 2; then B in W by A2,A4,CLASSES1:def 1; hence thesis by ORDINAL2:def 2; end; end; then reconsider ON = On W as Ordinal by ORDINAL1:31; ON c= W by ORDINAL2:9; then A6: ON,W are_equipotent or ON in W by A1,CLASSES1:def 2; A7: now assume ON in W; then ON in ON by ORDINAL2:def 2; hence contradiction; end; now let A; assume A,ON are_equipotent & not ON c= A; then A8: A,W are_equipotent & A in ON by A6,A7,ORDINAL1:26,WELLORD2:22; then A in W by ORDINAL2:def 2; hence contradiction by A2,A8,Th1; end; then reconsider ON as Cardinal by CARD_1:def 1; ON = Card ON by CARD_1:def 5; hence thesis by A6,A7,CARD_1:21; end; theorem Th11: On Tarski-Class W = Card Tarski-Class W by Th10; theorem Th12: W is_Tarski-Class & X in W implies Card X in W proof assume A1: W is_Tarski-Class & X in W; then W is subset-closed by CLASSES1:def 2; then Card X <` Card W & Card W = On W by A1,Th1,Th10; hence thesis by ORDINAL2:def 2; end; theorem X in Tarski-Class W implies Card X in Tarski-Class W by Th12; theorem Th14: W is_Tarski-Class & x in Card W implies x in W proof assume A1: W is_Tarski-Class; assume x in Card W; then x in On W by A1,Th10; hence x in W by ORDINAL2:def 2; end; theorem x in Card Tarski-Class W implies x in Tarski-Class W by Th14; theorem W is_Tarski-Class & m <` Card W implies m in W proof assume A1: W is_Tarski-Class; assume m in Card W; then m in On W by A1,Th10; hence thesis by ORDINAL2:def 2; end; theorem m <` Card Tarski-Class W implies m in Tarski-Class W proof assume m in Card Tarski-Class W; then m in On Tarski-Class W by Th11; hence thesis by ORDINAL2:def 2; end; theorem W is_Tarski-Class & m in W implies m c= W by Th6; theorem m in Tarski-Class W implies m c= Tarski-Class W by Th6; theorem Th20: W is_Tarski-Class implies Card W is_limit_ordinal proof assume A1: W is_Tarski-Class; now let A; assume A in Card W; then A in W by A1,Th14; then succ A in W by A1,Th6; then succ A in On W by ORDINAL2:def 2; hence succ A in Card W by A1,Th10; end; hence thesis by ORDINAL1:41; end; theorem Th21: W is_Tarski-Class & W <> {} implies Card W <> 0 & Card W <> {} & Card W is_limit_ordinal proof assume A1: W is_Tarski-Class & W <> {}; then A2: not W,{} are_equipotent by CARD_1:46; hence Card W <> 0 by CARD_1:21,47; thus thesis by A1,A2,Th20,CARD_1:21,47; end; theorem Th22: Card Tarski-Class W <> 0 & Card Tarski-Class W <> {} & Card Tarski-Class W is_limit_ordinal proof A1: not Tarski-Class W,{} are_equipotent by CARD_1:46; hence Card Tarski-Class W <> 0 by CARD_1:21,47; thus Card Tarski-Class W <> {} by A1,CARD_1:21,47; now let A; assume A in Card Tarski-Class W; then A in Tarski-Class W by Th14; then succ A in Tarski-Class W by Th6; then succ A in On Tarski-Class W by ORDINAL2:def 2; hence succ A in Card Tarski-Class W by Th11; end; hence thesis by ORDINAL1:41; end; reserve f,g for Function, L,L1 for T-Sequence, F for Cardinal-Function; theorem Th23: W is_Tarski-Class & (X in W & W is epsilon-transitive or X in W & X c= W or Card X <` Card W & X c= W) implies Funcs(X,W) c= W proof assume A1: W is_Tarski-Class; then A2: W is subset-closed by CLASSES1:def 2; assume X in W & W is epsilon-transitive or X in W & X c= W or Card X <` Card W & X c= W; then A3: X c= W & Card X <` Card W by A2,Th1,ORDINAL1:def 2; let x; assume A4: x in Funcs(X,W); then consider f such that A5: x = f & dom f = X & rng f c= W by FUNCT_2:def 2; A6: f c= W proof let y; assume A7: y in f; then consider y1,y2 being set such that A8: [y1,y2] = y by RELAT_1:def 1; A9: y1 in dom f & y2 = f.y1 by A7,A8,FUNCT_1:8; then y2 in rng f by FUNCT_1:def 5; hence y in W by A1,A3,A5,A8,A9,Th4 ; end; Card (f qua set) = Card X by A4,A5,CARD_2:7; hence x in W by A1,A3,A5,A6,CLASSES1:2; end; theorem X in Tarski-Class W & W is epsilon-transitive or X in Tarski-Class W & X c= Tarski-Class W or Card X <` Card Tarski-Class W & X c= Tarski-Class W implies Funcs(X,Tarski-Class W) c= Tarski-Class W proof assume A1: X in Tarski-Class W & W is epsilon-transitive or X in Tarski-Class W & X c= Tarski-Class W or Card X <` Card Tarski-Class W & X c= Tarski-Class W; W is epsilon-transitive implies Tarski-Class W is epsilon-transitive by CLASSES1:27; then A2: X c= Tarski-Class W & Card X <` Card Tarski-Class W by A1,CLASSES1:28,ORDINAL1:def 2; let x; assume A3: x in Funcs(X,Tarski-Class W); then consider f such that A4: x = f & dom f = X & rng f c= Tarski-Class W by FUNCT_2:def 2; A5: f c= Tarski-Class W proof let y; assume A6: y in f; then consider y1,y2 being set such that A7: [y1,y2] = y by RELAT_1:def 1; A8: y1 in dom f & y2 = f.y1 by A6,A7,FUNCT_1:8; then y2 in rng f by FUNCT_1:def 5; hence y in Tarski-Class W by A2,A4,A7,A8,CLASSES1:31; end; Card (f qua set) = Card X by A3,A4,CARD_2:7; hence x in Tarski-Class W by A2,A4,A5,CLASSES1:9; end; theorem Th25: dom L is_limit_ordinal & (for A st A in dom L holds L.A = Rank A) implies Rank dom L = Union L proof assume that A1: dom L is_limit_ordinal and A2: for A st A in dom L holds L.A = Rank A; A3: union rng L = Union L by PROB_1:def 3; now assume A4: dom L <> {}; thus Rank dom L c= Union L proof let x; assume x in Rank dom L; then consider A such that A5: A in dom L & x in Rank A by A1,A4,CLASSES1:35; L.A = Rank A by A2,A5; then Rank A in rng L by A5,FUNCT_1:def 5; hence thesis by A3,A5,TARSKI:def 4; end; thus Union L c= Rank dom L proof let x; assume x in Union L; then consider X such that A6: x in X & X in rng L by A3,TARSKI:def 4; consider y such that A7: y in dom L & X = L.y by A6,FUNCT_1:def 5; reconsider y as Ordinal by A7,ORDINAL1:23; X = Rank y by A2,A7; hence x in Rank dom L by A1,A6,A7,CLASSES1:35; end; end; hence thesis by A3,CLASSES1:33,RELAT_1:65,XBOOLE_0:def 10,ZFMISC_1:2; end; defpred PQ[Ordinal] means W is_Tarski-Class & $1 in On W implies Card Rank $1 <` Card W & Rank $1 in W; Lm2: PQ[{}] by Th10,CARD_1:47,CLASSES1:33,ORDINAL2:def 2; Lm3: PQ[A] implies PQ[succ A] proof assume A1: PQ[A]; let W; assume A2: W is_Tarski-Class & succ A in On W; then A3: A in succ A & Card W = On W & W is subset-closed by Th10,CLASSES1:def 2,ORDINAL1:10; then A in On W by A2,ORDINAL1:19; then Rank A in W by A1,A2; then bool Rank A in W & Rank succ A = bool Rank A by A2,CLASSES1:34,def 2; hence thesis by A3,Th1; end; Lm4: A <> {} & A is_limit_ordinal & (for B st B in A holds PQ[B]) implies PQ[A] proof assume that A1: A <> {} & A is_limit_ordinal and A2: for B st B in A holds PQ[B]; let W; assume A3: W is_Tarski-Class & A in On W; then A4: W is subset-closed by CLASSES1:def 2; deffunc f(Ordinal) = Rank $1; consider L such that A5: dom L = A & for B st B in A holds L.B = f(B) from TS_Lambda; deffunc g(set) = Card bool (L.$1); consider F such that A6: dom F = A & for x st x in A holds F.x = g(x) from CF_Lambda; A7: for x st x in dom Card L holds (Card L).x in F.x proof let x; assume x in dom Card L; then x in dom L by CARD_3:def 2; then F.x = Card bool (L.x) & Card (L.x) <` Card bool (L.x) & Card (L.x) = (Card L).x by A5,A6,CARD_1:30,CARD_3:def 2; hence thesis; end; dom Card L = dom L & Rank A = Union L by A1,A5,Th25,CARD_3:def 2; then A8: Card Rank A <=` Sum Card L & Sum Card L <` Product F by A5,A6,A7,CARD_3:54,56; then A9: Card Rank A <` Product F by ORDINAL1:22; A10: product F c= Funcs(A,W) proof let x; assume x in product F; then consider f such that A11: x = f & dom f = dom F & for x st x in dom F holds f.x in F.x by CARD_3:def 5; rng f c= W proof let z; assume z in rng f; then consider y such that A12: y in dom f & z = f.y by FUNCT_1:def 5; reconsider y as Ordinal by A6,A11,A12,ORDINAL1:23; y c= A & A in W by A3,A6,A11,A12,ORDINAL1:def 2,ORDINAL2:def 2; then A13: f.y in F.y & F.y = F.y & F.y = Card bool (L.y) & L.y = Rank y & L.y = L.y & y in W by A4,A5,A6,A11,A12,CLASSES1:def 1; then PQ[y] & y in On W by A2,A6,A11,A12,ORDINAL2:def 2; then L.y in W by A3,A13; then bool (L.y) in W by A3,CLASSES1:def 2; then Card bool (L.y) = Card bool (L.y) & Card bool (L.y) in W by A3,Th12; then F.y c= W by A3,A13,Th6; hence thesis by A12,A13; end; hence thesis by A6,A11,FUNCT_2:def 2; end; A14: A in W by A3,ORDINAL2:def 2; then A c= W by A3,Th6; then Funcs(A,W) c= W by A3,A14,Th23; then product F c= W & Product F = Card product F by A10,CARD_3:def 8,XBOOLE_1:1; then A15: Product F <=` Card W by CARD_1:27; hence Card Rank A <` Card W by A8,ORDINAL1:22; Rank A c= W proof let x; assume x in Rank A; then consider B such that A16: B in A & x in Rank B by A1,CLASSES1:35; B c= A by A16,ORDINAL1:def 2; then B in W by A4,A14,CLASSES1:def 1; then B in On W by ORDINAL2:def 2; then Rank B in W & Rank B is epsilon-transitive by A2,A3,A16,CLASSES1:37; then Rank B c= W by A4,Th8; hence x in W by A16; end; hence thesis by A3,A9,A15,CLASSES1:2; end; theorem Th26: W is_Tarski-Class & A in On W implies Card Rank A <` Card W & Rank A in W proof PQ[B] from Ordinal_Ind(Lm2,Lm3,Lm4); hence thesis; end; theorem A in On Tarski-Class W implies Card Rank A <` Card Tarski-Class W & Rank A in Tarski-Class W by Th26; theorem Th28: W is_Tarski-Class implies Rank Card W c= W proof assume A1: W is_Tarski-Class; then A2: W is subset-closed by CLASSES1:def 2; now assume A3: W <> {}; thus thesis proof let x such that A4: x in Rank Card W; Card W <> {} & Card W is_limit_ordinal by A1,A3,Th21; then consider A such that A5: A in Card W & x in Rank A by A4,CLASSES1:35; A in On W by A1,A5,Th10; then Rank A in W & Rank A is epsilon-transitive by A1,Th26,CLASSES1:37; then Rank A c= W by A2,Th8; hence x in W by A5; end; end; hence thesis by CARD_1:47,CLASSES1:33; end; theorem Th29: Rank Card Tarski-Class W c= Tarski-Class W proof let x such that A1: x in Rank Card Tarski-Class W; Card Tarski-Class W <> {} & Card Tarski-Class W is_limit_ordinal by Th22; then consider A such that A2: A in Card Tarski-Class W & x in Rank A by A1,CLASSES1:35; A in On Tarski-Class W by A2,Th11; then Rank A in Tarski-Class W & Rank A is epsilon-transitive by Th26,CLASSES1:37; then Rank A c= Tarski-Class W by Th8; hence x in Tarski-Class W by A2; end; deffunc f(set) = the_rank_of $1; deffunc g(set) = Card bool $1; theorem Th30: W is_Tarski-Class & W is epsilon-transitive & X in W implies the_rank_of X in W proof assume A1: W is_Tarski-Class & W is epsilon-transitive; then A2: W is subset-closed by CLASSES1:def 2; defpred P[Ordinal] means ex X st $1 = the_rank_of X & X in W & not $1 in W; assume X in W & not the_rank_of X in W; then A3: ex A st P[A]; consider A such that A4: P[A] and A5: for B st P[B] holds A c= B from Ordinal_Min(A3); consider X such that A6: A = the_rank_of X & X in W & not A in W by A4; A7: On W = Card W & X c= W by A1,A6,Th10,ORDINAL1:def 2; A8: On W = A proof not A in On W by A6,ORDINAL2:def 2; hence On W c= A by A7,ORDINAL1:26; X c= Rank Card W proof let x; assume A9: x in X; then the_rank_of x in A by A6,CLASSES1:76; then x in W & not A c= the_rank_of x by A7,A9,ORDINAL1:7; then the_rank_of x in W by A5; then the_rank_of x in Card W by A7,ORDINAL2:def 2; then x c= Rank the_rank_of x & Rank the_rank_of x in Rank Card W by CLASSES1:42,def 8; hence thesis by CLASSES1:47; end; hence thesis by A6,A7,CLASSES1:73; end; A10: Card X <` Card W by A2,A6,Th1; defpred P[set] means ex Y st Y in X & $1 = the_rank_of Y; consider LL being set such that A11: x in LL iff x in On W & P[x] from Separation; A12: LL c= On W proof let x; thus thesis by A11; end; now let Z; assume Z in union LL; then consider Y such that A13: Z in Y & Y in LL by TARSKI:def 4; Y in On W by A11,A13; then reconsider Y as Ordinal by ORDINAL2:def 2; A14: Z in Y by A13; hence Z is Ordinal by ORDINAL1:23; reconsider A = Z as Ordinal by A14,ORDINAL1:23; A c= Y & Y c= union LL by A13,ORDINAL1:def 2,ZFMISC_1:92; hence Z c= union LL by XBOOLE_1:1; end; then reconsider ULL = union LL as Ordinal by ORDINAL1:31; consider f such that A15: dom f = X & for x st x in X holds f.x = f(x) from Lambda; LL c= rng f proof let x; assume x in LL; then consider Y such that A16: Y in X & x = the_rank_of Y by A11; f.Y = x by A15,A16; hence thesis by A15,A16,FUNCT_1:def 5; end; then Card LL <=` Card X by A15,CARD_1:28; then Card LL <> Card W & On W c= W by A10,ORDINAL1:22,ORDINAL2:9; then not LL,W are_equipotent & LL c= W by A12,CARD_1:21,XBOOLE_1:1; then LL in W by A1,CLASSES1:def 2; then A17: Funcs(LL,W) c= W by A1,Th23; ULL = Union id LL proof Union id LL = union rng id LL by PROB_1:def 3 .= ULL by RELAT_1:71; hence thesis; end; then A18: Card ULL <=` Sum Card id LL by CARD_3:54; consider ff being Cardinal-Function such that A19: dom ff = LL & for x st x in LL holds ff.x = g(x) from CF_Lambda; A20: dom id LL = LL & dom Card id LL = dom id LL by CARD_3:def 2,RELAT_1:71; now let x; assume x in dom Card id LL; then (id LL).x = x & (Card id LL).x = Card ((id LL).x) & x = x & ff.x = Card bool x by A19,A20,CARD_3:def 2,FUNCT_1:35; hence (Card id LL).x in ff.x by CARD_1:30; end; then Sum Card id LL <` Product ff by A19,A20,CARD_3:56; then A21: Card ULL <` Product ff by A18,ORDINAL1:22; product ff c= Funcs(LL,W) proof let x; assume x in product ff; then consider g such that A22: x = g & dom g = dom ff & for x st x in dom ff holds g.x in ff.x by CARD_3:def 5; rng g c= W proof let y; assume y in rng g; then consider x such that A23: x in dom g & y = g.x by FUNCT_1:def 5; A24: y in ff.x & ff.x = ff.x & x = x & ff.x = Card bool x & x in On W by A12,A19,A22,A23; x in W by A12,A19,A22,A23,ORDINAL2:def 2; then bool x in W by A1,CLASSES1:def 2; then Card bool x in W by A1,Th12; then Card bool x c= W by A1,Th6; hence y in W by A24; end; hence thesis by A19,A22,FUNCT_2:def 2; end; then product ff c= W & Card product ff = Product ff by A17,CARD_3:def 8,XBOOLE_1:1; then A25: Product ff <=` Card W by CARD_1:27; On W c= ULL proof let x; assume A26: x in On W; then reconsider B = x as Ordinal by ORDINAL2:def 2; now assume A27: for Y st Y in X holds the_rank_of Y c= B; X c= Rank succ B proof let y; assume y in X; then the_rank_of y c= B by A27; then the_rank_of y in succ B by ORDINAL1:34; hence thesis by CLASSES1:74; end; then A c= succ B & B in W by A6,A26,CLASSES1:73,ORDINAL2:def 2; then A c= succ B & succ B in W by A1,Th6; hence contradiction by A2,A6,CLASSES1:def 1; end; then consider Y such that A28: Y in X & not the_rank_of Y c= B; the_rank_of Y in A by A6,A28,CLASSES1:76; then the_rank_of Y in LL by A8,A11,A28; then B in the_rank_of Y & the_rank_of Y c= ULL by A28,ORDINAL1:26,ZFMISC_1:92; hence x in ULL; end; then Card On W <=` Card ULL & On W = Card W & Card W = Card Card W by A1,Th10,CARD_1:27,def 5; hence contradiction by A21,A25,CARD_1:14; end; theorem Th31: W is_Tarski-Class & W is epsilon-transitive implies W c= Rank Card W proof assume A1: W is_Tarski-Class & W is epsilon-transitive; let x; assume x in W; then the_rank_of x in W by A1,Th30; then the_rank_of x in On W & On W = Card W by A1,Th10,ORDINAL2:def 2; then x c= Rank the_rank_of x & Rank the_rank_of x in Rank Card W by CLASSES1:42,def 8; hence thesis by CLASSES1:47; end; theorem Th32: W is_Tarski-Class & W is epsilon-transitive implies Rank Card W = W proof assume W is_Tarski-Class & W is epsilon-transitive; hence Rank Card W c= W & W c= Rank Card W by Th28,Th31; end; theorem W is_Tarski-Class & A in On W implies Card Rank A <=` Card W proof assume W is_Tarski-Class & A in On W; then Card Rank A <` Card W by Th26; hence thesis by CARD_1:13; end; theorem A in On Tarski-Class W implies Card Rank A <=` Card Tarski-Class W proof assume A in On Tarski-Class W; then Card Rank A <` Card Tarski-Class W by Th26; hence thesis by CARD_1:13; end; theorem Th35: W is_Tarski-Class implies Card W = Card Rank Card W proof assume W is_Tarski-Class; then Rank Card W c= W by Th28; then A1: Card Rank Card W <=` Card W by CARD_1:27; Card W = Card W & Card W c= Rank Card W by CLASSES1:44; then Card Card W = Card W & Card Card W <=` Card Rank Card W by CARD_1:27,def 5; hence thesis by A1,XBOOLE_0:def 10; end; theorem Card Tarski-Class W = Card Rank Card Tarski-Class W by Th35; theorem Th37: W is_Tarski-Class & X c= Rank Card W implies X,Rank Card W are_equipotent or X in Rank Card W proof assume that A1: W is_Tarski-Class and A2: X c= Rank Card W & not X,Rank Card W are_equipotent; A3: W <> {} by A2,CARD_1:47,CLASSES1:33,XBOOLE_1:3; Card W = Card Rank Card W by A1,Th35; then Card X <=` Card W & Card X <> Card W by A2,CARD_1:21,27; then A4: Card X <` Card W by CARD_1:13; defpred P[set] means ex Y st Y in X & $1 = the_rank_of Y; consider LL being set such that A5: x in LL iff x in On W & P[x] from Separation; A6: LL c= On W proof let x; thus thesis by A5; end; now let Z; assume Z in union LL; then consider Y such that A7: Z in Y & Y in LL by TARSKI:def 4; Y in On W by A5,A7; then reconsider Y as Ordinal by ORDINAL2:def 2; A8: Z in Y by A7; hence Z is Ordinal by ORDINAL1:23; reconsider A = Z as Ordinal by A8,ORDINAL1:23; A c= Y & Y c= union LL by A7,ORDINAL1:def 2,ZFMISC_1:92; hence Z c= union LL by XBOOLE_1:1; end; then reconsider ULL = union LL as Ordinal by ORDINAL1:31; consider f such that A9: dom f = X & for x st x in X holds f.x = f(x) from Lambda; LL c= rng f proof let x; assume x in LL; then consider Y such that A10: Y in X & x = the_rank_of Y by A5; f.Y = x by A9,A10; hence thesis by A9,A10,FUNCT_1:def 5; end; then Card LL <=` Card X by A9,CARD_1:28; then Card LL <> Card W & On W c= W by A4,ORDINAL1:22,ORDINAL2:9; then A11: not LL,W are_equipotent & LL c= W by A6,CARD_1:21,XBOOLE_1:1; then LL in W by A1,CLASSES1:def 2; then A12: Funcs(LL,W) c= W by A1,A11,Th23; ULL = Union id LL proof Union id LL = union rng id LL by PROB_1:def 3 .= ULL by RELAT_1:71; hence thesis; end; then A13: Card ULL <=` Sum Card id LL by CARD_3:54; consider ff being Cardinal-Function such that A14: dom ff = LL & for x st x in LL holds ff.x = g(x) from CF_Lambda; A15: dom id LL = LL & dom Card id LL = dom id LL by CARD_3:def 2,RELAT_1:71; now let x; assume x in dom Card id LL; then (id LL).x = x & (Card id LL).x = Card ((id LL).x) & x = x & ff.x = Card bool x by A14,A15,CARD_3:def 2,FUNCT_1:35; hence (Card id LL).x in ff.x by CARD_1:30; end; then A16: Sum Card id LL <` Product ff by A14,A15,CARD_3:56; product ff c= Funcs(LL,W) proof let x; assume x in product ff; then consider g such that A17: x = g & dom g = dom ff & for x st x in dom ff holds g.x in ff.x by CARD_3:def 5; rng g c= W proof let y; assume y in rng g; then consider x such that A18: x in dom g & y = g.x by FUNCT_1:def 5; A19: y in ff.x & ff.x = ff.x & x = x & ff.x = Card bool x & x in On W by A6,A14,A17,A18; x in W by A6,A14,A17,A18,ORDINAL2:def 2; then bool x in W by A1,CLASSES1:def 2; then Card bool x in W by A1,Th12; then Card bool x c= W by A1,Th6; hence y in W by A19; end; hence thesis by A14,A17,FUNCT_2:def 2; end; then product ff c= W & Card product ff = Product ff by A12,CARD_3:def 8,XBOOLE_1:1; then Product ff <=` Card W by CARD_1:27; then A20: Card ULL <` Card W by A13,A16,ORDINAL1:22; not W,{} are_equipotent by A3,CARD_1:46; then A21: Card W = On W & Card W <> {} & Card W is_limit_ordinal by A1,Th10,Th20,CARD_1:21,47; then union Card W = Card W & Card ULL <> Card W & Card Card W = Card W by A20,CARD_1:def 5,ORDINAL1:def 6; then ULL c= On W & ULL <> On W by A6,A21,ZFMISC_1:95; then ULL c< On W by XBOOLE_0:def 8; then ULL in Card W by A21,ORDINAL1:21; then succ ULL in Card W by A21,ORDINAL1:41; then A22: succ succ ULL in Card W by A21,ORDINAL1:41; X c= Rank succ ULL proof let x; assume A23: x in X; then A24: f.x = the_rank_of x & f.x in rng f & x = x & x in Rank Card W by A2,A9,FUNCT_1:def 5; consider A such that A25: A in Card W & x in Rank A by A2,A21,A23,CLASSES1:35; defpred P[Ordinal] means $1 in Card W & x c= Rank $1; x c= Rank A by A25,CLASSES1:38; then A26: ex A st P[A] by A25; consider A such that A27: P[A] and A28: for B st P[B] holds A c= B from Ordinal_Min(A26); now let B; assume x c= Rank B; then not B in Card W or A c= B by A28; then A c= Card W & Card W c= B or A c= B by A27,ORDINAL1:26; hence A c= B by XBOOLE_1:1; end; then A = the_rank_of x by A27,CLASSES1:def 8; then f.x in LL by A5,A21,A23,A24,A27; then the_rank_of x c= ULL by A24,ZFMISC_1:92; then x c= Rank the_rank_of x & Rank the_rank_of x c= Rank ULL by CLASSES1:43,def 8; then x c= Rank ULL by XBOOLE_1:1; hence x in Rank succ ULL by CLASSES1:36; end; then X in Rank succ succ ULL by CLASSES1:36; hence X in Rank Card W by A21,A22,CLASSES1:35; end; theorem X c= Rank Card Tarski-Class W implies X,Rank Card Tarski-Class W are_equipotent or X in Rank Card Tarski-Class W by Th37; theorem Th39: W is_Tarski-Class implies Rank Card W is_Tarski-Class proof assume A1: W is_Tarski-Class; set B = Rank Card W; thus for X,Y holds X in B & Y c= X implies Y in B by CLASSES1:47; now assume W <> {}; then not W,{} are_equipotent by CARD_1:46; then A2: Card W <> {} & Card W is_limit_ordinal by A1,Th20,CARD_1:21,47; thus for X holds X in B implies bool X in B proof let X; assume X in B; then consider A such that A3: A in Card W & X in Rank A by A2,CLASSES1:35; succ A in Card W & bool X in Rank succ A by A2,A3,CLASSES1:48,ORDINAL1:41; hence thesis by A2,CLASSES1:35; end; end; hence thesis by A1,Th37,CARD_1:47,CLASSES1:33; end; theorem Th40: Rank Card Tarski-Class W is_Tarski-Class by Th39; theorem Th41: X is epsilon-transitive & A in the_rank_of X implies ex Y st Y in X & the_rank_of Y = A proof assume A1: X is epsilon-transitive & A in the_rank_of X; assume A2: not thesis; defpred P[Ordinal] means ex Y st A in $1 & Y in X & the_rank_of Y = $1; A3: ex B st P[B] proof assume A4: for B,Y st A in B & Y in X holds the_rank_of Y <> B; X c= Rank A proof let x; assume A5: x in X; then not A in the_rank_of x by A4; then the_rank_of x c= A & the_rank_of x <> A by A2,A5,ORDINAL1:26; then the_rank_of x c< A by XBOOLE_0:def 8; then the_rank_of x in A by ORDINAL1:21; hence thesis by CLASSES1:74; end; then the_rank_of X c= A by CLASSES1:73; hence contradiction by A1,ORDINAL1:7; end; consider B such that A6: P[B] and A7: for C st P[C] holds B c= C from Ordinal_Min(A3); consider Y such that A8: A in B & Y in X & the_rank_of Y = B by A6; Y c= Rank A proof let x; assume A9: x in Y; then A10: the_rank_of x in B & Y c= X by A1,A8,CLASSES1:76,ORDINAL1:def 2; then x in X & not B c= the_rank_of x by A9,ORDINAL1:7; then not A in the_rank_of x by A7; then the_rank_of x c= A & the_rank_of x <> A by A2,A9,A10,ORDINAL1:26; then the_rank_of x c< A by XBOOLE_0:def 8; then the_rank_of x in A by ORDINAL1:21; hence thesis by CLASSES1:74; end; then the_rank_of Y c= A by CLASSES1:73; hence contradiction by A8,ORDINAL1:7; end; theorem Th42: X is epsilon-transitive implies Card the_rank_of X <=` Card X proof assume A1: X is epsilon-transitive; consider f such that A2: dom f = X & for x st x in X holds f.x = f(x) from Lambda; the_rank_of X c= rng f proof let x; assume A3: x in the_rank_of X; then reconsider x' = x as Ordinal by ORDINAL1:23; consider Y such that A4: Y in X & the_rank_of Y = x' by A1,A3,Th41; f.Y = x by A2,A4; hence thesis by A2,A4,FUNCT_1:def 5; end; hence Card the_rank_of X <=` Card X by A2,CARD_1:28; end; theorem Th43: W is_Tarski-Class & X is epsilon-transitive & X in W implies X in Rank Card W proof assume W is_Tarski-Class; then A1: W is subset-closed by CLASSES1:def 2; assume X is epsilon-transitive; then A2: Card the_rank_of X <=` Card X by Th42; assume X in W; then Card X <` Card W by A1,Th1; then Card the_rank_of X <` Card W & Card Card W = Card W & Card W = Card W by A2,CARD_1:def 5,ORDINAL1:22; then the_rank_of X in Card W by CARD_3:59; then Rank the_rank_of X in Rank Card W & X c= Rank the_rank_of X by CLASSES1:42,def 8; hence thesis by CLASSES1:47; end; theorem X is epsilon-transitive & X in Tarski-Class W implies X in Rank Card Tarski-Class W by Th43; theorem Th45: W is epsilon-transitive implies Rank Card Tarski-Class W is_Tarski-Class_of W proof assume A1: W is epsilon-transitive; W in Tarski-Class W by CLASSES1:5; hence W in Rank Card Tarski-Class W & Rank Card Tarski-Class W is_Tarski-Class by A1,Th40,Th43; end; theorem W is epsilon-transitive implies Rank Card Tarski-Class W = Tarski-Class W proof A1: W in Tarski-Class W by CLASSES1:5; assume W is epsilon-transitive; then W in Rank Card Tarski-Class W & Rank Card Tarski-Class W is_Tarski-Class_of W by A1,Th43,Th45; hence Rank Card Tarski-Class W c= Tarski-Class W & Tarski-Class W c= Rank Card Tarski-Class W by Th29,CLASSES1:def 4; end; definition let IT be set; attr IT is universal means :Def1: IT is epsilon-transitive & IT is_Tarski-Class; end; definition cluster universal -> epsilon-transitive being_Tarski-Class set; coherence by Def1; cluster epsilon-transitive being_Tarski-Class -> universal set; coherence by Def1; end; definition cluster universal non empty set; existence proof consider X; set Y = the_transitive-closure_of X; take V = Tarski-Class Y; Y is epsilon-transitive by CLASSES1:58; hence V is epsilon-transitive by CLASSES1:27; thus thesis; end; end; definition mode Universe is universal non empty set; end; reserve U1,U2,U3,Universum for Universe; canceled 3; theorem Th50: On Universum is Ordinal proof On Universum = Card Universum by Th10; hence thesis; end; theorem Th51: X is epsilon-transitive implies Tarski-Class X is universal proof assume X is epsilon-transitive; hence Tarski-Class X is epsilon-transitive & Tarski-Class X is_Tarski-Class by CLASSES1:27; end; theorem Tarski-Class Universum is Universe by Th51; definition let Universum; cluster On Universum -> ordinal; coherence by Th50; cluster Tarski-Class Universum -> universal; coherence by Th51; end; theorem Th53: Tarski-Class A is universal proof set M = Tarski-Class A; thus M is epsilon-transitive & M is_Tarski-Class by CLASSES1:27; end; definition let A; cluster Tarski-Class A -> universal; coherence by Th53; end; theorem Th54: Universum = Rank On Universum proof Card Universum = On Universum & Rank Card Universum = Universum by Th10,Th32; hence thesis; end; theorem Th55: On Universum <> {} & On Universum is_limit_ordinal proof Card Universum = On Universum by Th10; hence thesis by Th21; end; theorem U1 in U2 or U1 = U2 or U2 in U1 proof (On U1 in On U2 or On U1 = On U2 or On U2 in On U1) & U1 = Rank On U1 & U2 = Rank On U2 by Th54,ORDINAL1:24; hence thesis by CLASSES1:42; end; theorem Th57: U1 c= U2 or U2 in U1 proof (On U1 c= On U2 or On U2 in On U1) & U1 = Rank On U1 & U2 = Rank On U2 by Th54,ORDINAL1:26; hence thesis by CLASSES1:42,43; end; theorem Th58: U1,U2 are_c=-comparable proof (On U1 c= On U2 or On U2 c= On U1) & U1 = Rank On U1 & U2 = Rank On U2 by Th54; hence U1 c= U2 or U2 c= U1 by CLASSES1:43; end; theorem Th59: U1 in U2 & U2 in U3 implies U1 in U3 proof assume A1: U1 in U2 & U2 in U3; A2: U1 = Rank On U1 & U2 = Rank On U2 & U3 = Rank On U3 by Th54; then On U1 in On U2 & On U2 in On U3 by A1,CLASSES1:42; then On U1 in On U3 by ORDINAL1:19; hence thesis by A2,CLASSES1:42; end; canceled; theorem U1 \/ U2 is Universe & U1 /\ U2 is Universe proof U1,U2 are_c=-comparable by Th58; then U1 c= U2 or U2 c= U1 by XBOOLE_0:def 9; hence thesis by XBOOLE_1:12,28; end; theorem Th62: {} in Universum proof consider x being Element of Universum; {} c= x by XBOOLE_1:2; hence thesis by CLASSES1:def 1; end; theorem x in Universum implies {x} in Universum by Th3; theorem x in Universum & y in Universum implies {x,y} in Universum & [x,y] in Universum by Th3,Th4; theorem Th65: X in Universum implies bool X in Universum & union X in Universum & meet X in Universum proof assume A1: X in Universum; hence bool X in Universum by CLASSES1:def 2; Universum = Rank On Universum & On Universum <> {} & On Universum is_limit_ordinal by Th54,Th55; hence A2: union X in Universum by A1,CLASSES1:41; meet X c= union X by SETFAM_1:3; hence thesis by A2,CLASSES1:def 1; end; theorem Th66: X in Universum & Y in Universum implies X \/ Y in Universum & X /\ Y in Universum & X \ Y in Universum & X \+\ Y in Universum proof assume A1: X in Universum & Y in Universum; then {X,Y} in Universum & union {X,Y} = X \/ Y & meet {X,Y} = X /\ Y by Th3,SETFAM_1:12,ZFMISC_1:93; hence A2: X \/ Y in Universum & X /\ Y in Universum by Th65; X \ Y c= X & X \+\ Y = (X \/ Y)\(X /\ Y) & (X \/ Y)\(X /\ Y) c= (X \/ Y) by XBOOLE_1:36,101; hence thesis by A1,A2,CLASSES1:def 1; end; theorem Th67: X in Universum & Y in Universum implies [:X,Y:] in Universum & Funcs(X,Y) in Universum proof assume X in Universum & Y in Universum; then X \/ Y in Universum by Th66; then bool(X \/ Y) in Universum by Th65; then [:X,Y:] c= bool bool(X \/ Y) & bool bool(X \/ Y) in Universum by Th65,ZFMISC_1:105; hence [:X,Y:] in Universum by CLASSES1:def 1; then bool [:X,Y:] in Universum & Funcs(X,Y) c= bool [:X,Y:] by Th65, FRAENKEL:5; hence Funcs(X,Y) in Universum by CLASSES1:def 1; end; reserve u,v for Element of Universum; definition let U1; cluster non empty Element of U1; existence proof {} in U1 by Th62; then reconsider x = bool {} as Element of U1 by Th65; take x; thus thesis; end; end; definition let Universum,u; redefine func {u} -> Element of Universum; coherence by Th3; func bool u -> non empty Element of Universum; coherence by Th65; func union u -> Element of Universum; coherence by Th65; func meet u -> Element of Universum; coherence by Th65; let v; func {u,v} -> Element of Universum; coherence by Th3; func [u,v] -> Element of Universum; coherence by Th4; func u \/ v -> Element of Universum; coherence by Th66; func u /\ v -> Element of Universum; coherence by Th66; func u \ v -> Element of Universum; coherence by Th66; func u \+\ v -> Element of Universum; coherence by Th66; func [:u,v:] -> Element of Universum; coherence by Th67; func Funcs(u,v) -> Element of Universum; coherence by Th67; end; definition func FinSETS -> Universe equals: Def2: Tarski-Class {}; correctness; end; canceled; theorem Th69: Card Rank omega = Card omega proof deffunc h(Ordinal) = Rank $1; consider L such that A1: dom L = omega & for A st A in omega holds L.A = h(A) from TS_Lambda; A2: Rank omega = Union L by A1,Th25,ORDINAL2:19 .= union rng L by PROB_1:def 3; A3: omega c= Rank omega by CLASSES1:44; now let X,Y; assume X in rng L; then consider x such that A4: x in dom L & X = L.x by FUNCT_1:def 5; assume Y in rng L; then consider y such that A5: y in dom L & Y = L.y by FUNCT_1:def 5; reconsider x,y as Ordinal by A4,A5,ORDINAL1:23; X = Rank x & Y = Rank y & (x c= y or y c= x) by A1,A4,A5; then X c= Y or Y c= X by CLASSES1:43; hence X,Y are_c=-comparable by XBOOLE_0:def 9; end; then A6: rng L is c=-linear by ORDINAL1:def 9; now let X; assume X in rng L; then consider x such that A7: x in dom L & X = L.x by FUNCT_1:def 5; reconsider x as Ordinal by A7,ORDINAL1:23; X = Rank x by A1,A7; then X is finite by A1,A7,CARD_3:57; hence Card X <` Card omega by CARD_3:58; end; then Card Rank omega <=` Card omega & Card omega <=` Card Rank omega by A2,A3,A6,CARD_1:27,CARD_3:62; hence thesis by XBOOLE_0:def 10; end; theorem Th70: Rank omega is_Tarski-Class proof thus X in Rank omega & Y c= X implies Y in Rank omega by CLASSES1:47; thus X in Rank omega implies bool X in Rank omega proof assume X in Rank omega; then consider A such that A1: A in omega & X in Rank A by CLASSES1:35,ORDINAL2:19; succ A in omega & bool X in Rank succ A by A1,CLASSES1:48,ORDINAL1:41,ORDINAL2:19; hence thesis by CLASSES1:35,ORDINAL2:19; end; thus X c= Rank omega implies X,Rank omega are_equipotent or X in Rank omega proof assume A2: X c= Rank omega & not X,Rank omega are_equipotent & not X in Rank omega; then Card X <=` Card omega & Card X <> Card omega by Th69,CARD_1:21,27; then Card X = Card X & Card X in omega by CARD_1:13,84; then consider n such that A3: n = Card X; A4: Card X = Card n & omega c= Rank omega by A3,CARD_1:def 5,CLASSES1:44; then X,n are_equipotent & n is finite & {} in Rank omega by CARD_1:21,ORDINAL2:19; then reconsider X as finite set by CARD_1:68; defpred P[set,set] means the_rank_of $2 c= the_rank_of $1; A5: X <> {} by A2,A4,ORDINAL2:19; A6: for x,y holds P[x,y] or P[y,x]; A7: for x,y,z st P[x,y] & P[y,z] holds P[x,z] by XBOOLE_1:1; consider x such that A8: x in X & for y st y in X holds P[x,y] from MaxFinSetElem(A5,A6,A7); set A = the_rank_of x; now let Y; assume Y in X; then the_rank_of Y c= A & Y = Y by A8; hence the_rank_of Y in succ A by ORDINAL1:34; end; then A9: the_rank_of X c= succ A by CLASSES1:77; A in omega by A2,A8,CLASSES1:74; then succ A in omega by ORDINAL1:41,ORDINAL2:19; then the_rank_of X in omega by A9,ORDINAL1:22; hence thesis by A2,CLASSES1:74; end; end; theorem FinSETS = Rank omega proof A1: omega c= Rank omega by CLASSES1:44; then reconsider M = Rank omega as non empty set by ORDINAL2:19; M is epsilon-transitive & M is_Tarski-Class by Th70,CLASSES1:37; then M is Universe & M is_Tarski-Class_of {} by A1,Def1,CLASSES1:def 3,ORDINAL2 :19; hence FinSETS c= Rank omega by Def2,CLASSES1:def 4; A2: On FinSETS <> {} & On FinSETS is_limit_ordinal by Th55; then {} in On FinSETS by ORDINAL3:10; then omega c= On FinSETS & FinSETS = Rank On FinSETS by A2,Th54,ORDINAL2: def 5; hence thesis by CLASSES1:43; end; definition func SETS -> Universe equals: Def3: Tarski-Class FinSETS; correctness; end; definition let X be set; cluster the_transitive-closure_of X -> epsilon-transitive; coherence by CLASSES1:58; end; definition let X be epsilon-transitive set; cluster Tarski-Class X -> epsilon-transitive; coherence by CLASSES1:27; end; definition let A be Ordinal; cluster Rank A -> epsilon-transitive; coherence by CLASSES1:37; end; definition let X be set; func Universe_closure X -> Universe means :Def4: X c= it & for Y being Universe st X c= Y holds it c= Y; uniqueness proof let T1, T2 be Universe; assume A1: not thesis; then T1 c= T2 & T2 c= T1; hence thesis by A1,XBOOLE_0:def 10; end; existence proof per cases; suppose Rank the_rank_of X is Universe; then reconsider R = Rank the_rank_of X as Universe; take R; thus X c= R by CLASSES1:def 8; let Y be Universe; assume X c= Y; then the_rank_of X c= the_rank_of Y by CLASSES1:75; then A2: R c= Rank the_rank_of Y by CLASSES1:43; A3: Rank Card Y = Y by Th32; then the_rank_of Y c= Card Y by CLASSES1:def 8; then Rank the_rank_of Y c= Y by A3,CLASSES1:43; hence thesis by A2,XBOOLE_1:1; suppose A4: Rank the_rank_of X is not Universe; take R = Tarski-Class Rank the_rank_of X; X c= Rank the_rank_of X & Rank the_rank_of X in R by CLASSES1:5,def 8; then X in R by CLASSES1:def 1; hence X c= R by ORDINAL1:def 2; let Y be Universe; assume X c= Y; then A5: the_rank_of X c= the_rank_of Y by CLASSES1:75; A6: Rank Card Y = Y & Y c= Rank the_rank_of Y by Th32,CLASSES1:def 8; then Card Y c= the_rank_of Y & the_rank_of Y c= Card Y by CLASSES1:43,def 8; then Card Y = the_rank_of Y by XBOOLE_0:def 10; then the_rank_of X c< Card Y by A4,A5,A6,XBOOLE_0:def 8; then the_rank_of X in Card Y by ORDINAL1:21; then Rank the_rank_of X in Y by A6,CLASSES1:42; then Y is_Tarski-Class_of Rank the_rank_of X by CLASSES1:def 3; hence thesis by CLASSES1:def 4; end; end; deffunc C(Ordinal,set) = Tarski-Class $2; deffunc D(Ordinal,T-Sequence) = Universe_closure Union $2; definition mode FinSet is Element of FinSETS; mode Set is Element of SETS; let A; func UNIVERSE A means: Def5: ex L st it = last L & dom L = succ A & L.{} = FinSETS & (for C st succ C in succ A holds L.succ C = Tarski-Class(L.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds L.C = Universe_closure Union(L|C); correctness proof thus (ex x,L st x = last L & dom L = succ A & L.{} = FinSETS & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds L.C = D(C,L|C) ) & for x1,x2 being set st (ex L st x1 = last L & dom L = succ A & L.{} = FinSETS & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds L.C = D(C,L|C) ) & (ex L st x2 = last L & dom L = succ A & L.{} = FinSETS & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds L.C = D(C,L|C) ) holds x1 = x2 from TS_Def; end; end; deffunc u(Ordinal) = UNIVERSE $1; Lm5: now A1: for A,x holds x = u(A) iff ex L st x = last L & dom L = succ A & L.{} = FinSETS & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C in succ A & C <> {} & C is_limit_ordinal holds L.C = D(C,L|C) by Def5; thus u({}) = FinSETS from TS_Result0(A1); thus for A holds u(succ A) = C(A,u(A)) from TS_ResultS(A1); let A,L; assume that A2: A <> {} & A is_limit_ordinal and A3: dom L = A and A4: for B st B in A holds L.B = u(B); thus u(A) = D(A,L) from TS_ResultL(A1,A2,A3,A4); end; definition let A; cluster UNIVERSE A -> universal non empty; coherence proof defpred P[Ordinal] means UNIVERSE $1 is Universe; A1: P[{}] by Lm5; A2: P[B] implies P[succ B] proof assume P[B]; then reconsider UU = UNIVERSE B as Universe; UNIVERSE succ B = Tarski-Class UU by Lm5; hence P[succ B]; end; A3: for A st A <> {} & A is_limit_ordinal & for B st B in A holds P[B] holds P[A] proof let A such that A4: A <> {} & A is_limit_ordinal and for B st B in A holds P[B]; consider L such that A5: dom L = A & for B st B in A holds L.B = u(B) from TS_Lambda; UNIVERSE A = Universe_closure Union L by A4,A5,Lm5 .= Universe_closure union rng L by PROB_1:def 3; hence thesis; end; for A holds P[A] from Ordinal_Ind(A1,A2,A3); hence thesis; end; end; canceled 3; theorem UNIVERSE {} = FinSETS by Lm5; theorem UNIVERSE succ A = Tarski-Class UNIVERSE A by Lm5; theorem UNIVERSE one = SETS by Def3,Lm5,ORDINAL2:def 4; theorem A <> {} & A is_limit_ordinal & dom L = A & (for B st B in A holds L.B = UNIVERSE B) implies UNIVERSE A = Universe_closure Union L by Lm5; theorem FinSETS c= Universum & Tarski-Class {} c= Universum & UNIVERSE {} c= Universum proof {} <> On Universum by Th55; then {} in On Universum & Rank On Universum = Universum & On Universum c= Rank On Universum by Th54,CLASSES1:44,ORDINAL3:10; hence thesis by Def2,Lm5,Th5; end; theorem Th80: A in B iff UNIVERSE A in UNIVERSE B proof defpred P[Ordinal] means for A st A in $1 holds UNIVERSE A in UNIVERSE $1; A1: P[{}]; A2: for B st P[B] holds P[succ B] proof let B such that A3: P[B]; let A; A4: A c< B iff A c= B & A <> B by XBOOLE_0:def 8; assume A in succ B; then UNIVERSE succ B = Tarski-Class UNIVERSE B & A c= B by Lm5,ORDINAL1:34; then A5: UNIVERSE B in UNIVERSE succ B & (A in B or A = B) by A4,CLASSES1:5,ORDINAL1:21; then UNIVERSE A in UNIVERSE B or UNIVERSE A = UNIVERSE B by A3; hence thesis by A5,Th59; end; A6: for A st A <> {} & A is_limit_ordinal & for B st B in A holds P[B] holds P[A] proof let B; assume that A7: B <> {} & B is_limit_ordinal and for C st C in B for A st A in C holds UNIVERSE A in UNIVERSE C; let A; assume A in B; then A8: succ A in B by A7,ORDINAL1:41; consider L such that A9: dom L = B & for C st C in B holds L.C = u(C) from TS_Lambda; A10: UNIVERSE B = Universe_closure Union L by A7,A9,Lm5 .= Universe_closure union rng L by PROB_1:def 3; L.succ A = UNIVERSE succ A by A8,A9; then UNIVERSE succ A in rng L by A8,A9,FUNCT_1:def 5; then UNIVERSE succ A c= union rng L & union rng L c= UNIVERSE B by A10,Def4,ZFMISC_1:92; then UNIVERSE A in Tarski-Class UNIVERSE A & UNIVERSE succ A = Tarski-Class UNIVERSE A & UNIVERSE succ A c= UNIVERSE B by Lm5,CLASSES1:5,XBOOLE_1:1; hence thesis; end; A11:for B holds P[B] from Ordinal_Ind(A1,A2,A6); hence A in B implies UNIVERSE A in UNIVERSE B; assume A12: UNIVERSE A in UNIVERSE B & not A in B; B c< A iff B c= A & B <> A by XBOOLE_0:def 8; then B in A or B = A by A12,ORDINAL1:21,26; hence contradiction by A11,A12; end; theorem UNIVERSE A = UNIVERSE B implies A = B proof assume A1: UNIVERSE A = UNIVERSE B & A <> B; then A in B or B in A by ORDINAL1:24; then UNIVERSE A in UNIVERSE B or UNIVERSE B in UNIVERSE A by Th80; hence contradiction by A1; end; theorem A c= B iff UNIVERSE A c= UNIVERSE B proof thus A c= B implies UNIVERSE A c= UNIVERSE B proof assume A1: A c= B; assume not UNIVERSE A c= UNIVERSE B; then UNIVERSE B in UNIVERSE A by Th57; then B in A by Th80; hence contradiction by A1,ORDINAL1:7; end; assume A2: UNIVERSE A c= UNIVERSE B; assume not A c= B; then B in A by ORDINAL1:26; then UNIVERSE B in UNIVERSE A by Th80; hence contradiction by A2,ORDINAL1:7; end;