:: CLASSES2 semantic presentation

Lm1: for X being set holds Tarski-Class X is_Tarski-Class

proof end;

registration

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

end;

registration

let X be set ;
cluster Tarski-Class X -> subset-closed being_Tarski-Class ;
coherence by Lm1;

end;

theorem Th1: :: CLASSES2:1

for W, X being set st W is subset-closed & X in W holds
( not X,W are_equipotent & Card X <` Card W )

proof end;

theorem :: CLASSES2:2

canceled;

theorem Th3: :: CLASSES2:3

for W, x, y being set st W is_Tarski-Class & x in W & y in W holds
( {x} in W & {x,y} in W )

proof end;

theorem Th4: :: CLASSES2:4

for W, x, y being set st W is_Tarski-Class & x in W & y in W holds
[x,y] in W

proof end;

theorem Th5: :: CLASSES2:5

for W, X being set st W is_Tarski-Class & X in W holds
Tarski-Class X c= W

proof end;

theorem Th6: :: CLASSES2:6

for A being Ordinal
for W being set st W is_Tarski-Class & A in W holds
( succ A in W & A c= W )

proof end;

theorem :: CLASSES2:7

for A being Ordinal
for W being set st A in Tarski-Class W holds
( succ A in Tarski-Class W & A c= Tarski-Class W ) by Th6;

theorem Th8: :: CLASSES2:8

for W, X being set st W is subset-closed & X is epsilon-transitive & X in W holds
X c= W

proof end;

theorem :: CLASSES2:9

for X, W being set st X is epsilon-transitive & X in Tarski-Class W holds
X c= Tarski-Class W by Th8;

theorem Th10: :: CLASSES2:10

for W being set st W is_Tarski-Class holds
On W = Card W

proof end;

theorem :: CLASSES2:11

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

theorem Th12: :: CLASSES2:12

for W, X being set st W is_Tarski-Class & X in W holds
Card X in W

proof end;

theorem :: CLASSES2:13

for X, W being set st X in Tarski-Class W holds
Card X in Tarski-Class W by Th12;

theorem Th14: :: CLASSES2:14

for W, x being set st W is_Tarski-Class & x in Card W holds
x in W

proof end;

theorem :: CLASSES2:15

for x, W being set st x in Card (Tarski-Class W) holds
x in Tarski-Class W by Th14;

theorem :: CLASSES2:16

for m being Cardinal
for W being set st W is_Tarski-Class & m <` Card W holds
m in W

proof end;

theorem :: CLASSES2:17

for m being Cardinal
for W being set st m <` Card (Tarski-Class W) holds
m in Tarski-Class W

proof end;

theorem :: CLASSES2:18

for m being Cardinal
for W being set st W is_Tarski-Class & m in W holds
m c= W by Th6;

theorem :: CLASSES2:19

for m being Cardinal
for W being set st m in Tarski-Class W holds
m c= Tarski-Class W by Th6;

theorem Th20: :: CLASSES2:20

for W being set st W is_Tarski-Class holds
Card W is_limit_ordinal

proof end;

theorem Th21: :: CLASSES2:21

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

proof end;

theorem Th22: :: CLASSES2:22

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

proof end;

theorem Th23: :: CLASSES2:23

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

proof end;

theorem :: CLASSES2:24

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

proof end;

theorem Th25: :: CLASSES2:25

for L being T-Sequence st dom L is_limit_ordinal & ( for A being Ordinal st A in dom L holds
L . A = Rank A ) holds
Rank (dom L) = Union L

proof end;

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

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

Lm3: for A being Ordinal st S₁[A] holds
S₁[ succ A]

proof end;

Lm4: for A being Ordinal st A <> {} & A is_limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) holds
S₁[A]

proof end;

theorem Th26: :: CLASSES2:26

for A being Ordinal
for W being set st W is_Tarski-Class & A in On W holds
( Card (Rank A) <` Card W & Rank A in W )

proof end;

theorem :: CLASSES2:27

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

theorem Th28: :: CLASSES2:28

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

proof end;

theorem Th29: :: CLASSES2:29

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

proof end;

deffunc H₁( set ) -> set = the_rank_of $1;

deffunc H₂( set ) -> set = Card (bool $1);

theorem Th30: :: CLASSES2:30

for W, X being set st W is_Tarski-Class & W is epsilon-transitive & X in W holds
the_rank_of X in W

proof end;

theorem Th31: :: CLASSES2:31

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

proof end;

theorem Th32: :: CLASSES2:32

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

proof end;

theorem :: CLASSES2:33

for A being Ordinal
for W being set st W is_Tarski-Class & A in On W holds
Card (Rank A) <=` Card W

proof end;

theorem :: CLASSES2:34

for A being Ordinal
for W being set st A in On (Tarski-Class W) holds
Card (Rank A) <=` Card (Tarski-Class W)

proof end;

theorem Th35: :: CLASSES2:35

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

proof end;

theorem :: CLASSES2:36

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

theorem Th37: :: CLASSES2:37

for W, X being set st W is_Tarski-Class & X c= Rank (Card W) & not X, Rank (Card W) are_equipotent holds
X in Rank (Card W)

proof end;

theorem :: CLASSES2:38

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

theorem Th39: :: CLASSES2:39

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

proof end;

theorem :: CLASSES2:40

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

theorem Th41: :: CLASSES2:41

for A being Ordinal
for X being set st X is epsilon-transitive & A in the_rank_of X holds
ex Y being set st
( Y in X & the_rank_of Y = A )

proof end;

theorem Th42: :: CLASSES2:42

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

proof end;

theorem Th43: :: CLASSES2:43

for W, X being set st W is_Tarski-Class & X is epsilon-transitive & X in W holds
X in Rank (Card W)

proof end;

theorem :: CLASSES2:44

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

theorem Th45: :: CLASSES2:45

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

proof end;

theorem :: CLASSES2:46

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

proof end;

definition

let IT be set ;
attr IT is universal means :Def1: :: CLASSES2:def 1
( IT is epsilon-transitive & IT 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 :: CLASSES2:47

canceled;

theorem :: CLASSES2:48

canceled;

theorem :: CLASSES2:49

canceled;

theorem Th50: :: CLASSES2:50

for U being Universe holds On U is Ordinal

proof end;

theorem Th51: :: CLASSES2:51

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

proof end;

theorem :: CLASSES2:52

for U being Universe holds Tarski-Class U is Universe by Th51;

registration

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

end;

theorem Th53: :: CLASSES2:53

for A being Ordinal holds Tarski-Class A is universal

proof end;

registration

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

end;

theorem Th54: :: CLASSES2:54

for U being Universe holds U = Rank (On U)

proof end;

theorem Th55: :: CLASSES2:55

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

proof end;

theorem :: CLASSES2:56

for U1, U2 being Universe holds
( U1 in U2 or U1 = U2 or U2 in U1 )

proof end;

theorem Th57: :: CLASSES2:57

for U1, U2 being Universe holds
( U1 c= U2 or U2 in U1 )

proof end;

theorem Th58: :: CLASSES2:58

for U1, U2 being Universe holds U1,U2 are_c=-comparable

proof end;

theorem Th59: :: CLASSES2:59

for U1, U2, U3 being Universe st U1 in U2 & U2 in U3 holds
U1 in U3

proof end;

theorem :: CLASSES2:60

canceled;

theorem :: CLASSES2:61

for U1, U2 being Universe holds
( U1 \/ U2 is Universe & U1 /\ U2 is Universe )

proof end;

theorem Th62: :: CLASSES2:62

for U being Universe holds {} in U

proof end;

theorem :: CLASSES2:63

for x being set
for U being Universe st x in U holds
{x} in U by Th3;

theorem :: CLASSES2:64

for x, y being set
for U being Universe st x in U & y in U holds
( {x,y} in U & [x,y] in U ) by Th3, Th4;

theorem Th65: :: CLASSES2:65

for X being set
for U being Universe st X in U holds
( bool X in U & union X in U & meet X in U )

proof end;

theorem Th66: :: CLASSES2:66

for X, Y being set
for U being Universe st X in U & Y in U holds
( X \/ Y in U & X /\ Y in U & X \ Y in U & X \+\ Y in U )

proof end;

theorem Th67: :: CLASSES2:67

for X, Y being set
for U being Universe st X in U & Y in U holds
( [:X,Y:] in U & Funcs X,Y in U )

proof end;

registration

let U1 be Universe;
cluster non empty Element of U1;
existence

proof end;

end;

definition

let U be Universe;
let u be Element of U;
:: original: {
redefine func {u} -> Element of U;
coherence by Th3;
:: original: bool
redefine func bool u -> non empty Element of U;
coherence by Th65;
:: original: union
redefine func union u -> Element of U;
coherence by Th65;
:: original: meet
redefine func meet u -> Element of U;
coherence by Th65;
let v be Element of U;
:: original: {
redefine func {u,v} -> Element of U;
coherence by Th3;
:: original: [
redefine func [u,v] -> Element of U;
coherence by Th4;
:: original: \/
redefine func u \/ v -> Element of U;
coherence by Th66;
:: original: /\
redefine func u /\ v -> Element of U;
coherence by Th66;
:: original: \
redefine func u \ v -> Element of U;
coherence by Th66;
:: original: \+\
redefine func u \+\ v -> Element of U;
coherence by Th66;
:: original: [:
redefine func [:u,v:] -> Element of U;
coherence by Th67;
:: original: Funcs
redefine func Funcs u,v -> Element of U;
coherence by Th67;

end;

definition

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

end;

:: deftheorem defines FinSETS CLASSES2:def 2 :

theorem :: 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 :: CLASSES2:71

FinSETS = Rank omega

proof end;

definition

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

end;

:: deftheorem defines SETS CLASSES2:def 3 :

registration

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

end;

registration

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

end;

registration

let A be Ordinal;
cluster Rank A -> epsilon-transitive ;
coherence by CLASSES1:37;

end;

definition

let X be set ;
func Universe_closure X -> Universe means :Def4: :: CLASSES2:def 4
( X c= it & ( for Y being Universe st X c= Y holds
it c= Y ) );
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def4 defines Universe_closure CLASSES2:def 4 :

deffunc H₃( Ordinal, set ) -> set = Tarski-Class $2;

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

definition

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

proof end;

end;

:: deftheorem Def5 defines UNIVERSE CLASSES2:def 5 :

deffunc H₅( Ordinal) -> set = UNIVERSE $1;

Lm5: now

A1: for A being Ordinal
for x being set holds
( x = H₅(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = FinSETS & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = H₃(C,L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is_limit_ordinal holds
L . C = H₄(C,L | C) ) ) ) by Def5;
thus H₅( {} ) = FinSETS from ORDINAL2:sch 8( FinSETS , A1); :: thesis:
thus for A being Ordinal holds H₅( succ A) = H₃(A,H₅(A)) from ORDINAL2:sch 9( FinSETS , A1); :: thesis:
let A be Ordinal; :: thesis:
let L be T-Sequence; :: thesis:
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 = H₅(B) ; :: thesis:
thus H₅(A) = H₄(A,L) from ORDINAL2:sch 10( B A FinSETS , A1, A2, A3, A4); :: thesis:

end;

registration