:: Universal Classes :: by Bogdan Nowak and Grzegorz Bancerek :: :: Received April 10, 1990 :: 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 CARD_1, ORDINAL1, FUNCT_1, CLASSES1, TARSKI, ZFMISC_1, XBOOLE_0, RELAT_1, CARD_3, FUNCT_2, SUBSET_1, SETFAM_1, FINSET_1, ORDINAL2, CLASSES2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, FINSET_1, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, ORDINAL2, CLASSES1, CARD_3; constructors SETFAM_1, WELLORD2, ORDINAL2, CLASSES1, CARD_3, NUMBERS, FUNCT_2, XTUPLE_0; registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, CARD_1, CLASSES1; requirements SUBSET, BOOLE, NUMERALS; definitions TARSKI, ORDINAL1, CLASSES1, XBOOLE_0; equalities TARSKI, ORDINAL1; expansions 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, XBOOLE_1; schemes FUNCT_1, PARTFUN1, CARD_3, ORDINAL1, ORDINAL2, XBOOLE_0, CARD_2; begin reserve m for Cardinal, A,B,C for Ordinal, x,y,z,X,Y,Z,W for set, f for Function; Lm1: Tarski-Class X is Tarski proof Tarski-Class X is_Tarski-Class_of X by CLASSES1:def 4; hence thesis; end; registration cluster Tarski -> subset-closed for set; coherence; end; registration let X be set; cluster Tarski-Class X -> Tarski; coherence by Lm1; end; theorem Th1: W is subset-closed & X in W implies not X,W are_equipotent & card X in card W proof assume A1: W is subset-closed; assume A2: X in W; bool X c= W by A1,A2; then A3: card bool X c= card W by CARD_1:11; A4: card X in card bool X by CARD_1:14; then card X in card W by A3; then card X <> card W; hence thesis by A4,A3,CARD_1:5; end; theorem Th2: W is Tarski & x in W & y in W implies {x} in W & {x,y} in W proof defpred C[object] means $1 = {}; assume that A1: W is Tarski and A2: x in W and A3: y in W; A4: {x} c= bool x by ZFMISC_1:68; bool x in W by A1,A2; hence {x} in W by A1,A4,CLASSES1:def 1; then A5: bool {x} in W by A1; deffunc g(object) = x; deffunc f(object) = y; consider f such that A6: dom f = {{},{x}} & for z being object st z in {{},{x}} holds (C[z] implies f.z = f(z)) & (not C[z] implies f.z = g(z)) from PARTFUN1:sch 1; {x,y} c= rng f proof let z be object; A7: {} in {{},{x}} by TARSKI:def 2; A8: {x} in {{},{x}} by TARSKI:def 2; assume z in {x,y}; then z = x or z = y by TARSKI:def 2; then f.{} = z or f.{x} = z by A6,A7,A8; hence thesis by A6,A7,A8,FUNCT_1:def 3; end; then A9: card {x,y} c= card {{},{x}} by A6,CARD_1:12; A10: {x,y} c= W by A2,A3,TARSKI:def 2; bool {x} = {{},{x}} by ZFMISC_1:24; then card {{},{x}} in card W by A1,A5,Th1; then card {x,y} in card W by A9,ORDINAL1:12; hence thesis by A1,A10,CLASSES1:1; end; theorem Th3: W is Tarski & x in W & y in W implies [x,y] in W proof assume A1: W is Tarski; assume that A2: x in W and A3: y in W; A4: {x} in W by A1,A2,Th2; {x,y} in W by A1,A2,A3,Th2; hence thesis by A1,A4,Th2; end; theorem Th4: W is Tarski & X in W implies Tarski-Class X c= W proof assume that A1: W is Tarski and A2: X in W; reconsider D = W as non empty set by A2; D is_Tarski-Class_of X by A1,A2; hence thesis by CLASSES1:def 4; end; theorem Th5: W is Tarski & 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 by A2,A3; hence succ A in W by A1,ORDINAL2:3; let x be object; assume A4: x in A; then reconsider B = x as Ordinal; 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 Th5; theorem Th7: W is subset-closed & X is epsilon-transitive & X in W implies X c= W; theorem X is epsilon-transitive & X in Tarski-Class W implies X c= Tarski-Class W by Th7; theorem Th9: W is Tarski implies On W = card W proof assume A1: W is Tarski; now let X; assume A2: X in On W; hence X is Ordinal by ORDINAL1:def 9; reconsider A = X as Ordinal by A2,ORDINAL1:def 9; A3: X in W by A2,ORDINAL1:def 9; thus X c= On W proof let x be object; assume A4: x in X; then x in A; then reconsider B = x as Ordinal; B c= A by A4,ORDINAL1:def 2; then B in W by A1,A3,CLASSES1:def 1; hence thesis by ORDINAL1:def 9; end; end; then reconsider ON = On W as epsilon-transitive epsilon-connected set by ORDINAL1:19; A5: now assume ON in W; then ON in ON by ORDINAL1:def 9; hence contradiction; end; ON c= W by ORDINAL2:7; then A6: ON,W are_equipotent or ON in W by A1; now let A; assume that A7: A,ON are_equipotent and A8: not ON c= A; A in ON by A8,ORDINAL1:16; then A in W by ORDINAL1:def 9; hence contradiction by A1,A6,A5,A7,Th1,WELLORD2:15; end; then reconsider ON as Cardinal by CARD_1:def 1; ON = card ON; hence thesis by A6,A5,CARD_1:5; end; theorem On Tarski-Class W = card Tarski-Class W by Th9; theorem Th11: W is Tarski & X in W implies card X in W proof assume that A1: W is Tarski and A2: X in W; A3: card W = On W by A1,Th9; card X in card W by A1,A2,Th1; hence thesis by A3,ORDINAL1:def 9; end; theorem X in Tarski-Class W implies card X in Tarski-Class W by Th11; theorem Th13: W is Tarski & x in card W implies x in W proof assume A1: W is Tarski; assume x in card W; then x in On W by A1,Th9; hence thesis by ORDINAL1:def 9; end; theorem x in card Tarski-Class W implies x in Tarski-Class W by Th13; theorem W is Tarski & m in card W implies m in W proof assume A1: W is Tarski; assume m in card W; then m in On W by A1,Th9; hence thesis by ORDINAL1:def 9; end; theorem m in 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 Th9; hence thesis by ORDINAL1:def 9; end; theorem W is Tarski & m in W implies m c= W by Th5; theorem m in Tarski-Class W implies m c= Tarski-Class W by Th5; theorem Th19: W is Tarski implies card W is limit_ordinal proof assume A1: W is Tarski; now let A; assume A in card W; then A in W by A1,Th13; then succ A in W by A1,Th5; then succ A in On W by ORDINAL1:def 9; hence succ A in card W by A1,Th9; end; hence thesis by ORDINAL1:28; end; theorem W is Tarski & W <> {} implies card W <> 0 & card W <> {} & card W is limit_ordinal by Th19; theorem Th21: card Tarski-Class W <> 0 & card Tarski-Class W <> {} & card Tarski-Class W is limit_ordinal proof thus card Tarski-Class W <> 0; thus card Tarski-Class W <> {}; now let A; assume A in card Tarski-Class W; then A in Tarski-Class W by Th13; then succ A in Tarski-Class W by Th5; then succ A in On Tarski-Class W by ORDINAL1:def 9; hence succ A in card Tarski-Class W by Th9; end; hence thesis by ORDINAL1:28; end; reserve f,g for Function, L for Sequence, F for Cardinal-Function; theorem Th22: W is Tarski & (X in W & W is epsilon-transitive or X in W & X c= W or card X in card W & X c= W) implies Funcs(X,W) c= W proof assume A1: W is Tarski; assume that A2: X in W & W is epsilon-transitive or X in W & X c= W or card X in card W & X c= W; A3: card X in card W by A1,A2,Th1; let x be object; assume A4: x in Funcs(X,W); then consider f such that A5: x = f and A6: dom f = X and A7: rng f c= W by FUNCT_2:def 2; A8: X c= W by A2; A9: f c= W proof let y be object; assume A10: y in f; then consider y1,y2 being object such that A11: [y1,y2] = y by RELAT_1:def 1; A12: y1 in dom f by A10,A11,FUNCT_1:1; y2 = f.y1 by A10,A11,FUNCT_1:1; then y2 in rng f by A12,FUNCT_1:def 3; hence thesis by A1,A8,A6,A7,A11,A12,Th3; end; card f = card X by A4,A5,CARD_2:3; hence thesis by A1,A3,A5,A9,CLASSES1:1; 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 in card Tarski-Class W & X c= Tarski-Class W implies Funcs(X,Tarski-Class W) c= Tarski-Class W proof assume that A1: X in Tarski-Class W & W is epsilon-transitive or X in Tarski-Class W & X c= Tarski-Class W or card X in card Tarski-Class W & X c= Tarski-Class W; A2: card X in card Tarski-Class W by A1,CLASSES1:24; let x be object; assume A3: x in Funcs(X,Tarski-Class W); then consider f such that A4: x = f and A5: dom f = X and A6: rng f c= Tarski-Class W by FUNCT_2:def 2; W is epsilon-transitive implies Tarski-Class W is epsilon-transitive by CLASSES1:23; then A7: X c= Tarski-Class W by A1; A8: f c= Tarski-Class W proof let y be object; assume A9: y in f; then consider y1,y2 being object such that A10: [y1,y2] = y by RELAT_1:def 1; A11: y1 in dom f by A9,A10,FUNCT_1:1; y2 = f.y1 by A9,A10,FUNCT_1:1; then y2 in rng f by A11,FUNCT_1:def 3; hence thesis by A7,A5,A6,A10,A11,CLASSES1:27; end; card f = card X by A3,A4,CARD_2:3; hence thesis by A2,A4,A8,CLASSES1:6; end; theorem Th24: 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 CARD_3:def 4; now assume A4: dom L <> {}; thus Rank dom L c= Union L proof let x be object; assume x in Rank dom L; then consider A such that A5: A in dom L and A6: x in Rank A by A1,A4,CLASSES1:31; L.A = Rank A by A2,A5; then Rank A in rng L by A5,FUNCT_1:def 3; hence thesis by A3,A6,TARSKI:def 4; end; thus Union L c= Rank dom L proof let x be object; assume x in Union L; then consider X such that A7: x in X and A8: X in rng L by A3,TARSKI:def 4; consider y being object such that A9: y in dom L and A10: X = L.y by A8,FUNCT_1:def 3; reconsider y as Ordinal by A9; X = Rank y by A2,A9,A10; hence thesis by A1,A7,A9,CLASSES1:31; end; end; hence thesis by A3,CLASSES1:29,RELAT_1:42,ZFMISC_1:2; end; defpred PQ[Ordinal] means W is Tarski & $1 in On W implies card Rank $1 in card W & Rank $1 in W; Lm2: PQ[0] by Th9,CLASSES1:29,ORDINAL1:def 9; Lm3: PQ[A] implies PQ[succ A] proof assume A1: PQ[A]; A2: A in succ A by ORDINAL1:6; let W; assume that A3: W is Tarski and A4: succ A in On W; card W = On W by A3,Th9; then A in On W by A4,A2,ORDINAL1:10; then Rank A in W by A1,A3; then A5: bool Rank A in W by A3; Rank succ A = bool Rank A by CLASSES1:30; hence thesis by A3,A5,Th1; end; Lm4: A <> 0 & A is limit_ordinal & (for B st B in A holds PQ[B]) implies PQ[A ] proof deffunc f(Ordinal) = Rank $1; assume that A1: A <> 0 and A2: A is limit_ordinal and A3: for B st B in A holds PQ[B]; let W; assume that A4: W is Tarski and A5: A in On W; consider L such that A6: dom L = A & for B st B in A holds L.B = f(B) from ORDINAL2:sch 2; deffunc g(object) = card bool (L.$1); consider F such that A7: dom F = A & for x being set st x in A holds F.x = g(x) from CARD_3:sch 1; A8: product F c= Funcs(A,W) proof let x be object; assume x in product F; then consider f such that A9: x = f and A10: dom f = dom F and A11: for x being object st x in dom F holds f.x in F.x by CARD_3:def 5; rng f c= W proof A12: A in W by A5,ORDINAL1:def 9; let z be object; assume z in rng f; then consider y being object such that A13: y in dom f and A14: z = f.y by FUNCT_1:def 3; reconsider y as Ordinal by A7,A10,A13; A15: f.y in F.y by A10,A11,A13; y c= A by A7,A10,A13,ORDINAL1:def 2; then y in W by A4,A12,CLASSES1:def 1; then A16: y in On W by ORDINAL1:def 9; L.y = Rank y by A6,A7,A10,A13; then L.y in W by A3,A4,A7,A10,A13,A16; then bool (L.y) in W by A4; then A17: card bool (L.y) in W by A4,Th11; F.y = card bool (L.y) by A7,A10,A13; then F.y c= W by A4,A17,Th5; hence thesis by A14,A15; end; hence thesis by A7,A9,A10,FUNCT_2:def 2; end; A18: Product F = card product F by CARD_3:def 8; A19: A in W by A5,ORDINAL1:def 9; then A c= W by A4,Th5; then Funcs(A,W) c= W by A4,A19,Th22; then product F c= W by A8; then A20: Product F c= card W by A18,CARD_1:11; A21: for x being object st x in dom Card L holds (Card L).x in F.x proof let x be object; A22: card (L.x) in card bool (L.x) by CARD_1:14; assume x in dom Card L; then A23: x in dom L by CARD_3:def 2; then F.x = card bool (L.x) by A6,A7; hence thesis by A23,A22,CARD_3:def 2; end; dom Card L = dom L by CARD_3:def 2; then A24: Sum Card L in Product F by A6,A7,A21,CARD_3:41; A25: Rank A c= W proof let x be object; assume x in Rank A; then consider B such that A26: B in A and A27: x in Rank B by A1,A2,CLASSES1:31; B c= A by A26,ORDINAL1:def 2; then B in W by A4,A19,CLASSES1:def 1; then B in On W by ORDINAL1:def 9; then Rank B c= W by A3,A4,A26,Th7; hence thesis by A27; end; A28: Rank A = Union L by A2,A6,Th24; hence card Rank A in card W by A24,A20,CARD_3:39,ORDINAL1:12; card Rank A in Product F by A28,A24,CARD_3:39,ORDINAL1:12; hence thesis by A4,A20,A25,CLASSES1:1; end; theorem Th25: W is Tarski & A in On W implies card Rank A in card W & Rank A in W proof PQ[B] from ORDINAL2:sch 1(Lm2,Lm3,Lm4); hence thesis; end; theorem A in On Tarski-Class W implies card Rank A in card Tarski-Class W & Rank A in Tarski-Class W by Th25; theorem Th27: W is Tarski implies Rank card W c= W proof assume A1: W is Tarski; now assume A2: W <> {}; thus thesis proof A3: card W is limit_ordinal by A1,Th19; let x be object; assume x in Rank card W; then consider A such that A4: A in card W and A5: x in Rank A by A2,A3,CLASSES1:31; A in On W by A1,A4,Th9; then Rank A c= W by A1,Th7,Th25; hence thesis by A5; end; end; hence thesis by CLASSES1:29; end; theorem Th28: Rank card Tarski-Class W c= Tarski-Class W proof A1: card Tarski-Class W is limit_ordinal by Th21; let x be object; assume x in Rank card Tarski-Class W; then consider A such that A2: A in card Tarski-Class W and A3: x in Rank A by A1,CLASSES1:31; A in On Tarski-Class W by A2,Th9; then Rank A c= Tarski-Class W by Th7,Th25; hence thesis by A3; end; deffunc f(object) = the_rank_of $1; deffunc g(set) = card bool $1; theorem Th29: W is Tarski & W is epsilon-transitive & X in W implies the_rank_of X in W proof assume that A1: W is Tarski and A2: W is epsilon-transitive; A3: On W = card W by A1,Th9; defpred P[Ordinal] means ex X st $1 = the_rank_of X & X in W & not $1 in W; assume that A4: X in W and A5: not the_rank_of X in W; A6: ex A st P[A] by A4,A5; consider A such that A7: P[A] and A8: for B st P[B] holds A c= B from ORDINAL1:sch 1(A6); consider X such that A9: A = the_rank_of X and A10: X in W and A11: not A in W by A7; defpred P[object] means ex Y st Y in X & $1 = the_rank_of Y; consider LL being set such that A12: for x being object holds x in LL iff x in On W & P[x] from XBOOLE_0:sch 1; consider ff being Cardinal-Function such that A13: dom ff = LL & for x st x in LL holds ff.x = g(x) from CARD_3:sch 1; A14: LL c= On W by A12; A15: product ff c= Funcs(LL,W) proof let x be object; assume x in product ff; then consider g such that A16: x = g and A17: dom g = dom ff and A18: for x being object st x in dom ff holds g.x in ff.x by CARD_3:def 5; rng g c= W proof let y be object; assume y in rng g; then consider x being object such that A19: x in dom g and A20: y = g.x by FUNCT_1:def 3; reconsider x as set by TARSKI:1; A21: ff.x = card bool x by A13,A17,A19; x in W by A14,A13,A17,A19,ORDINAL1:def 9; then bool x in W by A1; then card bool x in W by A1,Th11; then A22: card bool x c= W by A1,Th5; y in ff.x by A17,A18,A19,A20; hence thesis by A21,A22; end; hence thesis by A13,A16,A17,FUNCT_2:def 2; end; now let Z; assume Z in union LL; then consider Y such that A23: Z in Y and A24: Y in LL by TARSKI:def 4; Y in On W by A12,A24; then reconsider Y as Ordinal by ORDINAL1:def 9; A25: Y c= union LL by A24,ZFMISC_1:74; A26: Z in Y by A23; hence Z is Ordinal; reconsider A = Z as Ordinal by A26; A c= Y by A23,ORDINAL1:def 2; hence Z c= union LL by A25; end; then reconsider ULL = union LL as epsilon-transitive epsilon-connected set by ORDINAL1:19; A27: dom Card id LL = dom id LL by CARD_3:def 2; A28: dom id LL = LL by RELAT_1:45; now let x be object; assume A29: x in dom Card id LL; then A30: (Card id LL).x = card ((id LL).x) by A27,CARD_3:def 2; A31: (id LL).x = x by A28,A27,A29,FUNCT_1:18; reconsider xx=x as set by TARSKI:1; ff.x = card bool xx by A13,A28,A27,A29; hence (Card id LL).x in ff.x by A31,A30,CARD_1:14; end; then A32: Sum Card id LL in Product ff by A13,A28,A27,CARD_3:41; Union id LL = union rng id LL by CARD_3:def 4 .= ULL by RELAT_1:45; then A33: card ULL in Product ff by A32,CARD_3:39,ORDINAL1:12; consider f such that A34: dom f = X & for x being object st x in X holds f.x = f(x) from FUNCT_1:sch 3; LL c= rng f proof let x be object; assume x in LL; then consider Y such that A35: Y in X and A36: x = the_rank_of Y by A12; f.Y = x by A34,A35,A36; hence thesis by A34,A35,FUNCT_1:def 3; end; then A37: card LL c= card X by A34,CARD_1:12; card X in card W by A1,A10,Th1; then card LL <> card W by A37,ORDINAL1:12; then A38: not LL,W are_equipotent by CARD_1:5; A39: card product ff = Product ff by CARD_3:def 8; A40: X c= W by A2,A10; X c= Rank card W proof let x be object; reconsider xx=x as set by TARSKI:1; assume A41: x in X; then not A c= the_rank_of xx by A9,CLASSES1:68,ORDINAL1:5; then the_rank_of xx in W by A8,A40,A41; then the_rank_of xx in card W by A3,ORDINAL1:def 9; then A42: Rank the_rank_of xx in Rank card W by CLASSES1:36; xx c= Rank the_rank_of xx by CLASSES1:def 9; hence thesis by A42,CLASSES1:41; end; then A43: A c= On W by A9,A3,CLASSES1:65; On W c= ULL proof let x be object; assume A44: x in On W; then reconsider B = x as Ordinal by ORDINAL1:def 9; now assume A45: for Y st Y in X holds the_rank_of Y c= B; X c= Rank succ B proof let y be object; reconsider yy=y as set by TARSKI:1; assume y in X; then the_rank_of yy c= B by A45; then the_rank_of yy in succ B by ORDINAL1:22; hence thesis by CLASSES1:66; end; then A46: A c= succ B by A9,CLASSES1:65; B in W by A44,ORDINAL1:def 9; then succ B in W by A1,Th5; hence contradiction by A1,A11,A46,CLASSES1:def 1; end; then consider Y such that A47: Y in X and A48: not the_rank_of Y c= B; the_rank_of Y in A by A9,A47,CLASSES1:68; then the_rank_of Y in LL by A43,A12,A47; then A49: the_rank_of Y c= ULL by ZFMISC_1:74; B in the_rank_of Y by A48,ORDINAL1:16; hence thesis by A49; end; then A50: card On W c= card ULL by CARD_1:11; On W c= W by ORDINAL2:7; then LL c= W by A14; then LL in W by A1,A38; then Funcs(LL,W) c= W by A1,A2,Th22; then product ff c= W by A15; then A51: Product ff c= card W by A39,CARD_1:11; On W = card W by A1,Th9; hence contradiction by A33,A51,A50,CARD_1:4; end; theorem Th30: W is Tarski & W is epsilon-transitive implies W c= Rank card W proof assume that A1: W is Tarski and A2: W is epsilon-transitive; let x be object; reconsider xx=x as set by TARSKI:1; assume x in W; then the_rank_of xx in W by A1,A2,Th29; then A3: the_rank_of xx in On W by ORDINAL1:def 9; On W = card W by A1,Th9; then A4: Rank the_rank_of xx in Rank card W by A3,CLASSES1:36; xx c= Rank the_rank_of xx by CLASSES1:def 9; hence thesis by A4,CLASSES1:41; end; theorem Th31: W is Tarski & W is epsilon-transitive implies Rank card W = W by Th27,Th30; theorem W is Tarski & A in On W implies card Rank A c= card W proof assume that A1: W is Tarski and A2: A in On W; card Rank A in card W by A1,A2,Th25; hence thesis by CARD_1:3; end; theorem A in On Tarski-Class W implies card Rank A c= card Tarski-Class W proof assume A in On Tarski-Class W; then card Rank A in card Tarski-Class W by Th25; hence thesis by CARD_1:3; end; theorem Th34: W is Tarski implies card W = card Rank card W proof assume W is Tarski; then A1: card Rank card W c= card W by Th27,CARD_1:11; card card W c= card Rank card W by CARD_1:11,CLASSES1:38; hence thesis by A1; end; theorem card Tarski-Class W = card Rank card Tarski-Class W by Th34; theorem Th36: W is Tarski & 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 and A2: X c= Rank card W and A3: not X,Rank card W are_equipotent; defpred P[object] means ex Y st Y in X & $1 = the_rank_of Y; consider LL being set such that A4: for x being object holds x in LL iff x in On W & P[x] from XBOOLE_0:sch 1; consider ff being Cardinal-Function such that A5: dom ff = LL & for x st x in LL holds ff.x = g(x) from CARD_3:sch 1; A6: LL c= On W by A4; A7: product ff c= Funcs(LL,W) proof let x be object; assume x in product ff; then consider g such that A8: x = g and A9: dom g = dom ff and A10: for x being object st x in dom ff holds g.x in ff.x by CARD_3:def 5; rng g c= W proof let y be object; assume y in rng g; then consider x being object such that A11: x in dom g and A12: y = g.x by FUNCT_1:def 3; reconsider x as set by TARSKI:1; A13: ff.x = card bool x by A5,A9,A11; x in W by A6,A5,A9,A11,ORDINAL1:def 9; then bool x in W by A1; then card bool x in W by A1,Th11; then A14: card bool x c= W by A1,Th5; y in ff.x by A9,A10,A11,A12; hence thesis by A13,A14; end; hence thesis by A5,A8,A9,FUNCT_2:def 2; end; A15: card W = card Rank card W by A1,Th34; then A16: card X <> card W by A3,CARD_1:5; On W c= W by ORDINAL2:7; then A17: LL c= W by A6; now let Z; assume Z in union LL; then consider Y such that A18: Z in Y and A19: Y in LL by TARSKI:def 4; Y in On W by A4,A19; then reconsider Y as Ordinal by ORDINAL1:def 9; A20: Y c= union LL by A19,ZFMISC_1:74; A21: Z in Y by A18; hence Z is Ordinal; reconsider A = Z as Ordinal by A21; A c= Y by A18,ORDINAL1:def 2; hence Z c= union LL by A20; end; then reconsider ULL = union LL as epsilon-transitive epsilon-connected set by ORDINAL1:19; A22: dom Card id LL = dom id LL by CARD_3:def 2; A23: dom id LL = LL by RELAT_1:45; now let x be object; assume A24: x in dom Card id LL; then A25: (Card id LL).x = card ((id LL).x) by A22,CARD_3:def 2; A26: (id LL).x = x by A23,A22,A24,FUNCT_1:18; reconsider xx=x as set by TARSKI:1; ff.x = card bool xx by A5,A23,A22,A24; hence (Card id LL).x in ff.x by A26,A25,CARD_1:14; end; then A27: Sum Card id LL in Product ff by A5,A23,A22,CARD_3:41; consider f such that A28: dom f = X & for x being object st x in X holds f.x = f(x) from FUNCT_1:sch 3; LL c= rng f proof let x be object; assume x in LL; then consider Y such that A29: Y in X and A30: x = the_rank_of Y by A4; f.Y = x by A28,A29,A30; hence thesis by A28,A29,FUNCT_1:def 3; end; then A31: card LL c= card X by A28,CARD_1:12; A32: card product ff = Product ff by CARD_3:def 8; card X c= card W by A2,A15,CARD_1:11; then card X in card W by A16,CARD_1:3; then card LL <> card W by A31,ORDINAL1:12; then not LL,W are_equipotent by CARD_1:5; then LL in W by A1,A17; then Funcs(LL,W) c= W by A1,A17,Th22; then product ff c= W by A7; then A33: Product ff c= card W by A32,CARD_1:11; A34: card W is limit_ordinal by A1,Th19; A35: card W = On W by A1,Th9; X c= Rank succ ULL proof let x be object; reconsider xx=x as set by TARSKI:1; defpred P[Ordinal] means $1 in card W & xx c= Rank $1; assume A36: x in X; then A37: f.x = the_rank_of xx by A28; consider A such that A38: A in card W and A39: x in Rank A by A2,A34,A36,CLASSES1:29,31; P[A] by A38,A39,ORDINAL1:def 2; then A40: ex A st P[A]; consider A such that A41: P[A] and A42: for B st P[B] holds A c= B from ORDINAL1:sch 1(A40); now let B; assume xx c= Rank B; then A c= card W & card W c= B or A c= B by A41,A42,ORDINAL1:16; hence A c= B; end; then A = the_rank_of xx by A41,CLASSES1:def 9; then f.x in LL by A4,A35,A36,A37,A41; then the_rank_of xx c= ULL by A37,ZFMISC_1:74; then A43: Rank the_rank_of xx c= Rank ULL by CLASSES1:37; xx c= Rank the_rank_of xx by CLASSES1:def 9; then xx c= Rank ULL by A43; hence thesis by CLASSES1:32; end; then A44: X in Rank succ succ ULL by CLASSES1:32; Union id LL = union rng id LL by CARD_3:def 4 .= ULL by RELAT_1:45; then card ULL in card W by A27,A33,CARD_3:39,ORDINAL1:12; then A45: ULL <> On W by A35; union card W = card W by A34; then ULL c= On W by A6,A35,ZFMISC_1:77; then ULL c< On W by A45; then ULL in card W by A35,ORDINAL1:11; then succ ULL in card W by A34,ORDINAL1:28; then succ succ ULL in card W by A34,ORDINAL1:28; hence thesis by A34,A44,CLASSES1:31; 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 Th36; theorem Th38: W is Tarski implies Rank card W is Tarski proof assume A1: W is Tarski; set B = Rank card W; thus for X,Y holds X in B & Y c= X implies Y in B by CLASSES1:41; now A2: card W is limit_ordinal by A1,Th19; assume A3: W <> {}; thus for X holds X in B implies bool X in B proof let X; assume X in B; then consider A such that A4: A in card W and A5: X in Rank A by A3,A2,CLASSES1:31; A6: bool X in Rank succ A by A5,CLASSES1:42; succ A in card W by A2,A4,ORDINAL1:28; hence thesis by A2,A6,CLASSES1:31; end; end; hence thesis by A1,Th36,CLASSES1:29; end; theorem Rank card Tarski-Class W is Tarski by Th38; theorem Th40: X is epsilon-transitive & A in the_rank_of X implies ex Y st Y in X & the_rank_of Y = A proof assume that A1: X is epsilon-transitive and A2: A in the_rank_of X; defpred P[Ordinal] means ex Y st A in $1 & Y in X & the_rank_of Y = $1; assume A3: not thesis; A4: ex B st P[B] proof assume A5: for B,Y st A in B & Y in X holds the_rank_of Y <> B; X c= Rank A proof let x be object; reconsider xx=x as set by TARSKI:1; assume A6: x in X; then A7: the_rank_of xx <> A by A3; the_rank_of xx c= A by A5,A6,ORDINAL1:16; then the_rank_of xx c< A by A7; then the_rank_of xx in A by ORDINAL1:11; hence thesis by CLASSES1:66; end; then the_rank_of X c= A by CLASSES1:65; hence contradiction by A2,ORDINAL1:5; end; consider B such that A8: P[B] and A9: for C st P[C] holds B c= C from ORDINAL1:sch 1(A4); consider Y such that A10: A in B and A11: Y in X and A12: the_rank_of Y = B by A8; Y c= Rank A proof let x be object; reconsider xx=x as set by TARSKI:1; A13: Y c= X by A1,A11; assume A14: x in Y; then the_rank_of xx in B by A12,CLASSES1:68; then not A in the_rank_of xx by A9,A14,A13,ORDINAL1:5; then A15: the_rank_of xx c= A by ORDINAL1:16; the_rank_of xx <> A by A3,A14,A13; then the_rank_of xx c< A by A15; then the_rank_of xx in A by ORDINAL1:11; hence thesis by CLASSES1:66; end; then the_rank_of Y c= A by CLASSES1:65; hence contradiction by A10,A12,ORDINAL1:5; end; theorem Th41: X is epsilon-transitive implies card the_rank_of X c= card X proof consider f such that A1: dom f = X & for x being object st x in X holds f.x = f(x) from FUNCT_1:sch 3; assume A2: X is epsilon-transitive; the_rank_of X c= rng f proof let x be object; assume A3: x in the_rank_of X; then reconsider x9 = x as Ordinal; consider Y such that A4: Y in X and A5: the_rank_of Y = x9 by A2,A3,Th40; f.Y = x by A1,A4,A5; hence thesis by A1,A4,FUNCT_1:def 3; end; hence thesis by A1,CARD_1:12; end; theorem Th42: W is Tarski & X is epsilon-transitive & X in W implies X in Rank card W proof assume A1: W is Tarski; assume A2: X is epsilon-transitive; assume X in W; then card X in card W by A1,Th1; then A3: card the_rank_of X in card W by A2,Th41,ORDINAL1:12; card card W = card W; then the_rank_of X in card W by A3,CARD_3:43; then A4: Rank the_rank_of X in Rank card W by CLASSES1:36; X c= Rank the_rank_of X by CLASSES1:def 9; hence thesis by A4,CLASSES1:41; end; theorem X is epsilon-transitive & X in Tarski-Class W implies X in Rank card Tarski-Class W by Th42; theorem Th44: W is epsilon-transitive implies Rank card Tarski-Class W is_Tarski-Class_of W by CLASSES1:2,Th38,Th42; theorem W is epsilon-transitive implies Rank card Tarski-Class W = Tarski-Class W proof assume W is epsilon-transitive; then Rank card Tarski-Class W is_Tarski-Class_of W by Th44; hence Rank card Tarski-Class W c= Tarski-Class W & Tarski-Class W c= Rank card Tarski-Class W by Th28,CLASSES1:def 4; end; definition let IT be set; attr IT is universal means IT is epsilon-transitive & IT is Tarski; end; registration cluster universal -> epsilon-transitive Tarski for set; coherence; cluster epsilon-transitive Tarski -> universal for set; coherence; end; registration cluster universal non empty for set; existence proof set X = the set; take V = Tarski-Class the_transitive-closure_of X; thus V is epsilon-transitive by CLASSES1:23; thus thesis; end; end; definition mode Universe is universal non empty set; end; reserve U1,U2,U for Universe; theorem Th46: On U is Ordinal proof On U = card U by Th9; hence thesis; end; theorem Th47: X is epsilon-transitive implies Tarski-Class X is universal by CLASSES1:23; theorem Tarski-Class U is Universe by Th47; registration let U; cluster On U -> ordinal; coherence by Th46; cluster Tarski-Class U -> universal; coherence by Th47; end; theorem Th49: Tarski-Class A is universal by CLASSES1:23; registration let A; cluster Tarski-Class A -> universal; coherence by Th49; end; theorem Th50: U = Rank On U proof card U = On U by Th9; hence thesis by Th31; end; theorem Th51: On U <> {} & On U is limit_ordinal proof card U = On U by Th9; hence thesis by Th19; end; theorem U1 in U2 or U1 = U2 or U2 in U1 proof A1: On U1 in On U2 or On U1 = On U2 or On U2 in On U1 by ORDINAL1:14; A2: U2 = Rank On U2 by Th50; U1 = Rank On U1 by Th50; hence thesis by A1,A2,CLASSES1:36; end; theorem Th53: U1 c= U2 or U2 in U1 proof A1: On U1 c= On U2 or On U2 in On U1 by ORDINAL1:16; A2: U2 = Rank On U2 by Th50; U1 = Rank On U1 by Th50; hence thesis by A1,A2,CLASSES1:36,37; end; theorem Th54: U1,U2 are_c=-comparable proof A1: On U1 c= On U2 or On U2 c= On U1; A2: U2 = Rank On U2 by Th50; U1 = Rank On U1 by Th50; hence U1 c= U2 or U2 c= U1 by A1,A2,CLASSES1:37; end; theorem U1 \/ U2 is Universe & U1 /\ U2 is Universe proof U1,U2 are_c=-comparable by Th54; then U1 c= U2 or U2 c= U1; hence thesis by XBOOLE_1:12,28; end; theorem Th56: {} in U proof {} c= the Element of U; hence thesis by CLASSES1:def 1; end; theorem x in U implies {x} in U by Th2; theorem x in U & y in U implies {x,y} in U & [x,y] in U by Th2,Th3; theorem Th59: X in U implies bool X in U & union X in U & meet X in U proof assume A1: X in U; hence bool X in U by CLASSES1:def 2; U = Rank On U by Th50; hence A2: union X in U by A1,CLASSES1:35; meet X c= union X by SETFAM_1:2; hence thesis by A2,CLASSES1:def 1; end; theorem Th60: X in U & Y in U implies X \/ Y in U & X /\ Y in U & X \ Y in U & X \+\ Y in U proof assume that A1: X in U and A2: Y in U; A3: union {X,Y} = X \/ Y by ZFMISC_1:75; A4: meet {X,Y} = X /\ Y by SETFAM_1:11; {X,Y} in U by A1,A2,Th2; hence A5: X \/ Y in U & X /\ Y in U by A3,A4,Th59; X \+\ Y = (X \/ Y)\(X /\ Y) by XBOOLE_1:101; hence thesis by A1,A5,CLASSES1:def 1; end; theorem Th61: X in U & Y in U implies [:X,Y:] in U & Funcs(X,Y) in U proof assume that A1: X in U and A2: Y in U; X \/ Y in U by A1,A2,Th60; then bool(X \/ Y) in U by Th59; then A3: bool bool(X \/ Y) in U by Th59; [:X,Y:] c= bool bool(X \/ Y) by ZFMISC_1:86; hence [:X,Y:] in U by A3,CLASSES1:def 1; then A4: bool [:X,Y:] in U by Th59; Funcs(X,Y) c= bool [:X,Y:] by FRAENKEL:2; hence thesis by A4,CLASSES1:def 1; end; reserve u,v for Element of U; registration let U1; cluster non empty for Element of U1; existence proof {} in U1 by Th56; then reconsider x = bool {} as Element of U1 by Th59; take x; thus thesis; end; end; definition let U,u; redefine func {u} -> Element of U; coherence by Th2; redefine func bool u -> Element of U; coherence by Th59; redefine func union u -> Element of U; coherence by Th59; redefine func meet u -> Element of U; coherence by Th59; let v; redefine func {u,v} -> Element of U; coherence by Th2; redefine func [u,v] -> Element of U; coherence by Th3; redefine func u \/ v -> Element of U; coherence by Th60; redefine func u /\ v -> Element of U; coherence by Th60; redefine func u \ v -> Element of U; coherence by Th60; redefine func u \+\ v -> Element of U; coherence by Th60; redefine func [:u,v:] -> Element of U; coherence by Th61; redefine func Funcs(u,v) -> Element of U; coherence by Th61; end; definition func FinSETS -> Universe equals Tarski-Class {}; correctness; end; Lm5: omega is limit_ordinal by ORDINAL1:def 11; theorem Th62: 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 ORDINAL2: sch 2; now let X,Y; assume X in rng L; then consider x being object such that A2: x in dom L and A3: X = L.x by FUNCT_1:def 3; assume Y in rng L; then consider y being object such that A4: y in dom L and A5: Y = L.y by FUNCT_1:def 3; reconsider x,y as Ordinal by A2,A4; A6: Y = Rank y by A1,A4,A5; A7: x c= y or y c= x; X = Rank x by A1,A2,A3; then X c= Y or Y c= X by A6,A7,CLASSES1:37; hence X,Y are_c=-comparable; end; then A8: rng L is c=-linear; A9: card omega c= card Rank omega by CARD_1:11,CLASSES1:38; A10: now let X; assume X in rng L; then consider x being object such that A11: x in dom L and A12: X = L.x by FUNCT_1:def 3; reconsider x as Ordinal by A11; X = Rank x by A1,A11,A12; hence card X in card omega by A1,A11,CARD_2:67,CARD_3:42; end; Rank omega = Union L by A1,Lm5,Th24 .= union rng L by CARD_3:def 4; then card Rank omega c= card omega by A8,A10,CARD_3:46; hence thesis by A9; end; theorem Th63: Rank omega is Tarski proof thus X in Rank omega & Y c= X implies Y in Rank omega by CLASSES1:41; 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 and A2: X in Rank A by Lm5,CLASSES1:31; A3: bool X in Rank succ A by A2,CLASSES1:42; succ A in omega by A1,Lm5,ORDINAL1:28; hence thesis by A3,Lm5,CLASSES1:31; end; thus X c= Rank omega implies X,Rank omega are_equipotent or X in Rank omega proof A4: 0 in omega; defpred P[object,object] means the_rank_of $2 c= the_rank_of $1; assume that A5: X c= Rank omega and A6: not X,Rank omega are_equipotent and A7: not X in Rank omega; A8: card X <> card omega by A6,Th62,CARD_1:5; card X c= card omega by A5,Th62,CARD_1:11; then card X in omega by A8,CARD_1:3; then reconsider X as finite set; A9: for x,y being object holds P[x,y] or P[y,x]; A10: for x,y,z being object st P[x,y] & P[y,z] holds P[x,z] by XBOOLE_1:1; omega c= Rank omega by CLASSES1:38; then A11: X <> {} by A7,A4; consider x being object such that A12: x in X & for y being object st y in X holds P[x,y] from CARD_2:sch 2(A11,A9,A10); set A = the_rank_of x; for Y st Y in X holds the_rank_of Y in succ A by A12,ORDINAL1:22; then A13: the_rank_of X c= succ A by CLASSES1:69; A in omega by A5,A12,CLASSES1:66; then succ A in omega by Lm5,ORDINAL1:28; then the_rank_of X in omega by A13,ORDINAL1:12; hence thesis by A7,CLASSES1:66; end; end; theorem FinSETS = Rank omega proof A1: omega c= Rank omega by CLASSES1:38; then reconsider M = Rank omega as non empty set; 0 in omega; then M is_Tarski-Class_of {} by A1,Th63; hence FinSETS c= Rank omega by CLASSES1:def 4; A2: {} in On FinSETS by Th51,ORDINAL3:8; A3: FinSETS = Rank On FinSETS by Th50; On FinSETS is limit_ordinal by Th51; then omega c= On FinSETS by A2,ORDINAL1:def 11; hence thesis by A3,CLASSES1:37; end; definition func SETS -> Universe equals Tarski-Class FinSETS; correctness; end; registration let X be set; cluster the_transitive-closure_of X -> epsilon-transitive; coherence; end; registration let X be epsilon-transitive set; cluster Tarski-Class X -> epsilon-transitive; coherence by CLASSES1:23; 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; 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 9; let Y be Universe; assume X c= Y; then the_rank_of X c= the_rank_of Y by CLASSES1:67; then A1: R c= Rank the_rank_of Y by CLASSES1:37; A2: Rank card Y = Y by Th31; then the_rank_of Y c= card Y by CLASSES1:def 9; then Rank the_rank_of Y c= Y by A2,CLASSES1:37; hence thesis by A1; end; suppose A3: Rank the_rank_of X is not Universe; take R = Tarski-Class Rank the_rank_of X; A4: Rank the_rank_of X in R by CLASSES1:2; X c= Rank the_rank_of X by CLASSES1:def 9; then X in R by A4,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:67; A6: Rank card Y = Y by Th31; then A7: the_rank_of Y c= card Y by CLASSES1:def 9; Y c= Rank the_rank_of Y by CLASSES1:def 9; then card Y c= the_rank_of Y by A6,CLASSES1:37; then card Y = the_rank_of Y by A7; then the_rank_of X c< card Y by A3,A5,A6; then the_rank_of X in card Y by ORDINAL1:11; then Rank the_rank_of X in Y by A6,CLASSES1:36; then Y is_Tarski-Class_of Rank the_rank_of X; hence thesis by CLASSES1:def 4; end; end; end; deffunc C(Ordinal,set) = Tarski-Class $2; deffunc D(Ordinal,Sequence) = Universe_closure Union $2; definition mode FinSet is Element of FinSETS; mode Set is Element of SETS; let A; func UNIVERSE A -> set means : Def5: ex L st it = last L & dom L = succ A & L.0 = 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 <> 0 & C is limit_ordinal holds L.C = Universe_closure Union(L|C); correctness proof (ex x being object, L st x = last L & dom L = succ A & L.0 = 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 <> 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 = 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 <> 0 & C is limit_ordinal holds L.C = D(C,L|C) ) & (ex L st x2 = last L & dom L = succ A & L.0 = 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 <> 0 & C is limit_ordinal holds L.C = D(C,L|C) ) holds x1 = x2 from ORDINAL2: sch 7; hence thesis; end; end; deffunc u(Ordinal) = UNIVERSE $1; Lm6: now A1: for A for x being object holds x = u(A) iff ex L st x = last L & dom L = succ A & L.0 = 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 <> 0 & C is limit_ordinal holds L.C = D(C,L|C) by Def5; thus u(0) = FinSETS from ORDINAL2:sch 8(A1); thus for A holds u(succ A) = C(A,u(A)) from ORDINAL2:sch 9(A1); let A,L; assume that A2: A <> 0 & 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 ORDINAL2:sch 10(A1,A2,A3,A4); end; registration let A; cluster UNIVERSE A -> universal non empty; coherence proof defpred P[Ordinal] means UNIVERSE $1 is Universe; A1: P[B] implies P[succ B] proof assume P[B]; then reconsider UU = UNIVERSE B as Universe; UNIVERSE succ B = Tarski-Class UU by Lm6; hence thesis; end; A2: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B] holds P[A] proof let A such that A3: A <> 0 and A4: 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 ORDINAL2:sch 2; UNIVERSE A = Universe_closure Union L by A3,A4,A5,Lm6 .= Universe_closure union rng L by CARD_3:def 4; hence thesis; end; A6: P[0] by Lm6; for A holds P[A] from ORDINAL2:sch 1(A6,A1,A2); hence thesis; end; end; theorem UNIVERSE {} = FinSETS by Lm6; theorem UNIVERSE succ A = Tarski-Class UNIVERSE A by Lm6; Lm7: 1 = succ 0; theorem UNIVERSE 1 = SETS by Lm6,Lm7; 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 Lm6; theorem FinSETS c= U & Tarski-Class {} c= U & UNIVERSE {} c= U proof A1: On U c= Rank On U by CLASSES1:38; A2: Rank On U = U by Th50; {} in On U by Th51,ORDINAL3:8; hence thesis by A2,A1,Lm6,Th4; end; theorem Th70: 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: for B st P[B] holds P[succ B] proof let B such that A2: P[B]; let A; assume A3: A in succ B; A c< B iff A c= B & A <> B; then A in B or A = B by A3,ORDINAL1:11,22; then A4: UNIVERSE A in UNIVERSE B or UNIVERSE A = UNIVERSE B by A2; UNIVERSE succ B = Tarski-Class UNIVERSE B by Lm6; then UNIVERSE B in UNIVERSE succ B by CLASSES1:2; hence thesis by A4,ORDINAL1:10; end; A5: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B] holds P[A] proof let B; assume that A6: B <> 0 and A7: 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; consider L such that A8: dom L = B & for C st C in B holds L.C = u(C) from ORDINAL2:sch 2; assume A in B; then A9: succ A in B by A7,ORDINAL1:28; then L.succ A = UNIVERSE succ A by A8; then UNIVERSE succ A in rng L by A9,A8,FUNCT_1:def 3; then A10: UNIVERSE succ A c= union rng L by ZFMISC_1:74; UNIVERSE B = Universe_closure Union L by A6,A7,A8,Lm6 .= Universe_closure union rng L by CARD_3:def 4; then union rng L c= UNIVERSE B by Def4; then A11: UNIVERSE succ A c= UNIVERSE B by A10; A12: UNIVERSE A in Tarski-Class UNIVERSE A by CLASSES1:2; UNIVERSE succ A = Tarski-Class UNIVERSE A by Lm6; hence thesis by A12,A11; end; A13: P[0]; A14: for B holds P[B] from ORDINAL2:sch 1(A13,A1,A5); hence A in B implies UNIVERSE A in UNIVERSE B; assume that A15: UNIVERSE A in UNIVERSE B and A16: not A in B; B in A or B = A by A16,ORDINAL1:16; hence contradiction by A14,A15; end; theorem UNIVERSE A = UNIVERSE B implies A = B proof assume that A1: UNIVERSE A = UNIVERSE B and A2: A <> B; A in B or B in A by A2,ORDINAL1:14; then UNIVERSE A in UNIVERSE B or UNIVERSE B in UNIVERSE A by Th70; 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 Th53; then B in A by Th70; hence contradiction by A1,ORDINAL1:5; end; assume A2: UNIVERSE A c= UNIVERSE B; assume not A c= B; then B in A by ORDINAL1:16; then UNIVERSE B in UNIVERSE A by Th70; hence contradiction by A2,ORDINAL1:5; end; reserve u,v for Element of Tarski-Class(X); theorem Tarski-Class(X,{}) in Tarski-Class(X,1) & Tarski-Class(X,{}) <> Tarski-Class(X,1) proof deffunc F(Ordinal) = Tarski-Class(X,$1); deffunc C(Ordinal,set) = { u : ex v st v in $2 & u c= v } \/ { bool v : v in $2 } \/ bool $2 /\ Tarski-Class X; deffunc D(Ordinal,Sequence) = (union rng $2) /\ Tarski-Class X; A1: for A for x being object holds x = F(A) iff ex L st x = last L & dom L = succ A & L.0 = { X } & (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 CLASSES1:def 5; A2: F(0) = { X } from ORDINAL2:sch 8(A1); then X in Tarski-Class(X,{}) by TARSKI:def 1; then A3: bool X in Tarski-Class X by CLASSES1:4; { X } c= bool X proof let x be object; assume x in { X }; then x = X by TARSKI:def 1; hence thesis by ZFMISC_1:def 1; end; then 1 = succ 0 & { X } in Tarski-Class X by A3,CLASSES1:3; thus then A4: Tarski-Class(X,{}) in Tarski-Class(X,1) by A2,CLASSES1:10; assume Tarski-Class(X,{}) = Tarski-Class(X,1); hence contradiction by A4; end;