:: CLASSES1 semantic presentation

begin


definition
let B be set ;
attrB is subset-closed  means :Def1: :: CLASSES1:def 1
 for X, Y being set st X in B & Y c= X holds
Y in B;
end;

:: deftheorem Def1 defines subset-closed CLASSES1:def_1_:_
 for B being set holds
( B is subset-closed iff for X, Y being set st X in B & Y c= X holds
Y in B );

definition
let B be set ;
attrB is Tarski  means :Def2: :: CLASSES1:def 2
( B is subset-closed & ( for X being set st X in B holds
bool X in B ) & ( for X being set holds
( not X c= B or X,B are_equipotent or X in B ) ) );
end;

:: deftheorem Def2 defines Tarski CLASSES1:def_2_:_
 for B being set holds
( B is Tarski iff ( B is subset-closed & ( for X being set st X in B holds
bool X in B ) & ( for X being set holds
( not X c= B or X,B are_equipotent or X in B ) ) ) );

definition
let A, B be set ;
predB is_Tarski-Class_of A means :Def3: :: CLASSES1:def 3
( A in B & B is Tarski );
end;

:: deftheorem Def3 defines is_Tarski-Class_of CLASSES1:def_3_:_
 for A, B being set holds
( B is_Tarski-Class_of A iff ( A in B & B is Tarski ) );

definition
let A be set ;
func Tarski-Class A ->  set  means :Def4: :: CLASSES1:def 4
( it is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds
it c= D ) );
existence
 ex b1 being set st
( b1 is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds
b1 c= D ) )
proof
consider Big being set  such that
A1: A in Big and
A2: for X, Y being set st X in Big & Y c= X holds
Y in Big and
A3: ( ( for X being set st X in Big holds
bool X in Big ) & ( for X being set holds
( not X c= Big or X,Big are_equipotent or X in Big ) ) ) by ZFMISC_1:112;
 Big is subset-closed by A2, Def1;
then A4: Big is Tarski by A3, Def2;
defpred S1[ set ] means $1 is_Tarski-Class_of A;
consider Classes being set  such that
A5: for X being set holds
( X in Classes iff ( X in bool Big & S1[X] ) ) from XBOOLE_0:sch_1();
set IT = meet Classes;
A6: ( Big in bool Big & Big is_Tarski-Class_of A ) by A1, A4, Def3, ZFMISC_1:def_1;
then A7: Big in Classes by A5;
A8: Classes <> {} by A5, A6;
A9: now__::_thesis:_for_X_being_set_st_X_in_Classes_holds_
A_in_X
let X be set ; ::_thesis: ( X in Classes implies A in X )
assume  X in Classes ; ::_thesis: A in X
then  X is_Tarski-Class_of A by A5;
hence  A in X by Def3; ::_thesis: verum
end;
then A10: A in meet Classes by A8, SETFAM_1:def_1;
take  meet Classes ; ::_thesis: ( meet Classes is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds
meet Classes c= D ) )
thus  A in meet Classes by A8, A9, SETFAM_1:def_1; :: according to CLASSES1:def_3 ::_thesis: ( meet Classes is Tarski & ( for D being set st D is_Tarski-Class_of A holds
meet Classes c= D ) )
thus A11: for X, Y being set st X in meet Classes & Y c= X holds
Y in meet Classes :: according to CLASSES1:def_1,CLASSES1:def_2 ::_thesis: ( ( for X being set st X in meet Classes holds
bool X in meet Classes ) & ( for X being set holds
( not X c= meet Classes or X, meet Classes are_equipotent or X in meet Classes ) ) & ( for D being set st D is_Tarski-Class_of A holds
meet Classes c= D ) )
proof
let X, Y be set ; ::_thesis: ( X in meet Classes & Y c= X implies Y in meet Classes )
assume that
A12: X in meet Classes and
A13: Y c= X ; ::_thesis: Y in meet Classes
now__::_thesis:_for_Z_being_set_st_Z_in_Classes_holds_
Y_in_Z
let Z be set ; ::_thesis: ( Z in Classes implies Y in Z )
assume A14: Z in Classes ; ::_thesis: Y in Z
then  Z is_Tarski-Class_of A by A5;
then  Z is Tarski by Def3;
then A15: Z is subset-closed by Def2;
 X in Z by A12, A14, SETFAM_1:def_1;
hence  Y in Z by A13, A15, Def1; ::_thesis: verum
end;
hence  Y in meet Classes by A8, SETFAM_1:def_1; ::_thesis: verum
end;
thus A16: for X being set st X in meet Classes holds
bool X in meet Classes ::_thesis: ( ( for X being set holds
( not X c= meet Classes or X, meet Classes are_equipotent or X in meet Classes ) ) & ( for D being set st D is_Tarski-Class_of A holds
meet Classes c= D ) )
proof
let X be set ; ::_thesis: ( X in meet Classes implies bool X in meet Classes )
assume A17: X in meet Classes ; ::_thesis: bool X in meet Classes
now__::_thesis:_for_Z_being_set_st_Z_in_Classes_holds_
bool_X_in_Z
let Z be set ; ::_thesis: ( Z in Classes implies bool X in Z )
assume A18: Z in Classes ; ::_thesis: bool X in Z
then  Z is_Tarski-Class_of A by A5;
then A19: Z is Tarski by Def3;
 X in Z by A17, A18, SETFAM_1:def_1;
hence  bool X in Z by A19, Def2; ::_thesis: verum
end;
hence  bool X in meet Classes by A8, SETFAM_1:def_1; ::_thesis: verum
end;
thus A20: for X being set holds
( not X c= meet Classes or X, meet Classes are_equipotent or X in meet Classes ) ::_thesis: for D being set st D is_Tarski-Class_of A holds
meet Classes c= D
proof
let X be set ; ::_thesis: ( not X c= meet Classes or X, meet Classes are_equipotent or X in meet Classes )
assume that
A21: X c= meet Classes and
A22: not X, meet Classes are_equipotent ; ::_thesis: X in meet Classes
now__::_thesis:_for_Z_being_set_st_Z_in_Classes_holds_
X_in_Z
let Z be set ; ::_thesis: ( Z in Classes implies X in Z )
assume A23: Z in Classes ; ::_thesis: X in Z
then  Z is_Tarski-Class_of A by A5;
then A24: Z is Tarski by Def3;
A25: meet Classes c= Z by A23, SETFAM_1:3;
then  X c= Z by A21, XBOOLE_1:1;
then  ( X,Z are_equipotent or X in Z ) by A24, Def2;
hence  X in Z by A21, A22, A25, CARD_1:24; ::_thesis: verum
end;
hence  X in meet Classes by A8, SETFAM_1:def_1; ::_thesis: verum
end;
let D be set ; ::_thesis: ( D is_Tarski-Class_of A implies meet Classes c= D )
assume A26: D is_Tarski-Class_of A ; ::_thesis: meet Classes c= D
then A27: A in D by Def3;
A28: D is Tarski by A26, Def3;
then A29: D is subset-closed by Def2;
A30: (meet Classes) /\ D is_Tarski-Class_of A
proof
thus  A in (meet Classes) /\ D by A10, A27, XBOOLE_0:def_4; :: according to CLASSES1:def_3 ::_thesis: (meet Classes) /\ D is Tarski
thus  for X, Y being set st X in (meet Classes) /\ D & Y c= X holds
Y in (meet Classes) /\ D :: according to CLASSES1:def_1,CLASSES1:def_2 ::_thesis: ( ( for X being set st X in (meet Classes) /\ D holds
bool X in (meet Classes) /\ D ) & ( for X being set holds
( not X c= (meet Classes) /\ D or X,(meet Classes) /\ D are_equipotent or X in (meet Classes) /\ D ) ) )
proof
let X, Y be set ; ::_thesis: ( X in (meet Classes) /\ D & Y c= X implies Y in (meet Classes) /\ D )
assume that
A31: X in (meet Classes) /\ D and
A32: Y c= X ; ::_thesis: Y in (meet Classes) /\ D
A33: X in meet Classes by A31, XBOOLE_0:def_4;
A34: X in D by A31, XBOOLE_0:def_4;
A35: Y in meet Classes by A11, A32, A33;
 Y in D by A29, A32, A34, Def1;
hence  Y in (meet Classes) /\ D by A35, XBOOLE_0:def_4; ::_thesis: verum
end;
thus  for X being set st X in (meet Classes) /\ D holds
bool X in (meet Classes) /\ D ::_thesis: for X being set holds
( not X c= (meet Classes) /\ D or X,(meet Classes) /\ D are_equipotent or X in (meet Classes) /\ D )
proof
let X be set ; ::_thesis: ( X in (meet Classes) /\ D implies bool X in (meet Classes) /\ D )
assume A36: X in (meet Classes) /\ D ; ::_thesis: bool X in (meet Classes) /\ D
then A37: X in meet Classes by XBOOLE_0:def_4;
A38: X in D by A36, XBOOLE_0:def_4;
A39: bool X in meet Classes by A16, A37;
 bool X in D by A28, A38, Def2;
hence  bool X in (meet Classes) /\ D by A39, XBOOLE_0:def_4; ::_thesis: verum
end;
let X be set ; ::_thesis: ( not X c= (meet Classes) /\ D or X,(meet Classes) /\ D are_equipotent or X in (meet Classes) /\ D )
assume that
A40: X c= (meet Classes) /\ D and
A41: not X,(meet Classes) /\ D are_equipotent ; ::_thesis: X in (meet Classes) /\ D
A42: (meet Classes) /\ D c= meet Classes by XBOOLE_1:17;
A43: (meet Classes) /\ D c= D by XBOOLE_1:17;
A44: not X, meet Classes are_equipotent by A40, A41, A42, CARD_1:24;
A45: ( X c= D & not X,D are_equipotent ) by A40, A41, A43, CARD_1:24, XBOOLE_1:1;
A46: X in meet Classes by A20, A40, A42, A44, XBOOLE_1:1;
 X in D by A28, A45, Def2;
hence  X in (meet Classes) /\ D by A46, XBOOLE_0:def_4; ::_thesis: verum
end;
 (meet Classes) /\ D c= Big
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (meet Classes) /\ D or x in Big )
assume  x in (meet Classes) /\ D ; ::_thesis: x in Big
then  x in meet Classes by XBOOLE_0:def_4;
hence  x in Big by A7, SETFAM_1:def_1; ::_thesis: verum
end;
then  (meet Classes) /\ D in Classes by A5, A30;
then A47: meet Classes c= (meet Classes) /\ D by SETFAM_1:3;
 (meet Classes) /\ D c= D by XBOOLE_1:17;
hence  meet Classes c= D by A47, XBOOLE_1:1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st b1 is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds
b1 c= D ) & b2 is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds
b2 c= D ) holds
b1 = b2
proof
let D1, D2 be set ; ::_thesis: ( D1 is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds
D1 c= D ) & D2 is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds
D2 c= D ) implies D1 = D2 )
assume A48: ( D1 is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds
D1 c= D ) & D2 is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds
D2 c= D ) ) ; ::_thesis: D1 = D2
thus  ( D1 c= D2 & D2 c= D1 ) by A48; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;
end;

:: deftheorem Def4 defines Tarski-Class CLASSES1:def_4_:_
 for A, b2 being set holds
( b2 = Tarski-Class A iff ( b2 is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds
b2 c= D ) ) );

registration
let A be set ;
cluster Tarski-Class A ->  non empty ;
coherence
 not Tarski-Class A is empty
proof
 Tarski-Class A is_Tarski-Class_of A by Def4;
hence  not Tarski-Class A is empty by Def3; ::_thesis: verum
end;
end;

theorem :: CLASSES1:1
for W being set holds
( W is Tarski iff ( W is subset-closed & ( for X being set st X in W holds
bool X in W ) & ( for X being set st X c= W & card X in card W holds
X in W ) ) )
proof
let W be set ; ::_thesis: ( W is Tarski iff ( W is subset-closed & ( for X being set st X in W holds
bool X in W ) & ( for X being set st X c= W & card X in card W holds
X in W ) ) )
hereby  ::_thesis: ( W is subset-closed & ( for X being set st X in W holds
bool X in W ) & ( for X being set st X c= W & card X in card W holds
X in W ) implies W is Tarski )
assume A1: W is Tarski ; ::_thesis: ( W is subset-closed & ( for X being set st X in W holds
bool X in W ) & ( for X being set st X c= W & card X in card W holds
X in W ) )
hence  ( W is subset-closed & ( for X being set st X in W holds
bool X in W ) ) by Def2; ::_thesis: for X being set st X c= W & card X in card W holds
X in W
let X be set ; ::_thesis: ( X c= W & card X in card W implies X in W )
assume that
A2: X c= W and
A3: card X in card W ; ::_thesis: X in W
 card X <> card W by A3;
then  not X,W are_equipotent by CARD_1:5;
hence  X in W by A1, A2, Def2; ::_thesis: verum
end;
now__::_thesis:_(_(_for_X_being_set_st_X_c=_W_&_card_X_in_card_W_holds_
X_in_W_)_implies_for_X_being_set_holds_
(_not_X_c=_W_or_X,W_are_equipotent_or_X_in_W_)_)
assume A4: for X being set st X c= W & card X in card W holds
X in W ; ::_thesis: for X being set holds
( not X c= W or X,W are_equipotent or X in W )
let X be set ; ::_thesis: ( not X c= W or X,W are_equipotent or X in W )
assume  X c= W ; ::_thesis: ( X,W are_equipotent or X in W )
then  ( ( card X c= card W & not card X in card W ) or X in W ) by A4, CARD_1:11;
then  ( card X = card W or X in W ) by CARD_1:3;
hence  ( X,W are_equipotent or X in W ) by CARD_1:5; ::_thesis: verum
end;
hence  ( W is subset-closed & ( for X being set st X in W holds
bool X in W ) & ( for X being set st X c= W & card X in card W holds
X in W ) implies W is Tarski ) by Def2; ::_thesis: verum
end;

theorem Th2: :: CLASSES1:2
for X being set holds X in Tarski-Class X
proof
let X be set ; ::_thesis: X in Tarski-Class X
 Tarski-Class X is_Tarski-Class_of X by Def4;
hence  X in Tarski-Class X by Def3; ::_thesis: verum
end;

theorem Th3: :: CLASSES1:3
for Y, X, Z being set st Y in Tarski-Class X & Z c= Y holds
Z in Tarski-Class X
proof
let Y, X, Z be set ; ::_thesis: ( Y in Tarski-Class X & Z c= Y implies Z in Tarski-Class X )
 Tarski-Class X is_Tarski-Class_of X by Def4;
then  Tarski-Class X is Tarski by Def3;
then  Tarski-Class X is subset-closed by Def2;
hence  ( Y in Tarski-Class X & Z c= Y implies Z in Tarski-Class X ) by Def1; ::_thesis: verum
end;

theorem Th4: :: CLASSES1:4
for Y, X being set st Y in Tarski-Class X holds
bool Y in Tarski-Class X
proof
let Y, X be set ; ::_thesis: ( Y in Tarski-Class X implies bool Y in Tarski-Class X )
 Tarski-Class X is_Tarski-Class_of X by Def4;
then  Tarski-Class X is Tarski by Def3;
hence  ( Y in Tarski-Class X implies bool Y in Tarski-Class X ) by Def2; ::_thesis: verum
end;

theorem Th5: :: CLASSES1:5
for Y, X being set holds
( not Y c= Tarski-Class X or Y, Tarski-Class X are_equipotent or Y in Tarski-Class X )
proof
let Y, X be set ; ::_thesis: ( not Y c= Tarski-Class X or Y, Tarski-Class X are_equipotent or Y in Tarski-Class X )
 Tarski-Class X is_Tarski-Class_of X by Def4;
then  Tarski-Class X is Tarski by Def3;
hence  ( not Y c= Tarski-Class X or Y, Tarski-Class X are_equipotent or Y in Tarski-Class X ) by Def2; ::_thesis: verum
end;

theorem :: CLASSES1:6
for Y, X being set st Y c= Tarski-Class X & card Y in card (Tarski-Class X) holds
Y in Tarski-Class X
proof
let Y, X be set ; ::_thesis: ( Y c= Tarski-Class X & card Y in card (Tarski-Class X) implies Y in Tarski-Class X )
assume that
A1: Y c= Tarski-Class X and
A2: card Y in card (Tarski-Class X) ; ::_thesis: Y in Tarski-Class X
 card Y <> card (Tarski-Class X) by A2;
then  not Y, Tarski-Class X are_equipotent by CARD_1:5;
hence  Y in Tarski-Class X by A1, Th5; ::_thesis: verum
end;


definition
let X be set ;
let A be Ordinal;
func Tarski-Class (X,A) ->  set  means :Def5: :: CLASSES1:def 5
 ex L being T-Sequence st
( it = last L & dom L = succ A & L . {} = {X} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = ( {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in L . C & u c= v )  }  \/  {  (bool v) where v is Element of Tarski-Class X : v in L . C  }  ) \/ ((bool (L . C)) /\ (Tarski-Class X)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = (union (rng (L | C))) /\ (Tarski-Class X) ) );
correctness
existence
ex b1 being set ex L being T-Sequence st
( b1 = last L & dom L = succ A & L . {} = {X} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = ( {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in L . C & u c= v )  }  \/  {  (bool v) where v is Element of Tarski-Class X : v in L . C  }  ) \/ ((bool (L . C)) /\ (Tarski-Class X)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = (union (rng (L | C))) /\ (Tarski-Class X) ) );
uniqueness
for b1, b2 being set st ex L being T-Sequence st
( b1 = last L & dom L = succ A & L . {} = {X} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = ( {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in L . C & u c= v )  }  \/  {  (bool v) where v is Element of Tarski-Class X : v in L . C  }  ) \/ ((bool (L . C)) /\ (Tarski-Class X)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = (union (rng (L | C))) /\ (Tarski-Class X) ) ) & ex L being T-Sequence st
( b2 = last L & dom L = succ A & L . {} = {X} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = ( {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in L . C & u c= v )  }  \/  {  (bool v) where v is Element of Tarski-Class X : v in L . C  }  ) \/ ((bool (L . C)) /\ (Tarski-Class X)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = (union (rng (L | C))) /\ (Tarski-Class X) ) ) holds
b1 = b2;
proof
deffunc H1( Ordinal, set ) ->  set = ( {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in $2 & u c= v )  }  \/  {  (bool v) where v is Element of Tarski-Class X : v in $2  }  ) \/ ((bool $2) /\ (Tarski-Class X));
deffunc H2( Ordinal, T-Sequence) ->  set = (union (rng $2)) /\ (Tarski-Class X);
thus  ( ex x being set ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = {X} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = H1(C,L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = H2(C,L | C) ) ) & ( for x1, x2 being set st ex L being T-Sequence st
( x1 = last L & dom L = succ A & L . {} = {X} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = H1(C,L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = H2(C,L | C) ) ) & ex L being T-Sequence st
( x2 = last L & dom L = succ A & L . {} = {X} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = H1(C,L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = H2(C,L | C) ) ) holds
x1 = x2 ) ) from ORDINAL2:sch_7(); ::_thesis: verum
end;
end;

:: deftheorem Def5 defines Tarski-Class CLASSES1:def_5_:_
 for X being set
for A being Ordinal
for b3 being set holds
( b3 = Tarski-Class (X,A) iff ex L being T-Sequence st
( b3 = last L & dom L = succ A & L . {} = {X} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = ( {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in L . C & u c= v )  }  \/  {  (bool v) where v is Element of Tarski-Class X : v in L . C  }  ) \/ ((bool (L . C)) /\ (Tarski-Class X)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = (union (rng (L | C))) /\ (Tarski-Class X) ) ) );

Lm1: now__::_thesis:_for_X_being_set_holds_
(_H1(_{}_)_=_{X}_&_(_for_A_being_Ordinal_holds_H1(_succ_A)_=_H2(A,H1(A))_)_&_(_for_A_being_Ordinal
for_L_being_T-Sequence_st_A_<>_{}_&_A_is_limit_ordinal_&_dom_L_=_A_&_(_for_B_being_Ordinal_st_B_in_A_holds_
L_._B_=_Tarski-Class_(X,B)_)_holds_
Tarski-Class_(X,A)_=_(union_(rng_L))_/\_(Tarski-Class_X)_)_)
let X be set ; ::_thesis: ( H1( {} ) = {X} & ( for A being Ordinal holds H1( succ A) = H2(A,H1(A)) ) & ( for A being Ordinal
for L being T-Sequence st A <> {} & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Tarski-Class (X,B) ) holds
Tarski-Class (X,A) = (union (rng L)) /\ (Tarski-Class X) ) )
deffunc H1( Ordinal) ->  set = Tarski-Class (X,$1);
deffunc H2( Ordinal, set ) ->  set = ( {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in $2 & u c= v )  }  \/  {  (bool v) where v is Element of Tarski-Class X : v in $2  }  ) \/ ((bool $2) /\ (Tarski-Class X));
deffunc H3( Ordinal, T-Sequence) ->  set = (union (rng $2)) /\ (Tarski-Class X);
A1: for A being Ordinal
for x being set holds
( x = H1(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = {X} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = H2(C,L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = H3(C,L | C) ) ) ) by Def5;
thus  H1( {} ) = {X} from ORDINAL2:sch_8(A1); ::_thesis: ( ( for A being Ordinal holds H1( succ A) = H2(A,H1(A)) ) & ( for A being Ordinal
for L being T-Sequence st A <> {} & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Tarski-Class (X,B) ) holds
Tarski-Class (X,A) = (union (rng L)) /\ (Tarski-Class X) ) )
thus  for A being Ordinal holds H1( succ A) = H2(A,H1(A)) from ORDINAL2:sch_9(A1); ::_thesis: for A being Ordinal
for L being T-Sequence st A <> {} & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Tarski-Class (X,B) ) holds
Tarski-Class (X,A) = (union (rng L)) /\ (Tarski-Class X)
thus  for A being Ordinal
for L being T-Sequence st A <> {} & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Tarski-Class (X,B) ) holds
Tarski-Class (X,A) = (union (rng L)) /\ (Tarski-Class X) ::_thesis: verum
proof
let A be Ordinal; ::_thesis: for L being T-Sequence st A <> {} & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Tarski-Class (X,B) ) holds
Tarski-Class (X,A) = (union (rng L)) /\ (Tarski-Class X)
let L be T-Sequence; ::_thesis: ( A <> {} & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Tarski-Class (X,B) ) implies Tarski-Class (X,A) = (union (rng L)) /\ (Tarski-Class X) )
assume that
A2: ( A <> {} & A is limit_ordinal ) and
A3: dom L = A and
A4: for B being Ordinal st B in A holds
L . B = H1(B) ; ::_thesis: Tarski-Class (X,A) = (union (rng L)) /\ (Tarski-Class X)
thus  H1(A) = H3(A,L) from ORDINAL2:sch_10(A1, A2, A3, A4); ::_thesis: verum
end;
end;

definition
let X be set ;
let A be Ordinal;
:: original: Tarski-Class
redefine func Tarski-Class (X,A) ->  Subset of (Tarski-Class X);
coherence
 Tarski-Class (X,A) is Subset of (Tarski-Class X)
proof
defpred S1[ Ordinal] means  Tarski-Class (X,$1) is Subset of (Tarski-Class X);
 {X} c= Tarski-Class X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {X} or x in Tarski-Class X )
assume  x in {X} ; ::_thesis: x in Tarski-Class X
then  x = X by TARSKI:def_1;
hence  x in Tarski-Class X by Th2; ::_thesis: verum
end;
then A1: S1[ {} ] by Lm1;
A2: for B being Ordinal st S1[B] holds
S1[ succ B]
proof
let B be Ordinal; ::_thesis: ( S1[B] implies S1[ succ B] )
assume  Tarski-Class (X,B) is Subset of (Tarski-Class X) ; ::_thesis: S1[ succ B]
then reconsider S = Tarski-Class (X,B) as Subset of (Tarski-Class X) ;
set Y = Tarski-Class (X,(succ B));
 Tarski-Class (X,(succ B)) c= Tarski-Class X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Tarski-Class (X,(succ B)) or x in Tarski-Class X )
assume  x in Tarski-Class (X,(succ B)) ; ::_thesis: x in Tarski-Class X
then  x in ( {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in S & u c= v )  }  \/  {  (bool v) where v is Element of Tarski-Class X : v in S  }  ) \/ ((bool S) /\ (Tarski-Class X)) by Lm1;
then A3: ( x in  {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in S & u c= v )  }  \/  {  (bool v) where v is Element of Tarski-Class X : v in S  }  or x in (bool S) /\ (Tarski-Class X) ) by XBOOLE_0:def_3;
A4: now__::_thesis:_(_x_in__{__u_where_u_is_Element_of_Tarski-Class_X_:_ex_v_being_Element_of_Tarski-Class_X_st_
(_v_in_S_&_u_c=_v_)__}__implies_x_in_Tarski-Class_X_)
assume  x in  {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in S & u c= v )  }  ; ::_thesis: x in Tarski-Class X
then  ex u being Element of Tarski-Class X st
( x = u & ex v being Element of Tarski-Class X st
( v in S & u c= v ) ) ;
hence  x in Tarski-Class X ; ::_thesis: verum
end;
now__::_thesis:_(_x_in__{__(bool_v)_where_v_is_Element_of_Tarski-Class_X_:_v_in_S__}__implies_x_in_Tarski-Class_X_)
assume  x in  {  (bool v) where v is Element of Tarski-Class X : v in S  }  ; ::_thesis: x in Tarski-Class X
then  ex v being Element of Tarski-Class X st
( x = bool v & v in S ) ;
hence  x in Tarski-Class X by Th4; ::_thesis: verum
end;
hence  x in Tarski-Class X by A3, A4, XBOOLE_0:def_3, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  S1[ succ B] ; ::_thesis: verum
end;
A5: for B being Ordinal st B <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds
S1[C] ) holds
S1[B]
proof
let B be Ordinal; ::_thesis: ( B <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds
S1[C] ) implies S1[B] )
assume that
A6: ( B <> {} & B is limit_ordinal ) and
 for C being Ordinal st C in B holds
Tarski-Class (X,C) is Subset of (Tarski-Class X) ; ::_thesis: S1[B]
deffunc H1( Ordinal) ->  set = Tarski-Class (X,$1);
consider L being T-Sequence such that
A7: ( dom L = B & ( for C being Ordinal st C in B holds
L . C = H1(C) ) ) from ORDINAL2:sch_2();
 Tarski-Class (X,B) = (union (rng L)) /\ (Tarski-Class X) by A6, A7, Lm1;
hence  S1[B] by XBOOLE_1:17; ::_thesis: verum
end;
 for A being Ordinal holds S1[A] from ORDINAL2:sch_1(A1, A2, A5);
hence  Tarski-Class (X,A) is Subset of (Tarski-Class X) ; ::_thesis: verum
end;
end;

theorem :: CLASSES1:7
for X being set holds Tarski-Class (X,{}) = {X} by Lm1;

theorem :: CLASSES1:8
for X being set
for A being Ordinal holds Tarski-Class (X,(succ A)) = ( {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class (X,A) & u c= v )  }  \/  {  (bool v) where v is Element of Tarski-Class X : v in Tarski-Class (X,A)  }  ) \/ ((bool (Tarski-Class (X,A))) /\ (Tarski-Class X)) by Lm1;

theorem Th9: :: CLASSES1:9
for X being set
for A being Ordinal st A <> {} & A is limit_ordinal holds
Tarski-Class (X,A) =  {  u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) )  }
proof
let X be set ; ::_thesis: for A being Ordinal st A <> {} & A is limit_ordinal holds
Tarski-Class (X,A) =  {  u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) )  }
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal implies Tarski-Class (X,A) =  {  u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) )  }  )
assume A1: ( A <> {} & A is limit_ordinal ) ; ::_thesis: Tarski-Class (X,A) =  {  u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) )  }
deffunc H1( Ordinal) ->  Subset of (Tarski-Class X) = Tarski-Class (X,$1);
consider L being T-Sequence such that
A2: ( dom L = A & ( for B being Ordinal st B in A holds
L . B = H1(B) ) ) from ORDINAL2:sch_2();
A3: Tarski-Class (X,A) = (union (rng L)) /\ (Tarski-Class X) by A1, A2, Lm1;
thus  Tarski-Class (X,A) c=  {  u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) )  }  c= Tarski-Class (X,A)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Tarski-Class (X,A) or x in  {  u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) )  }  )
assume  x in Tarski-Class (X,A) ; ::_thesis: x in  {  u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) )  }
then  x in union (rng L) by A3, XBOOLE_0:def_4;
then consider Y being set  such that
A4: x in Y and
A5: Y in rng L by TARSKI:def_4;
consider y being set  such that
A6: y in dom L and
A7: Y = L . y by A5, FUNCT_1:def_3;
reconsider y = y as Ordinal by A6;
 Y = Tarski-Class (X,y) by A2, A6, A7;
hence  x in  {  u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) )  }  by A2, A4, A6; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) )  }  or x in Tarski-Class (X,A) )
assume  x in  {  u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) )  }  ; ::_thesis: x in Tarski-Class (X,A)
then consider u being Element of Tarski-Class X such that
A8: x = u and
A9: ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) ) ;
consider B being Ordinal such that
A10: B in A and
A11: u in Tarski-Class (X,B) by A9;
 L . B = Tarski-Class (X,B) by A2, A10;
then  Tarski-Class (X,B) in rng L by A2, A10, FUNCT_1:def_3;
then  u in union (rng L) by A11, TARSKI:def_4;
hence  x in Tarski-Class (X,A) by A3, A8, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th10: :: CLASSES1:10
for Y, X being set
for A being Ordinal holds
( Y in Tarski-Class (X,(succ A)) iff ( ( Y c= Tarski-Class (X,A) & Y in Tarski-Class X ) or ex Z being set st
( Z in Tarski-Class (X,A) & ( Y c= Z or Y = bool Z ) ) ) )
proof
let Y, X be set ; ::_thesis: for A being Ordinal holds
( Y in Tarski-Class (X,(succ A)) iff ( ( Y c= Tarski-Class (X,A) & Y in Tarski-Class X ) or ex Z being set st
( Z in Tarski-Class (X,A) & ( Y c= Z or Y = bool Z ) ) ) )
let A be Ordinal; ::_thesis: ( Y in Tarski-Class (X,(succ A)) iff ( ( Y c= Tarski-Class (X,A) & Y in Tarski-Class X ) or ex Z being set st
( Z in Tarski-Class (X,A) & ( Y c= Z or Y = bool Z ) ) ) )
set T1 =  {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class (X,A) & u c= v )  }  ;
set T2 =  {  (bool v) where v is Element of Tarski-Class X : v in Tarski-Class (X,A)  }  ;
set T3 = (bool (Tarski-Class (X,A))) /\ (Tarski-Class X);
A1: Tarski-Class (X,(succ A)) = ( {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class (X,A) & u c= v )  }  \/  {  (bool v) where v is Element of Tarski-Class X : v in Tarski-Class (X,A)  }  ) \/ ((bool (Tarski-Class (X,A))) /\ (Tarski-Class X)) by Lm1;
thus  ( not Y in Tarski-Class (X,(succ A)) or ( Y c= Tarski-Class (X,A) & Y in Tarski-Class X ) or ex Z being set st
( Z in Tarski-Class (X,A) & ( Y c= Z or Y = bool Z ) ) ) ::_thesis: ( ( ( Y c= Tarski-Class (X,A) & Y in Tarski-Class X ) or ex Z being set st
( Z in Tarski-Class (X,A) & ( Y c= Z or Y = bool Z ) ) ) implies Y in Tarski-Class (X,(succ A)) )
proof
assume  Y in Tarski-Class (X,(succ A)) ; ::_thesis: ( ( Y c= Tarski-Class (X,A) & Y in Tarski-Class X ) or ex Z being set st
( Z in Tarski-Class (X,A) & ( Y c= Z or Y = bool Z ) ) )
then A2: ( Y in  {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class (X,A) & u c= v )  }  \/  {  (bool v) where v is Element of Tarski-Class X : v in Tarski-Class (X,A)  }  or Y in (bool (Tarski-Class (X,A))) /\ (Tarski-Class X) ) by A1, XBOOLE_0:def_3;
A3: now__::_thesis:_(_Y_in__{__u_where_u_is_Element_of_Tarski-Class_X_:_ex_v_being_Element_of_Tarski-Class_X_st_
(_v_in_Tarski-Class_(X,A)_&_u_c=_v_)__}__implies_ex_Z_being_set_st_
(_Z_in_Tarski-Class_(X,A)_&_(_Y_c=_Z_or_Y_=_bool_Z_)_)_)
assume  Y in  {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class (X,A) & u c= v )  }  ; ::_thesis: ex Z being set st
( Z in Tarski-Class (X,A) & ( Y c= Z or Y = bool Z ) )
then  ex u being Element of Tarski-Class X st
( Y = u & ex v being Element of Tarski-Class X st
( v in Tarski-Class (X,A) & u c= v ) ) ;
hence  ex Z being set st
( Z in Tarski-Class (X,A) & ( Y c= Z or Y = bool Z ) ) ; ::_thesis: verum
end;
A4: now__::_thesis:_(_Y_in__{__(bool_v)_where_v_is_Element_of_Tarski-Class_X_:_v_in_Tarski-Class_(X,A)__}__implies_ex_Z_being_set_st_
(_Z_in_Tarski-Class_(X,A)_&_(_Y_c=_Z_or_Y_=_bool_Z_)_)_)
assume  Y in  {  (bool v) where v is Element of Tarski-Class X : v in Tarski-Class (X,A)  }  ; ::_thesis: ex Z being set st
( Z in Tarski-Class (X,A) & ( Y c= Z or Y = bool Z ) )
then  ex v being Element of Tarski-Class X st
( Y = bool v & v in Tarski-Class (X,A) ) ;
hence  ex Z being set st
( Z in Tarski-Class (X,A) & ( Y c= Z or Y = bool Z ) ) ; ::_thesis: verum
end;
 ( not Y in (bool (Tarski-Class (X,A))) /\ (Tarski-Class X) or ( Y c= Tarski-Class (X,A) & Y in Tarski-Class X ) or ex Z being set st
( Z in Tarski-Class (X,A) & ( Y c= Z or Y = bool Z ) ) ) by XBOOLE_0:def_4;
hence  ( ( Y c= Tarski-Class (X,A) & Y in Tarski-Class X ) or ex Z being set st
( Z in Tarski-Class (X,A) & ( Y c= Z or Y = bool Z ) ) ) by A2, A3, A4, XBOOLE_0:def_3; ::_thesis: verum
end;
assume A5: ( ( Y c= Tarski-Class (X,A) & Y in Tarski-Class X ) or ex Z being set st
( Z in Tarski-Class (X,A) & ( Y c= Z or Y = bool Z ) ) ) ; ::_thesis: Y in Tarski-Class (X,(succ A))
A6: now__::_thesis:_(_Y_c=_Tarski-Class_(X,A)_&_Y_in_Tarski-Class_X_implies_Y_in_Tarski-Class_(X,(succ_A))_)
assume  ( Y c= Tarski-Class (X,A) & Y in Tarski-Class X ) ; ::_thesis: Y in Tarski-Class (X,(succ A))
then  Y in (bool (Tarski-Class (X,A))) /\ (Tarski-Class X) by XBOOLE_0:def_4;
hence  Y in Tarski-Class (X,(succ A)) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
now__::_thesis:_(_ex_Z_being_set_st_
(_Z_in_Tarski-Class_(X,A)_&_(_Y_c=_Z_or_Y_=_bool_Z_)_)_implies_Y_in_Tarski-Class_(X,(succ_A))_)
given Z being set  such that A7: Z in Tarski-Class (X,A) and
A8: ( Y c= Z or Y = bool Z ) ; ::_thesis: Y in Tarski-Class (X,(succ A))
reconsider Z = Z as Element of Tarski-Class X by A7;
reconsider y = Y as Element of Tarski-Class X by A7, A8, Th3, Th4;
A9: now__::_thesis:_(_Y_c=_Z_implies_Y_in_Tarski-Class_(X,(succ_A))_)
assume  Y c= Z ; ::_thesis: Y in Tarski-Class (X,(succ A))
then  y in  {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class (X,A) & u c= v )  }  by A7;
then  Y in  {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class (X,A) & u c= v )  }  \/  {  (bool v) where v is Element of Tarski-Class X : v in Tarski-Class (X,A)  }  by XBOOLE_0:def_3;
hence  Y in Tarski-Class (X,(succ A)) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
now__::_thesis:_(_Y_=_bool_Z_implies_Y_in_Tarski-Class_(X,(succ_A))_)
assume  Y = bool Z ; ::_thesis: Y in Tarski-Class (X,(succ A))
then  y in  {  (bool v) where v is Element of Tarski-Class X : v in Tarski-Class (X,A)  }  by A7;
then  Y in  {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class (X,A) & u c= v )  }  \/  {  (bool v) where v is Element of Tarski-Class X : v in Tarski-Class (X,A)  }  by XBOOLE_0:def_3;
hence  Y in Tarski-Class (X,(succ A)) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
hence  Y in Tarski-Class (X,(succ A)) by A8, A9; ::_thesis: verum
end;
hence  Y in Tarski-Class (X,(succ A)) by A5, A6; ::_thesis: verum
end;

theorem :: CLASSES1:11
for Y, Z, X being set
for A being Ordinal st Y c= Z & Z in Tarski-Class (X,A) holds
Y in Tarski-Class (X,(succ A)) by Th10;

theorem :: CLASSES1:12
for Y, X being set
for A being Ordinal st Y in Tarski-Class (X,A) holds
bool Y in Tarski-Class (X,(succ A)) by Th10;

theorem Th13: :: CLASSES1:13
for X, x being set
for A being Ordinal st A <> {} & A is limit_ordinal holds
( x in Tarski-Class (X,A) iff ex B being Ordinal st
( B in A & x in Tarski-Class (X,B) ) )
proof
let X, x be set ; ::_thesis: for A being Ordinal st A <> {} & A is limit_ordinal holds
( x in Tarski-Class (X,A) iff ex B being Ordinal st
( B in A & x in Tarski-Class (X,B) ) )
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal implies ( x in Tarski-Class (X,A) iff ex B being Ordinal st
( B in A & x in Tarski-Class (X,B) ) ) )
assume A1: ( A <> {} & A is limit_ordinal ) ; ::_thesis: ( x in Tarski-Class (X,A) iff ex B being Ordinal st
( B in A & x in Tarski-Class (X,B) ) )
then A2: Tarski-Class (X,A) =  {  u where u is Element of Tarski-Class X : ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) )  }  by Th9;
thus  ( x in Tarski-Class (X,A) implies ex B being Ordinal st
( B in A & x in Tarski-Class (X,B) ) ) ::_thesis: ( ex B being Ordinal st
( B in A & x in Tarski-Class (X,B) ) implies x in Tarski-Class (X,A) )
proof
assume  x in Tarski-Class (X,A) ; ::_thesis: ex B being Ordinal st
( B in A & x in Tarski-Class (X,B) )
then  ex u being Element of Tarski-Class X st
( x = u & ex B being Ordinal st
( B in A & u in Tarski-Class (X,B) ) ) by A2;
hence  ex B being Ordinal st
( B in A & x in Tarski-Class (X,B) ) ; ::_thesis: verum
end;
given B being Ordinal such that A3: B in A and
A4: x in Tarski-Class (X,B) ; ::_thesis: x in Tarski-Class (X,A)
reconsider u = x as Element of Tarski-Class X by A4;
 u in  {  v where v is Element of Tarski-Class X : ex B being Ordinal st
( B in A & v in Tarski-Class (X,B) )  }  by A3, A4;
hence  x in Tarski-Class (X,A) by A1, Th9; ::_thesis: verum
end;

theorem :: CLASSES1:14
for Y, X, Z being set
for A being Ordinal st A <> {} & A is limit_ordinal & Y in Tarski-Class (X,A) & ( Z c= Y or Z = bool Y ) holds
Z in Tarski-Class (X,A)
proof
let Y, X, Z be set ; ::_thesis: for A being Ordinal st A <> {} & A is limit_ordinal & Y in Tarski-Class (X,A) & ( Z c= Y or Z = bool Y ) holds
Z in Tarski-Class (X,A)
let A be Ordinal; ::_thesis: ( 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) )
assume that
A1: A <> {} and
A2: A is limit_ordinal and
A3: Y in Tarski-Class (X,A) ; ::_thesis: ( ( not Z c= Y & not Z = bool Y ) or Z in Tarski-Class (X,A) )
consider B being Ordinal such that
A4: B in A and
A5: Y in Tarski-Class (X,B) by A1, A2, A3, Th13;
A6: bool Y in Tarski-Class (X,(succ B)) by A5, Th10;
A7: ( Z c= Y implies Z in Tarski-Class (X,(succ B)) ) by A5, Th10;
A8: succ B in A by A2, A4, ORDINAL1:28;
assume  ( Z c= Y or Z = bool Y ) ; ::_thesis: Z in Tarski-Class (X,A)
hence  Z in Tarski-Class (X,A) by A2, A6, A7, A8, Th13; ::_thesis: verum
end;

theorem Th15: :: CLASSES1:15
for X being set
for A being Ordinal holds Tarski-Class (X,A) c= Tarski-Class (X,(succ A))
proof
let X be set ; ::_thesis: for A being Ordinal holds Tarski-Class (X,A) c= Tarski-Class (X,(succ A))
let A be Ordinal; ::_thesis: Tarski-Class (X,A) c= Tarski-Class (X,(succ A))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Tarski-Class (X,A) or x in Tarski-Class (X,(succ A)) )
assume  x in Tarski-Class (X,A) ; ::_thesis: x in Tarski-Class (X,(succ A))
then  x in  {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class (X,A) & u c= v )  }  ;
then A1: x in  {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class (X,A) & u c= v )  }  \/  {  (bool v) where v is Element of Tarski-Class X : v in Tarski-Class (X,A)  }  by XBOOLE_0:def_3;
 Tarski-Class (X,(succ A)) = ( {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class (X,A) & u c= v )  }  \/  {  (bool v) where v is Element of Tarski-Class X : v in Tarski-Class (X,A)  }  ) \/ ((bool (Tarski-Class (X,A))) /\ (Tarski-Class X)) by Lm1;
hence  x in Tarski-Class (X,(succ A)) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;

theorem Th16: :: CLASSES1:16
for X being set
for A, B being Ordinal st A c= B holds
Tarski-Class (X,A) c= Tarski-Class (X,B)
proof
let X be set ; ::_thesis: for A, B being Ordinal st A c= B holds
Tarski-Class (X,A) c= Tarski-Class (X,B)
let A, B be Ordinal; ::_thesis: ( A c= B implies Tarski-Class (X,A) c= Tarski-Class (X,B) )
defpred S1[ Ordinal] means ( A c= $1 implies Tarski-Class (X,A) c= Tarski-Class (X,$1) );
A1: for B being Ordinal st ( for C being Ordinal st C in B holds
S1[C] ) holds
S1[B]
proof
let B be Ordinal; ::_thesis: ( ( for C being Ordinal st C in B holds
S1[C] ) implies S1[B] )
assume that
A2: for C being Ordinal st C in B holds
S1[C] and
A3: A c= B ; ::_thesis: Tarski-Class (X,A) c= Tarski-Class (X,B)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Tarski-Class (X,A) or x in Tarski-Class (X,B) )
assume A4: x in Tarski-Class (X,A) ; ::_thesis: x in Tarski-Class (X,B)
now__::_thesis:_(_A_<>_B_implies_x_in_Tarski-Class_(X,B)_)
assume A5: A <> B ; ::_thesis: x in Tarski-Class (X,B)
then  A c< B by A3, XBOOLE_0:def_8;
then A6: A in B by ORDINAL1:11;
A7: B <> {} by A3, A5;
A8: now__::_thesis:_(_ex_C_being_Ordinal_st_B_=_succ_C_implies_x_in_Tarski-Class_(X,B)_)
given C being Ordinal such that A9: B = succ C ; ::_thesis: x in Tarski-Class (X,B)
 ( A c= C & C in B ) by A6, A9, ORDINAL1:22;
then A10: Tarski-Class (X,A) c= Tarski-Class (X,C) by A2;
 Tarski-Class (X,C) c= Tarski-Class (X,B) by A9, Th15;
then  Tarski-Class (X,A) c= Tarski-Class (X,B) by A10, XBOOLE_1:1;
hence  x in Tarski-Class (X,B) by A4; ::_thesis: verum
end;
now__::_thesis:_(_(_for_C_being_Ordinal_holds_B_<>_succ_C_)_implies_x_in_Tarski-Class_(X,B)_)
assume  for C being Ordinal holds B <> succ C ; ::_thesis: x in Tarski-Class (X,B)
then  B is limit_ordinal by ORDINAL1:29;
then  Tarski-Class (X,B) =  {  v where v is Element of Tarski-Class X : ex C being Ordinal st
( C in B & v in Tarski-Class (X,C) )  }  by A7, Th9;
hence  x in Tarski-Class (X,B) by A4, A6; ::_thesis: verum
end;
hence  x in Tarski-Class (X,B) by A8; ::_thesis: verum
end;
hence  x in Tarski-Class (X,B) by A4; ::_thesis: verum
end;
 for B being Ordinal holds S1[B] from ORDINAL1:sch_2(A1);
hence  ( A c= B implies Tarski-Class (X,A) c= Tarski-Class (X,B) ) ; ::_thesis: verum
end;

theorem Th17: :: CLASSES1:17
for X being set ex A being Ordinal st Tarski-Class (X,A) = Tarski-Class (X,(succ A))
proof
let X be set ; ::_thesis: ex A being Ordinal st Tarski-Class (X,A) = Tarski-Class (X,(succ A))
assume A1: for A being Ordinal holds Tarski-Class (X,A) <> Tarski-Class (X,(succ A)) ; ::_thesis: contradiction
defpred S1[ set ] means  ex A being Ordinal st $1 in Tarski-Class (X,A);
consider Z being set  such that
A2: for x being set holds
( x in Z iff ( x in Tarski-Class X & S1[x] ) ) from XBOOLE_0:sch_1();
defpred S2[ set , set ] means  ex A being Ordinal st
( $2 = A & $1 in Tarski-Class (X,(succ A)) & not $1 in Tarski-Class (X,A) );
A3: for x, y, z being set st S2[x,y] & S2[x,z] holds
y = z
proof
let x, y, z be set ; ::_thesis: ( S2[x,y] & S2[x,z] implies y = z )
given A being Ordinal such that A4: y = A and
A5: x in Tarski-Class (X,(succ A)) and
A6: not x in Tarski-Class (X,A) ; ::_thesis: ( not S2[x,z] or y = z )
given B being Ordinal such that A7: z = B and
A8: x in Tarski-Class (X,(succ B)) and
A9: not x in Tarski-Class (X,B) ; ::_thesis: y = z
assume A10: y <> z ; ::_thesis: contradiction
 ( A c= B or B c= A ) ;
then A11: ( A c< B or B c< A ) by A4, A7, A10, XBOOLE_0:def_8;
now__::_thesis:_not_A_c<_B
assume  A c< B ; ::_thesis: contradiction
then  A in B by ORDINAL1:11;
then  succ A c= B by ORDINAL1:21;
then  Tarski-Class (X,(succ A)) c= Tarski-Class (X,B) by Th16;
hence  contradiction by A5, A9; ::_thesis: verum
end;
then  B in A by A11, ORDINAL1:11;
then  succ B c= A by ORDINAL1:21;
then  Tarski-Class (X,(succ B)) c= Tarski-Class (X,A) by Th16;
hence  contradiction by A6, A8; ::_thesis: verum
end;
consider Y being set  such that
A12: for x being set holds
( x in Y iff ex y being set st
( y in Z & S2[y,x] ) ) from TARSKI:sch_1(A3);
now__::_thesis:_for_A_being_Ordinal_holds_A_in_Y
let A be Ordinal; ::_thesis: A in Y
A13: Tarski-Class (X,A) <> Tarski-Class (X,(succ A)) by A1;
A14: Tarski-Class (X,A) c= Tarski-Class (X,(succ A)) by Th15;
consider x being set  such that
A15: ( ( x in Tarski-Class (X,A) & not x in Tarski-Class (X,(succ A)) ) or ( x in Tarski-Class (X,(succ A)) & not x in Tarski-Class (X,A) ) ) by A13, TARSKI:1;
 x in Z by A2, A15;
hence  A in Y by A12, A14, A15; ::_thesis: verum
end;
hence  contradiction by ORDINAL1:26; ::_thesis: verum
end;

theorem Th18: :: CLASSES1:18
for X being set
for A being Ordinal st Tarski-Class (X,A) = Tarski-Class (X,(succ A)) holds
Tarski-Class (X,A) = Tarski-Class X
proof
let X be set ; ::_thesis: for A being Ordinal st Tarski-Class (X,A) = Tarski-Class (X,(succ A)) holds
Tarski-Class (X,A) = Tarski-Class X
let A be Ordinal; ::_thesis: ( Tarski-Class (X,A) = Tarski-Class (X,(succ A)) implies Tarski-Class (X,A) = Tarski-Class X )
assume A1: Tarski-Class (X,A) = Tarski-Class (X,(succ A)) ; ::_thesis: Tarski-Class (X,A) = Tarski-Class X
 {} c= A ;
then A2: Tarski-Class (X,{}) c= Tarski-Class (X,A) by Th16;
A3: ( Tarski-Class (X,{}) = {X} & X in {X} ) by Lm1, TARSKI:def_1;
 Tarski-Class (X,A) is_Tarski-Class_of X
proof
thus  X in Tarski-Class (X,A) by A2, A3; :: according to CLASSES1:def_3 ::_thesis: Tarski-Class (X,A) is Tarski
A4: Tarski-Class (X,(succ A)) = ( {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class (X,A) & u c= v )  }  \/  {  (bool v) where v is Element of Tarski-Class X : 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 A5: Tarski-Class X is Tarski by Def3;
thus  for Z, Y being set st Z in Tarski-Class (X,A) & Y c= Z holds
Y in Tarski-Class (X,A) :: according to CLASSES1:def_1,CLASSES1:def_2 ::_thesis: ( ( for X being set st X in Tarski-Class (X,A) holds
bool X in Tarski-Class (X,A) ) & ( for X being set holds
( not X c= Tarski-Class (X,A) or X, Tarski-Class (X,A) are_equipotent or X in Tarski-Class (X,A) ) ) )
proof
let Z, Y be set ; ::_thesis: ( Z in Tarski-Class (X,A) & Y c= Z implies Y in Tarski-Class (X,A) )
assume A6: ( Z in Tarski-Class (X,A) & Y c= Z ) ; ::_thesis: Y in Tarski-Class (X,A)
 Tarski-Class X is_Tarski-Class_of X by Def4;
then  Tarski-Class X is Tarski by Def3;
then  Tarski-Class X is subset-closed by Def2;
then reconsider y = Y as Element of Tarski-Class X by A6, Def1;
 ex v being Element of Tarski-Class X st
( v in Tarski-Class (X,A) & y c= v ) by A6;
then  Y in  {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class (X,A) & u c= v )  }  ;
then  Y in  {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class (X,A) & u c= v )  }  \/  {  (bool v) where v is Element of Tarski-Class X : v in Tarski-Class (X,A)  }  by XBOOLE_0:def_3;
hence  Y in Tarski-Class (X,A) by A1, A4, XBOOLE_0:def_3; ::_thesis: verum
end;
thus  for Y being set st Y in Tarski-Class (X,A) holds
bool Y in Tarski-Class (X,A) ::_thesis: for X being set holds
( not X c= Tarski-Class (X,A) or X, Tarski-Class (X,A) are_equipotent or X in Tarski-Class (X,A) )
proof
let Y be set ; ::_thesis: ( Y in Tarski-Class (X,A) implies bool Y in Tarski-Class (X,A) )
assume  Y in Tarski-Class (X,A) ; ::_thesis: bool Y in Tarski-Class (X,A)
then  bool Y in  {  (bool u) where u is Element of Tarski-Class X : u in Tarski-Class (X,A)  }  ;
then  bool Y in  {  u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class (X,A) & u c= v )  }  \/  {  (bool v) where v is Element of Tarski-Class X : v in Tarski-Class (X,A)  }  by XBOOLE_0:def_3;
hence  bool Y in Tarski-Class (X,A) by A1, A4, XBOOLE_0:def_3; ::_thesis: verum
end;
let Y be set ; ::_thesis: ( not Y c= Tarski-Class (X,A) or Y, Tarski-Class (X,A) are_equipotent or Y in Tarski-Class (X,A) )
assume that
A7: Y c= Tarski-Class (X,A) and
A8: not Y, Tarski-Class (X,A) are_equipotent ; ::_thesis: Y in Tarski-Class (X,A)
 Y c= Tarski-Class X by A7, XBOOLE_1:1;
then  ( Y, Tarski-Class X are_equipotent or Y in Tarski-Class X ) by A5, Def2;
hence  Y in Tarski-Class (X,A) by A1, A7, A8, Th10, CARD_1:24; ::_thesis: verum
end;
hence  ( Tarski-Class (X,A) c= Tarski-Class X & Tarski-Class X c= Tarski-Class (X,A) ) by Def4; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;

theorem Th19: :: CLASSES1:19
for X being set ex A being Ordinal st Tarski-Class (X,A) = Tarski-Class X
proof
let X be set ; ::_thesis: ex A being Ordinal st Tarski-Class (X,A) = Tarski-Class X
consider A being Ordinal such that
A1: Tarski-Class (X,A) = Tarski-Class (X,(succ A)) by Th17;
take  A ; ::_thesis: Tarski-Class (X,A) = Tarski-Class X
thus  Tarski-Class (X,A) = Tarski-Class X by A1, Th18; ::_thesis: verum
end;

theorem :: CLASSES1:20
for X being set ex A being Ordinal st
( Tarski-Class (X,A) = Tarski-Class X & ( for B being Ordinal st B in A holds
Tarski-Class (X,B) <> Tarski-Class X ) )
proof
let X be set ; ::_thesis: ex A being Ordinal st
( Tarski-Class (X,A) = Tarski-Class X & ( for B being Ordinal st B in A holds
Tarski-Class (X,B) <> Tarski-Class X ) )
defpred S1[ Ordinal] means  Tarski-Class (X,$1) = Tarski-Class X;
A1: ex A being Ordinal st S1[A] by Th19;
consider A being Ordinal such that
A2: ( S1[A] & ( for B being Ordinal st S1[B] holds
A c= B ) ) from ORDINAL1:sch_1(A1);
take  A ; ::_thesis: ( Tarski-Class (X,A) = Tarski-Class X & ( for B being Ordinal st B in A holds
Tarski-Class (X,B) <> Tarski-Class X ) )
thus  Tarski-Class (X,A) = Tarski-Class X by A2; ::_thesis: for B being Ordinal st B in A holds
Tarski-Class (X,B) <> Tarski-Class X
let B be Ordinal; ::_thesis: ( B in A implies Tarski-Class (X,B) <> Tarski-Class X )
assume  B in A ; ::_thesis: Tarski-Class (X,B) <> Tarski-Class X
hence  Tarski-Class (X,B) <> Tarski-Class X by A2, ORDINAL1:5; ::_thesis: verum
end;

theorem :: CLASSES1:21
for Y, X being set st Y <> X & Y in Tarski-Class X holds
ex A being Ordinal st
( not Y in Tarski-Class (X,A) & Y in Tarski-Class (X,(succ A)) )
proof
let Y, X be set ; ::_thesis: ( Y <> X & Y in Tarski-Class X implies ex A being Ordinal st
( not Y in Tarski-Class (X,A) & Y in Tarski-Class (X,(succ A)) ) )
assume that
A1: Y <> X and
A2: Y in Tarski-Class X ; ::_thesis: ex A being Ordinal st
( not Y in Tarski-Class (X,A) & Y in Tarski-Class (X,(succ A)) )
defpred S1[ Ordinal] means Y in Tarski-Class (X,$1);
 ex A being Ordinal st Tarski-Class (X,A) = Tarski-Class X by Th19;
then A3: ex A being Ordinal st S1[A] by A2;
consider A being Ordinal such that
A4: ( S1[A] & ( for B being Ordinal st S1[B] holds
A c= B ) ) from ORDINAL1:sch_1(A3);
A5: not Y in {X} by A1, TARSKI:def_1;
A6: Tarski-Class (X,{}) = {X} by Lm1;
now__::_thesis:_not_A_is_limit_ordinal
assume  A is limit_ordinal ; ::_thesis: contradiction
then  ex B being Ordinal st
( B in A & Y in Tarski-Class (X,B) ) by A4, A5, A6, Th13;
hence  contradiction by A4, ORDINAL1:5; ::_thesis: verum
end;
then consider B being Ordinal such that
A7: A = succ B by ORDINAL1:29;
take  B ; ::_thesis: ( not Y in Tarski-Class (X,B) & Y in Tarski-Class (X,(succ B)) )
 not A c= B by A7, ORDINAL1:5, ORDINAL1:6;
hence  ( not Y in Tarski-Class (X,B) & Y in Tarski-Class (X,(succ B)) ) by A4, A7; ::_thesis: verum
end;

theorem Th22: :: CLASSES1:22
for X being set st X is epsilon-transitive holds
for A being Ordinal st A <> {} holds
Tarski-Class (X,A) is epsilon-transitive
proof
let X be set ; ::_thesis: ( X is epsilon-transitive implies for A being Ordinal st A <> {} holds
Tarski-Class (X,A) is epsilon-transitive )
assume A1: for Y being set st Y in X holds
Y c= X ; :: according to ORDINAL1:def_2 ::_thesis: for A being Ordinal st A <> {} holds
Tarski-Class (X,A) is epsilon-transitive
defpred S1[ Ordinal] means ( $1 <> {} implies Tarski-Class (X,$1) is epsilon-transitive );
A2: for A being Ordinal st ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be Ordinal; ::_thesis: ( ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume that
A3: for B being Ordinal st B in A holds
S1[B] and
A4: A <> {} ; ::_thesis: Tarski-Class (X,A) is epsilon-transitive
let Y be set ; :: according to ORDINAL1:def_2 ::_thesis: ( not Y in Tarski-Class (X,A) or Y c= Tarski-Class (X,A) )
assume A5: Y in Tarski-Class (X,A) ; ::_thesis: Y c= Tarski-Class (X,A)
A6: now__::_thesis:_(_ex_B_being_Ordinal_st_A_=_succ_B_implies_Y_c=_Tarski-Class_(X,A)_)
given B being Ordinal such that A7: A = succ B ; ::_thesis: Y c= Tarski-Class (X,A)
 B in A by A7, ORDINAL1:6;
then A8: B c= A by ORDINAL1:def_2;
A9: S1[B] by A3, A7, ORDINAL1:6;
A10: Tarski-Class (X,B) c= Tarski-Class (X,A) by A8, Th16;
now__::_thesis:_(_not_Y_c=_Tarski-Class_(X,B)_implies_Y_c=_Tarski-Class_(X,A)_)
assume  not Y c= Tarski-Class (X,B) ; ::_thesis: Y c= Tarski-Class (X,A)
then consider Z being set  such that
A11: Z in Tarski-Class (X,B) and
A12: ( Y c= Z or Y = bool Z ) by A5, A7, Th10;
A13: now__::_thesis:_(_Y_=_bool_Z_implies_Y_c=_Tarski-Class_(X,A)_)
assume A14: Y = bool Z ; ::_thesis: Y c= Tarski-Class (X,A)
thus  Y c= Tarski-Class (X,A) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in Tarski-Class (X,A) )
assume  x in Y ; ::_thesis: x in Tarski-Class (X,A)
hence  x in Tarski-Class (X,A) by A7, A11, A14, Th10; ::_thesis: verum
end;
end;
now__::_thesis:_(_Y_c=_Z_implies_Y_c=_Tarski-Class_(X,A)_)
assume A15: Y c= Z ; ::_thesis: Y c= Tarski-Class (X,A)
thus  Y c= Tarski-Class (X,A) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in Tarski-Class (X,A) )
assume A16: x in Y ; ::_thesis: x in Tarski-Class (X,A)
then A17: x in Z by A15;
A18: now__::_thesis:_(_B_=_{}_implies_x_in_Tarski-Class_(X,A)_)
assume  B = {} ; ::_thesis: x in Tarski-Class (X,A)
then  Tarski-Class (X,B) = {X} by Lm1;
then A19: Z = X by A11, TARSKI:def_1;
then  x c= X by A1, A15, A16;
hence  x in Tarski-Class (X,A) by A7, A11, A19, Th10; ::_thesis: verum
end;
now__::_thesis:_(_B_<>_{}_implies_x_in_Tarski-Class_(X,A)_)
assume  B <> {} ; ::_thesis: x in Tarski-Class (X,A)
then  Z c= Tarski-Class (X,B) by A9, A11, ORDINAL1:def_2;
then  x in Tarski-Class (X,B) by A17;
hence  x in Tarski-Class (X,A) by A10; ::_thesis: verum
end;
hence  x in Tarski-Class (X,A) by A18; ::_thesis: verum
end;
end;
hence  Y c= Tarski-Class (X,A) by A12, A13; ::_thesis: verum
end;
hence  Y c= Tarski-Class (X,A) by A10, XBOOLE_1:1; ::_thesis: verum
end;
now__::_thesis:_(_(_for_B_being_Ordinal_holds_A_<>_succ_B_)_implies_Y_c=_Tarski-Class_(X,A)_)
assume A20: for B being Ordinal holds A <> succ B ; ::_thesis: Y c= Tarski-Class (X,A)
then  A is limit_ordinal by ORDINAL1:29;
then consider B being Ordinal such that
A21: B in A and
A22: Y in Tarski-Class (X,B) by A4, A5, Th13;
A23: succ B c= A by A21, ORDINAL1:21;
A24: succ B <> A by A20;
A25: Tarski-Class (X,B) c= Tarski-Class (X,(succ B)) by Th15;
A26: succ B c< A by A23, A24, XBOOLE_0:def_8;
A27: Tarski-Class (X,(succ B)) c= Tarski-Class (X,A) by A23, Th16;
 Tarski-Class (X,(succ B)) is epsilon-transitive by A3, A26, ORDINAL1:11;
then  Y c= Tarski-Class (X,(succ B)) by A22, A25, ORDINAL1:def_2;
hence  Y c= Tarski-Class (X,A) by A27, XBOOLE_1:1; ::_thesis: verum
end;
hence  Y c= Tarski-Class (X,A) by A6; ::_thesis: verum
end;
thus  for A being Ordinal holds S1[A] from ORDINAL1:sch_2(A2); ::_thesis: verum
end;

theorem Th23: :: CLASSES1:23
for X being set st X is epsilon-transitive holds
Tarski-Class X is epsilon-transitive
proof
let X be set ; ::_thesis: ( X is epsilon-transitive implies Tarski-Class X is epsilon-transitive )
consider A being Ordinal such that
A1: Tarski-Class (X,A) = Tarski-Class X by Th19;
 Tarski-Class (X,A) c= Tarski-Class (X,(succ A)) by Th15;
then A2: Tarski-Class (X,A) = Tarski-Class (X,(succ A)) by A1, XBOOLE_0:def_10;
assume  X is epsilon-transitive ; ::_thesis: Tarski-Class X is epsilon-transitive
hence  Tarski-Class X is epsilon-transitive by A1, A2, Th22; ::_thesis: verum
end;

theorem Th24: :: CLASSES1:24
for Y, X being set st Y in Tarski-Class X holds
card Y in card (Tarski-Class X)
proof
let Y, X be set ; ::_thesis: ( Y in Tarski-Class X implies card Y in card (Tarski-Class X) )
assume A1: Y in Tarski-Class X ; ::_thesis: card Y in card (Tarski-Class X)
 bool Y c= Tarski-Class X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in bool Y or x in Tarski-Class X )
assume  x in bool Y ; ::_thesis: x in Tarski-Class X
hence  x in Tarski-Class X by A1, Th3; ::_thesis: verum
end;
then  ( card Y in card (bool Y) & card (bool Y) c= card (Tarski-Class X) ) by CARD_1:11, CARD_1:14;
hence  card Y in card (Tarski-Class X) ; ::_thesis: verum
end;

theorem Th25: :: CLASSES1:25
for Y, X being set st Y in Tarski-Class X holds
not Y, Tarski-Class X are_equipotent
proof
let Y, X be set ; ::_thesis: ( Y in Tarski-Class X implies not Y, Tarski-Class X are_equipotent )
assume  Y in Tarski-Class X ; ::_thesis: not Y, Tarski-Class X are_equipotent
then  card Y in card (Tarski-Class X) by Th24;
then  card Y <> card (Tarski-Class X) ;
hence  not Y, Tarski-Class X are_equipotent by CARD_1:5; ::_thesis: verum
end;

theorem Th26: :: CLASSES1:26
for X, x, y being set st x in Tarski-Class X & y in Tarski-Class X holds
( {x} in Tarski-Class X & {x,y} in Tarski-Class X )
proof
let X, x, y be set ; ::_thesis: ( x in Tarski-Class X & y in Tarski-Class X implies ( {x} in Tarski-Class X & {x,y} in Tarski-Class X ) )
assume that
A1: x in Tarski-Class X and
A2: y in Tarski-Class X ; ::_thesis: ( {x} in Tarski-Class X & {x,y} in Tarski-Class X )
 bool x in Tarski-Class X by A1, Th4;
hence A3: {x} in Tarski-Class X by Th3, ZFMISC_1:68; ::_thesis: {x,y} in Tarski-Class X
 bool {x} = {{},{x}} by ZFMISC_1:24;
then A4: not {{},{x}}, Tarski-Class X are_equipotent by A3, Th4, Th25;
now__::_thesis:_(_x_<>_y_implies_{x,y}_in_Tarski-Class_X_)
assume A5: x <> y ; ::_thesis: {x,y} in Tarski-Class X
 {{},{x}},{x,y} are_equipotent
proof
defpred S1[ set ] means $1 = {} ;
deffunc H1( set ) ->  set = x;
deffunc H2( set ) ->  set = y;
consider f being Function such that
A6: ( dom f = {{},{x}} & ( for z being set st z in {{},{x}} holds
( ( S1[z] implies f . z = H1(z) ) & ( not S1[z] implies f . z = H2(z) ) ) ) ) from PARTFUN1:sch_1();
take  f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = {{},{x}} & rng f = {x,y} )
thus  f is one-to-one ::_thesis: ( dom f = {{},{x}} & rng f = {x,y} )
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A7: x1 in dom f and
A8: x2 in dom f ; ::_thesis: ( not f . x1 = f . x2 or x1 = x2 )
A9: ( x2 = {} or x2 = {x} ) by A6, A8, TARSKI:def_2;
A10: ( x1 = {} implies f . x1 = x ) by A6, A7;
 ( x1 <> {} implies f . x1 = y ) by A6, A7;
hence  ( not f . x1 = f . x2 or x1 = x2 ) by A5, A6, A7, A8, A9, A10, TARSKI:def_2; ::_thesis: verum
end;
thus  dom f = {{},{x}} by A6; ::_thesis: rng f = {x,y}
thus  rng f c= {x,y} :: according to XBOOLE_0:def_10 ::_thesis: {x,y} c= rng f
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f or z in {x,y} )
assume  z in rng f ; ::_thesis: z in {x,y}
then  ex u being set st
( u in dom f & z = f . u ) by FUNCT_1:def_3;
then  ( z = x or z = y ) by A6;
hence  z in {x,y} by TARSKI:def_2; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {x,y} or z in rng f )
assume  z in {x,y} ; ::_thesis: z in rng f
then A11: ( z = x or z = y ) by TARSKI:def_2;
A12: {} in dom f by A6, TARSKI:def_2;
A13: {x} in dom f by A6, TARSKI:def_2;
A14: f . {} = x by A6, A12;
 f . {x} = y by A6, A13;
hence  z in rng f by A11, A12, A13, A14, FUNCT_1:def_3; ::_thesis: verum
end;
then A15: not {x,y}, Tarski-Class X are_equipotent by A4, WELLORD2:15;
 {x,y} c= Tarski-Class X by A1, A2, ZFMISC_1:32;
hence  {x,y} in Tarski-Class X by A15, Th5; ::_thesis: verum
end;
hence  {x,y} in Tarski-Class X by A3, ENUMSET1:29; ::_thesis: verum
end;

theorem Th27: :: CLASSES1:27
for X, x, y being set st x in Tarski-Class X & y in Tarski-Class X holds
[x,y] in Tarski-Class X
proof
let X, x, y be set ; ::_thesis: ( x in Tarski-Class X & y in Tarski-Class X implies [x,y] in Tarski-Class X )
assume  ( x in Tarski-Class X & y in Tarski-Class X ) ; ::_thesis: [x,y] in Tarski-Class X
then  ( {x,y} in Tarski-Class X & {x} in Tarski-Class X ) by Th26;
hence  [x,y] in Tarski-Class X by Th26; ::_thesis: verum
end;

theorem :: CLASSES1:28
for Y, X, Z being set st Y c= Tarski-Class X & Z c= Tarski-Class X holds
[:Y,Z:] c= Tarski-Class X
proof
let Y, X, Z be set ; ::_thesis: ( Y c= Tarski-Class X & Z c= Tarski-Class X implies [:Y,Z:] c= Tarski-Class X )
assume A1: ( Y c= Tarski-Class X & Z c= Tarski-Class X ) ; ::_thesis: [:Y,Z:] c= Tarski-Class X
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in [:Y,Z:] or [x,b1] in Tarski-Class X )
let y be set ; ::_thesis: ( not [x,y] in [:Y,Z:] or [x,y] in Tarski-Class X )
assume  [x,y] in [:Y,Z:] ; ::_thesis: [x,y] in Tarski-Class X
then  ( x in Y & y in Z ) by ZFMISC_1:87;
hence  [x,y] in Tarski-Class X by A1, Th27; ::_thesis: verum
end;

definition
let A be Ordinal;
func Rank A ->  set  means :Def6: :: CLASSES1:def 6
 ex L being T-Sequence st
( it = last L & dom L = succ A & L . {} = {} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = bool (L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = union (rng (L | C)) ) );
correctness
existence
ex b1 being set ex L being T-Sequence st
( b1 = last L & dom L = succ A & L . {} = {} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = bool (L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = union (rng (L | C)) ) );
uniqueness
for b1, b2 being set st ex L being T-Sequence st
( b1 = last L & dom L = succ A & L . {} = {} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = bool (L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = union (rng (L | C)) ) ) & ex L being T-Sequence st
( b2 = last L & dom L = succ A & L . {} = {} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = bool (L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = union (rng (L | C)) ) ) holds
b1 = b2;
proof
deffunc H1( Ordinal, set ) ->  Element of bool (bool $2) = bool $2;
deffunc H2( Ordinal, T-Sequence) ->  set = union (rng $2);
thus  ( ex x being set ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = {} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = H1(C,L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = H2(C,L | C) ) ) & ( for x1, x2 being set st ex L being T-Sequence st
( x1 = last L & dom L = succ A & L . {} = {} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = H1(C,L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = H2(C,L | C) ) ) & ex L being T-Sequence st
( x2 = last L & dom L = succ A & L . {} = {} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = H1(C,L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = H2(C,L | C) ) ) holds
x1 = x2 ) ) from ORDINAL2:sch_7(); ::_thesis: verum
end;
end;

:: deftheorem Def6 defines Rank CLASSES1:def_6_:_
 for A being Ordinal
for b2 being set holds
( b2 = Rank A iff ex L being T-Sequence st
( b2 = last L & dom L = succ A & L . {} = {} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = bool (L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = union (rng (L | C)) ) ) );

deffunc H1( Ordinal) ->  set = Rank $1;

Lm2: now__::_thesis:_(_H1(_{}_)_=_{}_&_(_for_A_being_Ordinal_holds_H1(_succ_A)_=_H2(A,H1(A))_)_&_(_for_A_being_Ordinal
for_L_being_T-Sequence_st_A_<>_{}_&_A_is_limit_ordinal_&_dom_L_=_A_&_(_for_B_being_Ordinal_st_B_in_A_holds_
L_._B_=_Rank_B_)_holds_
Rank_A_=_union_(rng_L)_)_)
deffunc H2( Ordinal, set ) ->  Element of bool (bool $2) = bool $2;
deffunc H3( Ordinal, T-Sequence) ->  set = union (rng $2);
A1: for A being Ordinal
for x being set holds
( x = H1(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = {} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = H2(C,L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = H3(C,L | C) ) ) ) by Def6;
thus  H1( {} ) = {} from ORDINAL2:sch_8(A1); ::_thesis: ( ( for A being Ordinal holds H1( succ A) = H2(A,H1(A)) ) & ( for A being Ordinal
for L being T-Sequence st A <> {} & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Rank B ) holds
Rank A = union (rng L) ) )
thus  for A being Ordinal holds H1( succ A) = H2(A,H1(A)) from ORDINAL2:sch_9(A1); ::_thesis: for A being Ordinal
for L being T-Sequence st A <> {} & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Rank B ) holds
Rank A = union (rng L)
thus  for A being Ordinal
for L being T-Sequence st A <> {} & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Rank B ) holds
Rank A = union (rng L) ::_thesis: verum
proof
let A be Ordinal; ::_thesis: for L being T-Sequence st A <> {} & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Rank B ) holds
Rank A = union (rng L)
let L be T-Sequence; ::_thesis: ( A <> {} & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = Rank B ) implies Rank A = union (rng L) )
assume that
A2: ( A <> {} & A is limit_ordinal ) and
A3: dom L = A and
A4: for B being Ordinal st B in A holds
L . B = H1(B) ; ::_thesis: Rank A = union (rng L)
thus  H1(A) = H3(A,L) from ORDINAL2:sch_10(A1, A2, A3, A4); ::_thesis: verum
end;
end;

theorem :: CLASSES1:29
Rank {} = {} by Lm2;

theorem :: CLASSES1:30
for A being Ordinal holds Rank (succ A) = bool (Rank A) by Lm2;

theorem Th31: :: CLASSES1:31
for A being Ordinal st A <> {} & A is limit_ordinal holds
for x being set holds
( x in Rank A iff ex B being Ordinal st
( B in A & x in Rank B ) )
proof
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal implies for x being set holds
( x in Rank A iff ex B being Ordinal st
( B in A & x in Rank B ) ) )
assume A1: ( A <> {} & A is limit_ordinal ) ; ::_thesis: for x being set holds
( x in Rank A iff ex B being Ordinal st
( B in A & x in Rank B ) )
consider L being T-Sequence such that
A2: ( dom L = A & ( for B being Ordinal st B in A holds
L . B = H1(B) ) ) from ORDINAL2:sch_2();
A3: Rank A = union (rng L) by A1, A2, Lm2;
let x be set ; ::_thesis: ( x in Rank A iff ex B being Ordinal st
( B in A & x in Rank B ) )
thus  ( x in Rank A implies ex B being Ordinal st
( B in A & x in Rank B ) ) ::_thesis: ( ex B being Ordinal st
( B in A & x in Rank B ) implies x in Rank A )
proof
assume  x in Rank A ; ::_thesis: ex B being Ordinal st
( B in A & x in Rank B )
then consider Y being set  such that
A4: x in Y and
A5: Y in rng L by A3, TARSKI:def_4;
consider y being set  such that
A6: y in dom L and
A7: Y = L . y by A5, FUNCT_1:def_3;
reconsider y = y as Ordinal by A6;
take  y ; ::_thesis: ( y in A & x in Rank y )
thus  ( y in A & x in Rank y ) by A2, A4, A6, A7; ::_thesis: verum
end;
given B being Ordinal such that A8: B in A and
A9: x in Rank B ; ::_thesis: x in Rank A
 L . B = Rank B by A2, A8;
then  Rank B in rng L by A2, A8, FUNCT_1:def_3;
hence  x in Rank A by A3, A9, TARSKI:def_4; ::_thesis: verum
end;

theorem Th32: :: CLASSES1:32
for X being set
for A being Ordinal holds
( X c= Rank A iff X in Rank (succ A) )
proof
let X be set ; ::_thesis: for A being Ordinal holds
( X c= Rank A iff X in Rank (succ A) )
let A be Ordinal; ::_thesis: ( X c= Rank A iff X in Rank (succ A) )
thus  ( X c= Rank A implies X in Rank (succ A) ) ::_thesis: ( X in Rank (succ A) implies X c= Rank A )
proof
assume  X c= Rank A ; ::_thesis: X in Rank (succ A)
then  X in bool (Rank A) ;
hence  X in Rank (succ A) by Lm2; ::_thesis: verum
end;
assume  X in Rank (succ A) ; ::_thesis: X c= Rank A
then  X in bool (Rank A) by Lm2;
hence  X c= Rank A ; ::_thesis: verum
end;

registration
let A be Ordinal;
cluster Rank A ->  epsilon-transitive ;
coherence
 Rank A is epsilon-transitive
proof
defpred S1[ Ordinal] means  for X being set st X in Rank A holds
X c= Rank A;
A1: for A being Ordinal st ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be Ordinal; ::_thesis: ( ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume A2: for B being Ordinal st B in A holds
S1[B] ; ::_thesis: S1[A]
let X be set ; ::_thesis: ( X in Rank A implies X c= Rank A )
assume A3: X in Rank A ; ::_thesis: X c= Rank A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Rank A )
assume A4: x in X ; ::_thesis: x in Rank A
A5: now__::_thesis:_(_A_is_limit_ordinal_implies_x_in_Rank_A_)
assume A6: A is limit_ordinal ; ::_thesis: x in Rank A
then consider B being Ordinal such that
A7: B in A and
A8: X in Rank B by A3, Lm2, Th31;
 X c= Rank B by A2, A7, A8;
hence  x in Rank A by A4, A6, A7, Th31; ::_thesis: verum
end;
now__::_thesis:_(_not_A_is_limit_ordinal_implies_x_in_Rank_A_)
assume  not A is limit_ordinal ; ::_thesis: x in Rank A
then consider B being Ordinal such that
A9: A = succ B by ORDINAL1:29;
 X c= Rank B by A3, A9, Th32;
then  x c= Rank B by A2, A4, A9, ORDINAL1:6;
hence  x in Rank A by A9, Th32; ::_thesis: verum
end;
hence  x in Rank A by A5; ::_thesis: verum
end;
 for A being Ordinal holds S1[A] from ORDINAL1:sch_2(A1);
hence  S1[A] ; :: according to ORDINAL1:def_2 ::_thesis: verum
end;
end;

theorem :: CLASSES1:33
for A being Ordinal holds Rank A c= Rank (succ A)
proof
let A be Ordinal; ::_thesis: Rank A c= Rank (succ A)
 Rank A in bool (Rank A) by ZFMISC_1:def_1;
then  Rank A in Rank (succ A) by Lm2;
hence  Rank A c= Rank (succ A) by ORDINAL1:def_2; ::_thesis: verum
end;

theorem Th34: :: CLASSES1:34
for A being Ordinal holds union (Rank A) c= Rank A
proof
let A be Ordinal; ::_thesis: union (Rank A) c= Rank A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (Rank A) or x in Rank A )
assume  x in union (Rank A) ; ::_thesis: x in Rank A
then consider X being set  such that
A1: x in X and
A2: X in Rank A by TARSKI:def_4;
 X c= Rank A by A2, ORDINAL1:def_2;
hence  x in Rank A by A1; ::_thesis: verum
end;

theorem :: CLASSES1:35
for X being set
for A being Ordinal st X in Rank A holds
union X in Rank A
proof
let X be set ; ::_thesis: for A being Ordinal st X in Rank A holds
union X in Rank A
let A be Ordinal; ::_thesis: ( X in Rank A implies union X in Rank A )
assume A1: X in Rank A ; ::_thesis: union X in Rank A
A2: now__::_thesis:_(_ex_B_being_Ordinal_st_A_=_succ_B_implies_union_X_in_Rank_A_)
given B being Ordinal such that A3: A = succ B ; ::_thesis: union X in Rank A
 X c= Rank B by A1, A3, Th32;
then A4: union X c= union (Rank B) by ZFMISC_1:77;
 union (Rank B) c= Rank B by Th34;
then  union X c= Rank B by A4, XBOOLE_1:1;
hence  union X in Rank A by A3, Th32; ::_thesis: verum
end;
now__::_thesis:_(_A_<>_{}_&_(_for_B_being_Ordinal_holds_A_<>_succ_B_)_implies_union_X_in_Rank_A_)
assume that
A5: A <> {} and
A6: for B being Ordinal holds A <> succ B ; ::_thesis: union X in Rank A
A7: A is limit_ordinal by A6, ORDINAL1:29;
then consider B being Ordinal such that
A8: B in A and
A9: X in Rank B by A1, A5, Th31;
 X c= Rank B by A9, ORDINAL1:def_2;
then A10: union X c= union (Rank B) by ZFMISC_1:77;
 union (Rank B) c= Rank B by Th34;
then A11: union X c= Rank B by A10, XBOOLE_1:1;
A12: succ B c= A by A8, ORDINAL1:21;
 succ B <> A by A6;
then A13: succ B c< A by A12, XBOOLE_0:def_8;
A14: union X in Rank (succ B) by A11, Th32;
 succ B in A by A13, ORDINAL1:11;
hence  union X in Rank A by A7, A14, Th31; ::_thesis: verum
end;
hence  union X in Rank A by A1, A2, Lm2; ::_thesis: verum
end;

theorem Th36: :: CLASSES1:36
for A, B being Ordinal holds
( A in B iff Rank A in Rank B )
proof
let A, B be Ordinal; ::_thesis: ( A in B iff Rank A in Rank B )
defpred S1[ Ordinal, Ordinal] means ( $1 in $2 implies Rank $1 in Rank $2 );
A1: now__::_thesis:_for_A,_B_being_Ordinal_holds_S2[B]
let A be Ordinal; ::_thesis: for B being Ordinal holds S2[B]
defpred S2[ Ordinal] means S1[A,$1];
A2: for B being Ordinal st ( for C being Ordinal st C in B holds
S2[C] ) holds
S2[B]
proof
let B be Ordinal; ::_thesis: ( ( for C being Ordinal st C in B holds
S2[C] ) implies S2[B] )
assume that
A3: for C being Ordinal st C in B holds
S1[A,C] and
A4: A in B ; ::_thesis: Rank A in Rank B
A5: now__::_thesis:_(_ex_C_being_Ordinal_st_B_=_succ_C_implies_Rank_A_in_Rank_B_)
given C being Ordinal such that A6: B = succ C ; ::_thesis: Rank A in Rank B
A7: ( A in C implies Rank A in Rank C ) by A3, A6, ORDINAL1:6;
now__::_thesis:_(_not_A_in_C_implies_Rank_A_=_Rank_C_)
assume A8: not A in C ; ::_thesis: Rank A = Rank 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:11, ORDINAL1:22; ::_thesis: verum
end;
then  Rank A c= Rank C by A7, ORDINAL1:def_2;
hence  Rank A in Rank B by A6, Th32; ::_thesis: verum
end;
now__::_thesis:_(_(_for_C_being_Ordinal_holds_B_<>_succ_C_)_implies_Rank_A_in_Rank_B_)
assume A9: for C being Ordinal holds B <> succ C ; ::_thesis: Rank A in Rank B
then A10: B is limit_ordinal by ORDINAL1:29;
A11: B <> succ A by A9;
 succ A c= B by A4, ORDINAL1:21;
then  succ A c< B by A11, XBOOLE_0:def_8;
then A12: succ A in B by ORDINAL1:11;
 Rank A in Rank (succ A) by Th32;
hence  Rank A in Rank B by A10, A12, Th31; ::_thesis: verum
end;
hence  Rank A in Rank B by A5; ::_thesis: verum
end;
thus  for B being Ordinal holds S2[B] from ORDINAL1:sch_2(A2); ::_thesis: verum
end;
hence  S1[A,B] ; ::_thesis: ( Rank A in Rank B implies A in B )
assume that
A13: Rank A in Rank B and
A14: not A in B ; ::_thesis: contradiction
 ( B in A or B = A ) by A14, ORDINAL1:14;
hence  contradiction by A1, A13; ::_thesis: verum
end;

theorem Th37: :: CLASSES1:37
for A, B being Ordinal holds
( A c= B iff Rank A c= Rank B )
proof
let A, B be Ordinal; ::_thesis: ( A c= B iff Rank A c= Rank B )
thus  ( A c= B implies Rank A c= Rank B ) ::_thesis: ( Rank A c= Rank B implies A c= B )
proof
A1: ( A c< B iff ( A c= B & A <> B ) ) by XBOOLE_0:def_8;
assume  A c= B ; ::_thesis: Rank A c= Rank B
then  ( A = B or A in B ) by A1, ORDINAL1:11;
then  ( Rank A = Rank B or Rank A in Rank B ) by Th36;
hence  Rank A c= Rank B by ORDINAL1:def_2; ::_thesis: verum
end;
assume that
A2: Rank A c= Rank B and
A3: not A c= B ; ::_thesis: contradiction
 B in A by A3, ORDINAL1:16;
then  Rank B in Rank A by Th36;
hence  contradiction by A2, ORDINAL1:5; ::_thesis: verum
end;

theorem Th38: :: CLASSES1:38
for A being Ordinal holds A c= Rank A
proof
let A be Ordinal; ::_thesis: A c= Rank A
defpred S1[ Ordinal] means $1 c= Rank $1;
A1: S1[ {} ] by XBOOLE_1:2;
A2: for B being Ordinal st S1[B] holds
S1[ succ B]
proof
let B be Ordinal; ::_thesis: ( S1[B] implies S1[ succ B] )
assume  B c= Rank B ; ::_thesis: S1[ succ B]
then  B in Rank (succ B) by Th32;
then  ( B c= Rank (succ B) & {B} c= Rank (succ B) ) by ORDINAL1:def_2, ZFMISC_1:31;
hence  S1[ succ B] by XBOOLE_1:8; ::_thesis: verum
end;
A3: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume that
 A <> {} and
A4: A is limit_ordinal and
A5: for B being Ordinal st B in A holds
B c= Rank B ; ::_thesis: S1[A]
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in Rank A )
assume A6: x in A ; ::_thesis: x in Rank A
then reconsider B = x as Ordinal ;
A7: succ B in A by A4, A6, ORDINAL1:28;
A8: B c= Rank B by A5, A6;
A9: succ B c= A by A7, ORDINAL1:def_2;
A10: B in Rank (succ B) by A8, Th32;
 Rank (succ B) c= Rank A by A9, Th37;
hence  x in Rank A by A10; ::_thesis: verum
end;
 for B being Ordinal holds S1[B] from ORDINAL2:sch_1(A1, A2, A3);
hence  A c= Rank A ; ::_thesis: verum
end;

theorem :: CLASSES1:39
for A being Ordinal
for X being set st X in Rank A holds
( not X, Rank A are_equipotent & card X in card (Rank A) )
proof
defpred S1[ Ordinal] means  for X being set st X in Rank $1 holds
not X, Rank $1 are_equipotent ;
A1: for A being Ordinal st ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be Ordinal; ::_thesis: ( ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume A2: for B being Ordinal st B in A holds
S1[B] ; ::_thesis: S1[A]
let X be set ; ::_thesis: ( X in Rank A implies not X, Rank A are_equipotent )
assume A3: X in Rank A ; ::_thesis: not X, Rank A are_equipotent
A4: now__::_thesis:_(_ex_B_being_Ordinal_st_A_=_succ_B_implies_not_X,_Rank_A_are_equipotent_)
given B being Ordinal such that A5: A = succ B ; ::_thesis: not X, Rank A are_equipotent
 B in A by A5, ORDINAL1:6;
then A6: B c= A by ORDINAL1:def_2;
A7: Rank (succ B) = bool (Rank B) by Lm2;
then A8: not Rank B, Rank A are_equipotent by A5, CARD_1:13;
 Rank B c= Rank A by A6, Th37;
hence  not X, Rank A are_equipotent by A3, A5, A7, A8, CARD_1:24; ::_thesis: verum
end;
now__::_thesis:_(_A_<>_{}_&_(_for_B_being_Ordinal_holds_A_<>_succ_B_)_implies_not_X,_Rank_A_are_equipotent_)
assume that
A9: A <> {} and
A10: for B being Ordinal holds A <> succ B ; ::_thesis: not X, Rank A are_equipotent
 A is limit_ordinal by A10, ORDINAL1:29;
then consider B being Ordinal such that
A11: B in A and
A12: X in Rank B by A3, A9, Th31;
A13: Rank B in Rank A by A11, Th36;
A14: ( not X, Rank B are_equipotent & X c= Rank B ) by A2, A11, A12, ORDINAL1:def_2;
 Rank B c= Rank A by A13, ORDINAL1:def_2;
hence  not X, Rank A are_equipotent by A14, CARD_1:24; ::_thesis: verum
end;
hence  not X, Rank A are_equipotent by A3, A4, Lm2; ::_thesis: verum
end;
A15: for A being Ordinal holds S1[A] from ORDINAL1:sch_2(A1);
let A be Ordinal; ::_thesis: for X being set st X in Rank A holds
( not X, Rank A are_equipotent & card X in card (Rank A) )
let X be set ; ::_thesis: ( X in Rank A implies ( not X, Rank A are_equipotent & card X in card (Rank A) ) )
assume A16: X in Rank A ; ::_thesis: ( not X, Rank A are_equipotent & card X in card (Rank A) )
then A17: X c= Rank A by ORDINAL1:def_2;
A18: not X, Rank A are_equipotent by A15, A16;
A19: card X c= card (Rank A) by A17, CARD_1:11;
 card X <> card (Rank A) by A18, CARD_1:5;
hence  ( not X, Rank A are_equipotent & card X in card (Rank A) ) by A15, A16, A19, CARD_1:3; ::_thesis: verum
end;

theorem :: CLASSES1:40
for X being set
for A being Ordinal holds
( X c= Rank A iff bool X c= Rank (succ A) )
proof
let X be set ; ::_thesis: for A being Ordinal holds
( X c= Rank A iff bool X c= Rank (succ A) )
let A be Ordinal; ::_thesis: ( X c= Rank A iff bool X c= Rank (succ A) )
thus  ( X c= Rank A implies bool X c= Rank (succ A) ) ::_thesis: ( bool X c= Rank (succ A) implies X c= Rank A )
proof
assume A1: X c= Rank A ; ::_thesis: bool X c= Rank (succ A)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in bool X or x in Rank (succ A) )
assume  x in bool X ; ::_thesis: x in Rank (succ A)
then A2: x c= Rank A by A1, XBOOLE_1:1;
 Rank (succ A) = bool (Rank A) by Lm2;
hence  x in Rank (succ A) by A2; ::_thesis: verum
end;
assume A3: bool X c= Rank (succ A) ; ::_thesis: X c= Rank A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Rank A )
assume  x in X ; ::_thesis: x in Rank A
then  {x} c= X by ZFMISC_1:31;
then A4: {x} in bool X ;
 ( Rank (succ A) = bool (Rank A) & x in {x} ) by Lm2, TARSKI:def_1;
hence  x in Rank A by A3, A4; ::_thesis: verum
end;

theorem Th41: :: CLASSES1:41
for X, Y being set
for A being Ordinal st X c= Y & Y in Rank A holds
X in Rank A
proof
let X, Y be set ; ::_thesis: for A being Ordinal st X c= Y & Y in Rank A holds
X in Rank A
let A be Ordinal; ::_thesis: ( X c= Y & Y in Rank A implies X in Rank A )
assume that
A1: X c= Y and
A2: Y in Rank A ; ::_thesis: X in Rank A
A3: now__::_thesis:_(_ex_B_being_Ordinal_st_A_=_succ_B_implies_X_in_Rank_A_)
given B being Ordinal such that A4: A = succ B ; ::_thesis: X in Rank A
A5: Rank (succ B) = bool (Rank B) by Lm2;
then  X c= Rank B by A1, A2, A4, XBOOLE_1:1;
hence  X in Rank A by A4, A5; ::_thesis: verum
end;
now__::_thesis:_(_(_for_B_being_Ordinal_holds_A_<>_succ_B_)_implies_X_in_Rank_A_)
assume  for B being Ordinal holds A <> succ B ; ::_thesis: X in Rank A
then A6: A is limit_ordinal by ORDINAL1:29;
then consider B being Ordinal such that
A7: B in A and
A8: Y in Rank B by A2, Lm2, Th31;
 Y c= Rank B by A8, ORDINAL1:def_2;
then A9: X c= Rank B by A1, XBOOLE_1:1;
A10: bool (Rank B) = Rank (succ B) by Lm2;
 succ B in A by A6, A7, ORDINAL1:28;
hence  X in Rank A by A6, A9, A10, Th31; ::_thesis: verum
end;
hence  X in Rank A by A3; ::_thesis: verum
end;

theorem Th42: :: CLASSES1:42
for X being set
for A being Ordinal holds
( X in Rank A iff bool X in Rank (succ A) )
proof
let X be set ; ::_thesis: for A being Ordinal holds
( X in Rank A iff bool X in Rank (succ A) )
let A be Ordinal; ::_thesis: ( X in Rank A iff bool X in Rank (succ A) )
thus  ( X in Rank A implies bool X in Rank (succ A) ) ::_thesis: ( bool X in Rank (succ A) implies X in Rank A )
proof
assume A1: X in Rank A ; ::_thesis: bool X in Rank (succ A)
 bool X c= Rank A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in bool X or x in Rank A )
assume  x in bool X ; ::_thesis: x in Rank A
hence  x in Rank A by A1, Th41; ::_thesis: verum
end;
hence  bool X in Rank (succ A) by Th32; ::_thesis: verum
end;
assume  bool X in Rank (succ A) ; ::_thesis: X in Rank A
then  ( X in bool X & bool X c= Rank A ) by Th32, ZFMISC_1:def_1;
hence  X in Rank A ; ::_thesis: verum
end;

theorem Th43: :: CLASSES1:43
for x being set
for A being Ordinal holds
( x in Rank A iff {x} in Rank (succ A) )
proof
let x be set ; ::_thesis: for A being Ordinal holds
( x in Rank A iff {x} in Rank (succ A) )
let A be Ordinal; ::_thesis: ( x in Rank A iff {x} in Rank (succ A) )
 ( x in Rank A iff {x} c= Rank A ) by ZFMISC_1:31;
hence  ( x in Rank A iff {x} in Rank (succ A) ) by Th32; ::_thesis: verum
end;

theorem Th44: :: CLASSES1:44
for x, y being set
for A being Ordinal holds
( ( x in Rank A & y in Rank A ) iff {x,y} in Rank (succ A) )
proof
let x, y be set ; ::_thesis: for A being Ordinal holds
( ( x in Rank A & y in Rank A ) iff {x,y} in Rank (succ A) )
let A be Ordinal; ::_thesis: ( ( x in Rank A & y in Rank A ) iff {x,y} in Rank (succ A) )
 ( ( x in Rank A & y in Rank A ) iff {x,y} c= Rank A ) by ZFMISC_1:32;
hence  ( ( x in Rank A & y in Rank A ) iff {x,y} in Rank (succ A) ) by Th32; ::_thesis: verum
end;

theorem :: CLASSES1:45
for x, y being set
for A being Ordinal holds
( ( x in Rank A & y in Rank A ) iff [x,y] in Rank (succ (succ A)) )
proof
let x, y be set ; ::_thesis: for A being Ordinal holds
( ( x in Rank A & y in Rank A ) iff [x,y] in Rank (succ (succ A)) )
let A be Ordinal; ::_thesis: ( ( x in Rank A & y in Rank A ) iff [x,y] in Rank (succ (succ A)) )
A1: ( x in Rank A iff {x} in Rank (succ A) ) by Th43;
 ( ( x in Rank A & y in Rank A ) iff {x,y} in Rank (succ A) ) by Th44;
hence  ( ( x in Rank A & y in Rank A ) iff [x,y] in Rank (succ (succ A)) ) by A1, Th44; ::_thesis: verum
end;

theorem Th46: :: CLASSES1:46
for X being set
for A being Ordinal st X is epsilon-transitive & (Rank A) /\ (Tarski-Class X) = (Rank (succ A)) /\ (Tarski-Class X) holds
Tarski-Class X c= Rank A
proof
let X be set ; ::_thesis: for A being Ordinal st X is epsilon-transitive & (Rank A) /\ (Tarski-Class X) = (Rank (succ A)) /\ (Tarski-Class X) holds
Tarski-Class X c= Rank A
let A be Ordinal; ::_thesis: ( X is epsilon-transitive & (Rank A) /\ (Tarski-Class X) = (Rank (succ A)) /\ (Tarski-Class X) implies Tarski-Class X c= Rank A )
assume that
A1: X is epsilon-transitive and
A2: (Rank A) /\ (Tarski-Class X) = (Rank (succ A)) /\ (Tarski-Class X) ; ::_thesis: Tarski-Class X c= Rank A
given x being set  such that A3: ( x in Tarski-Class X & not x in Rank A ) ; :: according to TARSKI:def_3 ::_thesis: contradiction
 x in (Tarski-Class X) \ (Rank A) by A3, XBOOLE_0:def_5;
then consider Y being set  such that
A4: Y in (Tarski-Class X) \ (Rank A) and
A5: for x being set holds
( not x in (Tarski-Class X) \ (Rank A) or not x in Y ) by TARSKI:2;
 Tarski-Class X is epsilon-transitive by A1, Th23;
then A6: Y c= Tarski-Class X by A4, ORDINAL1:def_2;
 Y c= Rank A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in Rank A )
assume A7: x in Y ; ::_thesis: x in Rank A
then  not x in (Tarski-Class X) \ (Rank A) by A5;
hence  x in Rank A by A6, A7, XBOOLE_0:def_5; ::_thesis: verum
end;
then  Y in Rank (succ A) by Th32;
then A8: Y in (Rank (succ A)) /\ (Tarski-Class X) by A4, XBOOLE_0:def_4;
 not Y in Rank A by A4, XBOOLE_0:def_5;
hence  contradiction by A2, A8, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th47: :: CLASSES1:47
for X being set st X is epsilon-transitive holds
ex A being Ordinal st Tarski-Class X c= Rank A
proof
let X be set ; ::_thesis: ( X is epsilon-transitive implies ex A being Ordinal st Tarski-Class X c= Rank A )
assume A1: X is epsilon-transitive ; ::_thesis: ex A being Ordinal st Tarski-Class X c= Rank A
assume A2: for A being Ordinal holds not Tarski-Class X c= Rank A ; ::_thesis: contradiction
defpred S1[ set ] means  ex A being Ordinal st $1 in Rank A;
consider Power being set  such that
A3: for x being set holds
( x in Power iff ( x in Tarski-Class X & S1[x] ) ) from XBOOLE_0:sch_1();
defpred S2[ set , set ] means  ex A being Ordinal st
( $2 = A & not $1 in Rank A & $1 in Rank (succ A) );
A4: for x, y, z being set st S2[x,y] & S2[x,z] holds
y = z
proof
let x, y, z be set ; ::_thesis: ( S2[x,y] & S2[x,z] implies y = z )
given A1 being Ordinal such that A5: y = A1 and
A6: not x in Rank A1 and
A7: x in Rank (succ A1) ; ::_thesis: ( not S2[x,z] or y = z )
given A2 being Ordinal such that A8: z = A2 and
A9: not x in Rank A2 and
A10: x in Rank (succ A2) ; ::_thesis: y = z
assume  y <> z ; ::_thesis: contradiction
then  ( A1 in A2 or A2 in A1 ) by A5, A8, ORDINAL1:14;
then A11: ( succ A1 c= A2 or succ A2 c= A1 ) by ORDINAL1:21;
now__::_thesis:_not_succ_A1_c=_A2
assume  succ A1 c= A2 ; ::_thesis: contradiction
then  Rank (succ A1) c= Rank A2 by Th37;
hence  contradiction by A7, A9; ::_thesis: verum
end;
then  Rank (succ A2) c= Rank A1 by A11, Th37;
hence  contradiction by A6, A10; ::_thesis: verum
end;
consider Y being set  such that
A12: for x being set holds
( x in Y iff ex y being set st
( y in Power & S2[y,x] ) ) from TARSKI:sch_1(A4);
now__::_thesis:_for_A_being_Ordinal_holds_A_in_Y
let A be Ordinal; ::_thesis: A in Y
 (Rank A) /\ (Tarski-Class X) <> (Rank (succ A)) /\ (Tarski-Class X) by A1, A2, Th46;
then consider y being set  such that
A13: ( ( y in (Rank A) /\ (Tarski-Class X) & not y in (Rank (succ A)) /\ (Tarski-Class X) ) or ( y in (Rank (succ A)) /\ (Tarski-Class X) & not y in (Rank A) /\ (Tarski-Class X) ) ) by TARSKI:1;
 A in succ A by ORDINAL1:6;
then  A c= succ A by ORDINAL1:def_2;
then A14: Rank A c= Rank (succ A) by Th37;
then  (Rank A) /\ (Tarski-Class X) c= (Rank (succ A)) /\ (Tarski-Class X) by XBOOLE_1:26;
then A15: y in Rank (succ A) by A13, XBOOLE_0:def_4;
A16: y in Tarski-Class X by A13, XBOOLE_0:def_4;
A17: ( not y in Rank A or not y in Tarski-Class X ) by A13, A14, XBOOLE_0:def_4;
 y in Power by A3, A15, A16;
hence  A in Y by A12, A13, A15, A17, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  contradiction by ORDINAL1:26; ::_thesis: verum
end;

theorem Th48: :: CLASSES1:48
for X being set st X is epsilon-transitive holds
union X c= X
proof
let X be set ; ::_thesis: ( X is epsilon-transitive implies union X c= X )
assume A1: for Y being set st Y in X holds
Y c= X ; :: according to ORDINAL1:def_2 ::_thesis: union X c= X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union X or x in X )
assume  x in union X ; ::_thesis: x in X
then consider Y being set  such that
A2: x in Y and
A3: Y in X by TARSKI:def_4;
 Y c= X by A1, A3;
hence  x in X by A2; ::_thesis: verum
end;

theorem Th49: :: CLASSES1:49
for X, Y being set st X is epsilon-transitive & Y is epsilon-transitive holds
X \/ Y is epsilon-transitive
proof
let X, Y be set ; ::_thesis: ( X is epsilon-transitive & Y is epsilon-transitive implies X \/ Y is epsilon-transitive )
assume that
A1: for Z being set st Z in X holds
Z c= X and
A2: for Z being set st Z in Y holds
Z c= Y ; :: according to ORDINAL1:def_2 ::_thesis: X \/ Y is epsilon-transitive
let Z be set ; :: according to ORDINAL1:def_2 ::_thesis: ( not Z in X \/ Y or Z c= X \/ Y )
assume  Z in X \/ Y ; ::_thesis: Z c= X \/ Y
then  ( Z in X or Z in Y ) by XBOOLE_0:def_3;
then A3: ( Z c= X or Z c= Y ) by A1, A2;
 ( X c= X \/ Y & Y c= X \/ Y ) by XBOOLE_1:7;
hence  Z c= X \/ Y by A3, XBOOLE_1:1; ::_thesis: verum
end;

theorem :: CLASSES1:50
for X, Y being set st X is epsilon-transitive & Y is epsilon-transitive holds
X /\ Y is epsilon-transitive
proof
let X, Y be set ; ::_thesis: ( X is epsilon-transitive & Y is epsilon-transitive implies X /\ Y is epsilon-transitive )
assume that
A1: for Z being set st Z in X holds
Z c= X and
A2: for Z being set st Z in Y holds
Z c= Y ; :: according to ORDINAL1:def_2 ::_thesis: X /\ Y is epsilon-transitive
let Z be set ; :: according to ORDINAL1:def_2 ::_thesis: ( not Z in X /\ Y or Z c= X /\ Y )
assume A3: Z in X /\ Y ; ::_thesis: Z c= X /\ Y
then A4: Z in X by XBOOLE_0:def_4;
A5: Z in Y by A3, XBOOLE_0:def_4;
A6: Z c= X by A1, A4;
 Z c= Y by A2, A5;
hence  Z c= X /\ Y by A6, XBOOLE_1:19; ::_thesis: verum
end;

 deffunc H2( set , set ) ->  set = union $2;

definition
let X be set ;
func the_transitive-closure_of X ->  set  means :Def7: :: CLASSES1:def 7
 for x being set holds
( x in it iff ex f being Function ex n being Element of omega st
( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex f being Function ex n being Element of omega st
( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) )
proof
consider f being Function such that
A1: ( dom f = omega & f . 0 = X & ( for n being Nat holds f . (succ n) = H2(n,f . n) ) ) from ORDINAL2:sch_18();
take UNI = union (rng f); ::_thesis: for x being set holds
( x in UNI iff ex f being Function ex n being Element of omega st
( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) )
let x be set ; ::_thesis: ( x in UNI iff ex f being Function ex n being Element of omega st
( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) )
thus  ( x in UNI implies ex f being Function ex n being Element of omega st
( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) ) ::_thesis: ( ex f being Function ex n being Element of omega st
( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) implies x in UNI )
proof
assume  x in UNI ; ::_thesis: ex f being Function ex n being Element of omega st
( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) )
then consider Y being set  such that
A2: x in Y and
A3: Y in rng f by TARSKI:def_4;
consider y being set  such that
A4: y in dom f and
A5: Y = f . y by A3, FUNCT_1:def_3;
reconsider y = y as Element of omega by A1, A4;
take  f ; ::_thesis: ex n being Element of omega st
( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) )
take  y ; ::_thesis: ( x in f . y & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) )
thus  ( x in f . y & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) by A1, A2, A5; ::_thesis: verum
end;
deffunc H3( set , set ) ->  set = union $2;
given g being Function, n being Element of omega  such that A6: x in g . n and
A7: dom g = omega and
A8: g . 0 = X and
A9: for k being Nat holds g . (succ k) = H3(k,g . k) ; ::_thesis: x in UNI
A10: dom f = omega by A1;
A11: f . 0 = X by A1;
A12: for n being Nat holds f . (succ n) = H3(n,f . n) by A1;
 g = f from ORDINAL2:sch_20(A7, A8, A9, A10, A11, A12);
then  g . n in rng f by A1, FUNCT_1:def_3;
hence  x in UNI by A6, TARSKI:def_4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex f being Function ex n being Element of omega st
( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) ) ) & ( for x being set holds
( x in b2 iff ex f being Function ex n being Element of omega st
( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means  ex f being Function ex n being Element of omega st
( $1 in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) );
let U1, U2 be set ; ::_thesis: ( ( for x being set holds
( x in U1 iff ex f being Function ex n being Element of omega st
( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) ) ) & ( for x being set holds
( x in U2 iff ex f being Function ex n being Element of omega st
( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) ) ) implies U1 = U2 )
assume that
A13: for x being set holds
( x in U1 iff S1[x] ) and
A14: for x being set holds
( x in U2 iff S1[x] ) ; ::_thesis: U1 = U2
thus  U1 = U2 from XBOOLE_0:sch_2(A13, A14); ::_thesis: verum
end;
end;

:: deftheorem Def7 defines the_transitive-closure_of CLASSES1:def_7_:_
 for X, b2 being set holds
( b2 = the_transitive-closure_of X iff for x being set holds
( x in b2 iff ex f being Function ex n being Element of omega st
( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) ) );

theorem Th51: :: CLASSES1:51
for X being set holds the_transitive-closure_of X is epsilon-transitive
proof
let X be set ; ::_thesis: the_transitive-closure_of X is epsilon-transitive
let Y be set ; :: according to ORDINAL1:def_2 ::_thesis: ( not Y in the_transitive-closure_of X or Y c= the_transitive-closure_of X )
assume  Y in the_transitive-closure_of X ; ::_thesis: Y c= the_transitive-closure_of X
then consider f being Function, n being Element of omega  such that
A1: Y in f . n and
A2: ( dom f = omega & f . 0 = X ) and
A3: for k being Nat holds f . (succ k) = union (f . k) by Def7;
A4: f . (succ n) = union (f . n) by A3;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in the_transitive-closure_of X )
assume  x in Y ; ::_thesis: x in the_transitive-closure_of X
then A5: x in union (f . n) by A1, TARSKI:def_4;
reconsider m = succ n as Element of omega by ORDINAL1:def_12;
 x in f . m by A4, A5;
hence  x in the_transitive-closure_of X by A2, A3, Def7; ::_thesis: verum
end;

theorem Th52: :: CLASSES1:52
for X being set holds X c= the_transitive-closure_of X
proof
let X be set ; ::_thesis: X c= the_transitive-closure_of X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in the_transitive-closure_of X )
assume A1: x in X ; ::_thesis: x in the_transitive-closure_of X
consider f being Function such that
A2: dom f = omega and
A3: f . 0 = X and
A4: for n being Nat holds f . (succ n) = H2(n,f . n) from ORDINAL2:sch_18();
reconsider z = 0 as Element of omega by ORDINAL1:def_12;
 x in f . z by A1, A3;
hence  x in the_transitive-closure_of X by A2, A3, A4, Def7; ::_thesis: verum
end;

theorem Th53: :: CLASSES1:53
for X, Y being set st X c= Y & Y is epsilon-transitive holds
the_transitive-closure_of X c= Y
proof
let X, Y be set ; ::_thesis: ( X c= Y & Y is epsilon-transitive implies the_transitive-closure_of X c= Y )
assume that
A1: X c= Y and
A2: Y is epsilon-transitive ; ::_thesis: the_transitive-closure_of X c= Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the_transitive-closure_of X or x in Y )
assume  x in the_transitive-closure_of X ; ::_thesis: x in Y
then consider f being Function, n being Element of omega  such that
A3: x in f . n and
 dom f = omega and
A4: f . 0 = X and
A5: for k being Nat holds f . (succ k) = union (f . k) by Def7;
defpred S1[ Nat] means f . $1 c= Y;
A6: S1[ 0 ] by A1, A4;
A7: for k being Nat st S1[k] holds
S1[ succ k]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[ succ k] )
assume  f . k c= Y ; ::_thesis: S1[ succ k]
then A8: union (f . k) c= union Y by ZFMISC_1:77;
 ( f . (succ k) = union (f . k) & union Y c= Y ) by A2, A5, Th48;
hence  S1[ succ k] by A8, XBOOLE_1:1; ::_thesis: verum
end;
 S1[n] from ORDINAL2:sch_17(A6, A7);
then  f . n c= Y ;
hence  x in Y by A3; ::_thesis: verum
end;

theorem Th54: :: CLASSES1:54
for X, Y being set st ( for Z being set st X c= Z & Z is epsilon-transitive holds
Y c= Z ) & X c= Y & Y is epsilon-transitive holds
the_transitive-closure_of X = Y
proof
let X, Y be set ; ::_thesis: ( ( for Z being set 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 )
assume A1: for Z being set st X c= Z & Z is epsilon-transitive holds
Y c= Z ; ::_thesis: ( not X c= Y or not Y is epsilon-transitive or the_transitive-closure_of X = Y )
assume  ( X c= Y & Y is epsilon-transitive ) ; ::_thesis: the_transitive-closure_of X = Y
hence  the_transitive-closure_of X c= Y by Th53; :: according to XBOOLE_0:def_10 ::_thesis: Y c= the_transitive-closure_of X
 the_transitive-closure_of X is epsilon-transitive by Th51;
hence  Y c= the_transitive-closure_of X by A1, Th52; ::_thesis: verum
end;

theorem Th55: :: CLASSES1:55
for X being set st X is epsilon-transitive holds
the_transitive-closure_of X = X
proof
let X be set ; ::_thesis: ( X is epsilon-transitive implies the_transitive-closure_of X = X )
 for Z being set st X c= Z & Z is epsilon-transitive holds
X c= Z ;
hence  ( X is epsilon-transitive implies the_transitive-closure_of X = X ) by Th54; ::_thesis: verum
end;

theorem :: CLASSES1:56
the_transitive-closure_of {} = {} by Th55;

theorem :: CLASSES1:57
for A being Ordinal holds the_transitive-closure_of A = A by Th55;

theorem Th58: :: CLASSES1:58
for X, Y being set st X c= Y holds
the_transitive-closure_of X c= the_transitive-closure_of Y
proof
let X, Y be set ; ::_thesis: ( X c= Y implies the_transitive-closure_of X c= the_transitive-closure_of Y )
assume A1: X c= Y ; ::_thesis: the_transitive-closure_of X c= the_transitive-closure_of Y
 Y c= the_transitive-closure_of Y by Th52;
then  X c= the_transitive-closure_of Y by A1, XBOOLE_1:1;
hence  the_transitive-closure_of X c= the_transitive-closure_of Y by Th51, Th53; ::_thesis: verum
end;

theorem :: CLASSES1:59
for X being set holds the_transitive-closure_of (the_transitive-closure_of X) = the_transitive-closure_of X by Th51, Th55;

theorem :: CLASSES1:60
for X, Y being set holds the_transitive-closure_of (X \/ Y) = (the_transitive-closure_of X) \/ (the_transitive-closure_of Y)
proof
let X, Y be set ; ::_thesis: the_transitive-closure_of (X \/ Y) = (the_transitive-closure_of X) \/ (the_transitive-closure_of Y)
 ( X c= the_transitive-closure_of X & Y c= the_transitive-closure_of Y ) by Th52;
then A1: X \/ Y c= (the_transitive-closure_of X) \/ (the_transitive-closure_of Y) by XBOOLE_1:13;
A2: ( the_transitive-closure_of X is epsilon-transitive & the_transitive-closure_of Y is epsilon-transitive ) by Th51;
 the_transitive-closure_of (X \/ Y) c= the_transitive-closure_of ((the_transitive-closure_of X) \/ (the_transitive-closure_of Y)) by A1, Th58;
hence  the_transitive-closure_of (X \/ Y) c= (the_transitive-closure_of X) \/ (the_transitive-closure_of Y) by A2, Th49, Th55; :: according to XBOOLE_0:def_10 ::_thesis: (the_transitive-closure_of X) \/ (the_transitive-closure_of Y) c= the_transitive-closure_of (X \/ Y)
 ( 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 Th58, XBOOLE_1:7;
hence  (the_transitive-closure_of X) \/ (the_transitive-closure_of Y) c= the_transitive-closure_of (X \/ Y) by XBOOLE_1:8; ::_thesis: verum
end;

theorem :: CLASSES1:61
for X, Y being set holds the_transitive-closure_of (X /\ Y) c= (the_transitive-closure_of X) /\ (the_transitive-closure_of Y)
proof
let X, Y be set ; ::_thesis: the_transitive-closure_of (X /\ Y) c= (the_transitive-closure_of X) /\ (the_transitive-closure_of Y)
 ( 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 Th58, XBOOLE_1:17;
hence  the_transitive-closure_of (X /\ Y) c= (the_transitive-closure_of X) /\ (the_transitive-closure_of Y) by XBOOLE_1:19; ::_thesis: verum
end;

theorem Th62: :: CLASSES1:62
for X being set ex A being Ordinal st X c= Rank A
proof
let X be set ; ::_thesis: ex A being Ordinal st X c= Rank A
consider A being Ordinal such that
A1: Tarski-Class (the_transitive-closure_of X) c= Rank A by Th47, Th51;
take  A ; ::_thesis: X c= Rank A
 the_transitive-closure_of X in Tarski-Class (the_transitive-closure_of X) by Th2;
then  X in Tarski-Class (the_transitive-closure_of X) by Th3, Th52;
hence  X c= Rank A by A1, ORDINAL1:def_2; ::_thesis: verum
end;

definition
let X be set ;
func the_rank_of X ->  Ordinal means :Def8: :: CLASSES1:def 8
( X c= Rank it & ( for B being Ordinal st X c= Rank B holds
it c= B ) );
existence
 ex b1 being Ordinal st
( X c= Rank b1 & ( for B being Ordinal st X c= Rank B holds
b1 c= B ) )
proof
defpred S1[ Ordinal] means X c= Rank $1;
A1: ex A being Ordinal st S1[A] by Th62;
thus  ex A being Ordinal st
( S1[A] & ( for B being Ordinal st S1[B] holds
A c= B ) ) from ORDINAL1:sch_1(A1); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Ordinal st X c= Rank b1 & ( for B being Ordinal st X c= Rank B holds
b1 c= B ) & X c= Rank b2 & ( for B being Ordinal st X c= Rank B holds
b2 c= B ) holds
b1 = b2
proof
let A1, A2 be Ordinal; ::_thesis: ( X c= Rank A1 & ( for B being Ordinal st X c= Rank B holds
A1 c= B ) & X c= Rank A2 & ( for B being Ordinal st X c= Rank B holds
A2 c= B ) implies A1 = A2 )
assume A2: ( X c= Rank A1 & ( for B being Ordinal st X c= Rank B holds
A1 c= B ) & X c= Rank A2 & ( for B being Ordinal st X c= Rank B holds
A2 c= B ) ) ; ::_thesis: A1 = A2
thus  ( A1 c= A2 & A2 c= A1 ) by A2; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;
end;

:: deftheorem Def8 defines the_rank_of CLASSES1:def_8_:_
 for X being set
for b2 being Ordinal holds
( b2 = the_rank_of X iff ( X c= Rank b2 & ( for B being Ordinal st X c= Rank B holds
b2 c= B ) ) );

theorem Th63: :: CLASSES1:63
for X being set holds the_rank_of (bool X) = succ (the_rank_of X)
proof
let X be set ; ::_thesis: the_rank_of (bool X) = succ (the_rank_of X)
A1: X c= Rank (the_rank_of X) by Def8;
A2: bool X c= Rank (succ (the_rank_of X))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in bool X or x in Rank (succ (the_rank_of X)) )
assume  x in bool X ; ::_thesis: x in Rank (succ (the_rank_of X))
then A3: x c= Rank (the_rank_of X) by A1, XBOOLE_1:1;
 bool (Rank (the_rank_of X)) = Rank (succ (the_rank_of X)) by Lm2;
hence  x in Rank (succ (the_rank_of X)) by A3; ::_thesis: verum
end;
 for A being Ordinal st bool X c= Rank A holds
succ (the_rank_of X) c= A
proof
let A be Ordinal; ::_thesis: ( bool X c= Rank A implies succ (the_rank_of X) c= A )
assume A4: bool X c= Rank A ; ::_thesis: succ (the_rank_of X) c= A
defpred S1[ Ordinal] means X in Rank $1;
A5: X in bool X by ZFMISC_1:def_1;
then A6: ex A being Ordinal st S1[A] by A4;
consider B being Ordinal such that
A7: ( S1[B] & ( for C being Ordinal st S1[C] holds
B c= C ) ) from ORDINAL1:sch_1(A6);
now__::_thesis:_not__for_C_being_Ordinal_holds_B_<>_succ_C
assume  for C being Ordinal holds B <> succ C ; ::_thesis: contradiction
then  B is limit_ordinal by ORDINAL1:29;
then  ex C being Ordinal st
( C in B & X in Rank C ) by A7, Lm2, Th31;
hence  contradiction by A7, ORDINAL1:5; ::_thesis: verum
end;
then consider C being Ordinal such that
A8: B = succ C ;
 X c= Rank C by A7, A8, Th32;
then  the_rank_of X c= C by Def8;
then A9: the_rank_of X in B by A8, ORDINAL1:22;
 B c= A by A4, A5, A7;
hence  succ (the_rank_of X) c= A by A9, ORDINAL1:21; ::_thesis: verum
end;
hence  the_rank_of (bool X) = succ (the_rank_of X) by A2, Def8; ::_thesis: verum
end;

theorem :: CLASSES1:64
for A being Ordinal holds the_rank_of (Rank A) = A
proof
let A be Ordinal; ::_thesis: the_rank_of (Rank A) = A
 for B being Ordinal st Rank A c= Rank B holds
A c= B by Th37;
hence  the_rank_of (Rank A) = A by Def8; ::_thesis: verum
end;

theorem Th65: :: CLASSES1:65
for X being set
for A being Ordinal holds
( X c= Rank A iff the_rank_of X c= A )
proof
let X be set ; ::_thesis: for A being Ordinal holds
( X c= Rank A iff the_rank_of X c= A )
let A be Ordinal; ::_thesis: ( X c= Rank A iff the_rank_of X c= A )
thus  ( X c= Rank A implies the_rank_of X c= A ) by Def8; ::_thesis: ( the_rank_of X c= A implies X c= Rank A )
assume  the_rank_of X c= A ; ::_thesis: X c= Rank A
then A1: Rank (the_rank_of X) c= Rank A by Th37;
 X c= Rank (the_rank_of X) by Def8;
hence  X c= Rank A by A1, XBOOLE_1:1; ::_thesis: verum
end;

theorem Th66: :: CLASSES1:66
for X being set
for A being Ordinal holds
( X in Rank A iff the_rank_of X in A )
proof
let X be set ; ::_thesis: for A being Ordinal holds
( X in Rank A iff the_rank_of X in A )
let A be Ordinal; ::_thesis: ( X in Rank A iff the_rank_of X in A )
thus  ( X in Rank A implies the_rank_of X in A ) ::_thesis: ( the_rank_of X in A implies X in Rank A )
proof
assume  X in Rank A ; ::_thesis: the_rank_of X in A
then  bool X in Rank (succ A) by Th42;
then A1: bool X c= Rank A by Th32;
 the_rank_of (bool X) = succ (the_rank_of X) by Th63;
then A2: the_rank_of X in the_rank_of (bool X) by ORDINAL1:6;
 the_rank_of (bool X) c= A by A1, Def8;
hence  the_rank_of X in A by A2; ::_thesis: verum
end;
assume  the_rank_of X in A ; ::_thesis: X in Rank A
then A3: succ (the_rank_of X) c= A by ORDINAL1:21;
 X c= Rank (the_rank_of X) by Def8;
then A4: X in Rank (succ (the_rank_of X)) by Th32;
 Rank (succ (the_rank_of X)) c= Rank A by A3, Th37;
hence  X in Rank A by A4; ::_thesis: verum
end;

theorem :: CLASSES1:67
for X, Y being set st X c= Y holds
the_rank_of X c= the_rank_of Y
proof
let X, Y be set ; ::_thesis: ( X c= Y implies the_rank_of X c= the_rank_of Y )
assume A1: X c= Y ; ::_thesis: the_rank_of X c= the_rank_of Y
 Y c= Rank (the_rank_of Y) by Def8;
then  X c= Rank (the_rank_of Y) by A1, XBOOLE_1:1;
hence  the_rank_of X c= the_rank_of Y by Def8; ::_thesis: verum
end;

theorem Th68: :: CLASSES1:68
for X, Y being set st X in Y holds
the_rank_of X in the_rank_of Y
proof
let X, Y be set ; ::_thesis: ( X in Y implies the_rank_of X in the_rank_of Y )
assume A1: X in Y ; ::_thesis: the_rank_of X in the_rank_of Y
 Y c= Rank (the_rank_of Y) by Def8;
hence  the_rank_of X in the_rank_of Y by A1, Th66; ::_thesis: verum
end;

theorem Th69: :: CLASSES1:69
for X being set
for A being Ordinal holds
( the_rank_of X c= A iff for Y being set st Y in X holds
the_rank_of Y in A )
proof
let X be set ; ::_thesis: for A being Ordinal holds
( the_rank_of X c= A iff for Y being set st Y in X holds
the_rank_of Y in A )
let A be Ordinal; ::_thesis: ( the_rank_of X c= A iff for Y being set st Y in X holds
the_rank_of Y in A )
set R = the_rank_of X;
A1: X c= Rank (the_rank_of X) by Def8;
thus  ( the_rank_of X c= A implies for Y being set st Y in X holds
the_rank_of Y in A ) ::_thesis: ( ( for Y being set st Y in X holds
the_rank_of Y in A ) implies the_rank_of X c= A )
proof
assume A2: the_rank_of X c= A ; ::_thesis: for Y being set st Y in X holds
the_rank_of Y in A
let Y be set ; ::_thesis: ( Y in X implies the_rank_of Y in A )
assume  Y in X ; ::_thesis: the_rank_of Y in A
then A3: Y in Rank (the_rank_of X) by A1;
 Rank (the_rank_of X) c= Rank A by A2, Th37;
hence  the_rank_of Y in A by A3, Th66; ::_thesis: verum
end;
assume A4: for Y being set st Y in X holds
the_rank_of Y in A ; ::_thesis: the_rank_of X c= A
 X c= Rank A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Rank A )
assume  x in X ; ::_thesis: x in Rank A
then  the_rank_of x in A by A4;
hence  x in Rank A by Th66; ::_thesis: verum
end;
hence  the_rank_of X c= A by Def8; ::_thesis: verum
end;

theorem Th70: :: CLASSES1:70
for X being set
for A being Ordinal holds
( A c= the_rank_of X iff for B being Ordinal st B in A holds
ex Y being set st
( Y in X & B c= the_rank_of Y ) )
proof
let X be set ; ::_thesis: for A being Ordinal holds
( A c= the_rank_of X iff for B being Ordinal st B in A holds
ex Y being set st
( Y in X & B c= the_rank_of Y ) )
let A be Ordinal; ::_thesis: ( A c= the_rank_of X iff for B being Ordinal st B in A holds
ex Y being set st
( Y in X & B c= the_rank_of Y ) )
thus  ( A c= the_rank_of X implies for B being Ordinal st B in A holds
ex Y being set st
( Y in X & B c= the_rank_of Y ) ) ::_thesis: ( ( for B being Ordinal st B in A holds
ex Y being set st
( Y in X & B c= the_rank_of Y ) ) implies A c= the_rank_of X )
proof
assume A1: A c= the_rank_of X ; ::_thesis: for B being Ordinal st B in A holds
ex Y being set st
( Y in X & B c= the_rank_of Y )
let B be Ordinal; ::_thesis: ( B in A implies ex Y being set st
( Y in X & B c= the_rank_of Y ) )
assume  B in A ; ::_thesis: ex Y being set st
( Y in X & B c= the_rank_of Y )
then  not the_rank_of X c= B by A1, ORDINAL1:5;
then  not X c= Rank B by Def8;
then A2: X \ (Rank B) <> {} by XBOOLE_1:37;
set x = the Element of X \ (Rank B);
take  the Element of X \ (Rank B) ; ::_thesis: ( the Element of X \ (Rank B) in X & B c= the_rank_of the Element of X \ (Rank B) )
A3: not the Element of X \ (Rank B) in Rank B by A2, XBOOLE_0:def_5;
thus  the Element of X \ (Rank B) in X by A2, XBOOLE_0:def_5; ::_thesis: B c= the_rank_of the Element of X \ (Rank B)
 not the_rank_of the Element of X \ (Rank B) in B by A3, Th66;
hence  B c= the_rank_of the Element of X \ (Rank B) by ORDINAL1:16; ::_thesis: verum
end;
assume A4: for B being Ordinal st B in A holds
ex Y being set st
( Y in X & B c= the_rank_of Y ) ; ::_thesis: A c= the_rank_of X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in the_rank_of X )
assume A5: x in A ; ::_thesis: x in the_rank_of X
then reconsider x = x as Ordinal ;
consider Y being set  such that
A6: Y in X and
A7: x c= the_rank_of Y by A4, A5;
 the_rank_of Y in the_rank_of X by A6, Th68;
hence  x in the_rank_of X by A7, ORDINAL1:12; ::_thesis: verum
end;

theorem :: CLASSES1:71
for X being set holds
( the_rank_of X = {} iff X = {} )
proof
let X be set ; ::_thesis: ( the_rank_of X = {} iff X = {} )
thus  ( the_rank_of X = {} implies X = {} ) ::_thesis: ( X = {} implies the_rank_of X = {} )
proof
assume  the_rank_of X = {} ; ::_thesis: X = {}
then  X c= Rank {} by Def8;
hence  X = {} by Lm2; ::_thesis: verum
end;
assume  X = {} ; ::_thesis: the_rank_of X = {}
then  for Y being set st Y in X holds
the_rank_of Y in {} ;
hence  the_rank_of X c= {} by Th69; :: according to XBOOLE_0:def_10 ::_thesis: {} c= the_rank_of X
thus  {} c= the_rank_of X ; ::_thesis: verum
end;

theorem Th72: :: CLASSES1:72
for X being set
for A being Ordinal st the_rank_of X = succ A holds
ex Y being set st
( Y in X & the_rank_of Y = A )
proof
let X be set ; ::_thesis: for A being Ordinal st the_rank_of X = succ A holds
ex Y being set st
( Y in X & the_rank_of Y = A )
let A be Ordinal; ::_thesis: ( the_rank_of X = succ A implies ex Y being set st
( Y in X & the_rank_of Y = A ) )
assume A1: the_rank_of X = succ A ; ::_thesis: ex Y being set st
( Y in X & the_rank_of Y = A )
 A in succ A by ORDINAL1:6;
then consider Y being set  such that
A2: Y in X and
A3: A c= the_rank_of Y by A1, Th70;
take  Y ; ::_thesis: ( Y in X & the_rank_of Y = A )
 the_rank_of Y in the_rank_of X by A2, Th68;
then  the_rank_of Y c= A by A1, ORDINAL1:22;
hence  ( Y in X & the_rank_of Y = A ) by A2, A3, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: CLASSES1:73
for A being Ordinal holds the_rank_of A = A
proof
let A be Ordinal; ::_thesis: the_rank_of A = A
 A c= Rank A by Th38;
hence  the_rank_of A c= A by Th65; :: according to XBOOLE_0:def_10 ::_thesis: A c= the_rank_of A
defpred S1[ Ordinal] means $1 c= the_rank_of $1;
A1: for A being Ordinal st ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be Ordinal; ::_thesis: ( ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume A2: for B being Ordinal st B in A holds
B c= the_rank_of B ; ::_thesis: S1[A]
now__::_thesis:_for_B_being_Ordinal_st_B_in_A_holds_
ex_Y_being_set_st_
(_Y_in_A_&_B_c=_the_rank_of_Y_)
let B be Ordinal; ::_thesis: ( B in A implies ex Y being set st
( Y in A & B c= the_rank_of Y ) )
assume A3: B in A ; ::_thesis: ex Y being set st
( Y in A & B c= the_rank_of Y )
reconsider Y = B as set ;
take Y = Y; ::_thesis: ( Y in A & B c= the_rank_of Y )
thus  ( Y in A & B c= the_rank_of Y ) by A2, A3; ::_thesis: verum
end;
hence  S1[A] by Th70; ::_thesis: verum
end;
 for B being Ordinal holds S1[B] from ORDINAL1:sch_2(A1);
hence  A c= the_rank_of A ; ::_thesis: verum
end;

theorem :: CLASSES1:74
for X being set holds
( the_rank_of (Tarski-Class X) <> {} & the_rank_of (Tarski-Class X) is limit_ordinal )
proof
let X be set ; ::_thesis: ( the_rank_of (Tarski-Class X) <> {} & the_rank_of (Tarski-Class X) is limit_ordinal )
A1: Tarski-Class X c= Rank (the_rank_of (Tarski-Class X)) by Def8;
thus  the_rank_of (Tarski-Class X) <> {} ::_thesis: the_rank_of (Tarski-Class X) is limit_ordinal
proof
assume  the_rank_of (Tarski-Class X) = {} ; ::_thesis: contradiction
then  Tarski-Class X c= {} by Def8, Lm2;
hence  contradiction ; ::_thesis: verum
end;
assume  not the_rank_of (Tarski-Class X) is limit_ordinal ; ::_thesis: contradiction
then consider A being Ordinal such that
A2: the_rank_of (Tarski-Class X) = succ A by ORDINAL1:29;
consider Y being set  such that
A3: Y in Tarski-Class X and
A4: the_rank_of Y = A by A2, Th72;
A5: bool Y in Tarski-Class X by A3, Th4;
A6: the_rank_of (bool Y) = succ A by A4, Th63;
 bool Y c= Rank A by A1, A2, A5, Th32;
then  succ A c= A by A6, Def8;
then  A in A by ORDINAL1:21;
hence  contradiction ; ::_thesis: verum
end;

begin


scheme :: CLASSES1:sch 1
NonUniqFuncEx{ F1() ->  set , P1[ set , set ] } :
 ex f being Function st
( dom f = F1() & ( for e being set st e in F1() holds
P1[e,f . e] ) )
provided
A1: for e being set st e in F1() holds
ex u being set st P1[e,u]
proof
percases ( F1() = {} or F1() <> {} ) ;
suppose F1() = {} ; ::_thesis: ex f being Function st
( dom f = F1() & ( for e being set st e in F1() holds
P1[e,f . e] ) )
then A2: for e being set st e in F1() holds
ex u being set st
( u in {} & P1[e,u] ) ;
 ex f being Function st
( dom f = F1() & rng f c= {} & ( for e being set st e in F1() holds
P1[e,f . e] ) ) from FUNCT_1:sch_5(A2);
hence  ex f being Function st
( dom f = F1() & ( for e being set st e in F1() holds
P1[e,f . e] ) ) ; ::_thesis: verum
end;
suppose F1() <> {} ; ::_thesis: ex f being Function st
( dom f = F1() & ( for e being set st e in F1() holds
P1[e,f . e] ) )
then reconsider D = F1() as non empty set ;
defpred S1[ set , Ordinal] means  ex u being set st
( u in Rank $2 & P1[$1,u] );
A3: for e being Element of D ex A being Ordinal st S1[e,A]
proof
let e be Element of D; ::_thesis: ex A being Ordinal st S1[e,A]
consider u being set  such that
A4: P1[e,u] by A1;
 u c= Rank (the_rank_of u) by Def8;
then  u in Rank (succ (the_rank_of u)) by Th32;
hence  ex A being Ordinal st S1[e,A] by A4; ::_thesis: verum
end;
consider F being Function such that
A5: ( dom F = D & ( for d being Element of D ex A being Ordinal st
( A = F . d & S1[d,A] & ( for B being Ordinal st S1[d,B] holds
A c= B ) ) ) ) from ORDINAL1:sch_6(A3);
A6: for e being set st e in F1() holds
ex u being set st
( u in Rank (sup (rng F)) & P1[e,u] )
proof
let e be set ; ::_thesis: ( e in F1() implies ex u being set st
( u in Rank (sup (rng F)) & P1[e,u] ) )
assume A7: e in F1() ; ::_thesis: ex u being set st
( u in Rank (sup (rng F)) & P1[e,u] )
then consider A being Ordinal such that
A8: A = F . e and
A9: ex u being set st
( u in Rank A & P1[e,u] ) and
 for B being Ordinal st ex u being set st
( u in Rank B & P1[e,u] ) holds
A c= B by A5;
consider u being set  such that
A10: ( u in Rank A & P1[e,u] ) by A9;
take  u ; ::_thesis: ( u in Rank (sup (rng F)) & P1[e,u] )
 A in rng F by A5, A7, A8, FUNCT_1:def_3;
then  A in sup (rng F) by ORDINAL2:19;
then  A c= sup (rng F) by ORDINAL1:def_2;
then  Rank A c= Rank (sup (rng F)) by Th37;
hence  ( u in Rank (sup (rng F)) & P1[e,u] ) by A10; ::_thesis: verum
end;
 ex f being Function st
( dom f = F1() & rng f c= Rank (sup (rng F)) & ( for e being set st e in F1() holds
P1[e,f . e] ) ) from FUNCT_1:sch_5(A6);
hence  ex f being Function st
( dom f = F1() & ( for e being set st e in F1() holds
P1[e,f . e] ) ) ; ::_thesis: verum
end;
end;
end;

definition
let F, G be Relation;
predF,G are_fiberwise_equipotent  means :Def9: :: CLASSES1:def 9
 for x being set holds card (Coim (F,x)) = card (Coim (G,x));
reflexivity
 for F being Relation
for x being set holds card (Coim (F,x)) = card (Coim (F,x)) ;
symmetry
 for F, G being Relation st ( for x being set holds card (Coim (F,x)) = card (Coim (G,x)) ) holds
for x being set holds card (Coim (G,x)) = card (Coim (F,x)) ;
end;

:: deftheorem Def9 defines are_fiberwise_equipotent CLASSES1:def_9_:_
 for F, G being Relation holds
( F,G are_fiberwise_equipotent iff for x being set holds card (Coim (F,x)) = card (Coim (G,x)) );

Lm3:  for F being Function
for x being set st not x in rng F holds
Coim (F,x) = {}
proof
let F be Function; ::_thesis: for x being set st not x in rng F holds
Coim (F,x) = {}
let x be set ; ::_thesis: ( not x in rng F implies Coim (F,x) = {} )
assume A1: not x in rng F ; ::_thesis: Coim (F,x) = {}
now__::_thesis:_not_rng_F_meets_{x}
assume  rng F meets {x} ; ::_thesis: contradiction
then  ex y being set st
( y in rng F & y in {x} ) by XBOOLE_0:3;
hence  contradiction by A1, TARSKI:def_1; ::_thesis: verum
end;
hence  Coim (F,x) = {} by RELAT_1:138; ::_thesis: verum
end;

theorem Th75: :: CLASSES1:75
for F, G being Function st F,G are_fiberwise_equipotent holds
rng F = rng G
proof
let F, G be Function; ::_thesis: ( F,G are_fiberwise_equipotent implies rng F = rng G )
assume A1: F,G are_fiberwise_equipotent ; ::_thesis: rng F = rng G
thus  rng F c= rng G :: according to XBOOLE_0:def_10 ::_thesis: rng G c= rng F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F or x in rng G )
assume that
A2: x in rng F and
A3: not x in rng G ; ::_thesis: contradiction
 card (Coim (F,x)) = card (Coim (G,x)) by A1, Def9;
then A4: Coim (F,x), Coim (G,x) are_equipotent by CARD_1:5;
A5: ex y being set st
( y in dom F & F . y = x ) by A2, FUNCT_1:def_3;
 Coim (G,x) = {} by A3, Lm3;
then  ( x in {x} & F " {x} = {} ) by A4, CARD_1:26, TARSKI:def_1;
hence  contradiction by A5, FUNCT_1:def_7; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng G or x in rng F )
assume that
A6: x in rng G and
A7: not x in rng F ; ::_thesis: contradiction
 card (Coim (G,x)) = card (Coim (F,x)) by A1, Def9;
then A8: G " {x},F " {x} are_equipotent by CARD_1:5;
A9: ex y being set st
( y in dom G & G . y = x ) by A6, FUNCT_1:def_3;
 Coim (F,x) = {} by A7, Lm3;
then  ( x in {x} & Coim (G,x) = {} ) by A8, CARD_1:26, TARSKI:def_1;
hence  contradiction by A9, FUNCT_1:def_7; ::_thesis: verum
end;

theorem :: CLASSES1:76
for F, G, H being Function st F,G are_fiberwise_equipotent & F,H are_fiberwise_equipotent holds
G,H are_fiberwise_equipotent
proof
let F, G, H be Function; ::_thesis: ( F,G are_fiberwise_equipotent & F,H are_fiberwise_equipotent implies G,H are_fiberwise_equipotent )
assume that
A1: F,G are_fiberwise_equipotent and
A2: F,H are_fiberwise_equipotent ; ::_thesis: G,H are_fiberwise_equipotent
let x be set ; :: according to CLASSES1:def_9 ::_thesis: card (Coim (G,x)) = card (Coim (H,x))
thus  card (Coim (G,x)) = card (Coim (F,x)) by A1, Def9
.= card (Coim (H,x)) by A2, Def9 ; ::_thesis: verum
end;

theorem Th77: :: CLASSES1:77
for F, G being Function holds
( F,G are_fiberwise_equipotent iff ex H being Function st
( dom H = dom F & rng H = dom G & H is one-to-one & F = G * H ) )
proof
let F, G be Function; ::_thesis: ( F,G are_fiberwise_equipotent iff ex H being Function st
( dom H = dom F & rng H = dom G & H is one-to-one & F = G * H ) )
thus  ( F,G are_fiberwise_equipotent implies ex H being Function st
( dom H = dom F & rng H = dom G & H is one-to-one & F = G * H ) ) ::_thesis: ( ex H being Function st
( dom H = dom F & rng H = dom G & H is one-to-one & F = G * H ) implies F,G are_fiberwise_equipotent )
proof
assume A1: F,G are_fiberwise_equipotent ; ::_thesis: ex H being Function st
( dom H = dom F & rng H = dom G & H is one-to-one & F = G * H )
defpred S1[ set , set ] means ( $2 is Function & ( for f being Function st $2 = f holds
( dom f = F " {$1} & rng f = G " {$1} & f is one-to-one ) ) );
A2: for x being set st x in rng F holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in rng F implies ex y being set st S1[x,y] )
assume  x in rng F ; ::_thesis: ex y being set st S1[x,y]
 card (Coim (F,x)) = card (Coim (G,x)) by A1, Def9;
then  F " {x},G " {x} are_equipotent by CARD_1:5;
then consider H being Function such that
A3: ( H is one-to-one & dom H = F " {x} & rng H = G " {x} ) by WELLORD2:def_4;
take  H ; ::_thesis: S1[x,H]
thus  H is Function ; ::_thesis: for f being Function st H = f holds
( dom f = F " {x} & rng f = G " {x} & f is one-to-one )
let g be Function; ::_thesis: ( H = g implies ( dom g = F " {x} & rng g = G " {x} & g is one-to-one ) )
assume  g = H ; ::_thesis: ( dom g = F " {x} & rng g = G " {x} & g is one-to-one )
hence  ( dom g = F " {x} & rng g = G " {x} & g is one-to-one ) by A3; ::_thesis: verum
end;
consider W being Function such that
A4: ( dom W = rng F & ( for x being set st x in rng F holds
S1[x,W . x] ) ) from CLASSES1:sch_1(A2);
defpred S2[ set , set ] means  for H being Function st H = W . (F . $1) holds
$2 = H . $1;
set df = dom F;
set dg = dom G;
A5: for x being set st x in dom F holds
ex y being set st
( y in dom G & S2[x,y] )
proof
let x be set ; ::_thesis: ( x in dom F implies ex y being set st
( y in dom G & S2[x,y] ) )
assume A6: x in dom F ; ::_thesis: ex y being set st
( y in dom G & S2[x,y] )
then A7: F . x in rng F by FUNCT_1:def_3;
then reconsider f = W . (F . x) as Function by A4;
A8: ( dom f = F " {(F . x)} & rng f = G " {(F . x)} ) by A4, A7;
take y = f . x; ::_thesis: ( y in dom G & S2[x,y] )
 F . x in {(F . x)} by TARSKI:def_1;
then  x in F " {(F . x)} by A6, FUNCT_1:def_7;
then  f . x in G " {(F . x)} by A8, FUNCT_1:def_3;
hence  y in dom G by FUNCT_1:def_7; ::_thesis: S2[x,y]
let g be Function; ::_thesis: ( g = W . (F . x) implies y = g . x )
assume  g = W . (F . x) ; ::_thesis: y = g . x
hence  y = g . x ; ::_thesis: verum
end;
consider IT being Function such that
A9: ( dom IT = dom F & rng IT c= dom G & ( for x being set st x in dom F holds
S2[x,IT . x] ) ) from FUNCT_1:sch_5(A5);
take  IT ; ::_thesis: ( dom IT = dom F & rng IT = dom G & IT is one-to-one & F = G * IT )
thus  dom IT = dom F by A9; ::_thesis: ( rng IT = dom G & IT is one-to-one & F = G * IT )
 dom G c= rng IT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom G or x in rng IT )
assume A10: x in dom G ; ::_thesis: x in rng IT
then A11: G . x in rng G by FUNCT_1:def_3;
A12: rng F = rng G by A1, Th75;
then reconsider f = W . (G . x) as Function by A4, A11;
A13: dom f = F " {(G . x)} by A4, A11, A12;
A14: rng f = G " {(G . x)} by A4, A11, A12;
 G . x in {(G . x)} by TARSKI:def_1;
then  x in rng f by A10, A14, FUNCT_1:def_7;
then consider z being set  such that
A15: z in dom f and
A16: f . z = x by FUNCT_1:def_3;
A17: z in dom F by A13, A15, FUNCT_1:def_7;
 F . z in {(G . x)} by A13, A15, FUNCT_1:def_7;
then  F . z = G . x by TARSKI:def_1;
then  IT . z = x by A9, A16, A17;
hence  x in rng IT by A9, A17, FUNCT_1:def_3; ::_thesis: verum
end;
hence  rng IT = dom G by A9, XBOOLE_0:def_10; ::_thesis: ( IT is one-to-one & F = G * IT )
now__::_thesis:_for_x,_y_being_set_st_x_in_dom_IT_&_y_in_dom_IT_&_IT_._x_=_IT_._y_holds_
x_=_y
let x, y be set ; ::_thesis: ( x in dom IT & y in dom IT & IT . x = IT . y implies x = y )
assume that
A18: x in dom IT and
A19: y in dom IT and
A20: IT . x = IT . y ; ::_thesis: x = y
A21: F . x in rng F by A9, A18, FUNCT_1:def_3;
A22: F . y in rng F by A9, A19, FUNCT_1:def_3;
then reconsider f1 = W . (F . x), f2 = W . (F . y) as Function by A4, A21;
A23: ( IT . x = f1 . x & IT . y = f2 . y ) by A9, A18, A19;
A24: dom f1 = F " {(F . x)} by A4, A21;
A25: rng f1 = G " {(F . x)} by A4, A21;
A26: f1 is one-to-one by A4, A21;
A27: dom f2 = F " {(F . y)} by A4, A22;
A28: rng f2 = G " {(F . y)} by A4, A22;
A29: F . x in {(F . x)} by TARSKI:def_1;
A30: F . y in {(F . y)} by TARSKI:def_1;
A31: x in F " {(F . x)} by A9, A18, A29, FUNCT_1:def_7;
A32: y in F " {(F . y)} by A9, A19, A30, FUNCT_1:def_7;
A33: f1 . x in rng f1 by A24, A31, FUNCT_1:def_3;
 f2 . y in rng f2 by A27, A32, FUNCT_1:def_3;
then  f1 . x in (G " {(F . x)}) /\ (G " {(F . y)}) by A20, A23, A25, A28, A33, XBOOLE_0:def_4;
then  f1 . x in G " ({(F . x)} /\ {(F . y)}) by FUNCT_1:68;
then A34: G . (f1 . x) in {(F . x)} /\ {(F . y)} by FUNCT_1:def_7;
then A35: G . (f1 . x) in {(F . x)} by XBOOLE_0:def_4;
A36: G . (f1 . x) in {(F . y)} by A34, XBOOLE_0:def_4;
A37: G . (f1 . x) = F . x by A35, TARSKI:def_1;
 G . (f1 . x) = F . y by A36, TARSKI:def_1;
hence  x = y by A20, A23, A24, A26, A31, A32, A37, FUNCT_1:def_4; ::_thesis: verum
end;
hence  IT is one-to-one by FUNCT_1:def_4; ::_thesis: F = G * IT
A38: dom (G * IT) = dom F by A9, RELAT_1:27;
now__::_thesis:_for_x_being_set_st_x_in_dom_F_holds_
F_._x_=_(G_*_IT)_._x
let x be set ; ::_thesis: ( x in dom F implies F . x = (G * IT) . x )
assume A39: x in dom F ; ::_thesis: F . x = (G * IT) . x
then A40: F . x in rng F by FUNCT_1:def_3;
then reconsider f = W . (F . x) as Function by A4;
A41: ( dom f = F " {(F . x)} & rng f = G " {(F . x)} ) by A4, A40;
 F . x in {(F . x)} by TARSKI:def_1;
then  x in F " {(F . x)} by A39, FUNCT_1:def_7;
then  f . x in G " {(F . x)} by A41, FUNCT_1:def_3;
then  G . (f . x) in {(F . x)} by FUNCT_1:def_7;
then A42: G . (f . x) = F . x by TARSKI:def_1;
 IT . x = f . x by A9, A39;
hence  F . x = (G * IT) . x by A9, A39, A42, FUNCT_1:13; ::_thesis: verum
end;
hence  F = G * IT by A38, FUNCT_1:2; ::_thesis: verum
end;
given H being Function such that A43: dom H = dom F and
A44: rng H = dom G and
A45: H is one-to-one and
A46: F = G * H ; ::_thesis: F,G are_fiberwise_equipotent
let x be set ; :: according to CLASSES1:def_9 ::_thesis: card (Coim (F,x)) = card (Coim (G,x))
set t = H | (F " {x});
A47: H | (F " {x}) is one-to-one by A45, FUNCT_1:52;
A48: dom (H | (F " {x})) = F " {x} by A43, RELAT_1:62, RELAT_1:132;
 rng (H | (F " {x})) = G " {x}
proof
thus  rng (H | (F " {x})) c= G " {x} :: according to XBOOLE_0:def_10 ::_thesis: G " {x} c= rng (H | (F " {x}))
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng (H | (F " {x})) or z in G " {x} )
assume  z in rng (H | (F " {x})) ; ::_thesis: z in G " {x}
then consider y being set  such that
A49: y in dom (H | (F " {x})) and
A50: (H | (F " {x})) . y = z by FUNCT_1:def_3;
 F . y in {x} by A48, A49, FUNCT_1:def_7;
then A51: F . y = x by TARSKI:def_1;
A52: z = H . y by A49, A50, FUNCT_1:47;
 dom (H | (F " {x})) = (dom H) /\ (F " {x}) by RELAT_1:61;
then A53: y in dom H by A49, XBOOLE_0:def_4;
then A54: z in dom G by A44, A52, FUNCT_1:def_3;
 x = G . z by A46, A51, A52, A53, FUNCT_1:13;
then  G . z in {x} by TARSKI:def_1;
hence  z in G " {x} by A54, FUNCT_1:def_7; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in G " {x} or z in rng (H | (F " {x})) )
assume A55: z in G " {x} ; ::_thesis: z in rng (H | (F " {x}))
then A56: z in dom G by FUNCT_1:def_7;
 G . z in {x} by A55, FUNCT_1:def_7;
then A57: G . z = x by TARSKI:def_1;
consider y being set  such that
A58: y in dom H and
A59: H . y = z by A44, A56, FUNCT_1:def_3;
 F . y = x by A46, A57, A58, A59, FUNCT_1:13;
then  F . y in {x} by TARSKI:def_1;
then A60: y in dom (H | (F " {x})) by A43, A48, A58, FUNCT_1:def_7;
then  (H | (F " {x})) . y in rng (H | (F " {x})) by FUNCT_1:def_3;
hence  z in rng (H | (F " {x})) by A59, A60, FUNCT_1:47; ::_thesis: verum
end;
then  F " {x},G " {x} are_equipotent by A47, A48, WELLORD2:def_4;
hence  card (Coim (F,x)) = card (Coim (G,x)) by CARD_1:5; ::_thesis: verum
end;

theorem Th78: :: CLASSES1:78
for F, G being Function holds
( F,G are_fiberwise_equipotent iff for X being set holds card (F " X) = card (G " X) )
proof
let F, G be Function; ::_thesis: ( F,G are_fiberwise_equipotent iff for X being set holds card (F " X) = card (G " X) )
thus  ( F,G are_fiberwise_equipotent implies for X being set holds card (F " X) = card (G " X) ) ::_thesis: ( ( for X being set holds card (F " X) = card (G " X) ) implies F,G are_fiberwise_equipotent )
proof
assume  F,G are_fiberwise_equipotent ; ::_thesis: for X being set holds card (F " X) = card (G " X)
then consider H being Function such that
A1: dom H = dom F and
A2: rng H = dom G and
A3: H is one-to-one and
A4: F = G * H by Th77;
let X be set ; ::_thesis: card (F " X) = card (G " X)
set t = H | (F " X);
A5: H | (F " X) is one-to-one by A3, FUNCT_1:52;
A6: dom (H | (F " X)) = F " X by A1, RELAT_1:62, RELAT_1:132;
 rng (H | (F " X)) = G " X
proof
thus  rng (H | (F " X)) c= G " X :: according to XBOOLE_0:def_10 ::_thesis: G " X c= rng (H | (F " X))
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng (H | (F " X)) or z in G " X )
assume  z in rng (H | (F " X)) ; ::_thesis: z in G " X
then consider y being set  such that
A7: y in dom (H | (F " X)) and
A8: (H | (F " X)) . y = z by FUNCT_1:def_3;
A9: F . y in X by A6, A7, FUNCT_1:def_7;
A10: z = H . y by A7, A8, FUNCT_1:47;
 dom (H | (F " X)) = (dom H) /\ (F " X) by RELAT_1:61;
then A11: y in dom H by A7, XBOOLE_0:def_4;
then A12: z in dom G by A2, A10, FUNCT_1:def_3;
 G . z in X by A4, A9, A10, A11, FUNCT_1:13;
hence  z in G " X by A12, FUNCT_1:def_7; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in G " X or z in rng (H | (F " X)) )
assume A13: z in G " X ; ::_thesis: z in rng (H | (F " X))
then A14: z in dom G by FUNCT_1:def_7;
A15: G . z in X by A13, FUNCT_1:def_7;
consider y being set  such that
A16: y in dom H and
A17: H . y = z by A2, A14, FUNCT_1:def_3;
 F . y in X by A4, A15, A16, A17, FUNCT_1:13;
then A18: y in dom (H | (F " X)) by A1, A6, A16, FUNCT_1:def_7;
then  (H | (F " X)) . y in rng (H | (F " X)) by FUNCT_1:def_3;
hence  z in rng (H | (F " X)) by A17, A18, FUNCT_1:47; ::_thesis: verum
end;
then  F " X,G " X are_equipotent by A5, A6, WELLORD2:def_4;
hence  card (F " X) = card (G " X) by CARD_1:5; ::_thesis: verum
end;
assume  for X being set holds card (F " X) = card (G " X) ; ::_thesis: F,G are_fiberwise_equipotent
hence  for x being set holds card (Coim (F,x)) = card (Coim (G,x)) ; :: according to CLASSES1:def_9 ::_thesis: verum
end;

theorem :: CLASSES1:79
for D being non empty set
for F, G being Function st rng F c= D & rng G c= D & ( for d being Element of D holds card (Coim (F,d)) = card (Coim (G,d)) ) holds
F,G are_fiberwise_equipotent
proof
let D be non empty set ; ::_thesis: for F, G being Function st rng F c= D & rng G c= D & ( for d being Element of D holds card (Coim (F,d)) = card (Coim (G,d)) ) holds
F,G are_fiberwise_equipotent
let F, G be Function; ::_thesis: ( rng F c= D & rng G c= D & ( for d being Element of D holds card (Coim (F,d)) = card (Coim (G,d)) ) implies F,G are_fiberwise_equipotent )
assume that
A1: rng F c= D and
A2: rng G c= D ; ::_thesis: ( ex d being Element of D st not card (Coim (F,d)) = card (Coim (G,d)) or F,G are_fiberwise_equipotent )
assume A3: for d being Element of D holds card (Coim (F,d)) = card (Coim (G,d)) ; ::_thesis: F,G are_fiberwise_equipotent
let x be set ; :: according to CLASSES1:def_9 ::_thesis: card (Coim (F,x)) = card (Coim (G,x))
percases ( not x in rng F or x in rng F ) ;
suppose not x in rng F ; ::_thesis: card (Coim (F,x)) = card (Coim (G,x))
then A4: Coim (F,x) = {} by Lm3;
now__::_thesis:_not_x_in_rng_G
assume A5: x in rng G ; ::_thesis: contradiction
then reconsider d = x as Element of D by A2;
 card (Coim (G,d)) = card (Coim (F,d)) by A3;
then  G " {d},F " {d} are_equipotent by CARD_1:5;
then A6: G " {x} = {} by A4, CARD_1:26;
consider y being set  such that
A7: y in dom G and
A8: G . y = x by A5, FUNCT_1:def_3;
 G . y in {x} by A8, TARSKI:def_1;
hence  contradiction by A6, A7, FUNCT_1:def_7; ::_thesis: verum
end;
hence  card (Coim (F,x)) = card (Coim (G,x)) by A4, Lm3; ::_thesis: verum
end;
suppose x in rng F ; ::_thesis: card (Coim (F,x)) = card (Coim (G,x))
then reconsider d = x as Element of D by A1;
 card (Coim (F,d)) = card (Coim (G,d)) by A3;
hence  card (Coim (F,x)) = card (Coim (G,x)) ; ::_thesis: verum
end;
end;
end;

theorem Th80: :: CLASSES1:80
for F, G being Function st dom F = dom G holds
( F,G are_fiberwise_equipotent iff ex P being Permutation of (dom F) st F = G * P )
proof
let F, G be Function; ::_thesis: ( dom F = dom G implies ( F,G are_fiberwise_equipotent iff ex P being Permutation of (dom F) st F = G * P ) )
assume A1: dom F = dom G ; ::_thesis: ( F,G are_fiberwise_equipotent iff ex P being Permutation of (dom F) st F = G * P )
thus  ( F,G are_fiberwise_equipotent implies ex P being Permutation of (dom F) st F = G * P ) ::_thesis: ( ex P being Permutation of (dom F) st F = G * P implies F,G are_fiberwise_equipotent )
proof
assume  F,G are_fiberwise_equipotent ; ::_thesis: ex P being Permutation of (dom F) st F = G * P
then consider I being Function such that
A2: dom I = dom F and
A3: rng I = dom G and
A4: I is one-to-one and
A5: F = G * I by Th77;
reconsider I = I as Function of (dom F),(dom F) by A1, A2, A3, FUNCT_2:2;
reconsider I = I as Permutation of (dom F) by A1, A3, A4, FUNCT_2:57;
take  I ; ::_thesis: F = G * I
thus  F = G * I by A5; ::_thesis: verum
end;
given P being Permutation of (dom F) such that A6: F = G * P ; ::_thesis: F,G are_fiberwise_equipotent
 ( P is Function of (dom F),(dom F) & dom F = {} implies dom F = {} ) ;
then  ( rng P = dom F & dom P = dom F ) by FUNCT_2:def_1, FUNCT_2:def_3;
hence  F,G are_fiberwise_equipotent by A1, A6, Th77; ::_thesis: verum
end;

theorem :: CLASSES1:81
for F, G being Function st F,G are_fiberwise_equipotent holds
card (dom F) = card (dom G)
proof
let F, G be Function; ::_thesis: ( F,G are_fiberwise_equipotent implies card (dom F) = card (dom G) )
assume  F,G are_fiberwise_equipotent ; ::_thesis: card (dom F) = card (dom G)
then  ( card (F " (rng F)) = card (G " (rng F)) & rng F = rng G ) by Th75, Th78;
hence  card (dom F) = card (G " (rng G)) by RELAT_1:134
.= card (dom G) by RELAT_1:134 ;
::_thesis: verum
end;

theorem :: CLASSES1:82
for f being set
for p being Relation
for x being set st x in rng p holds
the_rank_of x in the_rank_of [p,f]
proof
let f be set ; ::_thesis: for p being Relation
for x being set st x in rng p holds
the_rank_of x in the_rank_of [p,f]
let p be Relation; ::_thesis: for x being set st x in rng p holds
the_rank_of x in the_rank_of [p,f]
let y be set ; ::_thesis: ( y in rng p implies the_rank_of y in the_rank_of [p,f] )
assume  y in rng p ; ::_thesis: the_rank_of y in the_rank_of [p,f]
then consider x being set  such that
A1: [x,y] in p by XTUPLE_0:def_13;
A2: p in {p,f} by TARSKI:def_2;
A3: {p,f} in {{p,f},{p}} by TARSKI:def_2;
A4: y in {x,y} by TARSKI:def_2;
A5: {x,y} in {{x,y},{x}} by TARSKI:def_2;
A6: the_rank_of y in the_rank_of {x,y} by A4, Th68;
A7: the_rank_of {x,y} in the_rank_of [x,y] by A5, Th68;
A8: the_rank_of p in the_rank_of {p,f} by A2, Th68;
A9: the_rank_of {p,f} in the_rank_of [p,f] by A3, Th68;
A10: the_rank_of y in the_rank_of [x,y] by A6, A7, ORDINAL1:10;
A11: the_rank_of [x,y] in the_rank_of p by A1, Th68;
A12: the_rank_of p in the_rank_of [p,f] by A8, A9, ORDINAL1:10;
 the_rank_of y in the_rank_of p by A10, A11, ORDINAL1:10;
hence  the_rank_of y in the_rank_of [p,f] by A12, ORDINAL1:10; ::_thesis: verum
end;

theorem :: CLASSES1:83
for f, g, h being Function st dom f = dom g & rng f c= dom h & rng g c= dom h & f,g are_fiberwise_equipotent holds
h * f,h * g are_fiberwise_equipotent
proof
let f, g, h be Function; ::_thesis: ( dom f = dom g & rng f c= dom h & rng g c= dom h & f,g are_fiberwise_equipotent implies h * f,h * g are_fiberwise_equipotent )
assume that
A1: dom f = dom g and
A2: rng f c= dom h and
A3: rng g c= dom h and
A4: f,g are_fiberwise_equipotent ; ::_thesis: h * f,h * g are_fiberwise_equipotent
consider p being Permutation of (dom f) such that
A5: f = g * p by A1, A4, Th80;
A6: dom (h * f) = dom f by A2, RELAT_1:27;
A7: dom (h * g) = dom g by A3, RELAT_1:27;
 h * f = (h * g) * p by A5, RELAT_1:36;
hence  h * f,h * g are_fiberwise_equipotent by A1, A6, A7, Th80; ::_thesis: verum
end;