### Tarski's Classes and Ranks

by
Grzegorz Bancerek

Copyright (c) 1990 Association of Mizar Users

MML identifier: CLASSES1
[ MML identifier index ]

```environ

vocabulary FUNCT_1, TARSKI, SETFAM_1, BOOLE, CARD_1, ORDINAL1, ORDINAL2,
RELAT_1, MCART_1, CLASSES1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
NUMBERS, NAT_1, ORDINAL1, MCART_1, ORDINAL2, CARD_1;
constructors SETFAM_1, NAT_1, MCART_1, WELLORD2, CARD_1, MEMBERED, XBOOLE_0;
clusters SUBSET_1, ORDINAL1, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
requirements NUMERALS, SUBSET, BOOLE;
definitions TARSKI, ORDINAL1, WELLORD2, FUNCT_1, XBOOLE_0;
theorems TARSKI, SETFAM_1, ZFMISC_1, ORDINAL1, MCART_1, ORDINAL2, FUNCT_1,
CARD_1, WELLORD2, ENUMSET1, XBOOLE_0, XBOOLE_1;
schemes ORDINAL1, ORDINAL2, TARSKI, PARTFUN1, NAT_1, RECDEF_1, XBOOLE_0;

begin

reserve W,X,Y,Z for set,
f,g for Function,
a,x,y,z for set;

definition let B be set;
attr B is subset-closed means
:Def1: for X,Y holds X in B & Y c= X implies Y in B;
end;

definition let B be set;
attr B is being_Tarski-Class means
:Def2:  B is subset-closed &
(for X holds X in B implies bool X in B) &
(for X holds X c= B implies X,B are_equipotent or X in B);
synonym B is_Tarski-Class;
end;

definition let A,B be set;
pred B is_Tarski-Class_of A means
:Def3: A in B & B is_Tarski-Class;
end;

definition let A be set;
func Tarski-Class A -> set means
:Def4: it is_Tarski-Class_of A &
for D being set st D is_Tarski-Class_of A holds it c= D;
existence
proof
consider Big being set such that
A1:   A in Big &
(for X,Y holds X in Big & Y c= X implies Y in Big) &
(for X holds X in Big implies bool X in Big) &
(for X holds X c= Big implies X,Big are_equipotent or X in Big)
by ZFMISC_1:136;
Big is subset-closed by A1,Def1;
then A2:  Big is_Tarski-Class by A1,Def2;
defpred P[set] means \$1 is_Tarski-Class_of A;
consider Classes being set such that
A3:   X in Classes iff X in bool Big & P[X] from Separation;
set IT = meet Classes;
A4: Big in bool Big & Big is_Tarski-Class_of A by A1,A2,Def3,ZFMISC_1:def 1;
then A5:  Big in Classes by A3;
A6:     Classes <> {} by A3,A4;
A7:     now let X; assume X in Classes;
then X is_Tarski-Class_of A by A3;
hence A in X by Def3;
end;
then A8:   A in IT by A6,SETFAM_1:def 1;
take IT;
thus A in IT by A6,A7,SETFAM_1:def 1;
thus
A9:  X in IT & Y c= X implies Y in IT
proof assume
A10:     X in IT & Y c= X;
now let Z; assume
A11:       Z in Classes;
then Z is_Tarski-Class_of A by A3;
then Z is_Tarski-Class by Def3;
then Z is subset-closed by Def2;
then (for X,Y holds X in Z & Y c= X implies Y in Z) & X in Z
by A10,A11,Def1,SETFAM_1:def 1;
hence Y in Z by A10;
end;
hence Y in IT by A6,SETFAM_1:def 1;
end;
thus
A12:  X in IT implies bool X in IT
proof assume
A13:     X in IT;
now let Z; assume
A14:       Z in Classes;
then Z is_Tarski-Class_of A by A3;
then Z is_Tarski-Class by Def3;
then (for X holds X in Z implies bool X in Z) & X in Z
by A13,A14,Def2,SETFAM_1:def 1;
hence bool X in Z;
end;
hence bool X in IT by A6,SETFAM_1:def 1;
end;
thus
A15:  X c= IT implies X,IT are_equipotent or X in IT
proof assume that
A16:     X c= IT and
A17:     not X,IT are_equipotent;
now let Z; assume
A18:       Z in Classes;
then Z is_Tarski-Class_of A by A3;
then A19:          Z is_Tarski-Class by Def3;
A20:       IT c= Z by A18,SETFAM_1:4;
then X c= Z by A16,XBOOLE_1:1;
then X,Z are_equipotent or X in Z by A19,Def2;
hence X in Z by A16,A17,A20,CARD_1:44;
end;
hence X in IT by A6,SETFAM_1:def 1;
end;
let D be set; assume
D is_Tarski-Class_of A;
then A21:   A in D & D is_Tarski-Class by Def3;
then A22: D is subset-closed by Def2;
A23:   IT /\ D is_Tarski-Class_of A
proof
thus A in IT /\ D by A8,A21,XBOOLE_0:def 3;
thus X in IT /\ D & Y c= X implies Y in IT /\ D
proof assume
A24:        X in IT /\ D & Y c= X;
then X in IT & X in D by XBOOLE_0:def 3;
then Y in IT & Y in D by A9,A22,A24,Def1;
hence Y in IT /\ D by XBOOLE_0:def 3;
end;
thus X in IT /\ D implies bool X in IT /\ D
proof assume X in IT /\ D;
then X in IT & X in D by XBOOLE_0:def 3;
then bool X in IT & bool X in D by A12,A21,Def2;
hence bool X in IT /\ D by XBOOLE_0:def 3;
end;
let X such that
A25:     X c= IT /\ D and
A26:     not X,IT /\ D are_equipotent;
A27:     IT /\ D c= IT & IT /\ D c= D by XBOOLE_1:17;
then A28:     X c= IT & X c= D by A25,XBOOLE_1:1;
not X,IT are_equipotent & not X,D are_equipotent
by A25,A26,A27,CARD_1:44;
then X in IT & X in D by A15,A21,A28,Def2;
hence X in IT /\ D by XBOOLE_0:def 3;
end;
IT /\ D c= Big
proof let x; assume x in IT /\ D;
then x in IT by XBOOLE_0:def 3;
hence x in Big by A5,SETFAM_1:def 1;
end;
then IT /\ D in Classes by A3,A23;
then IT c= IT /\ D & IT /\ D c= D by SETFAM_1:4,XBOOLE_1:17;
hence thesis by XBOOLE_1:1;
end;
uniqueness
proof let D1,D2 be set such that
A29:  D1 is_Tarski-Class_of A &
for D being set st D is_Tarski-Class_of A holds D1 c= D and
A30:  D2 is_Tarski-Class_of A &
for D being set st D is_Tarski-Class_of A holds D2 c= D;
thus D1 c= D2 & D2 c= D1 by A29,A30;
end;
end;

definition let A be set;
cluster Tarski-Class A -> non empty;
coherence
proof
Tarski-Class A is_Tarski-Class_of A by Def4; hence thesis by Def3;
end;
end;

canceled;

theorem
W is_Tarski-Class iff
W is subset-closed &
(for X st X in W holds bool X in W) &
(for X st X c= W & Card X <` Card W holds X in W)
proof
hereby assume
A1: W is_Tarski-Class;
hence W is subset-closed &
for X st X in W holds bool X in W by Def2;
let X;
assume
A2: X c= W & Card X <` Card W;
then Card X <> Card W;
then not X,W are_equipotent by CARD_1:21;
hence X in W by A1,A2,Def2;
end;
now assume
A3:    for X st X c= W & Card X <` Card W holds X in W;
let X; assume X c= W;
then Card X <=` Card W & not Card X <` Card W or X in W by A3,CARD_1:27;
then Card X = Card W or X in W by CARD_1:13;
hence X,W are_equipotent or X in W by CARD_1:21;
end;
hence thesis by Def2;
end;

canceled 2;

theorem
Th5: X in Tarski-Class X
proof Tarski-Class X is_Tarski-Class_of X by Def4;
hence thesis by Def3;
end;

theorem
Th6: Y in Tarski-Class X & Z c= Y implies Z in Tarski-Class X
proof
Tarski-Class X is_Tarski-Class_of X by Def4;
then Tarski-Class X is_Tarski-Class by Def3;
then Tarski-Class X is subset-closed by Def2;
hence thesis by Def1;
end;

theorem
Th7: Y in Tarski-Class X implies bool Y in Tarski-Class X
proof Tarski-Class X is_Tarski-Class_of X by Def4;
then Tarski-Class X is_Tarski-Class by Def3;
hence thesis by Def2;
end;

theorem
Th8: Y c= Tarski-Class X implies
Y,Tarski-Class X are_equipotent or Y in Tarski-Class X
proof Tarski-Class X is_Tarski-Class_of X by Def4;
then Tarski-Class X is_Tarski-Class by Def3;
hence thesis by Def2;
end;

theorem
Y c= Tarski-Class X & Card Y <` Card Tarski-Class X implies
Y in Tarski-Class X
proof assume
A1:  Y c= Tarski-Class X & Card Y <` Card Tarski-Class X;
then Card Y <> Card Tarski-Class X;
then not Y,Tarski-Class X are_equipotent by CARD_1:21;
hence thesis by A1,Th8;
end;

reserve u,v for Element of Tarski-Class(X),
A,B,C for Ordinal,
L,L1 for T-Sequence;

definition let X,A;
func Tarski-Class(X,A) means
:Def5:
ex L st it = last L & dom L = succ A & L.{} = { X } &
(for C st succ C in succ A holds
L.succ C = { u : ex v st v in L.C & u c= v } \/
{ bool v : v in L.C } \/
bool(L.C) /\ Tarski-Class X) &
for C st C in succ A & C <> {} & C is_limit_ordinal
holds L.C = (union rng(L|C)) /\ Tarski-Class X;
correctness
proof
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,T-Sequence) = (union rng \$2) /\ Tarski-Class X;
thus (ex x,L st x = last L & dom L = succ A & L.{} = {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 <> {} & 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.{} = {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 <> {} & C is_limit_ordinal
holds L.C = D(C,L|C) ) &
(ex L st x2 = last L & dom L = succ A & L.{} = {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 <> {} & C is_limit_ordinal
holds L.C = D(C,L|C) )
holds x1 = x2 from TS_Def;
end;
end;

Lm1:
now let X;
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,T-Sequence) = (union rng \$2) /\ Tarski-Class X;
A1: for A,x holds x = F(A) iff
ex L st x = last L & dom L = succ A & L.{} = { 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 <> {} & C is_limit_ordinal
holds L.C = D(C,L|C) by Def5;
thus F({}) = { X } from TS_Result0(A1);
thus for A holds F(succ A) = C(A,F(A)) from TS_ResultS(A1);
thus A <> {} & A is_limit_ordinal & dom L = A &
(for B st B in A holds L.B = Tarski-Class(X,B)) implies
Tarski-Class(X,A) = (union rng L) /\ Tarski-Class X
proof assume that
A2:    A <> {} & A is_limit_ordinal and
A3:    dom L = A and
A4:    for B st B in A holds L.B = F(B);
thus F(A) = D(A,L) from TS_ResultL(A1,A2,A3,A4);
end;
end;

definition let X,A;
redefine func Tarski-Class(X,A) -> Subset of Tarski-Class X;
coherence
proof
defpred P[Ordinal] means Tarski-Class(X,\$1) is Subset of Tarski-Class X;
{ X } c= Tarski-Class X
proof let x; assume x in { X };
then x = X by TARSKI:def 1;
hence thesis by Th5;
end;
then A1: P[{}] by Lm1;
A2:   P[B] implies P[succ B]
proof assume Tarski-Class(X,B) is Subset of Tarski-Class X;
then reconsider S = Tarski-Class(X,B) as Subset of Tarski-Class X;
set Y = Tarski-Class(X,succ B);
Y c= Tarski-Class X
proof let x; assume x in Y;
then x in { u : ex v st v in S & u c= v } \/ { bool v : v in S } \/
bool S /\ Tarski-Class X by Lm1;
then A3:           x in { u : ex v st v in S & u c= v } \/ { bool v : v in S }
or
x in bool S /\ Tarski-Class X by XBOOLE_0:def 2;
A4:        now assume x in { u : ex v st v in S & u c= v };
then ex u st x = u & ex v st v in S & u c= v;
hence thesis;
end;
now assume x in { bool v : v in S };
then ex v st x = bool v & v in S;
hence thesis by Th7;
end;
hence thesis by A3,A4,XBOOLE_0:def 2,def 3;
end;
hence thesis;
end;
A5:   for B st B <> {} & B is_limit_ordinal &
for C st C in B holds P[C] holds P[B]
proof let B such that
A6:     B <> {} & B is_limit_ordinal and
for C st C in B holds Tarski-Class(X,C) is Subset of Tarski-Class X;
deffunc f(Ordinal) = Tarski-Class(X,\$1);
consider L such that
A7:     dom L = B & for C st C in B holds L.C = f(C) from TS_Lambda;
Tarski-Class(X,B) = (union rng L) /\ Tarski-Class X &
(union rng L) /\ Tarski-Class X c= Tarski-Class X
by A6,A7,Lm1,XBOOLE_1:17;
hence thesis;
end;
for A holds P[A] from Ordinal_Ind(A1,A2,A5);
hence thesis;
end;
end;

theorem
Tarski-Class(X,{}) = { X } by Lm1;

theorem
Tarski-Class(X,succ A) =
{ u : ex v st v in Tarski-Class(X,A) & u c= v } \/
{ bool v : v in Tarski-Class(X,A) } \/
bool Tarski-Class(X,A) /\ Tarski-Class X by Lm1;

theorem
Th12: A <> {} & A is_limit_ordinal implies
Tarski-Class(X,A) = { u : ex B st B in A & u in Tarski-Class(X,B) }
proof assume
A1:  A <> {} & A is_limit_ordinal;
deffunc f(Ordinal) = Tarski-Class(X,\$1);
consider L such that
A2:  dom L = A & for B st B in A holds L.B = f(B) from TS_Lambda;
A3:  Tarski-Class(X,A) = (union rng L) /\ Tarski-Class X by A1,A2,Lm1;
thus Tarski-Class(X,A) c= { u : ex B st B in A & u in Tarski-Class(X,B) }
proof let x; assume x in Tarski-Class(X,A);
then x in union rng L by A3,XBOOLE_0:def 3;
then consider Y such that
A4:     x in Y & Y in rng L by TARSKI:def 4;
consider y such that
A5:     y in dom L & Y = L.y by A4,FUNCT_1:def 5;
reconsider y as Ordinal by A5,ORDINAL1:23;
Y = Tarski-Class(X,y) by A2,A5;
hence thesis by A2,A4,A5;
end;
let x; assume x in { u : ex B st B in A & u in Tarski-Class(X,B) };
then consider u such that
A6:  x = u & ex B st B in A & u in Tarski-Class(X,B);
consider B such that
A7:  B in A & u in Tarski-Class(X,B) by A6;
L.B = Tarski-Class(X,B) by A2,A7;
then Tarski-Class(X,B) in rng L by A2,A7,FUNCT_1:def 5;
then u in union rng L & u in Tarski-Class X by A7,TARSKI:def 4;
hence thesis by A3,A6,XBOOLE_0:def 3;
end;

theorem
Th13: Y in Tarski-Class(X,succ A) iff
Y c= Tarski-Class(X,A) & Y in Tarski-Class X or
ex Z st Z in Tarski-Class(X,A) & (Y c= Z or Y = bool Z)
proof
set T1 = { u : ex v st v in Tarski-Class(X,A) & u c= v };
set T2 = { bool v : v in Tarski-Class(X,A) };
set T3 = bool Tarski-Class(X,A) /\ Tarski-Class X;
A1:  Tarski-Class(X,succ A) = T1 \/ T2 \/ T3 by Lm1;
thus Y in Tarski-Class(X,succ A) implies
Y c= Tarski-Class(X,A) & Y in Tarski-Class X or
ex Z st Z in Tarski-Class(X,A) & (Y c= Z or Y = bool Z)
proof assume
Y in Tarski-Class(X,succ A);
then A2:       Y in T1 \/ T2 or Y in T3 by A1,XBOOLE_0:def 2;
A3:     now assume Y in T1;
then ex u st Y = u & ex v st v in Tarski-Class(X,A) & u c= v;
hence ex Z st Z in Tarski-Class(X,A) & (Y c= Z or Y = bool Z);
end;
A4:     now assume Y in T2;
then ex v st Y = bool v & v in Tarski-Class(X,A);
hence ex Z st Z in Tarski-Class(X,A) & (Y c= Z or Y = bool Z);
end;
now assume Y in T3;
then Y in bool Tarski-Class(X,A) & Y in Tarski-Class X by XBOOLE_0:def
3;
hence thesis;
end;
hence thesis by A2,A3,A4,XBOOLE_0:def 2;
end;
assume
A5:  Y c= Tarski-Class(X,A) & Y in Tarski-Class X or
ex Z st Z in Tarski-Class(X,A) & (Y c= Z or Y = bool Z);
A6:  now assume
Y c= Tarski-Class(X,A) & Y in Tarski-Class X;
then Y in T3 by XBOOLE_0:def 3;
hence Y in Tarski-Class(X,succ A) by A1,XBOOLE_0:def 2;
end;
now given Z such that
A7:   Z in Tarski-Class(X,A) & (Y c= Z or Y = bool Z);
reconsider Z as Element of Tarski-Class X by A7;
reconsider y = Y as Element of Tarski-Class X by A7,Th6,Th7;
A8:   now assume Y c= Z;
then y in T1 by A7; then Y in T1 \/ T2 by XBOOLE_0:def 2;
hence thesis by A1,XBOOLE_0:def 2;
end;
now assume Y = bool Z;
then y in T2 by A7; then Y in T1 \/ T2 by XBOOLE_0:def 2;
hence thesis by A1,XBOOLE_0:def 2;
end;
hence thesis by A7,A8;
end;
hence thesis by A5,A6;
end;

theorem
Y c= Z & Z in Tarski-Class(X,A) implies Y in Tarski-Class(X,succ A) by Th13;

theorem
Y in Tarski-Class(X,A) implies bool Y in Tarski-Class(X,succ A) by Th13;

theorem
Th16: A <> {} & A is_limit_ordinal implies
(x in Tarski-Class(X,A) iff ex B st B in A & x in Tarski-Class(X,B))
proof assume
A1:  A <> {} & A is_limit_ordinal;
then A2:  Tarski-Class(X,A) = { u : ex B st B in A & u in Tarski-Class(X,B) }
by Th12;
thus x in Tarski-Class(X,A) implies ex B st B in A & x in Tarski-Class(X,B)
proof assume x in Tarski-Class(X,A);
then ex u st x = u & ex B st B in A & u in Tarski-Class(X,B) by A2;
hence thesis;
end;
given B such that
A3:  B in A & x in Tarski-Class(X,B);
reconsider u = x as Element of Tarski-Class X by A3;
u in { v : ex B st B in A & v in Tarski-Class(X,B) } by A3;
hence thesis by A1,Th12;
end;

theorem
A <> {} & A is_limit_ordinal & Y in Tarski-Class(X,A) &
(Z c= Y or Z = bool Y) implies Z in Tarski-Class(X,A)
proof assume
A1:  A <> {} & A is_limit_ordinal & Y in Tarski-Class(X,A);
then consider B such that
A2:  B in A & Y in Tarski-Class(X,B) by Th16;
A3:  bool Y in Tarski-Class(X,succ B) by A2,Th13;
A4:  Z c= Y implies Z in Tarski-Class(X,succ B) by A2,Th13;
A5:  succ B in A by A1,A2,ORDINAL1:41;
assume Z c= Y or Z = bool Y;
hence thesis by A1,A3,A4,A5,Th16;
end;

theorem
Th18: Tarski-Class(X,A) c= Tarski-Class(X,succ A)
proof let x; assume
x in Tarski-Class(X,A);
then x in { u : ex v st v in Tarski-Class(X,A) & u c= v };
then A1:  x in { u : ex v st v in Tarski-Class(X,A) & u c= v } \/
{ bool v : v in Tarski-Class(X,A) } by XBOOLE_0:def 2;
Tarski-Class(X,succ A) =
{ u : ex v st v in Tarski-Class(X,A) & u c= v } \/
{ bool v : v in Tarski-Class(X,A) } \/
bool Tarski-Class(X,A) /\ Tarski-Class X by Lm1;
hence thesis by A1,XBOOLE_0:def 2;
end;

theorem
Th19: A c= B implies Tarski-Class(X,A) c= Tarski-Class(X,B)
proof
defpred OnP[Ordinal] means
A c= \$1 implies Tarski-Class(X,A) c= Tarski-Class(X,\$1);
A1:for B st for C st C in B holds OnP[C] holds OnP[B]
proof let B such that
A2:     for C st C in B holds OnP[C] and
A3:     A c= B;
let x; assume
A4:     x in Tarski-Class(X,A);
now assume A5: A <> B;
then A c< B by A3,XBOOLE_0:def 8;
then A6:       A in B by ORDINAL1:21;
A c= B & B <> A iff A c< B by XBOOLE_0:def 8;
then A7:       B <> {} by A3,A5,ORDINAL1:21;
A8:       now given C such that
A9:        B = succ C;
A c= C & C in B by A6,A9,ORDINAL1:34;
then Tarski-Class(X,A) c= Tarski-Class(X,C) &
Tarski-Class(X,C) c= Tarski-Class(X,B) by A2,A9,Th18;
then Tarski-Class(X,A) c= Tarski-Class(X,B) by XBOOLE_1:1;
hence thesis by A4;
end;
now assume for C holds B <> succ C;
then B is_limit_ordinal by ORDINAL1:42;
then Tarski-Class(X,B) = { v : ex C st C in B & v in Tarski-Class(X,C) }
by A7,Th12;
hence thesis by A4,A6;
end;
hence thesis by A8;
end;
hence thesis by A4;
end;
for B holds OnP[B] from Transfinite_Ind(A1);
hence thesis;
end;

theorem
Th20: ex A st Tarski-Class(X,A) = Tarski-Class(X,succ A)
proof assume
A1:  for A holds Tarski-Class(X,A) <> Tarski-Class(X,succ A);
defpred P[set] means ex A st \$1 in Tarski-Class(X,A);
consider Z such that
A2:  x in Z iff x in Tarski-Class X & P[x] from Separation;
defpred P[set,set] means
ex A st \$2 = A & \$1 in Tarski-Class(X,succ A) & not \$1 in
Tarski-Class(X,A);
A3:  for x,y,z st P[x,y] & P[x,z] holds y = z
proof let x,y,z;
given A such that
A4:    y = A & x in Tarski-Class(X,succ A) & not x in Tarski-Class(X,A);
given B such that
A5:    z = B & x in Tarski-Class(X,succ B) & not x in Tarski-Class(X,B);
assume A6: y <> z;
A c= B or B c= A;
then A7:     A c< B or B c< A by A4,A5,A6,XBOOLE_0:def 8;
now assume A c< B;
then A in B by ORDINAL1:21;
then succ A c= B by ORDINAL1:33;
then Tarski-Class(X,succ A) c= Tarski-Class(X,B) by Th19;
end;
then B in A by A7,ORDINAL1:21;
then succ B c= A by ORDINAL1:33;
then Tarski-Class(X,succ B) c= Tarski-Class(X,A) by Th19;
end;
consider Y such that
A8:  x in Y iff ex y st y in Z & P[y,x] from Fraenkel(A3);
now let A;
A9:    Tarski-Class(X,A) <> Tarski-Class(X,succ A) &
Tarski-Class(X,A) c= Tarski-Class(X,succ A) by A1,Th18;
then consider x such that
A10: not (x in Tarski-Class(X,A) iff x in Tarski-Class(X,succ A)) by TARSKI:2;
x in Z by A2,A10;
hence A in Y by A8,A9,A10;
end;
end;

theorem
Th21: Tarski-Class(X,A) = Tarski-Class(X,succ A) implies
Tarski-Class(X,A) = Tarski-Class X
proof assume
A1:  Tarski-Class(X,A) = Tarski-Class(X,succ A);
{} = {} & {} c= A by XBOOLE_1:2;
then A2:    Tarski-Class(X,{}) c= Tarski-Class(X,A) &
Tarski-Class(X,{}) = { X } & X in { X }
by Lm1,Th19,TARSKI:def 1;
Tarski-Class(X,A) is_Tarski-Class_of X
proof
thus X in Tarski-Class(X,A) by A2;
A3:     Tarski-Class(X,succ A) =
{ u : ex v st v in Tarski-Class(X,A) & u c= v } \/
{ bool v : v in Tarski-Class(X,A) } \/
bool Tarski-Class(X,A) /\ Tarski-Class X by Lm1;
Tarski-Class X is_Tarski-Class_of X by Def4;
then A4:       Tarski-Class X is_Tarski-Class by Def3;
thus Z in Tarski-Class(X,A) & Y c= Z implies Y in Tarski-Class(X,A)
proof assume
A5:        Z in Tarski-Class(X,A) & Y c= Z;
Tarski-Class X is_Tarski-Class_of X by Def4;
then Tarski-Class X is_Tarski-Class by Def3;
then Tarski-Class X is subset-closed by Def2;
then reconsider y = Y as Element of Tarski-Class X
by A5,Def1;
ex v st v in Tarski-Class(X,A) & y c= v by A5;
then Y in { u : ex v st v in Tarski-Class(X,A) & u c= v };
then Y in { u : ex v st v in Tarski-Class(X,A) & u c= v } \/
{ bool v : v in Tarski-Class(X,A) } by XBOOLE_0:def 2;
hence Y in Tarski-Class(X,A) by A1,A3,XBOOLE_0:def 2;
end;
thus Y in Tarski-Class(X,A) implies bool Y in Tarski-Class(X,A)
proof assume
Y in Tarski-Class(X,A);
then bool Y in { bool u : u in Tarski-Class(X,A) };
then bool Y in { u : ex v st v in Tarski-Class(X,A) & u c= v } \/
{ bool v : v in Tarski-Class(X,A) } by XBOOLE_0:def 2;
hence bool Y in Tarski-Class(X,A) by A1,A3,XBOOLE_0:def 2;
end;
let Y; assume that
A6:     Y c= Tarski-Class(X,A) and
A7:     not Y,Tarski-Class(X,A) are_equipotent;
Y c= Tarski-Class X by A6,XBOOLE_1:1;
then Y,Tarski-Class X are_equipotent or Y in Tarski-Class X by A4,Def2;
hence Y in Tarski-Class(X,A) by A1,A6,A7,Th13,CARD_1:44;
end; hence Tarski-Class(X,A) c= Tarski-Class X &
Tarski-Class X c= Tarski-Class(X,A) by Def4;
end;

theorem
Th22: ex A st Tarski-Class(X,A) = Tarski-Class X
proof
consider A such that
A1:  Tarski-Class(X,A) = Tarski-Class(X,succ A) by Th20;
take A;
thus thesis by A1,Th21;
end;

theorem
ex A st Tarski-Class(X,A) = Tarski-Class X &
for B st B in A holds Tarski-Class(X,B) <> Tarski-Class X
proof
defpred P[Ordinal] means Tarski-Class(X,\$1) = Tarski-Class X;
A1:  ex A st P[A] by Th22;
consider A such that
A2:  P[A] & for B st P[B] holds A c= B from Ordinal_Min(A1);
take A;
thus Tarski-Class(X,A) = Tarski-Class X by A2;
let B; assume B in A;
then not A c= B by ORDINAL1:7;
hence thesis by A2;
end;

theorem
Y <> X & Y in Tarski-Class X implies
ex A st not Y in Tarski-Class(X,A) & Y in Tarski-Class(X,succ A)
proof assume
A1:  Y <> X & Y in Tarski-Class X;
defpred P[Ordinal] means Y in Tarski-Class(X,\$1);
ex A st Tarski-Class(X,A) = Tarski-Class X by Th22;
then A2:  ex A st P[A] by A1;
consider A such that
A3:  P[A] & for B st P[B] holds A c= B from Ordinal_Min(A2);
A4:    not Y in { X } & Tarski-Class(X,{}) = { X } by A1,Lm1,TARSKI:def 1;
now assume A is_limit_ordinal;
then consider B such that
A5:    B in A & Y in Tarski-Class(X,B) by A3,A4,Th16;
A c= B by A3,A5;
end;
then consider B such that
A6:  A = succ B by ORDINAL1:42;
take B;
B in A by A6,ORDINAL1:10;
then not A c= B by ORDINAL1:7;
hence thesis by A3,A6;
end;

theorem
Th25: X is epsilon-transitive implies
for A st A <> {} holds Tarski-Class(X,A) is epsilon-transitive
proof assume
A1:  Y in X implies Y c= X;
defpred OnP[Ordinal] means
\$1 <> {} implies Tarski-Class(X,\$1) is epsilon-transitive;
A2:for A st for B st B in A holds OnP[B] holds OnP[A]
proof let A such that
A3:     for B st B in A holds OnP[B] and
A4:     A <> {};
let Y such that
A5:     Y in Tarski-Class(X,A);
A6:     now given B such that
A7:      A = succ B;
B in A by A7,ORDINAL1:10;
then A8:      B c= A & OnP[B] by A3,ORDINAL1:def 2;
then A9:      Tarski-Class(X,B) c= Tarski-Class(X,A) by Th19;
now assume not Y c= Tarski-Class(X,B);
then consider Z such that
A10:        Z in Tarski-Class(X,B) & (Y c= Z or Y = bool Z) by A5,A7,Th13;
A11:        now assume
A12:          Y = bool Z;
thus thesis
proof let x;
assume x in Y;
hence thesis by A7,A10,A12,Th13;
end;
end;
now assume
A13:          Y c= Z;
thus thesis
proof let x; assume A14: x in Y;
then A15:             x in Z by A13;
A16:             now assume B = {};
then Tarski-Class(X,B) = { X } by Lm1;
then A17:               Z = X by A10,TARSKI:def 1;
then x c= X by A1,A13,A14;
hence x in Tarski-Class(X,A) by A7,A10,A17,Th13;
end;
now assume B <> {};
then Z c= Tarski-Class(X,B) by A8,A10,ORDINAL1:def 2;
then x in Tarski-Class(X,B) by A15;
hence thesis by A9;
end;
hence thesis by A16;
end;
end;
hence thesis by A10,A11;
end;
hence thesis by A9,XBOOLE_1:1;
end;
now assume
A18:       for B holds A <> succ B;
then A is_limit_ordinal by ORDINAL1:42;
then consider B such that
A19:       B in A & Y in Tarski-Class(X,B) by A4,A5,Th16;
A20:      succ B c= A & succ B <> A & succ B <> {} &
Tarski-Class(X,B) c= Tarski-Class(X,succ B)
by A18,A19,Th18,ORDINAL1:33;
then succ B c< A by XBOOLE_0:def 8;
then A21:       succ B in A & succ B <> {} & Y in Tarski-Class(X,succ B) &
Tarski-Class(X,succ B) c= Tarski-Class(X,A)
by A19,A20,Th19,ORDINAL1:21;
then Tarski-Class(X,succ B) is epsilon-transitive by A3;
then Y c= Tarski-Class(X,succ B) by A19,A20,ORDINAL1:def 2;
hence thesis by A21,XBOOLE_1:1;
end;
hence thesis by A6;
end;
thus for A holds OnP[A] from Transfinite_Ind(A2);
end;

theorem
Tarski-Class(X,{}) in Tarski-Class(X,one) &
Tarski-Class(X,{}) <> Tarski-Class(X,one)
proof
A1:  Tarski-Class(X,{}) = { X } by Lm1;
then X in Tarski-Class(X,{}) by TARSKI:def 1;
then A2:  bool X in Tarski-Class X by Th7;
{ X } c= bool X
proof let a; assume a in { X }; then a = X by TARSKI:def 1;
hence a in bool X by ZFMISC_1:def 1;
end;
then { X } in Tarski-Class X by A2,Th6;
hence
A3:  Tarski-Class(X,{}) in Tarski-Class(X,one) by A1,Th13,ORDINAL2:def 4;
assume Tarski-Class(X,{}) = Tarski-Class(X,one);
end;

theorem
Th27: X is epsilon-transitive implies Tarski-Class X is epsilon-transitive
proof
consider A such that
A1:  Tarski-Class(X,A) = Tarski-Class X by Th22;
Tarski-Class(X,A) c= Tarski-Class(X,succ A) &
Tarski-Class(X,succ A) c= Tarski-Class X by Th18;
then A2:  Tarski-Class(X,A) = Tarski-Class(X,succ A) by A1,XBOOLE_0:def 10;
assume X is epsilon-transitive;
hence thesis by A1,A2,Th25;
end;

theorem
Th28: Y in Tarski-Class X implies Card Y <` Card Tarski-Class X
proof assume
A1:  Y in Tarski-Class X;
bool Y c= Tarski-Class X
proof let x;
assume x in bool Y;
hence x in Tarski-Class X by A1,Th6;
end;
then Card Y <` Card bool Y & Card bool Y <=` Card Tarski-Class X
by CARD_1:27,30;
hence Card Y <` Card Tarski-Class X;
end;

theorem
Th29: Y in Tarski-Class X implies not Y,Tarski-Class X are_equipotent
proof assume Y in Tarski-Class X;
then Card Y <` Card Tarski-Class X by Th28;
then Card Y <> Card Tarski-Class X;
hence thesis by CARD_1:21;
end;

theorem
Th30: x in Tarski-Class X & y in Tarski-Class X implies
{x} in Tarski-Class X & {x,y} in Tarski-Class X
proof assume
A1:  x in Tarski-Class X & y in Tarski-Class X;
then {x} c= bool x & bool x in Tarski-Class X by Th7,ZFMISC_1:80;
hence
A2:  {x} in Tarski-Class X by Th6;
then bool {x} = {{},{x}} & bool {x} in Tarski-Class X by Th7,ZFMISC_1:30;
then A3:  not {{},{x}},Tarski-Class X are_equipotent by Th29;
now assume
A4:    x <> y;
{{},{x}},{x,y} are_equipotent
proof
defpred C[set] means \$1 = {};
deffunc f(set) = x;
deffunc g(set) = y;
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;
take f;
thus f is one-to-one
proof let x1,x2 be set; assume x1 in dom f & x2 in dom f;
then {} <> {x} & (x1 = {} or x1 = {x}) & (x2 = {} or x2 = {x}) &
(x1 = {} implies f.x1 = x) & (x1 <> {} implies f.x1 = y) &
(x2 = {} implies f.x2 = x) & (x2 <> {} implies f.x2 = y)
by A5,TARSKI:def 2;
hence thesis by A4;
end;
thus dom f = {{},{x}} by A5;
thus rng f c= {x,y}
proof let z; assume z in rng f;
then consider u being set such that
A6:          u in dom f & z = f.u by FUNCT_1:def 5;
u = {} or u <> {};
then z = x or z = y by A5,A6;
hence thesis by TARSKI:def 2;
end;
let z; assume z in {x,y};
then A7:       z = x or z = y by TARSKI:def 2;
A8:       {} in dom f & {x} in dom f & {} <> {x} by A5,TARSKI:def 2;
then f.{} = x & f.{x} = y by A5;
hence z in rng f by A7,A8,FUNCT_1:def 5;
end;
then not {x,y},Tarski-Class X are_equipotent & {x,y} c= Tarski-Class X
by A1,A3,WELLORD2:22,ZFMISC_1:38;
hence thesis by Th8;
end;
hence thesis by A2,ENUMSET1:69;
end;

theorem
Th31: x in Tarski-Class X & y in Tarski-Class X implies [x,y] in
Tarski-Class X
proof assume x in Tarski-Class X & y in Tarski-Class X;
then {x,y} in Tarski-Class X & {x} in Tarski-Class X by Th30;
then {{x,y},{x}} in Tarski-Class X by Th30;
hence thesis by TARSKI:def 5;
end;

theorem
Y c= Tarski-Class X & Z c= Tarski-Class X implies [:Y,Z:] c= Tarski-Class X
proof assume
A1:  Y c= Tarski-Class X & Z c= Tarski-Class X;
let x; assume
A2:  x in [:Y,Z:];
then A3:  x = [x`1,x`2] by MCART_1:23;
x`1 in Y & x`2 in Z by A2,MCART_1:10; hence x in
Tarski-Class X by A1,A3,Th31;
end;

definition let A;
func Rank(A) means
:Def6:
ex L st it = last L & dom L = succ A & L.{} = {} &
(for C st succ C in succ A holds L.succ C = bool(L.C)) &
for C st C in succ A & C <> {} & C is_limit_ordinal
holds L.C = union rng(L|C);
correctness
proof
deffunc C(Ordinal,set) = bool \$2;
deffunc D(Ordinal,T-Sequence) = union rng \$2;
thus (ex x,L st x = last L & dom L = succ A & L.{} = {} &
(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.{} = {} &
(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.{} = {} &
(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 F(Ordinal) = Rank \$1;

Lm2:
now
deffunc C(Ordinal,set) = bool \$2;
deffunc D(Ordinal,T-Sequence) = union rng \$2;
A1:  for A,x holds x = F(A) iff
ex L st x = last L & dom L = succ A & L.{} = {} &
(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 Def6;
thus F({}) = {} from TS_Result0(A1);
thus for A holds F(succ A) = C(A,F(A)) from TS_ResultS(A1);
thus A <> {} & A is_limit_ordinal & dom L = A &
(for B st B in A holds L.B = Rank B) implies Rank A = union rng L
proof assume that
A2:    A <> {} & A is_limit_ordinal and
A3:    dom L = A and
A4:    for B st B in A holds L.B = F(B);
thus F(A) = D(A,L) from TS_ResultL(A1,A2,A3,A4);
end;
end;

theorem
Rank {} = {} by Lm2;

theorem
Rank succ A = bool Rank A by Lm2;

theorem
Th35: A <> {} & A is_limit_ordinal implies
for x holds x in Rank A iff ex B st B in A & x in Rank B
proof assume
A1:  A <> {} & A is_limit_ordinal;
consider L such that
A2:  dom L = A & for B st B in A holds L.B = F(B) from TS_Lambda;
A3:  Rank A = union rng L by A1,A2,Lm2;
let x;
thus x in Rank A implies ex B st B in A & x in Rank B
proof assume x in Rank A;
then consider Y such that
A4:     x in Y & Y in rng L by A3,TARSKI:def 4;
consider y such that
A5:     y in dom L & Y = L.y by A4,FUNCT_1:def 5;
reconsider y as Ordinal by A5,ORDINAL1:23;
take y;
thus thesis by A2,A4,A5;
end;
given B such that
A6:  B in A & x in Rank B;
L.B = Rank B by A2,A6;
then Rank B in rng L by A2,A6,FUNCT_1:def 5;
hence x in Rank A by A3,A6,TARSKI:def 4;
end;

theorem
Th36: X c= Rank A iff X in Rank succ A
proof
thus X c= Rank A implies X in Rank succ A
proof assume X c= Rank A;
then X in bool Rank A;
hence thesis by Lm2;
end;
assume X in Rank succ A;
then X in bool Rank A by Lm2;
hence X c= Rank A;
end;

theorem
Th37: Rank A is epsilon-transitive
proof
defpred P[Ordinal] means X in Rank \$1 implies X c= Rank \$1;
A1:for A st for B st B in A holds P[B] holds P[A]
proof let A such that
A2:     for B st B in A holds P[B];
let X such that
A3:     X in Rank A;
let x such that
A4:     x in X;
A5:     now assume
A6:      A is_limit_ordinal;
then consider B such that
A7:      B in A & X in Rank B by A3,Lm2,Th35;
X c= Rank B by A2,A7; hence x in Rank A by A4,A6,A7,Th35;
end;
now assume not A is_limit_ordinal;
then consider B such that
A8:      A = succ B by ORDINAL1:42;
B in A & X c= Rank B by A3,A8,Th36,ORDINAL1:10;
then x c= Rank B by A2,A4;
hence x in Rank A by A8,Th36;
end;
hence thesis by A5;
end;
for A holds P[A] from Transfinite_Ind(A1);
hence P[A];
end;

theorem
Th38: X in Rank A implies X c= Rank A
proof
Rank A is epsilon-transitive by Th37;
hence thesis by ORDINAL1:def 2;
end;

theorem
Rank A c= Rank succ A
proof
Rank A in bool Rank A by ZFMISC_1:def 1;
then Rank A in Rank succ A by Lm2;
hence thesis by Th38;
end;

theorem
Th40: union Rank A c= Rank A
proof let x; assume
x in union Rank A;
then consider X such that
A1:  x in X & X in Rank A by TARSKI:def 4;
X c= Rank A by A1,Th38;
hence x in Rank A by A1;
end;

theorem
X in Rank A implies union X in Rank A
proof assume
A1:  X in Rank A;
A2:  now given B such that
A3:   A = succ B;
X c= Rank B by A1,A3,Th36;
then union X c= union Rank B & union Rank B c= Rank B by Th40,ZFMISC_1:95
;
then union X c= Rank B by XBOOLE_1:1;
hence thesis by A3,Th36;
end;
now assume
A4:   A <> {} & for B holds A <> succ B;
then A5:   A is_limit_ordinal by ORDINAL1:42;
then consider B such that
A6:   B in A & X in Rank B by A1,A4,Th35;
X c= Rank B by A6,Th38;
then union X c= union Rank B & union Rank B c= Rank B by Th40,ZFMISC_1:95
;
then A7:    union X c= Rank B & succ B c= A & succ B <> A
by A4,A6,ORDINAL1:33,XBOOLE_1:1;
then succ B c< A by XBOOLE_0:def 8;
then union X in Rank succ B & succ B in A by A7,Th36,ORDINAL1:21;
hence thesis by A5,Th35;
end;
hence union X in Rank A by A1,A2,Lm2;
end;

theorem
Th42: A in B iff Rank A in Rank B
proof
defpred OnP[Ordinal,Ordinal] means \$1 in \$2 implies Rank \$1 in Rank \$2;
A1:  now let A;
defpred P[Ordinal] means OnP[A,\$1];
A2:  for B st for C st C in B holds P[C] holds P[B]
proof let B such that
A3:       for C st C in B holds OnP[A,C] and
A4:       A in B;
A5:       now given C such that
A6:        B = succ C;
C in B by A6,ORDINAL1:10;
then A7:        A in C implies Rank A in Rank C by A3;
now assume A8: not A in C;
A c= C & A <> C iff A c< C by XBOOLE_0:def 8;
hence Rank A = Rank C by A4,A6,A8,ORDINAL1:21,34;
end;
then Rank A c= Rank C by A7,Th38;
hence thesis by A6,Th36;
end;
now assume for C holds B <> succ C;
then A9:        B is_limit_ordinal & B <> succ A by ORDINAL1:42;
succ A c= B & Rank A c= Rank A by A4,ORDINAL1:33;
then succ A c< B by A9,XBOOLE_0:def 8;
then succ A in B & Rank A in Rank succ A by Th36,ORDINAL1:21;
hence thesis by A9,Th35;
end;
hence thesis by A5;
end;
thus for B holds P[B] from Transfinite_Ind(A2);
end;
hence OnP[A,B];
assume
A10:  Rank A in Rank B & not A in B;
then B in A or B = A by ORDINAL1:24;
end;

theorem
Th43: A c= B iff Rank A c= Rank B
proof
thus A c= B implies Rank A c= Rank B
proof A1: A c< B iff A c= B & A <> B by XBOOLE_0:def 8;
assume A c= B;
then A = B or A in B by A1,ORDINAL1:21;
then Rank A = Rank B or Rank A in Rank B by Th42;
hence thesis by Th38;
end;
assume
A2:  Rank A c= Rank B & not A c= B;
then B in A by ORDINAL1:26;
then Rank B in Rank A by Th42;
end;

theorem
Th44: A c= Rank A
proof
defpred P[Ordinal] means \$1 c= Rank \$1;
A1: P[{}] by XBOOLE_1:2;
A2:  P[B] implies P[succ B]
proof assume B c= Rank B;
then B in Rank succ B by Th36;
then B c= Rank succ B & {B} c= Rank succ B by Th38,ZFMISC_1:37;
then B \/ {B} c= Rank succ B by XBOOLE_1:8;
hence thesis by ORDINAL1:def 1;
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
A5:    for B st B in A holds B c= Rank B;
let x; assume
A6:    x in A;
then reconsider B = x as Ordinal by ORDINAL1:23;
succ B in A by A4,A6,ORDINAL1:41;
then B c= Rank B & succ B c= A by A5,A6,ORDINAL1:def 2;
then B in Rank succ B & Rank succ B c= Rank A by Th36,Th43;
hence thesis;
end;
for B holds P[B] from Ordinal_Ind(A1,A2,A3);
hence thesis;
end;

theorem
for A,X st X in Rank A holds
not X,Rank A are_equipotent & Card X <` Card Rank A
proof
defpred OnP[Ordinal] means
for X st X in Rank \$1 holds not X,Rank \$1 are_equipotent;
A1:for A st for B st B in A holds OnP[B] holds OnP[A]
proof let A such that
A2:     for B st B in A holds OnP[B];
let X; assume
A3:     X in Rank A;
A4:     now given B such that
A5:      A = succ B;
B in A by A5,ORDINAL1:10;
then B c= A & Rank succ B = bool Rank B by Lm2,ORDINAL1:def 2;
then X c= Rank B & not Rank B,Rank A are_equipotent & Rank B c= Rank
A
by A3,A5,Th43,CARD_1:29;
hence thesis by CARD_1:44;
end;
now assume
A6:      A <> {} & for B holds A <> succ B;
then A is_limit_ordinal by ORDINAL1:42;
then consider B such that
A7:      B in A & X in Rank B by A3,A6,Th35;
A8:      not X,Rank B are_equipotent by A2,A7;
Rank B in Rank A by A7,Th42;
then X c= Rank B & Rank B c= Rank A by A7,Th38;
hence thesis by A8,CARD_1:44;
end;
hence thesis by A3,A4,Lm2;
end;
A9:  for A holds OnP[A] from Transfinite_Ind(A1);
let A,X; assume A10: X in Rank A;
then X c= Rank A & not X,Rank A are_equipotent by A9,Th38;
then Card X <=` Card Rank A & Card X <> Card Rank A by CARD_1:21,27;
hence thesis by A9,A10,CARD_1:13;
end;

theorem
X c= Rank A iff bool X c= Rank succ A
proof
thus X c= Rank A implies bool X c= Rank succ A
proof assume
A1:     X c= Rank A;
let x;
assume x in bool X;
then x c= Rank A & Rank succ A = bool Rank A by A1,Lm2,XBOOLE_1:1;
hence thesis;
end;
assume
A2:  bool X c= Rank succ A;
let x; assume x in X;
then { x } c= X by ZFMISC_1:37;
then { x } in bool X & Rank succ A = bool Rank A by Lm2;
then { x } c= Rank A & x in { x } by A2,TARSKI:def 1;
hence x in Rank A;
end;

theorem
Th47: X c= Y & Y in Rank A implies X in Rank A
proof assume
A1:  X c= Y & Y in Rank A;
A2:  now given B such that
A3:   A = succ B;
A4:   Rank succ B = bool Rank B by Lm2;
then X c= Rank B by A1,A3,XBOOLE_1:1;
hence X in Rank A by A3,A4;
end;
now assume for B holds A <> succ B;
then A5:   A is_limit_ordinal by ORDINAL1:42;
then consider B such that
A6:   B in A & Y in Rank B by A1,Lm2,Th35;
Y c= Rank B by A6,Th38;
then X c= Rank B by A1,XBOOLE_1:1;
then X in bool Rank B & bool Rank B = Rank succ B & succ B in A
by A5,A6,Lm2,ORDINAL1:41;
hence X in Rank A by A5,Th35;
end;
hence thesis by A2;
end;

theorem
Th48: X in Rank A iff bool X in Rank succ A
proof
thus X in Rank A implies bool X in Rank succ A
proof assume A1: X in Rank A;
bool X c= Rank A
proof let x;
assume x in bool X;
hence x in Rank A by A1,Th47;
end;
hence thesis by Th36;
end;
assume bool X in Rank succ A;
then X in bool X & bool X c= Rank A by Th36,ZFMISC_1:def 1;
hence thesis;
end;

theorem
Th49: x in Rank A iff {x} in Rank succ A
proof
(x in Rank A iff {x} c= Rank A) &
({x} c= Rank A iff {x} in Rank succ A) by Th36,ZFMISC_1:37;
hence thesis;
end;

theorem
Th50: x in Rank A & y in Rank A iff {x,y} in Rank succ A
proof
(x in Rank A & y in Rank A iff {x,y} c= Rank A) &
({x,y} c= Rank A iff {x,y} in Rank succ A) by Th36,ZFMISC_1:38;
hence thesis;
end;

theorem
x in Rank A & y in Rank A iff [x,y] in Rank succ succ A
proof
(x in Rank A iff {x} in Rank succ A) &
(x in Rank A & y in Rank A iff {x,y} in Rank succ A) &
({x} in Rank succ A & {x,y} in Rank succ A iff
{{x,y},{x}} in Rank succ succ A) & {{x,y},{x}} = [x,y]
by Th49,Th50,TARSKI:def 5;
hence thesis;
end;

theorem
Th52: X is epsilon-transitive &
Rank A /\ Tarski-Class X = Rank succ A /\ Tarski-Class X implies
Tarski-Class X c= Rank A
proof assume that
A1:  X is epsilon-transitive and
A2:  Rank A /\ Tarski-Class X = Rank succ A /\ Tarski-Class X;
given x such that
A3:  x in Tarski-Class X & not x in Rank A;
x in (Tarski-Class X) \ Rank A by A3,XBOOLE_0:def 4;
then consider Y such that
A4:  Y in (Tarski-Class X) \ Rank A and
A5:  not ex x st x in (Tarski-Class X) \ Rank A & x in Y by TARSKI:7;
Tarski-Class X is epsilon-transitive & Y in Tarski-Class X
by A1,A4,Th27,XBOOLE_0:def 4;
then A6:  Y c= Tarski-Class X by ORDINAL1:def 2;
Y c= Rank A
proof let x; assume x in Y;
then not x in (Tarski-Class X) \ Rank A & x in Tarski-Class X by A5,A6;
hence x in Rank A by XBOOLE_0:def 4;
end;
then Y in Rank succ A & Y in Tarski-Class X by A4,Th36,XBOOLE_0:def 4;
then Y in Rank succ A /\ Tarski-Class X & not Y in
Rank A by A4,XBOOLE_0:def 3,def 4;
end;

theorem
Th53: X is epsilon-transitive implies ex A st Tarski-Class X c= Rank A
proof assume
A1:  X is epsilon-transitive;
assume
A2: not Tarski-Class X c= Rank A;
A3:  Rank A /\ Tarski-Class X <> Rank succ A /\ Tarski-Class X
proof not Tarski-Class X c= Rank A by A2;
hence thesis by A1,Th52;
end;
defpred P[set] means ex A st \$1 in Rank A;
consider Power being set such that
A4:  x in Power iff x in Tarski-Class X & P[x] from Separation;
defpred P[set,set] means
ex A st \$2 = A & not \$1 in Rank A & \$1 in Rank succ A;
A5:  for x,y,z st P[x,y] & P[x,z] holds y = z
proof let x,y,z;
given A1 being Ordinal such that
A6:    y = A1 & not x in Rank A1 & x in Rank succ A1;
given A2 being Ordinal such that
A7:    z = A2 & not x in Rank A2 & x in Rank succ A2;
assume y <> z;
then A1 in A2 or A2 in A1 by A6,A7,ORDINAL1:24;
then A8:    succ A1 c= A2 or succ A2 c= A1 by ORDINAL1:33;
now assume succ A1 c= A2;
then Rank succ A1 c= Rank A2 by Th43;
end;
then Rank succ A2 c= Rank A1 by A8,Th43;
end;
consider Y such that
A9:  x in Y iff ex y st y in Power & P[y,x] from Fraenkel(A5);
now let A;
Rank A /\ Tarski-Class X <> Rank succ A /\ Tarski-Class X by A3;
then consider y such that
A10:    not (y in Rank A /\ Tarski-Class X iff y in
Rank succ A /\ Tarski-Class X)
by TARSKI:2;
A in succ A by ORDINAL1:10;
then A c= succ A by ORDINAL1:def 2;
then Rank A c= Rank succ A by Th43;
then Rank A /\ Tarski-Class X c= Rank succ A /\
Tarski-Class X by XBOOLE_1:26;
then y in Rank succ A & y in Tarski-Class X &
(not y in Rank A or not y in Tarski-Class X) by A10,XBOOLE_0:def 3;
then y in Power & P[y,A] by A4;
hence A in Y by A9;
end;
end;

theorem
Th54: X is epsilon-transitive implies union X c= X
proof assume
A1:  Y in X implies Y c= X;
let x; assume x in union X;
then consider Y such that
A2:  x in Y & Y in X by TARSKI:def 4;
Y c= X by A1,A2;
hence thesis by A2;
end;

theorem
Th55: X is epsilon-transitive & Y is epsilon-transitive implies
X \/ Y is epsilon-transitive
proof assume that
A1:  Z in X implies Z c= X and
A2:  Z in Y implies Z c= Y;
let Z; assume Z in X \/ Y;
then Z in X or Z in Y by XBOOLE_0:def 2;
then (Z c= X or Z c= Y) & X c= X \/ Y & Y c= X \/ Y by A1,A2,XBOOLE_1:7;
hence thesis by XBOOLE_1:1;
end;

theorem
X is epsilon-transitive & Y is epsilon-transitive implies
X /\ Y is epsilon-transitive
proof assume that
A1:  Z in X implies Z c= X and
A2:  Z in Y implies Z c= Y;
let Z; assume Z in X /\ Y;
then Z in X & Z in Y by XBOOLE_0:def 3;
then Z c= X & Z c= Y by A1,A2;
hence thesis by XBOOLE_1:19;
end;

reserve k,n for Nat;

deffunc f(set,set) = union \$2;

definition let X;
func the_transitive-closure_of X -> set means
:Def7:
x in it iff ex f,n st x in f.n & dom f = NAT & f.0 = X &
for k holds f.(k+1) = union(f.k);
existence
proof
consider f such that
A1:   dom f = NAT & f.0 = X &
for n being Element of NAT holds f.(n+1) = f(n,f.n) from LambdaRecEx;
take UNI = union rng f;
let x;
thus x in UNI implies
ex f,n st x in f.n & dom f = NAT & f.0 = X &
for k holds f.(k+1) = union(f.k)
proof assume x in UNI;
then consider Y such that
A2:      x in Y & Y in rng f by TARSKI:def 4;
consider y such that
A3:      y in dom f & Y = f.y by A2,FUNCT_1:def 5;
reconsider y as Element of NAT by A1,A3;
take f,y; thus thesis by A1,A2,A3;
end;
deffunc f(set,set) = union \$2;
given g,n such that
A4:   x in g.n and
A5:   dom g = NAT & g.0 = X &
for k holds g.(k+1) = f(k,g.k);
A6:   dom f = NAT & f.0 = X &
for n holds f.(n+1) = f(n,f.n) by A1;
g = f from LambdaRecUn(A5,A6);
then g.n in rng f by A1,FUNCT_1:def 5;
hence x in UNI by A4,TARSKI:def 4;
end;
uniqueness
proof
defpred P[set] means
ex f,n st \$1 in f.n & dom f = NAT & f.0 = X &
for k holds f.(k+1) = union(f.k);
let U1,U2 be set such that
A7:  x in U1 iff P[x] and
A8:  x in U2 iff P[x];
thus U1 = U2 from Extensionality(A7,A8);
end;
end;

canceled;

theorem
Th58: the_transitive-closure_of X is epsilon-transitive
proof let Y; assume Y in the_transitive-closure_of X;
then consider f,n such that
A1:  Y in f.n and
A2:  dom f = NAT & f.0 = X &
for k holds f.(k+1) = union(f.k) by Def7;
A3:  f.(n+1) = union(f.n) by A2;
let x; assume x in Y;
then x in union(f.n) by A1,TARSKI:def 4;
hence x in the_transitive-closure_of X by A2,A3,Def7;
end;

theorem
Th59: X c= the_transitive-closure_of X
proof let x such that
A1:  x in X;
ex f st dom f = NAT & f.0 = X &
for n being Element of NAT holds f.(n+1) = f(n,f.n)
from LambdaRecEx;
hence x in the_transitive-closure_of X by A1,Def7;
end;

theorem
Th60: X c= Y & Y is epsilon-transitive implies
the_transitive-closure_of X c= Y
proof assume
A1:  X c= Y & Y is epsilon-transitive;
let x; assume x in the_transitive-closure_of X;
then consider f,n such that
A2:  x in f.n & dom f = NAT & f.0 = X &
for k holds f.(k+1) = union(f.k) by Def7;
defpred P[Nat] means f.\$1 c= Y;
A3:  P[0] by A1,A2;
A4:  for k st P[k] holds P[k+1]
proof let k; assume f.k c= Y;
then union (f.k) c= union Y & f.(k+1) = union (f.k) & f.(k+1) = f.(k+1)
&
union Y c= Y by A1,A2,Th54,ZFMISC_1:95;
hence thesis by XBOOLE_1:1;
end;
P[k] from Ind(A3,A4);
then f.n = f.n & f.n c= Y;
hence x in Y by A2;
end;

theorem
Th61: (for Z st X c= Z & Z is epsilon-transitive holds Y c= Z) & X c= Y &
Y is epsilon-transitive implies the_transitive-closure_of X = Y
proof assume
A1:  (for Z st X c= Z & Z is epsilon-transitive holds Y c= Z);
assume X c= Y & Y is epsilon-transitive;
hence the_transitive-closure_of X c= Y by Th60;
the_transitive-closure_of X is epsilon-transitive &
X c= the_transitive-closure_of X by Th58,Th59;
hence Y c= the_transitive-closure_of X by A1;
end;

theorem
Th62: X is epsilon-transitive implies the_transitive-closure_of X = X
proof
(for Z st X c= Z & Z is epsilon-transitive holds X c= Z) & X c= X;
hence thesis by Th61;
end;

theorem
the_transitive-closure_of {} = {} by Th62;

theorem
the_transitive-closure_of A = A by Th62;

theorem Th65:
X c= Y implies the_transitive-closure_of X c= the_transitive-closure_of Y
proof assume
A1:  X c= Y;
Y c= the_transitive-closure_of Y by Th59;
then X c= the_transitive-closure_of Y &
the_transitive-closure_of Y is epsilon-transitive by A1,Th58,XBOOLE_1:1;
hence thesis by Th60;
end;

theorem
the_transitive-closure_of the_transitive-closure_of X =
the_transitive-closure_of X
proof
the_transitive-closure_of X is epsilon-transitive by Th58;
hence thesis by Th62;
end;

theorem
the_transitive-closure_of (X \/ Y) =
the_transitive-closure_of X \/ the_transitive-closure_of Y
proof
X c= the_transitive-closure_of X & Y c= the_transitive-closure_of Y
by Th59;
then X \/ Y c= the_transitive-closure_of X \/ the_transitive-closure_of Y
&
the_transitive-closure_of X is epsilon-transitive &
the_transitive-closure_of Y is epsilon-transitive by Th58,XBOOLE_1:13
;
then the_transitive-closure_of (X \/ Y) c=
the_transitive-closure_of
(the_transitive-closure_of X \/ the_transitive-closure_of Y) &
the_transitive-closure_of X \/ the_transitive-closure_of Y
is epsilon-transitive by Th55,Th65;
hence the_transitive-closure_of (X \/ Y) c=
the_transitive-closure_of X \/ the_transitive-closure_of Y by Th62;
X c= X \/ Y & Y c= X \/ Y by XBOOLE_1:7;
then the_transitive-closure_of X c= the_transitive-closure_of (X \/ Y) &
the_transitive-closure_of Y c= the_transitive-closure_of (X \/ Y) by Th65;
hence thesis by XBOOLE_1:8;
end;

theorem
the_transitive-closure_of (X /\ Y) c=
the_transitive-closure_of X /\ the_transitive-closure_of Y
proof
X /\ Y c= X & X /\ Y c= Y by XBOOLE_1:17;
then the_transitive-closure_of (X /\ Y) c= the_transitive-closure_of X &
the_transitive-closure_of (X /\ Y) c= the_transitive-closure_of Y by Th65;
hence thesis by XBOOLE_1:19;
end;

theorem
Th69: ex A st X c= Rank A
proof the_transitive-closure_of X is epsilon-transitive by Th58;
then consider A such that
A1:  Tarski-Class the_transitive-closure_of X c= Rank A by Th53;
take A;
the_transitive-closure_of X in Tarski-Class the_transitive-closure_of X &
X c= the_transitive-closure_of X by Th5,Th59;
then X in Tarski-Class the_transitive-closure_of X by Th6;
then X in Rank A & Rank A is epsilon-transitive by A1,Th37;
hence thesis by ORDINAL1:def 2;
end;

definition let X;
func the_rank_of X -> Ordinal means
:Def8:   X c= Rank it & for B st X c= Rank B holds it c= B;
existence
proof
defpred P[Ordinal] means X c= Rank \$1;
A1:   ex A st P[A] by Th69;
thus ex A st P[A] & for B st P[B] holds A c= B from Ordinal_Min(A1);
end;
uniqueness
proof let A1,A2 be Ordinal such that
A2:  X c= Rank A1 & for B st X c= Rank B holds A1 c= B and
A3:  X c= Rank A2 & for B st X c= Rank B holds A2 c= B;
thus A1 c= A2 & A2 c= A1 by A2,A3;
end;
end;

canceled;

theorem
Th71: the_rank_of bool X = succ the_rank_of X
proof
A1:  X c= Rank the_rank_of X &
for A st X c= Rank A holds the_rank_of X c= A by Def8;
A2:  bool X c= Rank succ the_rank_of X
proof let x;
assume x in bool X;
then x c= Rank the_rank_of X &
bool Rank the_rank_of X = Rank succ the_rank_of X by A1,Lm2,XBOOLE_1:1;
hence thesis;
end;
for A st bool X c= Rank A holds succ the_rank_of X c= A
proof let A such that
A3:     bool X c= Rank A;
defpred P[Ordinal] means X in Rank \$1;
A4: X in bool X by ZFMISC_1:def 1;
then A5:     ex A st P[A] by A3;
consider B such that
A6:     P[B] & for C st P[C] holds B c= C from Ordinal_Min(A5);
now assume for C holds B <> succ C;
then B is_limit_ordinal by ORDINAL1:42;
then consider C such that
A7:       C in B & X in Rank C by A6,Lm2,Th35;
B c= C by A6,A7;
end;
then consider C such that
A8:     B = succ C;
X c= Rank C by A6,A8,Th36;
then the_rank_of X c= C by Def8;
then the_rank_of X in B by A8,ORDINAL1:34;
then succ the_rank_of X c= B & B c= A by A3,A4,A6,ORDINAL1:33;
hence thesis by XBOOLE_1:1;
end;
hence thesis by A2,Def8;
end;

theorem
the_rank_of Rank A = A
proof
Rank A c= Rank A & for B st Rank A c= Rank B holds A c= B by Th43;
hence thesis by Def8;
end;

theorem
Th73: X c= Rank A iff the_rank_of X c= A
proof
thus X c= Rank A implies the_rank_of X c= A by Def8;
assume the_rank_of X c= A;
then Rank the_rank_of X c= Rank A & X c= Rank the_rank_of X by Def8,Th43;
hence thesis by XBOOLE_1:1;
end;

theorem
Th74: X in Rank A iff the_rank_of X in A
proof
thus X in Rank A implies the_rank_of X in A
proof assume
X in Rank A;
then bool X in Rank succ A by Th48;
then bool X c= Rank A & the_rank_of bool X = succ the_rank_of X
by Th36,Th71;
then the_rank_of X in the_rank_of bool X & the_rank_of bool X c= A
by Def8,ORDINAL1:10;
hence thesis;
end;
assume the_rank_of X in A;
then succ the_rank_of X c= A & X c= Rank the_rank_of X by Def8,ORDINAL1:33
;
then X in Rank succ the_rank_of X & Rank succ the_rank_of X c= Rank A by
Th36,Th43;
hence thesis;
end;

theorem
X c= Y implies the_rank_of X c= the_rank_of Y
proof assume
A1:  X c= Y;
Y c= Rank the_rank_of Y by Def8;
then X c= Rank the_rank_of Y by A1,XBOOLE_1:1;
hence thesis by Def8;
end;

theorem
Th76: X in Y implies the_rank_of X in the_rank_of Y
proof assume
A1:  X in Y;
Y c= Rank the_rank_of Y by Def8; hence thesis by A1,Th74;
end;

theorem
Th77: the_rank_of X c= A iff for Y st Y in X holds the_rank_of Y in A
proof
set R = the_rank_of X;
A1:  X c= Rank R & for B st X c= Rank B holds R c= B by Def8;
thus the_rank_of X c= A implies for Y st Y in X holds the_rank_of Y in A
proof assume
A2:     the_rank_of X c= A;
let Y; assume Y in X;
then Y in Rank R & Rank R c= Rank A by A1,A2,Th43;
hence the_rank_of Y in A by Th74;
end;
assume
A3:  for Y st Y in X holds the_rank_of Y in A;
X c= Rank A
proof let x;
assume x in X;
then the_rank_of x in A by A3;
hence x in Rank A by Th74;
end;
hence thesis by Def8;
end;

theorem
Th78: A c= the_rank_of X iff for B st B in A ex Y st Y in
X & B c= the_rank_of Y
proof
thus A c= the_rank_of X implies
for B st B in A ex Y st Y in X & B c= the_rank_of Y
proof assume
A1:     A c= the_rank_of X;
let B; assume B in A;
then not the_rank_of X c= B by A1,ORDINAL1:7;
then not X c= Rank B by Def8;
then A2:     X \ Rank B <> {} by XBOOLE_1:37;
consider x being Element of X \ Rank B;
take x;
A3:     x in X & not x in Rank B by A2,XBOOLE_0:def 4;
thus x in X by A2,XBOOLE_0:def 4;
not the_rank_of x in B by A3,Th74;
hence thesis by ORDINAL1:26;
end;
assume
A4:  for B st B in A ex Y st Y in X & B c= the_rank_of Y;
let x; assume
A5:  x in A;
then reconsider x as Ordinal by ORDINAL1:23;
consider Y such that
A6:  Y in X & x c= the_rank_of Y by A4,A5;
the_rank_of Y in the_rank_of X by A6,Th76;
hence thesis by A6,ORDINAL1:22;
end;

theorem
the_rank_of X = {} iff X = {}
proof
thus the_rank_of X = {} implies X = {}
proof assume the_rank_of X = {};
then X c= Rank {} & Rank {} = {} by Def8,Lm2;
hence X = {} by XBOOLE_1:3;
end;
assume
X = {};
then for Y st Y in X holds the_rank_of Y in {};
hence the_rank_of X c= {} by Th77;
thus {} c= the_rank_of X by XBOOLE_1:2;
end;

theorem
Th80: the_rank_of X = succ A implies ex Y st Y in X & the_rank_of Y = A
proof assume
A1:  the_rank_of X = succ A;
then A in succ A & succ A c= the_rank_of X by ORDINAL1:10;
then consider Y such that
A2:  Y in X & A c= the_rank_of Y by Th78;
take Y;
the_rank_of Y in the_rank_of X by A2,Th76;
then the_rank_of Y c= A by A1,ORDINAL1:34;
hence thesis by A2,XBOOLE_0:def 10;
end;

theorem
the_rank_of A = A
proof A c= Rank A by Th44;
hence the_rank_of A c= A by Th73;
defpred P[Ordinal] means \$1 c= the_rank_of \$1;
A1:  for A st for B st B in A holds P[B] holds P[A]
proof let A such that
A2:     for B st B in A holds B c= the_rank_of B;
now let B such that
A3:       B in A;
reconsider Y = B as set;
take Y; thus Y in A & B c= the_rank_of Y by A2,A3;
end;
hence thesis by Th78;
end;
P[B] from Transfinite_Ind(A1);
hence thesis;
end;

theorem
the_rank_of Tarski-Class X <> {} &
the_rank_of Tarski-Class X is_limit_ordinal
proof
A1:  Tarski-Class X c= Rank the_rank_of Tarski-Class X &
for A st Tarski-Class X c= Rank A holds the_rank_of Tarski-Class X c= A
by Def8;
thus the_rank_of Tarski-Class X <> {}
proof assume the_rank_of Tarski-Class X = {};
then Tarski-Class X c= {} by Def8,Lm2;
end;
assume not thesis;
then consider A such that
A2:  the_rank_of Tarski-Class X = succ A by ORDINAL1:42;
consider Y such that
A3:  Y in Tarski-Class X & the_rank_of Y = A by A2,Th80;
A4:    bool Y in Tarski-Class X & the_rank_of bool Y = succ A
by A3,Th7,Th71;
then bool Y c= Rank A by A1,A2,Th36;
then succ A c= A by A4,Def8;
then A in A by ORDINAL1:33;