:: Universal Classes
:: by Bogdan Nowak and Grzegorz Bancerek
::
:: Received April 10, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users

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

proof end;

registration

cluster Tarski -> subset-closed for set ;

coherence
for b₁ being set st b₁ is Tarski holds
b₁ is subset-closed ;

end;

registration

let X be set ;

cluster Tarski-Class X -> Tarski ;

coherence
Tarski-Class X is Tarski by Lm1;

end;

theorem Th1: :: CLASSES2:1

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

proof end;

theorem Th2: :: CLASSES2:2

for x, y, W being set st W is Tarski & x in W & y in W holds
( {x} in W & {x,y} in W )

proof end;

theorem Th3: :: CLASSES2:3

for x, y, W being set st W is Tarski & x in W & y in W holds
[x,y] in W

proof end;

theorem Th4: :: CLASSES2:4

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

proof end;

theorem Th5: :: CLASSES2:5

for A being Ordinal
for W being set st W is Tarski & A in W holds
( succ A in W & A c= W )

proof end;

theorem :: CLASSES2:6

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

theorem Th7: :: CLASSES2:7

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

theorem :: CLASSES2:8

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

theorem Th9: :: CLASSES2:9

for W being set st W is Tarski holds
On W = card W

proof end;

theorem :: CLASSES2:10

for W being set holds On (Tarski-Class W) = card (Tarski-Class W) by Th9;

theorem Th11: :: CLASSES2:11

for X, W being set st W is Tarski & X in W holds
card X in W

proof end;

theorem :: CLASSES2:12

for X, W being set st X in Tarski-Class W holds
card X in Tarski-Class W by Th11;

theorem Th13: :: CLASSES2:13

for x, W being set st W is Tarski & x in card W holds
x in W

proof end;

theorem :: CLASSES2:14

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

theorem :: CLASSES2:15

for m being Cardinal
for W being set st W is Tarski & m in card W holds
m in W

proof end;

theorem :: CLASSES2:16

for m being Cardinal
for W being set st m in card (Tarski-Class W) holds
m in Tarski-Class W

proof end;

theorem :: CLASSES2:17

for m being Cardinal
for W being set st W is Tarski & m in W holds
m c= W by Th5;

theorem :: CLASSES2:18

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

theorem Th19: :: CLASSES2:19

for W being set st W is Tarski holds
card W is limit_ordinal

proof end;

theorem :: CLASSES2:20

for W being set st W is Tarski & W <> {} holds
( card W <> 0 & card W <> {} & card W is limit_ordinal ) by Th19;

theorem Th21: :: CLASSES2:21

for W being set holds
( card (Tarski-Class W) <> 0 & card (Tarski-Class W) <> {} & card (Tarski-Class W) is limit_ordinal )

proof end;

theorem Th22: :: CLASSES2:22

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

proof end;

theorem :: CLASSES2:23

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 in card (Tarski-Class W) & X c= Tarski-Class W ) ) holds
Funcs (X,(Tarski-Class W)) c= Tarski-Class W

proof end;

theorem Th24: :: CLASSES2:24

for L being 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 & $1 in On W holds
( card (Rank $1) in card W & Rank $1 in W );

Lm2: S₁[ 0 ]
by Th9, CLASSES1:29, ORDINAL1:def 9;

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

proof end;

Lm4: for A being Ordinal st A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) holds
S₁[A]

proof end;

theorem Th25: :: CLASSES2:25

for A being Ordinal
for W being set st W is Tarski & A in On W holds
( card (Rank A) in card W & Rank A in W )

proof end;

theorem :: CLASSES2:26

for A being Ordinal
for W being set st A in On (Tarski-Class W) holds
( card (Rank A) in card (Tarski-Class W) & Rank A in Tarski-Class W ) by Th25;

theorem Th27: :: CLASSES2:27

for W being set st W is Tarski holds
Rank (card W) c= W

proof end;

theorem Th28: :: CLASSES2:28

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

proof end;

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

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

theorem Th29: :: CLASSES2:29

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

proof end;

theorem Th30: :: CLASSES2:30

for W being set st W is Tarski & W is epsilon-transitive holds
W c= Rank (card W)

proof end;

theorem Th31: :: CLASSES2:31

for W being set st W is Tarski & W is epsilon-transitive holds
Rank (card W) = W by Th27, Th30;

theorem :: CLASSES2:32

for A being Ordinal
for W being set st W is Tarski & A in On W holds
card (Rank A) c= card W

proof end;

theorem :: CLASSES2:33

for A being Ordinal
for W being set st A in On (Tarski-Class W) holds
card (Rank A) c= card (Tarski-Class W)

proof end;

theorem Th34: :: CLASSES2:34

for W being set st W is Tarski holds
card W = card (Rank (card W))

proof end;

theorem :: CLASSES2:35

for W being set holds card (Tarski-Class W) = card (Rank (card (Tarski-Class W))) by Th34;

theorem Th36: :: CLASSES2:36

for X, W being set st W is Tarski & X c= Rank (card W) & not X, Rank (card W) are_equipotent holds
X in Rank (card W)

proof end;

theorem :: CLASSES2:37

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

theorem Th38: :: CLASSES2:38

for W being set st W is Tarski holds
Rank (card W) is Tarski

proof end;

theorem :: CLASSES2:39

for W being set holds Rank (card (Tarski-Class W)) is Tarski by Th38;

theorem Th40: :: CLASSES2:40

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 Th41: :: CLASSES2:41

for X being set st X is epsilon-transitive holds
card (the_rank_of X) c= card X

proof end;

theorem Th42: :: CLASSES2:42

for X, W being set st W is Tarski & X is epsilon-transitive & X in W holds
X in Rank (card W)

proof end;

theorem :: CLASSES2:43

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

theorem Th44: :: CLASSES2:44

for W being set st W is epsilon-transitive holds
Rank (card (Tarski-Class W)) is_Tarski-Class_of W by CLASSES1:2, Th38, Th42;

theorem :: CLASSES2:45

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 :: CLASSES2:def 1
( IT is epsilon-transitive & IT is Tarski );

end;

:: deftheorem defines universal CLASSES2:def 1 :
for IT being set holds
( IT is universal iff ( IT is epsilon-transitive & IT is Tarski ) );

registration

cluster universal -> epsilon-transitive Tarski for set ;

coherence
for b₁ being set st b₁ is universal holds
( b₁ is epsilon-transitive & b₁ is Tarski ) ;

cluster epsilon-transitive Tarski -> universal for set ;

coherence
for b₁ being set st b₁ is epsilon-transitive & b₁ is Tarski holds
b₁ is universal ;

end;

registration

cluster non empty universal for set ;

existence
ex b₁ being set st
( b₁ is universal & not b₁ is empty )

proof end;

end;

definition

mode Universe is non empty universal set ;

end;

theorem Th46: :: CLASSES2:46

for U being Universe holds On U is Ordinal

proof end;

theorem Th47: :: CLASSES2:47

for X being set st X is epsilon-transitive holds
Tarski-Class X is universal by CLASSES1:23;

theorem :: CLASSES2:48

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

registration

let U be Universe;

cluster On U -> ordinal ;

coherence
On U is ordinal by Th46;

cluster Tarski-Class U -> universal ;

coherence
Tarski-Class U is universal by Th47;

end;

theorem Th49: :: CLASSES2:49

for A being Ordinal holds Tarski-Class A is universal by CLASSES1:23;

registration

let A be Ordinal;

cluster Tarski-Class A -> universal ;

coherence
Tarski-Class A is universal by Th49;

end;

theorem Th50: :: CLASSES2:50

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

proof end;

theorem Th51: :: CLASSES2:51

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

proof end;

theorem :: CLASSES2:52

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

proof end;

theorem Th53: :: CLASSES2:53

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

proof end;

theorem Th54: :: CLASSES2:54

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

proof end;

theorem :: CLASSES2:55

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

proof end;

theorem Th56: :: CLASSES2:56

for U being Universe holds {} in U

proof end;

theorem :: CLASSES2:57

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

theorem :: CLASSES2:58

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 Th2, Th3;

theorem Th59: :: CLASSES2:59

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 Th60: :: CLASSES2:60

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 Th61: :: CLASSES2:61

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 for Element of U1;

existence
not for b₁ being Element of U1 holds b₁ is empty

proof end;

end;

definition

let U be Universe;
let u be Element of U;
:: original: {
redefine func {u} -> Element of U;
coherence
{u} is Element of U by Th2;
:: original: bool
redefine func bool u -> Element of U;
coherence
bool u is Element of U by Th59;
:: original: union
redefine func union u -> Element of U;
coherence
union u is Element of U by Th59;
:: original: meet
redefine func meet u -> Element of U;
coherence
meet u is Element of U by Th59;
let v be Element of U;
:: original: {
redefine func {u,v} -> Element of U;
coherence
{u,v} is Element of U by Th2;
:: original: [
redefine func [u,v] -> Element of U;
coherence
[u,v] is Element of U by Th3;
:: original: \/
redefine func u \/ v -> Element of U;
coherence
u \/ v is Element of U by Th60;
:: original: /\
redefine func u /\ v -> Element of U;
coherence
u /\ v is Element of U by Th60;
:: original: \
redefine func u \ v -> Element of U;
coherence
u \ v is Element of U by Th60;
:: original: \+\
redefine func u \+\ v -> Element of U;
coherence
u \+\ v is Element of U by Th60;
:: original: [:
redefine func [:u,v:] -> Element of U;
coherence
[:u,v:] is Element of U by Th61;
:: original: Funcs
redefine func Funcs (u,v) -> Element of U;
coherence
Funcs (u,v) is Element of U by Th61;

end;

definition

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

correctness
coherence
Tarski-Class {} is Universe;
;

end;

:: deftheorem defines FinSETS CLASSES2:def 2 :
FinSETS = Tarski-Class {};

Lm5: omega is limit_ordinal
by ORDINAL1:def 11;

theorem Th62: :: CLASSES2:62

card (Rank omega) = card omega

proof end;

theorem Th63: :: CLASSES2:63

Rank omega is Tarski

proof end;

theorem :: CLASSES2:64

FinSETS = Rank omega

proof end;

definition

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

correctness
coherence
Tarski-Class FinSETS is Universe;
;

end;

:: deftheorem defines SETS CLASSES2:def 3 :
SETS = Tarski-Class FinSETS;

registration

let X be set ;

cluster the_transitive-closure_of X -> epsilon-transitive ;

coherence
the_transitive-closure_of X is epsilon-transitive ;

end;

registration

let X be epsilon-transitive set ;

cluster Tarski-Class X -> epsilon-transitive ;

coherence
Tarski-Class X is epsilon-transitive by CLASSES1:23;

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
for b₁, b₂ being Universe st X c= b₁ & ( for Y being Universe st X c= Y holds
b₁ c= Y ) & X c= b₂ & ( for Y being Universe st X c= Y holds
b₂ c= Y ) holds
b₁ = b₂ ;
existence
ex b₁ being Universe st
( X c= b₁ & ( for Y being Universe st X c= Y holds
b₁ c= Y ) )

proof end;

end;

:: deftheorem Def4 defines Universe_closure CLASSES2:def 4 :
for X being set
for b₂ being Universe holds
( b₂ = Universe_closure X iff ( X c= b₂ & ( for Y being Universe st X c= Y holds
b₂ c= Y ) ) );

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

deffunc H₄( Ordinal, 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 Sequence st
( it = last L & dom L = succ A & L . 0 = 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 <> 0 & C is limit_ordinal holds
L . C = Universe_closure (Union (L | C)) ) );

correctness
existence
ex b₁ being set ex L being Sequence st
( b₁ = last L & dom L = succ A & L . 0 = 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 <> 0 & C is limit_ordinal holds
L . C = Universe_closure (Union (L | C)) ) );
uniqueness
for b₁, b₂ being set st ex L being Sequence st
( b₁ = last L & dom L = succ A & L . 0 = 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 <> 0 & C is limit_ordinal holds
L . C = Universe_closure (Union (L | C)) ) ) & ex L being Sequence st
( b₂ = last L & dom L = succ A & L . 0 = 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 <> 0 & C is limit_ordinal holds
L . C = Universe_closure (Union (L | C)) ) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def5 defines UNIVERSE CLASSES2:def 5 :
for A being Ordinal
for b₂ being set holds
( b₂ = UNIVERSE A iff ex L being Sequence st
( b₂ = last L & dom L = succ A & L . 0 = 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 <> 0 & C is limit_ordinal holds
L . C = Universe_closure (Union (L | C)) ) ) );

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

Lm6: now :: thesis: ( H₅( 0 ) = FinSETS & ( for A being Ordinal holds H₅( succ A) = H₃(A,H₅(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 = H₅(B) ) holds
H₅(A) = H₄(A,L) ) )

A1: for A being Ordinal
for x being object holds
( x = H₅(A) iff ex L being Sequence st
( x = last L & dom L = succ A & L . 0 = 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 <> 0 & C is limit_ordinal holds
L . C = H₄(C,L | C) ) ) ) by Def5;
thus H₅( 0 ) = FinSETS from ORDINAL2:sch 8(A1); :: thesis: ( ( for A being Ordinal holds H₅( succ A) = H₃(A,H₅(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 = H₅(B) ) holds
H₅(A) = H₄(A,L) ) )
thus for A being Ordinal holds H₅( succ A) = H₃(A,H₅(A)) from ORDINAL2:sch 9(A1); :: 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 = H₅(B) ) holds
H₅(A) = H₄(A,L)
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 = H₅(B) ) holds
H₅(A) = H₄(A,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 = H₅(B) ) implies H₅(A) = H₄(A,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 = H₅(B) ; :: thesis: H₅(A) = H₄(A,L)
thus H₅(A) = H₄(A,L) from ORDINAL2:sch 10(A1, A2, A3, A4); :: thesis: verum

end;

registration

let A be Ordinal;

cluster UNIVERSE A -> non empty universal ;

coherence
( UNIVERSE A is universal & not UNIVERSE A is empty )

proof end;

end;

theorem :: CLASSES2:65

UNIVERSE {} = FinSETS by Lm6;

theorem :: CLASSES2:66

for A being Ordinal holds UNIVERSE (succ A) = Tarski-Class (UNIVERSE A) by Lm6;

Lm7: 1 = succ 0
;

theorem :: CLASSES2:67

UNIVERSE 1 = SETS by Lm6, Lm7;

theorem :: CLASSES2:68

for A being Ordinal
for L being Sequence st A <> {} & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = UNIVERSE B ) holds
UNIVERSE A = Universe_closure (Union L) by Lm6;

theorem :: CLASSES2:69

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

proof end;

theorem Th70: :: CLASSES2:70

for A, B being Ordinal holds
( A in B iff UNIVERSE A in UNIVERSE B )

proof end;

theorem :: CLASSES2:71

for A, B being Ordinal st UNIVERSE A = UNIVERSE B holds
A = B

proof end;

theorem :: CLASSES2:72

for A, B being Ordinal holds
( A c= B iff UNIVERSE A c= UNIVERSE B )

proof end;

theorem :: CLASSES2:73

for X being set holds
( Tarski-Class (X,{}) in Tarski-Class (X,1) & Tarski-Class (X,{}) <> Tarski-Class (X,1) )

proof end;