:: Universal Classes
:: by Bogdan Nowak and Grzegorz Bancerek
::
:: Received April 10, 1990
:: Copyright (c) 1990-2019 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;