:: Tarski's Classes and Ranks
:: by Grzegorz Bancerek
::
:: Copyright (c) 1990-2021 Association of Mizar Users

definition
let B be set ;
attr B 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 ;
attr B is Tarski means :: 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 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 ;
pred B is_Tarski-Class_of A means :: CLASSES1:def 3
( A in B & B is Tarski );
end;

:: deftheorem 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 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
;
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 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 end;

theorem Th2: :: CLASSES1:2
for X being set holds X in Tarski-Class X
proof end;

theorem Th3: :: CLASSES1:3
for X, Y, Z being set st Y in Tarski-Class X & Z c= Y holds
Z in Tarski-Class X
proof end;

theorem Th4: :: CLASSES1:4
for X, Y being set st Y in Tarski-Class X holds
bool Y in Tarski-Class X
proof end;

theorem Th5: :: CLASSES1:5
for X, Y being set holds
( not Y c= Tarski-Class X or Y, Tarski-Class X are_equipotent or Y in Tarski-Class X )
proof end;

theorem :: CLASSES1:6
for X, Y being set st Y c= Tarski-Class X & card Y in card () holds
Y in Tarski-Class X
proof end;

definition
let X be set ;
let A be Ordinal;
func Tarski-Class (X,A) -> set means :Def5: :: CLASSES1:def 5
ex L being Sequence st
( it = last L & dom L = succ A & L . 0 = {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)) /\ ()) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
L . C = (union (rng (L | C))) /\ () ) );
correctness
existence
ex b1 being set ex L being Sequence st
( b1 = last L & dom L = succ A & L . 0 = {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)) /\ ()) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
L . C = (union (rng (L | C))) /\ () ) )
;
uniqueness
for b1, b2 being set st ex L being Sequence st
( b1 = last L & dom L = succ A & L . 0 = {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)) /\ ()) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
L . C = (union (rng (L | C))) /\ () ) ) & ex L being Sequence st
( b2 = last L & dom L = succ A & L . 0 = {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)) /\ ()) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
L . C = (union (rng (L | C))) /\ () ) ) holds
b1 = b2
;
proof 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 Sequence st
( b3 = last L & dom L = succ A & L . 0 = {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)) /\ ()) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
L . C = (union (rng (L | C))) /\ () ) ) );

Lm1: now :: thesis: for X being set holds
( H1( 0 ) = {X} & ( for A being Ordinal holds H1( succ A) = H2(A,H1(A)) ) & ( for A being Ordinal
for L being Sequence st A <> 0 & 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)) /\ () ) )
let X be set ; :: thesis: ( H1( 0 ) = {X} & ( for A being Ordinal holds H1( succ A) = H2(A,H1(A)) ) & ( for A being Ordinal
for L being Sequence st A <> 0 & 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)) /\ () ) )

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) /\ ());
deffunc H3( Ordinal, Sequence) -> set = (union (rng $2)) /\ (); A1: for A being Ordinal for x being object holds ( x = H1(A) iff ex L being Sequence st ( x = last L & dom L = succ A & L . 0 = {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 <> 0 & C is limit_ordinal holds L . C = H3(C,L | C) ) ) ) by Def5; thus H1( 0 ) = {X} from :: thesis: ( ( for A being Ordinal holds H1( succ A) = H2(A,H1(A)) ) & ( for A being Ordinal for L being Sequence st A <> 0 & 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)) /\ () ) ) thus for A being Ordinal holds H1( succ A) = H2(A,H1(A)) from :: thesis: for A being Ordinal for L being Sequence st A <> 0 & 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)) /\ () thus for A being Ordinal for L being Sequence st A <> 0 & 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)) /\ () :: thesis: verum proof let A be Ordinal; :: thesis: for L being Sequence st A <> 0 & 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)) /\ () let L be Sequence; :: thesis: ( A <> 0 & 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)) /\ () ) assume that A2: ( A <> 0 & 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)) /\ () 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 (); coherence Tarski-Class (X,A) is Subset of () proof 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))) /\ ()) 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 end; theorem Th10: :: CLASSES1:10 for X, Y 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 end; theorem :: CLASSES1:11 for X, Y, Z 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 X, Y 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 end; theorem :: CLASSES1:14 for X, Y, 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 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 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 end; theorem Th17: :: CLASSES1:17 for X being set ex A being Ordinal st Tarski-Class (X,A) = Tarski-Class (X,(succ A)) proof 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 end; theorem Th19: :: CLASSES1:19 for X being set ex A being Ordinal st Tarski-Class (X,A) = Tarski-Class X proof 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 end; theorem :: CLASSES1:21 for X, Y 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 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 end; theorem Th23: :: CLASSES1:23 for X being set st X is epsilon-transitive holds Tarski-Class X is epsilon-transitive proof end; theorem Th24: :: CLASSES1:24 for X, Y being set st Y in Tarski-Class X holds card Y in card () proof end; theorem Th25: :: CLASSES1:25 for X, Y being set st Y in Tarski-Class X holds not Y, Tarski-Class X are_equipotent proof end; theorem Th26: :: CLASSES1:26 for X, x, y being set holds ( ( x in Tarski-Class X implies {x} in Tarski-Class X ) & ( x in Tarski-Class X & y in Tarski-Class X implies {x,y} in Tarski-Class X ) ) proof 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 end; theorem :: CLASSES1:28 for X, Y, Z being set st Y c= Tarski-Class X & Z c= Tarski-Class X holds [:Y,Z:] c= Tarski-Class X proof end; definition let A be Ordinal; func Rank A -> set means :Def6: :: CLASSES1:def 6 ex L being Sequence st ( it = last L & dom L = succ A & L . 0 = {} & ( 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 <> 0 & C is limit_ordinal holds L . C = union (rng (L | C)) ) ); correctness existence ex b1 being set ex L being Sequence st ( b1 = last L & dom L = succ A & L . 0 = {} & ( 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 <> 0 & C is limit_ordinal holds L . C = union (rng (L | C)) ) ) ; uniqueness for b1, b2 being set st ex L being Sequence st ( b1 = last L & dom L = succ A & L . 0 = {} & ( 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 <> 0 & C is limit_ordinal holds L . C = union (rng (L | C)) ) ) & ex L being Sequence st ( b2 = last L & dom L = succ A & L . 0 = {} & ( 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 <> 0 & C is limit_ordinal holds L . C = union (rng (L | C)) ) ) holds b1 = b2 ; proof 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 Sequence st ( b2 = last L & dom L = succ A & L . 0 = {} & ( 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 <> 0 & C is limit_ordinal holds L . C = union (rng (L | C)) ) ) ); deffunc H1( Ordinal) -> set = Rank$1;

Lm2: now :: thesis: ( H1( 0 ) = {} & ( for A being Ordinal holds H1( succ A) = H2(A,H1(A)) ) & ( for A being Ordinal
for L being Sequence st A <> 0 & 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, Sequence) -> set = union (rng $2); A1: for A being Ordinal for x being object holds ( x = H1(A) iff ex L being Sequence st ( x = last L & dom L = succ A & L . 0 = {} & ( 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 <> 0 & C is limit_ordinal holds L . C = H3(C,L | C) ) ) ) by Def6; thus H1( 0 ) = {} from :: thesis: ( ( for A being Ordinal holds H1( succ A) = H2(A,H1(A)) ) & ( for A being Ordinal for L being Sequence st A <> 0 & 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 :: thesis: for A being Ordinal for L being Sequence st A <> 0 & 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 Sequence st A <> 0 & 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 Sequence st A <> 0 & 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 Sequence; :: thesis: ( A <> 0 & 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 <> 0 & 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 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 end; registration let A be Ordinal; coherence proof end; end; theorem :: CLASSES1:33 for A being Ordinal holds Rank A c= Rank (succ A) proof end; theorem Th34: :: CLASSES1:34 for A being Ordinal holds union (Rank A) c= Rank A proof end; theorem :: CLASSES1:35 for X being set for A being Ordinal st X in Rank A holds union X in Rank A proof end; theorem Th36: :: CLASSES1:36 for A, B being Ordinal holds ( A in B iff Rank A in Rank B ) proof end; theorem Th37: :: CLASSES1:37 for A, B being Ordinal holds ( A c= B iff Rank A c= Rank B ) proof end; theorem Th38: :: CLASSES1:38 for A being Ordinal holds A c= Rank A proof 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 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 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 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 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 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 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 end; theorem Th46: :: CLASSES1:46 for X being set for A being Ordinal st X is epsilon-transitive & (Rank A) /\ () = (Rank (succ A)) /\ () holds Tarski-Class X c= Rank A proof 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 end; theorem Th48: :: CLASSES1:48 for X being set st X is epsilon-transitive holds union X c= X proof 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 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 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 object 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 object 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 end;
uniqueness
for b1, b2 being set st ( for x being object 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 object 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 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 object 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) ) ) ) );

registration
let X be set ;
coherence
proof end;
end;

theorem :: CLASSES1:51
for X being set holds the_transitive-closure_of X is epsilon-transitive ;

theorem Th52: :: CLASSES1:52
for X being set holds X c= the_transitive-closure_of X
proof 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 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 by ;

theorem Th55: :: CLASSES1:55
for X being set st X is epsilon-transitive holds
the_transitive-closure_of X = X
proof end;

theorem :: CLASSES1:56

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 end;

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

theorem :: CLASSES1:60
for X, Y being set holds the_transitive-closure_of (X \/ Y) = \/
proof end;

theorem :: CLASSES1:61
for X, Y being set holds the_transitive-closure_of (X /\ Y) c= /\
proof end;

theorem Th62: :: CLASSES1:62
for X being set ex A being Ordinal st X c= Rank A
proof end;

definition
let x be object ;
func the_rank_of x -> Ordinal means :Def8: :: CLASSES1:def 8
( x in Rank (succ it) & ( for B being Ordinal st x in Rank (succ B) holds
it c= B ) );
existence
ex b1 being Ordinal st
( x in Rank (succ b1) & ( for B being Ordinal st x in Rank (succ B) holds
b1 c= B ) )
proof end;
uniqueness
for b1, b2 being Ordinal st x in Rank (succ b1) & ( for B being Ordinal st x in Rank (succ B) holds
b1 c= B ) & x in Rank (succ b2) & ( for B being Ordinal st x in Rank (succ B) holds
b2 c= B ) holds
b1 = b2
;
end;

:: deftheorem Def8 defines the_rank_of CLASSES1:def 8 :
for x being object
for b2 being Ordinal holds
( b2 = the_rank_of x iff ( x in Rank (succ b2) & ( for B being Ordinal st x in Rank (succ B) holds
b2 c= B ) ) );

definition
let X be set ;
redefine func the_rank_of X means :Def9: :: CLASSES1:def 9
( X c= Rank it & ( for B being Ordinal st X c= Rank B holds
it c= B ) );
compatibility
for b1 being Ordinal holds
( b1 = the_rank_of X iff ( X c= Rank b1 & ( for B being Ordinal st X c= Rank B holds
b1 c= B ) ) )
proof end;
end;

:: deftheorem Def9 defines the_rank_of CLASSES1:def 9 :
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 ()
proof end;

theorem :: CLASSES1:64
for A being Ordinal holds the_rank_of (Rank A) = A
proof 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 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 end;

theorem :: CLASSES1:67
for X, Y being set st X c= Y holds
the_rank_of X c= the_rank_of Y
proof 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 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 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 end;

theorem :: CLASSES1:71
for X being set holds
( the_rank_of X = {} iff X = {} )
proof 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 end;

theorem :: CLASSES1:73
for A being Ordinal holds the_rank_of A = A
proof end;

theorem :: CLASSES1:74
for X being set holds
( the_rank_of () <> {} & the_rank_of () is limit_ordinal )
proof end;

scheme :: CLASSES1:sch 1
NonUniqFuncEx{ F1() -> set , P1[ object , object ] } :
ex f being Function st
( dom f = F1() & ( for e being object st e in F1() holds
P1[e,f . e] ) )
provided
A1: for e being object st e in F1() holds
ex u being object st P1[e,u]
proof end;

:: from RFINSEQ, 2008.10.10, A.T.
definition
let F, G be Relation;
pred F,G are_fiberwise_equipotent means :: CLASSES1:def 10
for x being object holds card (Coim (F,x)) = card (Coim (G,x));
reflexivity
for F being Relation
for x being object holds card (Coim (F,x)) = card (Coim (F,x))
;
symmetry
for F, G being Relation st ( for x being object holds card (Coim (F,x)) = card (Coim (G,x)) ) holds
for x being object holds card (Coim (G,x)) = card (Coim (F,x))
;
end;

:: deftheorem defines are_fiberwise_equipotent CLASSES1:def 10 :
for F, G being Relation holds
( F,G are_fiberwise_equipotent iff for x being object holds card (Coim (F,x)) = card (Coim (G,x)) );

Lm3: for F being Function
for x being object st not x in rng F holds
Coim (F,x) = {}

proof end;

theorem Th75: :: CLASSES1:75
for F, G being Function st F,G are_fiberwise_equipotent holds
rng F = rng G
proof 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 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 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 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 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 end;

theorem :: CLASSES1:81
for F, G being Function st F,G are_fiberwise_equipotent holds
card (dom F) = card (dom G)
proof end;

:: from CIRCCOMB, 2009.01.26, A.T.
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 end;

:: from BAGORDER, 2011.07.24, A.T.
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 end;

scheme :: CLASSES1:sch 2
LambdaAB{ F1() -> set , F2() -> set , F3( Element of F2()) -> set } :
ex f being Function st
( dom f = F1() & ( for x being Element of F2() st x in F1() holds
f . x = F3(x) ) )
proof end;

theorem :: CLASSES1:84
for x, y being set holds
( the_rank_of x in the_rank_of [x,y] & the_rank_of y in the_rank_of [x,y] )
proof end;