:: CLASSES1 semantic presentation

definition

let c₁ be set ;
attr a₁ is subset-closed means :Def1: :: CLASSES1:def 1
for b₁, b₂ being set st b₁ in a₁ & b₂ c= b₁ holds
b₂ in a₁;

end;

:: deftheorem Def1 defines subset-closed CLASSES1:def 1 :

definition

let c₁ be set ;
attr a₁ is being_Tarski-Class means :Def2: :: CLASSES1:def 2
( a₁ is subset-closed & ( for b₁ being set st b₁ in a₁ holds
bool b₁ in a₁ ) & ( for b₁ being set holds
( not b₁ c= a₁ or b₁,a₁ are_equipotent or b₁ in a₁ ) ) );

end;

:: deftheorem Def2 defines being_Tarski-Class CLASSES1:def 2 :

notation

let c₁ be set ;
synonym c₁ is_Tarski-Class for being_Tarski-Class c₁;

end;

definition

let c₁, c₂ be set ;
pred c₂ is_Tarski-Class_of c₁ means :Def3: :: CLASSES1:def 3
( a₁ in a₂ & a₂ is_Tarski-Class );

end;

:: deftheorem Def3 defines is_Tarski-Class_of CLASSES1:def 3 :

definition

let c₁ be set ;
func Tarski-Class c₁ -> set means :Def4: :: CLASSES1:def 4
( a₂ is_Tarski-Class_of a₁ & ( for b₁ being set st b₁ is_Tarski-Class_of a₁ holds
a₂ c= b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Tarski-Class CLASSES1:def 4 :

registration

let c₁ be set ;
cluster Tarski-Class a₁ -> non empty ;
coherence

proof end;

end;

theorem Th1: :: CLASSES1:1

canceled;

theorem Th2: :: CLASSES1:2

for b₁ being set holds
( b₁ is_Tarski-Class iff ( b₁ is subset-closed & ( for b₂ being set st b₂ in b₁ holds
bool b₂ in b₁ ) & ( for b₂ being set st b₂ c= b₁ & Card b₂ <` Card b₁ holds
b₂ in b₁ ) ) )

proof end;

theorem Th3: :: CLASSES1:3

canceled;

theorem Th4: :: CLASSES1:4

canceled;

theorem Th5: :: CLASSES1:5

for b₁ being set holds b₁ in Tarski-Class b₁

proof end;

theorem Th6: :: CLASSES1:6

for b₁, b₂, b₃ being set st b₁ in Tarski-Class b₂ & b₃ c= b₁ holds
b₃ in Tarski-Class b₂

proof end;

theorem Th7: :: CLASSES1:7

for b₁, b₂ being set st b₁ in Tarski-Class b₂ holds
bool b₁ in Tarski-Class b₂

proof end;

theorem Th8: :: CLASSES1:8

for b₁, b₂ being set holds
( not b₁ c= Tarski-Class b₂ or b₁, Tarski-Class b₂ are_equipotent or b₁ in Tarski-Class b₂ )

proof end;

theorem Th9: :: CLASSES1:9

for b₁, b₂ being set st b₁ c= Tarski-Class b₂ & Card b₁ <` Card (Tarski-Class b₂) holds
b₁ in Tarski-Class b₂

proof end;

definition

let c₁ be set ;
let c₂ be Ordinal;
func Tarski-Class c₁,c₂ -> set means :Def5: :: CLASSES1:def 5
ex b₁ being T-Sequence st
( a₃ = last b₁ & dom b₁ = succ a₂ & b₁ . {} = {a₁} & ( for b₂ being Ordinal st succ b₂ in succ a₂ holds
b₁ . (succ b₂) = ({ b₃ where B is Element of Tarski-Class a₁ : ex b₁ being Element of Tarski-Class a₁ st
( b₄ in b₁ . b₂ & b₃ c= b₄ ) } \/ { (bool b₃) where B is Element of Tarski-Class a₁ : b₃ in b₁ . b₂ } ) \/ ((bool (b₁ . b₂)) /\ (Tarski-Class a₁)) ) & ( for b₂ being Ordinal st b₂ in succ a₂ & b₂ <> {} & b₂ is_limit_ordinal holds
b₁ . b₂ = (union (rng (b₁ | b₂))) /\ (Tarski-Class a₁) ) );
correctness

proof end;

end;

:: deftheorem Def5 defines Tarski-Class CLASSES1:def 5 :

E10: now

let c₁ be set ;
deffunc H₁( Ordinal) -> set = Tarski-Class c₁,a₁;
deffunc H₂( Ordinal, set ) -> set = ({ b₁ where B is Element of Tarski-Class c₁ : ex b₁ being Element of Tarski-Class c₁ st
( b₂ in a₂ & b₁ c= b₂ ) } \/ { (bool b₁) where B is Element of Tarski-Class c₁ : b₁ in a₂ } ) \/ ((bool a₂) /\ (Tarski-Class c₁));
deffunc H₃( Ordinal, T-Sequence) -> set = (union (rng a₂)) /\ (Tarski-Class c₁);
E11: for b₁ being Ordinal
for b₂ being set holds
( b₂ = H₁(b₁) iff ex b₃ being T-Sequence st
( b₂ = last b₃ & dom b₃ = succ b₁ & b₃ . {} = {c₁} & ( for b₄ being Ordinal st succ b₄ in succ b₁ holds
b₃ . (succ b₄) = H₂(b₄,b₃ . b₄) ) & ( for b₄ being Ordinal st b₄ in succ b₁ & b₄ <> {} & b₄ is_limit_ordinal holds
b₃ . b₄ = H₃(b₄,b₃ | b₄) ) ) ) by Def5;
thus H₁( {} ) = {c₁} from ORDINAL2:sch 8(E11);
thus for b₁ being Ordinal holds H₁( succ b₁) = H₂(b₁,H₁(b₁)) from ORDINAL2:sch 9(E11);
thus for b₁ being Ordinal
for b₂ being T-Sequence st b₁ <> {} & b₁ is_limit_ordinal & dom b₂ = b₁ & ( for b₃ being Ordinal st b₃ in b₁ holds
b₂ . b₃ = Tarski-Class c₁,b₃ ) holds
Tarski-Class c₁,b₁ = (union (rng b₂)) /\ (Tarski-Class c₁)

proof

let c₂ be Ordinal;
let c₃ be T-Sequence;
assume that
E12: ( c₂ <> {} & c₂ is_limit_ordinal ) and
E13: dom c₃ = c₂ and
E14: for b₁ being Ordinal st b₁ in c₂ holds
c₃ . b₁ = H₁(b₁) ;
thus H₁(c₂) = H₃(c₂,c₃) from ORDINAL2:sch 10(E11, E12, E13, E14);

end;

definition

let c₁ be set ;
let c₂ be Ordinal;
redefine func Tarski-Class as Tarski-Class c₁,c₂ -> Subset of (Tarski-Class a₁);
coherence

proof end;

end;

theorem Th10: :: CLASSES1:10

for b₁ being set holds Tarski-Class b₁,{} = {b₁} by Lemma10;

theorem Th11: :: CLASSES1:11

for b₁ being set
for b₂ being Ordinal holds Tarski-Class b₁,(succ b₂) = ({ b₃ where B is Element of Tarski-Class b₁ : ex b₁ being Element of Tarski-Class b₁ st
( b₄ in Tarski-Class b₁,b₂ & b₃ c= b₄ ) } \/ { (bool b₃) where B is Element of Tarski-Class b₁ : b₃ in Tarski-Class b₁,b₂ } ) \/ ((bool (Tarski-Class b₁,b₂)) /\ (Tarski-Class b₁)) by Lemma10;

theorem Th12: :: CLASSES1:12

for b₁ being set
for b₂ being Ordinal st b₂ <> {} & b₂ is_limit_ordinal holds
Tarski-Class b₁,b₂ = { b₃ where B is Element of Tarski-Class b₁ : ex b₁ being Ordinal st
( b₄ in b₂ & b₃ in Tarski-Class b₁,b₄ ) }

proof end;

theorem Th13: :: CLASSES1:13

for b₁, b₂ being set
for b₃ being Ordinal holds
( b₁ in Tarski-Class b₂,(succ b₃) iff ( ( b₁ c= Tarski-Class b₂,b₃ & b₁ in Tarski-Class b₂ ) or ex b₄ being set st
( b₄ in Tarski-Class b₂,b₃ & ( b₁ c= b₄ or b₁ = bool b₄ ) ) ) )

proof end;

theorem Th14: :: CLASSES1:14

for b₁, b₂, b₃ being set
for b₄ being Ordinal st b₁ c= b₂ & b₂ in Tarski-Class b₃,b₄ holds
b₁ in Tarski-Class b₃,(succ b₄) by Th13;

theorem Th15: :: CLASSES1:15

for b₁, b₂ being set
for b₃ being Ordinal st b₁ in Tarski-Class b₂,b₃ holds
bool b₁ in Tarski-Class b₂,(succ b₃) by Th13;

theorem Th16: :: CLASSES1:16

for b₁, b₂ being set
for b₃ being Ordinal st b₃ <> {} & b₃ is_limit_ordinal holds
( b₂ in Tarski-Class b₁,b₃ iff ex b₄ being Ordinal st
( b₄ in b₃ & b₂ in Tarski-Class b₁,b₄ ) )

proof end;

theorem Th17: :: CLASSES1:17

for b₁, b₂, b₃ being set
for b₄ being Ordinal st b₄ <> {} & b₄ is_limit_ordinal & b₁ in Tarski-Class b₂,b₄ & ( b₃ c= b₁ or b₃ = bool b₁ ) holds
b₃ in Tarski-Class b₂,b₄

proof end;

theorem Th18: :: CLASSES1:18

for b₁ being set
for b₂ being Ordinal holds Tarski-Class b₁,b₂ c= Tarski-Class b₁,(succ b₂)

proof end;

theorem Th19: :: CLASSES1:19

for b₁ being set
for b₂, b₃ being Ordinal st b₂ c= b₃ holds
Tarski-Class b₁,b₂ c= Tarski-Class b₁,b₃

proof end;

theorem Th20: :: CLASSES1:20

for b₁ being set ex b₂ being Ordinal st Tarski-Class b₁,b₂ = Tarski-Class b₁,(succ b₂)

proof end;

theorem Th21: :: CLASSES1:21

for b₁ being set
for b₂ being Ordinal st Tarski-Class b₁,b₂ = Tarski-Class b₁,(succ b₂) holds
Tarski-Class b₁,b₂ = Tarski-Class b₁

proof end;

theorem Th22: :: CLASSES1:22

for b₁ being set ex b₂ being Ordinal st Tarski-Class b₁,b₂ = Tarski-Class b₁

proof end;

theorem Th23: :: CLASSES1:23

for b₁ being set ex b₂ being Ordinal st
( Tarski-Class b₁,b₂ = Tarski-Class b₁ & ( for b₃ being Ordinal st b₃ in b₂ holds
Tarski-Class b₁,b₃ <> Tarski-Class b₁ ) )

proof end;

theorem Th24: :: CLASSES1:24

for b₁, b₂ being set st b₁ <> b₂ & b₁ in Tarski-Class b₂ holds
ex b₃ being Ordinal st
( not b₁ in Tarski-Class b₂,b₃ & b₁ in Tarski-Class b₂,(succ b₃) )

proof end;

theorem Th25: :: CLASSES1:25

for b₁ being set st b₁ is epsilon-transitive holds
for b₂ being Ordinal st b₂ <> {} holds
Tarski-Class b₁,b₂ is epsilon-transitive

proof end;

theorem Th26: :: CLASSES1:26

for b₁ being set holds
( Tarski-Class b₁,{} in Tarski-Class b₁,one & Tarski-Class b₁,{} <> Tarski-Class b₁,one )

proof end;

theorem Th27: :: CLASSES1:27

for b₁ being set st b₁ is epsilon-transitive holds
Tarski-Class b₁ is epsilon-transitive

proof end;

theorem Th28: :: CLASSES1:28

for b₁, b₂ being set st b₁ in Tarski-Class b₂ holds
Card b₁ <` Card (Tarski-Class b₂)

proof end;

theorem Th29: :: CLASSES1:29

for b₁, b₂ being set st b₁ in Tarski-Class b₂ holds
not b₁, Tarski-Class b₂ are_equipotent

proof end;

theorem Th30: :: CLASSES1:30

for b₁, b₂, b₃ being set st b₂ in Tarski-Class b₁ & b₃ in Tarski-Class b₁ holds
( {b₂} in Tarski-Class b₁ & {b₂,b₃} in Tarski-Class b₁ )

proof end;

theorem Th31: :: CLASSES1:31

for b₁, b₂, b₃ being set st b₂ in Tarski-Class b₁ & b₃ in Tarski-Class b₁ holds
[b₂,b₃] in Tarski-Class b₁

proof end;

theorem Th32: :: CLASSES1:32

for b₁, b₂, b₃ being set st b₁ c= Tarski-Class b₂ & b₃ c= Tarski-Class b₂ holds
[:b₁,b₃:] c= Tarski-Class b₂

proof end;

definition

let c₁ be Ordinal;
func Rank c₁ -> set means :Def6: :: CLASSES1:def 6
ex b₁ being T-Sequence st
( a₂ = last b₁ & dom b₁ = succ a₁ & b₁ . {} = {} & ( for b₂ being Ordinal st succ b₂ in succ a₁ holds
b₁ . (succ b₂) = bool (b₁ . b₂) ) & ( for b₂ being Ordinal st b₂ in succ a₁ & b₂ <> {} & b₂ is_limit_ordinal holds
b₁ . b₂ = union (rng (b₁ | b₂)) ) );
correctness

proof end;

end;

:: deftheorem Def6 defines Rank CLASSES1:def 6 :

deffunc H₁( Ordinal) -> set = Rank a₁;

E26: now

deffunc H₂( Ordinal, set ) -> set = bool a₂;
deffunc H₃( Ordinal, T-Sequence) -> set = union (rng a₂);
E27: for b₁ being Ordinal
for b₂ being set holds
( b₂ = H₁(b₁) iff ex b₃ being T-Sequence st
( b₂ = last b₃ & dom b₃ = succ b₁ & b₃ . {} = {} & ( for b₄ being Ordinal st succ b₄ in succ b₁ holds
b₃ . (succ b₄) = H₂(b₄,b₃ . b₄) ) & ( for b₄ being Ordinal st b₄ in succ b₁ & b₄ <> {} & b₄ is_limit_ordinal holds
b₃ . b₄ = H₃(b₄,b₃ | b₄) ) ) ) by Def6;
thus H₁( {} ) = {} from ORDINAL2:sch 8(E27);
thus for b₁ being Ordinal holds H₁( succ b₁) = H₂(b₁,H₁(b₁)) from ORDINAL2:sch 9(E27);
thus for b₁ being Ordinal
for b₂ being T-Sequence st b₁ <> {} & b₁ is_limit_ordinal & dom b₂ = b₁ & ( for b₃ being Ordinal st b₃ in b₁ holds
b₂ . b₃ = Rank b₃ ) holds
Rank b₁ = union (rng b₂)

proof

let c₁ be Ordinal;
let c₂ be T-Sequence;
assume that
E28: ( c₁ <> {} & c₁ is_limit_ordinal ) and
E29: dom c₂ = c₁ and
E30: for b₁ being Ordinal st b₁ in c₁ holds
c₂ . b₁ = H₁(b₁) ;
thus H₁(c₁) = H₃(c₁,c₂) from ORDINAL2:sch 10(E27, E28, E29, E30);

end;

theorem Th33: :: CLASSES1:33

Rank {} = {} by Lemma26;

theorem Th34: :: CLASSES1:34

for b₁ being Ordinal holds Rank (succ b₁) = bool (Rank b₁) by Lemma26;

theorem Th35: :: CLASSES1:35

for b₁ being Ordinal st b₁ <> {} & b₁ is_limit_ordinal holds
for b₂ being set holds
( b₂ in Rank b₁ iff ex b₃ being Ordinal st
( b₃ in b₁ & b₂ in Rank b₃ ) )

proof end;

theorem Th36: :: CLASSES1:36

for b₁ being set
for b₂ being Ordinal holds
( b₁ c= Rank b₂ iff b₁ in Rank (succ b₂) )

proof end;

theorem Th37: :: CLASSES1:37

for b₁ being Ordinal holds Rank b₁ is epsilon-transitive

proof end;

theorem Th38: :: CLASSES1:38

for b₁ being set
for b₂ being Ordinal st b₁ in Rank b₂ holds
b₁ c= Rank b₂

proof end;

theorem Th39: :: CLASSES1:39

for b₁ being Ordinal holds Rank b₁ c= Rank (succ b₁)

proof end;

theorem Th40: :: CLASSES1:40

for b₁ being Ordinal holds union (Rank b₁) c= Rank b₁

proof end;

theorem Th41: :: CLASSES1:41

for b₁ being set
for b₂ being Ordinal st b₁ in Rank b₂ holds
union b₁ in Rank b₂

proof end;

theorem Th42: :: CLASSES1:42

for b₁, b₂ being Ordinal holds
( b₁ in b₂ iff Rank b₁ in Rank b₂ )

proof end;

theorem Th43: :: CLASSES1:43

for b₁, b₂ being Ordinal holds
( b₁ c= b₂ iff Rank b₁ c= Rank b₂ )

proof end;

theorem Th44: :: CLASSES1:44

for b₁ being Ordinal holds b₁ c= Rank b₁

proof end;

theorem Th45: :: CLASSES1:45

for b₁ being Ordinal
for b₂ being set st b₂ in Rank b₁ holds
( not b₂, Rank b₁ are_equipotent & Card b₂ <` Card (Rank b₁) )

proof end;

theorem Th46: :: CLASSES1:46

for b₁ being set
for b₂ being Ordinal holds
( b₁ c= Rank b₂ iff bool b₁ c= Rank (succ b₂) )

proof end;

theorem Th47: :: CLASSES1:47

for b₁, b₂ being set
for b₃ being Ordinal st b₁ c= b₂ & b₂ in Rank b₃ holds
b₁ in Rank b₃

proof end;

theorem Th48: :: CLASSES1:48

for b₁ being set
for b₂ being Ordinal holds
( b₁ in Rank b₂ iff bool b₁ in Rank (succ b₂) )

proof end;

theorem Th49: :: CLASSES1:49

for b₁ being set
for b₂ being Ordinal holds
( b₁ in Rank b₂ iff {b₁} in Rank (succ b₂) )

proof end;

theorem Th50: :: CLASSES1:50

for b₁, b₂ being set
for b₃ being Ordinal holds
( ( b₁ in Rank b₃ & b₂ in Rank b₃ ) iff {b₁,b₂} in Rank (succ b₃) )

proof end;

theorem Th51: :: CLASSES1:51

for b₁, b₂ being set
for b₃ being Ordinal holds
( ( b₁ in Rank b₃ & b₂ in Rank b₃ ) iff [b₁,b₂] in Rank (succ (succ b₃)) )

proof end;

theorem Th52: :: CLASSES1:52

for b₁ being set
for b₂ being Ordinal st b₁ is epsilon-transitive & (Rank b₂) /\ (Tarski-Class b₁) = (Rank (succ b₂)) /\ (Tarski-Class b₁) holds
Tarski-Class b₁ c= Rank b₂

proof end;

theorem Th53: :: CLASSES1:53

for b₁ being set st b₁ is epsilon-transitive holds
ex b₂ being Ordinal st Tarski-Class b₁ c= Rank b₂

proof end;

theorem Th54: :: CLASSES1:54

for b₁ being set st b₁ is epsilon-transitive holds
union b₁ c= b₁

proof end;

theorem Th55: :: CLASSES1:55

for b₁, b₂ being set st b₁ is epsilon-transitive & b₂ is epsilon-transitive holds
b₁ \/ b₂ is epsilon-transitive

proof end;

theorem Th56: :: CLASSES1:56

for b₁, b₂ being set st b₁ is epsilon-transitive & b₂ is epsilon-transitive holds
b₁ /\ b₂ is epsilon-transitive

proof end;

deffunc H₂( set , set ) -> set = union a₂;

definition

let c₁ be set ;
func the_transitive-closure_of c₁ -> set means :Def7: :: CLASSES1:def 7
for b₁ being set holds
( b₁ in a₂ iff ex b₂ being Functionex b₃ being Nat st
( b₁ in b₂ . b₃ & dom b₂ = NAT & b₂ . 0 = a₁ & ( for b₄ being Nat holds b₂ . (b₄ + 1) = union (b₂ . b₄) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines the_transitive-closure_of CLASSES1:def 7 :

theorem Th57: :: CLASSES1:57

canceled;

theorem Th58: :: CLASSES1:58

for b₁ being set holds the_transitive-closure_of b₁ is epsilon-transitive

proof end;

theorem Th59: :: CLASSES1:59

for b₁ being set holds b₁ c= the_transitive-closure_of b₁

proof end;

theorem Th60: :: CLASSES1:60

for b₁, b₂ being set st b₁ c= b₂ & b₂ is epsilon-transitive holds
the_transitive-closure_of b₁ c= b₂

proof end;

theorem Th61: :: CLASSES1:61

for b₁, b₂ being set st ( for b₃ being set st b₁ c= b₃ & b₃ is epsilon-transitive holds
b₂ c= b₃ ) & b₁ c= b₂ & b₂ is epsilon-transitive holds
the_transitive-closure_of b₁ = b₂

proof end;

theorem Th62: :: CLASSES1:62

for b₁ being set st b₁ is epsilon-transitive holds
the_transitive-closure_of b₁ = b₁

proof end;

theorem Th63: :: CLASSES1:63

the_transitive-closure_of {} = {} by Th62;

theorem Th64: :: CLASSES1:64

for b₁ being Ordinal holds the_transitive-closure_of b₁ = b₁ by Th62;

theorem Th65: :: CLASSES1:65

for b₁, b₂ being set st b₁ c= b₂ holds
the_transitive-closure_of b₁ c= the_transitive-closure_of b₂

proof end;

theorem Th66: :: CLASSES1:66

for b₁ being set holds the_transitive-closure_of (the_transitive-closure_of b₁) = the_transitive-closure_of b₁

proof end;

theorem Th67: :: CLASSES1:67

for b₁, b₂ being set holds the_transitive-closure_of (b₁ \/ b₂) = (the_transitive-closure_of b₁) \/ (the_transitive-closure_of b₂)

proof end;

theorem Th68: :: CLASSES1:68

for b₁, b₂ being set holds the_transitive-closure_of (b₁ /\ b₂) c= (the_transitive-closure_of b₁) /\ (the_transitive-closure_of b₂)

proof end;

theorem Th69: :: CLASSES1:69

for b₁ being set ex b₂ being Ordinal st b₁ c= Rank b₂

proof end;

definition

let c₁ be set ;
func the_rank_of c₁ -> Ordinal means :Def8: :: CLASSES1:def 8
( a₁ c= Rank a₂ & ( for b₁ being Ordinal st a₁ c= Rank b₁ holds
a₂ c= b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines the_rank_of CLASSES1:def 8 :

theorem Th70: :: CLASSES1:70

canceled;

theorem Th71: :: CLASSES1:71

for b₁ being set holds the_rank_of (bool b₁) = succ (the_rank_of b₁)

proof end;

theorem Th72: :: CLASSES1:72

for b₁ being Ordinal holds the_rank_of (Rank b₁) = b₁

proof end;

theorem Th73: :: CLASSES1:73

for b₁ being set
for b₂ being Ordinal holds
( b₁ c= Rank b₂ iff the_rank_of b₁ c= b₂ )

proof end;

theorem Th74: :: CLASSES1:74

for b₁ being set
for b₂ being Ordinal holds
( b₁ in Rank b₂ iff the_rank_of b₁ in b₂ )

proof end;

theorem Th75: :: CLASSES1:75

for b₁, b₂ being set st b₁ c= b₂ holds
the_rank_of b₁ c= the_rank_of b₂

proof end;

theorem Th76: :: CLASSES1:76

for b₁, b₂ being set st b₁ in b₂ holds
the_rank_of b₁ in the_rank_of b₂

proof end;

theorem Th77: :: CLASSES1:77

for b₁ being set
for b₂ being Ordinal holds
( the_rank_of b₁ c= b₂ iff for b₃ being set st b₃ in b₁ holds
the_rank_of b₃ in b₂ )

proof end;

theorem Th78: :: CLASSES1:78

for b₁ being set
for b₂ being Ordinal holds
( b₂ c= the_rank_of b₁ iff for b₃ being Ordinal st b₃ in b₂ holds
ex b₄ being set st
( b₄ in b₁ & b₃ c= the_rank_of b₄ ) )

proof end;

theorem Th79: :: CLASSES1:79

for b₁ being set holds
( the_rank_of b₁ = {} iff b₁ = {} )

proof end;

theorem Th80: :: CLASSES1:80

for b₁ being set
for b₂ being Ordinal st the_rank_of b₁ = succ b₂ holds
ex b₃ being set st
( b₃ in b₁ & the_rank_of b₃ = b₂ )

proof end;

theorem Th81: :: CLASSES1:81

for b₁ being Ordinal holds the_rank_of b₁ = b₁

proof end;

theorem Th82: :: CLASSES1:82

for b₁ being set holds
( the_rank_of (Tarski-Class b₁) <> {} & the_rank_of (Tarski-Class b₁) is_limit_ordinal )

proof end;