:: CLASSES2 semantic presentation

Lemma1: for b₁ being set holds Tarski-Class b₁ is_Tarski-Class

proof end;

registration

cluster being_Tarski-Class -> subset-closed set ;
coherence by CLASSES1:def 2;

end;

registration

let c₁ be set ;
cluster Tarski-Class a₁ -> subset-closed being_Tarski-Class ;
coherence by Lemma1;

end;

theorem Th1: :: CLASSES2:1

for b₁, b₂ being set st b₁ is subset-closed & b₂ in b₁ holds
( not b₂,b₁ are_equipotent & Card b₂ <` Card b₁ )

proof end;

theorem Th2: :: CLASSES2:2

canceled;

theorem Th3: :: CLASSES2:3

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

proof end;

theorem Th4: :: CLASSES2:4

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

proof end;

theorem Th5: :: CLASSES2:5

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

proof end;

theorem Th6: :: CLASSES2:6

for b₁ being Ordinal
for b₂ being set st b₂ is_Tarski-Class & b₁ in b₂ holds
( succ b₁ in b₂ & b₁ c= b₂ )

proof end;

theorem Th7: :: CLASSES2:7

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

theorem Th8: :: CLASSES2:8

for b₁, b₂ being set st b₁ is subset-closed & b₂ is epsilon-transitive & b₂ in b₁ holds
b₂ c= b₁

proof end;

theorem Th9: :: CLASSES2:9

for b₁, b₂ being set st b₁ is epsilon-transitive & b₁ in Tarski-Class b₂ holds
b₁ c= Tarski-Class b₂ by Th8;

theorem Th10: :: CLASSES2:10

for b₁ being set st b₁ is_Tarski-Class holds
On b₁ = Card b₁

proof end;

theorem Th11: :: CLASSES2:11

for b₁ being set holds On (Tarski-Class b₁) = Card (Tarski-Class b₁) by Th10;

theorem Th12: :: CLASSES2:12

for b₁, b₂ being set st b₁ is_Tarski-Class & b₂ in b₁ holds
Card b₂ in b₁

proof end;

theorem Th13: :: CLASSES2:13

for b₁, b₂ being set st b₁ in Tarski-Class b₂ holds
Card b₁ in Tarski-Class b₂ by Th12;

theorem Th14: :: CLASSES2:14

for b₁, b₂ being set st b₁ is_Tarski-Class & b₂ in Card b₁ holds
b₂ in b₁

proof end;

theorem Th15: :: CLASSES2:15

for b₁, b₂ being set st b₁ in Card (Tarski-Class b₂) holds
b₁ in Tarski-Class b₂ by Th14;

theorem Th16: :: CLASSES2:16

for b₁ being Cardinal
for b₂ being set st b₂ is_Tarski-Class & b₁ <` Card b₂ holds
b₁ in b₂

proof end;

theorem Th17: :: CLASSES2:17

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

proof end;

theorem Th18: :: CLASSES2:18

for b₁ being Cardinal
for b₂ being set st b₂ is_Tarski-Class & b₁ in b₂ holds
b₁ c= b₂ by Th6;

theorem Th19: :: CLASSES2:19

for b₁ being Cardinal
for b₂ being set st b₁ in Tarski-Class b₂ holds
b₁ c= Tarski-Class b₂ by Th6;

theorem Th20: :: CLASSES2:20

for b₁ being set st b₁ is_Tarski-Class holds
Card b₁ is_limit_ordinal

proof end;

theorem Th21: :: CLASSES2:21

for b₁ being set st b₁ is_Tarski-Class & b₁ <> {} holds
( Card b₁ <> 0 & Card b₁ <> {} & Card b₁ is_limit_ordinal )

proof end;

theorem Th22: :: CLASSES2:22

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

proof end;

theorem Th23: :: CLASSES2:23

for b₁, b₂ being set st b₁ is_Tarski-Class & ( ( b₂ in b₁ & b₁ is epsilon-transitive ) or ( b₂ in b₁ & b₂ c= b₁ ) or ( Card b₂ <` Card b₁ & b₂ c= b₁ ) ) holds
Funcs b₂,b₁ c= b₁

proof end;

theorem Th24: :: CLASSES2:24

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

proof end;

theorem Th25: :: CLASSES2:25

for b₁ being T-Sequence st dom b₁ is_limit_ordinal & ( for b₂ being Ordinal st b₂ in dom b₁ holds
b₁ . b₂ = Rank b₂ ) holds
Rank (dom b₁) = Union b₁

proof end;

defpred S₁[ Ordinal] means for b₁ being set st b₁ is_Tarski-Class & a₁ in On b₁ holds
( Card (Rank a₁) <` Card b₁ & Rank a₁ in b₁ );

Lemma16: S₁[ {} ]
by Th10, CARD_1:47, CLASSES1:33, ORDINAL2:def 2;

Lemma17: for b₁ being Ordinal st S₁[b₁] holds
S₁[ succ b₁]

proof end;

Lemma18: for b₁ being Ordinal st b₁ <> {} & b₁ is_limit_ordinal & ( for b₂ being Ordinal st b₂ in b₁ holds
S₁[b₂] ) holds
S₁[b₁]

proof end;

theorem Th26: :: CLASSES2:26

for b₁ being Ordinal
for b₂ being set st b₂ is_Tarski-Class & b₁ in On b₂ holds
( Card (Rank b₁) <` Card b₂ & Rank b₁ in b₂ )

proof end;

theorem Th27: :: CLASSES2:27

for b₁ being Ordinal
for b₂ being set st b₁ in On (Tarski-Class b₂) holds
( Card (Rank b₁) <` Card (Tarski-Class b₂) & Rank b₁ in Tarski-Class b₂ ) by Th26;

theorem Th28: :: CLASSES2:28

for b₁ being set st b₁ is_Tarski-Class holds
Rank (Card b₁) c= b₁

proof end;

theorem Th29: :: CLASSES2:29

for b₁ being set holds Rank (Card (Tarski-Class b₁)) c= Tarski-Class b₁

proof end;

deffunc H₁( set ) -> set = the_rank_of a₁;

deffunc H₂( set ) -> set = Card (bool a₁);

theorem Th30: :: CLASSES2:30

for b₁, b₂ being set st b₁ is_Tarski-Class & b₁ is epsilon-transitive & b₂ in b₁ holds
the_rank_of b₂ in b₁

proof end;

theorem Th31: :: CLASSES2:31

for b₁ being set st b₁ is_Tarski-Class & b₁ is epsilon-transitive holds
b₁ c= Rank (Card b₁)

proof end;

theorem Th32: :: CLASSES2:32

for b₁ being set st b₁ is_Tarski-Class & b₁ is epsilon-transitive holds
Rank (Card b₁) = b₁

proof end;

theorem Th33: :: CLASSES2:33

for b₁ being Ordinal
for b₂ being set st b₂ is_Tarski-Class & b₁ in On b₂ holds
Card (Rank b₁) <=` Card b₂

proof end;

theorem Th34: :: CLASSES2:34

for b₁ being Ordinal
for b₂ being set st b₁ in On (Tarski-Class b₂) holds
Card (Rank b₁) <=` Card (Tarski-Class b₂)

proof end;

theorem Th35: :: CLASSES2:35

for b₁ being set st b₁ is_Tarski-Class holds
Card b₁ = Card (Rank (Card b₁))

proof end;

theorem Th36: :: CLASSES2:36

for b₁ being set holds Card (Tarski-Class b₁) = Card (Rank (Card (Tarski-Class b₁))) by Th35;

theorem Th37: :: CLASSES2:37

for b₁, b₂ being set st b₁ is_Tarski-Class & b₂ c= Rank (Card b₁) & not b₂, Rank (Card b₁) are_equipotent holds
b₂ in Rank (Card b₁)

proof end;

theorem Th38: :: CLASSES2:38

for b₁, b₂ being set holds
( not b₁ c= Rank (Card (Tarski-Class b₂)) or b₁, Rank (Card (Tarski-Class b₂)) are_equipotent or b₁ in Rank (Card (Tarski-Class b₂)) ) by Th37;

theorem Th39: :: CLASSES2:39

for b₁ being set st b₁ is_Tarski-Class holds
Rank (Card b₁) is_Tarski-Class

proof end;

theorem Th40: :: CLASSES2:40

for b₁ being set holds Rank (Card (Tarski-Class b₁)) is_Tarski-Class by Th39;

theorem Th41: :: CLASSES2:41

for b₁ being Ordinal
for b₂ being set st b₂ is epsilon-transitive & b₁ in the_rank_of b₂ holds
ex b₃ being set st
( b₃ in b₂ & the_rank_of b₃ = b₁ )

proof end;

theorem Th42: :: CLASSES2:42

for b₁ being set st b₁ is epsilon-transitive holds
Card (the_rank_of b₁) <=` Card b₁

proof end;

theorem Th43: :: CLASSES2:43

for b₁, b₂ being set st b₁ is_Tarski-Class & b₂ is epsilon-transitive & b₂ in b₁ holds
b₂ in Rank (Card b₁)

proof end;

theorem Th44: :: CLASSES2:44

for b₁, b₂ being set st b₁ is epsilon-transitive & b₁ in Tarski-Class b₂ holds
b₁ in Rank (Card (Tarski-Class b₂)) by Th43;

theorem Th45: :: CLASSES2:45

for b₁ being set st b₁ is epsilon-transitive holds
Rank (Card (Tarski-Class b₁)) is_Tarski-Class_of b₁

proof end;

theorem Th46: :: CLASSES2:46

for b₁ being set st b₁ is epsilon-transitive holds
Rank (Card (Tarski-Class b₁)) = Tarski-Class b₁

proof end;

definition

let c₁ be set ;
attr a₁ is universal means :Def1: :: CLASSES2:def 1
( a₁ is epsilon-transitive & a₁ is_Tarski-Class );

end;

:: deftheorem Def1 defines universal CLASSES2:def 1 :

registration

cluster universal -> epsilon-transitive subset-closed being_Tarski-Class set ;
coherence by Def1;
cluster epsilon-transitive being_Tarski-Class -> universal set ;
coherence by Def1;

end;

registration

cluster epsilon-transitive non empty subset-closed being_Tarski-Class universal set ;
existence

proof end;

end;

definition

mode Universe is non empty universal set ;

end;

theorem Th47: :: CLASSES2:47

canceled;

theorem Th48: :: CLASSES2:48

canceled;

theorem Th49: :: CLASSES2:49

canceled;

theorem Th50: :: CLASSES2:50

for b₁ being Universe holds On b₁ is Ordinal

proof end;

theorem Th51: :: CLASSES2:51

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

proof end;

theorem Th52: :: CLASSES2:52

for b₁ being Universe holds Tarski-Class b₁ is Universe by Th51;

registration

let c₁ be Universe;
cluster On a₁ -> ordinal ;
coherence by Th50;
cluster Tarski-Class a₁ -> epsilon-transitive subset-closed being_Tarski-Class universal ;
coherence by Th51;

end;

theorem Th53: :: CLASSES2:53

for b₁ being Ordinal holds Tarski-Class b₁ is universal

proof end;

registration

let c₁ be Ordinal;
cluster Tarski-Class a₁ -> epsilon-transitive subset-closed being_Tarski-Class universal ;
coherence by Th53;

end;

theorem Th54: :: CLASSES2:54

for b₁ being Universe holds b₁ = Rank (On b₁)

proof end;

theorem Th55: :: CLASSES2:55

for b₁ being Universe holds
( On b₁ <> {} & On b₁ is_limit_ordinal )

proof end;

theorem Th56: :: CLASSES2:56

for b₁, b₂ being Universe holds
( b₁ in b₂ or b₁ = b₂ or b₂ in b₁ )

proof end;

theorem Th57: :: CLASSES2:57

for b₁, b₂ being Universe holds
( b₁ c= b₂ or b₂ in b₁ )

proof end;

theorem Th58: :: CLASSES2:58

for b₁, b₂ being Universe holds b₁,b₂ are_c=-comparable

proof end;

theorem Th59: :: CLASSES2:59

for b₁, b₂, b₃ being Universe st b₁ in b₂ & b₂ in b₃ holds
b₁ in b₃

proof end;

theorem Th60: :: CLASSES2:60

canceled;

theorem Th61: :: CLASSES2:61

for b₁, b₂ being Universe holds
( b₁ \/ b₂ is Universe & b₁ /\ b₂ is Universe )

proof end;

theorem Th62: :: CLASSES2:62

for b₁ being Universe holds {} in b₁

proof end;

theorem Th63: :: CLASSES2:63

for b₁ being set
for b₂ being Universe st b₁ in b₂ holds
{b₁} in b₂ by Th3;

theorem Th64: :: CLASSES2:64

for b₁, b₂ being set
for b₃ being Universe st b₁ in b₃ & b₂ in b₃ holds
( {b₁,b₂} in b₃ & [b₁,b₂] in b₃ ) by Th3, Th4;

theorem Th65: :: CLASSES2:65

for b₁ being set
for b₂ being Universe st b₁ in b₂ holds
( bool b₁ in b₂ & union b₁ in b₂ & meet b₁ in b₂ )

proof end;

theorem Th66: :: CLASSES2:66

for b₁, b₂ being set
for b₃ being Universe st b₁ in b₃ & b₂ in b₃ holds
( b₁ \/ b₂ in b₃ & b₁ /\ b₂ in b₃ & b₁ \ b₂ in b₃ & b₁ \+\ b₂ in b₃ )

proof end;

theorem Th67: :: CLASSES2:67

for b₁, b₂ being set
for b₃ being Universe st b₁ in b₃ & b₂ in b₃ holds
( [:b₁,b₂:] in b₃ & Funcs b₁,b₂ in b₃ )

proof end;

registration

let c₁ be Universe;
cluster non empty Element of a₁;
existence

proof end;

end;

definition

let c₁ be Universe;
let c₂ be Element of c₁;
redefine func { as {c₂} -> Element of a₁;
coherence by Th3;
redefine func bool as bool c₂ -> non empty Element of a₁;
coherence by Th65;
redefine func union as union c₂ -> Element of a₁;
coherence by Th65;
redefine func meet as meet c₂ -> Element of a₁;
coherence by Th65;
let c₃ be Element of c₁;
redefine func { as {c₂,c₃} -> Element of a₁;
coherence by Th3;
redefine func [ as [c₂,c₃] -> Element of a₁;
coherence by Th4;
redefine func \/ as c₂ \/ c₃ -> Element of a₁;
coherence by Th66;
redefine func /\ as c₂ /\ c₃ -> Element of a₁;
coherence by Th66;
redefine func \ as c₂ \ c₃ -> Element of a₁;
coherence by Th66;
redefine func \+\ as c₂ \+\ c₃ -> Element of a₁;
coherence by Th66;
redefine func [: as [:c₂,c₃:] -> Element of a₁;
coherence by Th67;
redefine func Funcs as Funcs c₂,c₃ -> Element of a₁;
coherence by Th67;

end;

definition

func FinSETS -> Universe equals :: CLASSES2:def 2
Tarski-Class {} ;
correctness ;

end;

:: deftheorem Def2 defines FinSETS CLASSES2:def 2 :

theorem Th68: :: CLASSES2:68

canceled;

theorem Th69: :: CLASSES2:69

Card (Rank omega ) = Card omega

proof end;

theorem Th70: :: CLASSES2:70

Rank omega is_Tarski-Class

proof end;

theorem Th71: :: CLASSES2:71

FinSETS = Rank omega

proof end;

definition

func SETS -> Universe equals :: CLASSES2:def 3
Tarski-Class FinSETS ;
correctness ;

end;

:: deftheorem Def3 defines SETS CLASSES2:def 3 :

registration

let c₁ be set ;
cluster the_transitive-closure_of a₁ -> epsilon-transitive ;
coherence by CLASSES1:58;

end;

registration

let c₁ be epsilon-transitive set ;
cluster Tarski-Class a₁ -> epsilon-transitive subset-closed being_Tarski-Class universal ;
coherence by CLASSES1:27;

end;

registration

let c₁ be Ordinal;
cluster Rank a₁ -> epsilon-transitive ;
coherence by CLASSES1:37;

end;

definition

let c₁ be set ;
func Universe_closure c₁ -> Universe means :Def4: :: CLASSES2:def 4
( a₁ c= a₂ & ( for b₁ being Universe st a₁ c= b₁ holds
a₂ c= b₁ ) );
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def4 defines Universe_closure CLASSES2:def 4 :

deffunc H₃( Ordinal, set ) -> set = Tarski-Class a₂;

deffunc H₄( Ordinal, T-Sequence) -> Universe = Universe_closure (Union a₂);

definition

mode FinSet is Element of FinSETS ;
mode Set is Element of SETS ;
let c₁ be Ordinal;
func UNIVERSE c₁ -> set means :Def5: :: CLASSES2:def 5
ex b₁ being T-Sequence st
( a₂ = last b₁ & dom b₁ = succ a₁ & b₁ . {} = FinSETS & ( for b₂ being Ordinal st succ b₂ in succ a₁ holds
b₁ . (succ b₂) = Tarski-Class (b₁ . b₂) ) & ( for b₂ being Ordinal st b₂ in succ a₁ & b₂ <> {} & b₂ is_limit_ordinal holds
b₁ . b₂ = Universe_closure (Union (b₁ | b₂)) ) );
correctness

proof end;

end;

:: deftheorem Def5 defines UNIVERSE CLASSES2:def 5 :

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

E49: now

E50: 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₃ . {} = FinSETS & ( 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₅( {} ) = FinSETS from ORDINAL2:sch 8(E50);
thus for b₁ being Ordinal holds H₅( succ b₁) = H₃(b₁,H₅(b₁)) from ORDINAL2:sch 9(E50);
let c₁ be Ordinal;
let c₂ be T-Sequence;
assume that
E51: ( c₁ <> {} & c₁ is_limit_ordinal ) and
E52: dom c₂ = c₁ and
E53: for b₁ being Ordinal st b₁ in c₁ holds
c₂ . b₁ = H₅(b₁) ;
thus H₅(c₁) = H₄(c₁,c₂) from ORDINAL2:sch 10(E50, E51, E52, E53);

end;

registration

let c₁ be Ordinal;
cluster UNIVERSE a₁ -> epsilon-transitive non empty subset-closed being_Tarski-Class universal ;
coherence

proof end;

end;

theorem Th72: :: CLASSES2:72

canceled;

theorem Th73: :: CLASSES2:73

canceled;

theorem Th74: :: CLASSES2:74

canceled;

theorem Th75: :: CLASSES2:75

UNIVERSE {} = FinSETS by Lemma49;

theorem Th76: :: CLASSES2:76

for b₁ being Ordinal holds UNIVERSE (succ b₁) = Tarski-Class (UNIVERSE b₁) by Lemma49;

theorem Th77: :: CLASSES2:77

UNIVERSE one = SETS by Lemma49, ORDINAL2:def 4;

theorem Th78: :: CLASSES2:78

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₃ = UNIVERSE b₃ ) holds
UNIVERSE b₁ = Universe_closure (Union b₂) by Lemma49;

theorem Th79: :: CLASSES2:79

for b₁ being Universe holds
( FinSETS c= b₁ & Tarski-Class {} c= b₁ & UNIVERSE {} c= b₁ )

proof end;

theorem Th80: :: CLASSES2:80

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

proof end;

theorem Th81: :: CLASSES2:81

for b₁, b₂ being Ordinal st UNIVERSE b₁ = UNIVERSE b₂ holds
b₁ = b₂

proof end;

theorem Th82: :: CLASSES2:82

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

proof end;