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


begin

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

registration
cluster Tarski  ->  subset-closed for set ;
coherence
 for b1 being set st b1 is Tarski holds
b1 is subset-closed by CLASSES1:def_2;
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 W, X being set st W is subset-closed & X in W holds
( not X,W are_equipotent & card X in card W )
proofend;

theorem Th2: :: CLASSES2:2
for W, x, y being set st W is Tarski & x in W & y in W holds
( {x} in W & {x,y} in W )
proofend;

theorem Th3: :: CLASSES2:3
for W, x, y being set st W is Tarski & x in W & y in W holds
[x,y] in W
proofend;

theorem Th4: :: CLASSES2:4
for W, X being set st W is Tarski & X in W holds
Tarski-Class X c= W
proofend;

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 )
proofend;

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 W, X being set st W is subset-closed & X is epsilon-transitive & X in W holds
X c= W
proofend;

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

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

theorem Th11: :: CLASSES2:11
for W, X being set st W is Tarski & X in W holds
card X in W
proofend;

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 W, x being set st W is Tarski & x in card W holds
x in W
proofend;

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

theorem :: CLASSES2:16
for m being Cardinal
for W being set st m in card (Tarski-Class W) holds
m in Tarski-Class W
proofend;

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

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

theorem Th21: :: CLASSES2:21
for W being set holds
( card (Tarski-Class W) <> 0 &amp; card (Tarski-Class W) <> {} &amp; card (Tarski-Class W) is limit_ordinal )
proofend;

theorem Th22: :: CLASSES2:22
for W, X being set st W is Tarski &amp; ( ( X in W &amp; W is epsilon-transitive ) or ( X in W &amp; X c= W ) or ( card X in card W &amp; X c= W ) ) holds
Funcs (X,W) c= W
proofend;

theorem :: CLASSES2:23
for X, W being set st ( ( X in Tarski-Class W &amp; W is epsilon-transitive ) or ( X in Tarski-Class W &amp; X c= Tarski-Class W ) or ( card X in card (Tarski-Class W) &amp; X c= Tarski-Class W ) ) holds
Funcs (X,(Tarski-Class W)) c= Tarski-Class W
proofend;

theorem Th24: :: CLASSES2:24
for L being T-Sequence st dom L is limit_ordinal &amp; ( for A being Ordinal st A in dom L holds
L . A = Rank A ) holds
Rank (dom L) = Union L
proofend;

defpred S1[ Ordinal] means  for W being set st W is Tarski &amp; $1 in On W holds
( card (Rank $1) in card W &amp; Rank $1 in W );

Lm2:  S1[ {} ]
by Th9, CARD_1:27, CLASSES1:29, ORDINAL1:def_9;

Lm3:  for A being Ordinal st S1[A] holds
S1[ succ A]
proofend;

Lm4:  for A being Ordinal st A <> {} &amp; A is limit_ordinal &amp; ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proofend;

theorem Th25: :: CLASSES2:25
for A being Ordinal
for W being set st W is Tarski &amp; A in On W holds
( card (Rank A) in card W &amp; Rank A in W )
proofend;

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) &amp; 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
proofend;

theorem Th28: :: CLASSES2:28
for W being set holds Rank (card (Tarski-Class W)) c= Tarski-Class W
proofend;

deffunc H1( set ) ->  set = the_rank_of $1;

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

theorem Th29: :: CLASSES2:29
for W, X being set st W is Tarski &amp; W is epsilon-transitive &amp; X in W holds
the_rank_of X in W
proofend;

theorem Th30: :: CLASSES2:30
for W being set st W is Tarski &amp; W is epsilon-transitive holds
W c= Rank (card W)
proofend;

theorem Th31: :: CLASSES2:31
for W being set st W is Tarski &amp; W is epsilon-transitive holds
Rank (card W) = W
proofend;

theorem :: CLASSES2:32
for A being Ordinal
for W being set st W is Tarski &amp; A in On W holds
card (Rank A) c= card W
proofend;

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)
proofend;

theorem Th34: :: CLASSES2:34
for W being set st W is Tarski holds
card W = card (Rank (card W))
proofend;

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 W, X being set st W is Tarski &amp; X c= Rank (card W) &amp; not X, Rank (card W) are_equipotent holds
X in Rank (card W)
proofend;

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

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 &amp; A in the_rank_of X holds
ex Y being set st
( Y in X &amp; the_rank_of Y = A )
proofend;

theorem Th41: :: CLASSES2:41
for X being set st X is epsilon-transitive holds
card (the_rank_of X) c= card X
proofend;

theorem Th42: :: CLASSES2:42
for W, X being set st W is Tarski &amp; X is epsilon-transitive &amp; X in W holds
X in Rank (card W)
proofend;

theorem :: CLASSES2:43
for X, W being set st X is epsilon-transitive &amp; 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
proofend;

theorem :: CLASSES2:45
for W being set st W is epsilon-transitive holds
Rank (card (Tarski-Class W)) = Tarski-Class W
proofend;

definition
let IT be set ;
attrIT is universal  means :Def1: :: CLASSES2:def 1
( IT is epsilon-transitive &amp; IT is Tarski );
end;

:: deftheorem Def1 defines universal CLASSES2:def_1_:_
 for IT being set holds
( IT is universal iff ( IT is epsilon-transitive &amp; IT is Tarski ) );

registration
cluster universal  ->  epsilon-transitive Tarski for set ;
coherence
 for b1 being set st b1 is universal holds
( b1 is epsilon-transitive &amp; b1 is Tarski ) by Def1;
cluster epsilon-transitive Tarski  ->  universal for set ;
coherence
 for b1 being set st b1 is epsilon-transitive &amp; b1 is Tarski holds
b1 is universal by Def1;
end;

registration
cluster non empty universal for set ;
existence
 ex b1 being set st
( b1 is universal &amp; not b1 is empty )
proofend;
end;

definition
mode Universe is non empty universal set ;
end;

theorem Th46: :: CLASSES2:46
for U being Universe holds On U is Ordinal
proofend;

theorem Th47: :: CLASSES2:47
for X being set st X is epsilon-transitive holds
Tarski-Class X is universal
proofend;

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

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)
proofend;

theorem Th51: :: CLASSES2:51
for U being Universe holds
( On U <> {} &amp; On U is limit_ordinal )
proofend;

theorem :: CLASSES2:52
for U1, U2 being Universe holds
( U1 in U2 or U1 = U2 or U2 in U1 )
proofend;

theorem Th53: :: CLASSES2:53
for U1, U2 being Universe holds
( U1 c= U2 or U2 in U1 )
proofend;

theorem Th54: :: CLASSES2:54
for U1, U2 being Universe holds U1,U2 are_c=-comparable
proofend;

theorem :: CLASSES2:55
for U1, U2 being Universe holds
( U1 \/ U2 is Universe &amp; U1 /\ U2 is Universe )
proofend;

theorem Th56: :: CLASSES2:56
for U being Universe holds {} in U
proofend;

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 &amp; y in U holds
( {x,y} in U &amp; [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 &amp; union X in U &amp; meet X in U )
proofend;

theorem Th60: :: CLASSES2:60
for X, Y being set
for U being Universe st X in U &amp; Y in U holds
( X \/ Y in U &amp; X /\ Y in U &amp; X \ Y in U &amp; X \+\ Y in U )
proofend;

theorem Th61: :: CLASSES2:61
for X, Y being set
for U being Universe st X in U &amp; Y in U holds
( [:X,Y:] in U &amp; Funcs (X,Y) in U )
proofend;

registration
let U1 be Universe;
cluster non empty for Element of U1;
existence
 not for b1 being Element of U1 holds b1 is empty
proofend;
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 funcu \/ v ->  Element of U;
coherence
 u \/ v is Element of U by Th60;
:: original:/\
redefine funcu /\ v ->  Element of U;
coherence
 u /\ v is Element of U by Th60;
:: original:\
redefine funcu \ v ->  Element of U;
coherence
 u \ v is Element of U by Th60;
:: original:\+\
redefine funcu \+\ 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
proofend;

theorem Th63: :: CLASSES2:63
Rank omega is Tarski
proofend;

theorem :: CLASSES2:64
FinSETS = Rank omega
proofend;

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 by CLASSES1:51;
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 &amp; ( for Y being Universe st X c= Y holds
it c= Y ) );
uniqueness
 for b1, b2 being Universe st X c= b1 &amp; ( for Y being Universe st X c= Y holds
b1 c= Y ) &amp; X c= b2 &amp; ( for Y being Universe st X c= Y holds
b2 c= Y ) holds
b1 = b2
proofend;
existence
 ex b1 being Universe st
( X c= b1 &amp; ( for Y being Universe st X c= Y holds
b1 c= Y ) )
proofend;
end;

:: deftheorem Def4 defines Universe_closure CLASSES2:def_4_:_
 for X being set
for b2 being Universe holds
( b2 = Universe_closure X iff ( X c= b2 &amp; ( for Y being Universe st X c= Y holds
b2 c= Y ) ) );

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

deffunc H4( 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 &amp; dom L = succ A &amp; L . {} = FinSETS &amp; ( for C being Ordinal st succ C in succ A holds
L . (succ C) = Tarski-Class (L . C) ) &amp; ( for C being Ordinal st C in succ A &amp; C <> {} &amp; C is limit_ordinal holds
L . C = Universe_closure (Union (L | C)) ) );
correctness
existence
ex b1 being set ex L being T-Sequence st
( b1 = last L &amp; dom L = succ A &amp; L . {} = FinSETS &amp; ( for C being Ordinal st succ C in succ A holds
L . (succ C) = Tarski-Class (L . C) ) &amp; ( for C being Ordinal st C in succ A &amp; C <> {} &amp; C is limit_ordinal holds
L . C = Universe_closure (Union (L | C)) ) );
uniqueness
for b1, b2 being set st ex L being T-Sequence st
( b1 = last L &amp; dom L = succ A &amp; L . {} = FinSETS &amp; ( for C being Ordinal st succ C in succ A holds
L . (succ C) = Tarski-Class (L . C) ) &amp; ( for C being Ordinal st C in succ A &amp; C <> {} &amp; C is limit_ordinal holds
L . C = Universe_closure (Union (L | C)) ) ) &amp; ex L being T-Sequence st
( b2 = last L &amp; dom L = succ A &amp; L . {} = FinSETS &amp; ( for C being Ordinal st succ C in succ A holds
L . (succ C) = Tarski-Class (L . C) ) &amp; ( for C being Ordinal st C in succ A &amp; C <> {} &amp; C is limit_ordinal holds
L . C = Universe_closure (Union (L | C)) ) ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def5 defines UNIVERSE CLASSES2:def_5_:_
 for A being Ordinal
for b2 being set holds
( b2 = UNIVERSE A iff ex L being T-Sequence st
( b2 = last L &amp; dom L = succ A &amp; L . {} = FinSETS &amp; ( for C being Ordinal st succ C in succ A holds
L . (succ C) = Tarski-Class (L . C) ) &amp; ( for C being Ordinal st C in succ A &amp; C <> {} &amp; C is limit_ordinal holds
L . C = Universe_closure (Union (L | C)) ) ) );

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

Lm6: now__::_thesis:_(_H5(_{}_)_=_FinSETS_&amp;_(_for_A_being_Ordinal_holds_H5(_succ_A)_=_H3(A,H5(A))_)_&amp;_(_for_A_being_Ordinal
for_L_being_T-Sequence_st_A_<>_{}_&amp;_A_is_limit_ordinal_&amp;_dom_L_=_A_&amp;_(_for_B_being_Ordinal_st_B_in_A_holds_
L_._B_=_H5(B)_)_holds_
H5(A)_=_H4(A,L)_)_)
A1: for A being Ordinal
for x being set holds
( x = H5(A) iff ex L being T-Sequence st
( x = last L &amp; dom L = succ A &amp; L . {} = FinSETS &amp; ( for C being Ordinal st succ C in succ A holds
L . (succ C) = H3(C,L . C) ) &amp; ( for C being Ordinal st C in succ A &amp; C <> {} &amp; C is limit_ordinal holds
L . C = H4(C,L | C) ) ) ) by Def5;
thus  H5( {} ) = FinSETS from ORDINAL2:sch_8(A1); ::_thesis: ( ( for A being Ordinal holds H5( succ A) = H3(A,H5(A)) ) &amp; ( for A being Ordinal
for L being T-Sequence st A <> {} &amp; A is limit_ordinal &amp; dom L = A &amp; ( for B being Ordinal st B in A holds
L . B = H5(B) ) holds
H5(A) = H4(A,L) ) )
thus  for A being Ordinal holds H5( succ A) = H3(A,H5(A)) from ORDINAL2:sch_9(A1); ::_thesis: for A being Ordinal
for L being T-Sequence st A <> {} &amp; A is limit_ordinal &amp; dom L = A &amp; ( for B being Ordinal st B in A holds
L . B = H5(B) ) holds
H5(A) = H4(A,L)
let A be Ordinal; ::_thesis: for L being T-Sequence st A <> {} &amp; A is limit_ordinal &amp; dom L = A &amp; ( for B being Ordinal st B in A holds
L . B = H5(B) ) holds
H5(A) = H4(A,L)
let L be T-Sequence; ::_thesis: ( A <> {} &amp; A is limit_ordinal &amp; dom L = A &amp; ( for B being Ordinal st B in A holds
L . B = H5(B) ) implies H5(A) = H4(A,L) )
assume that
A2: ( A <> {} &amp; A is limit_ordinal ) and
A3: dom L = A and
A4: for B being Ordinal st B in A holds
L . B = H5(B) ; ::_thesis: H5(A) = H4(A,L)
thus  H5(A) = H4(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 &amp; not UNIVERSE A is empty )
proofend;
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 T-Sequence st A <> {} &amp; A is limit_ordinal &amp; dom L = A &amp; ( 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 &amp; Tarski-Class {} c= U &amp; UNIVERSE {} c= U )
proofend;

theorem Th70: :: CLASSES2:70
for A, B being Ordinal holds
( A in B iff UNIVERSE A in UNIVERSE B )
proofend;

theorem :: CLASSES2:71
for A, B being Ordinal st UNIVERSE A = UNIVERSE B holds
A = B
proofend;

theorem :: CLASSES2:72
for A, B being Ordinal holds
( A c= B iff UNIVERSE A c= UNIVERSE B )
proofend;

theorem :: CLASSES2:73
for X being set holds
( Tarski-Class (X,{}) in Tarski-Class (X,1) &amp; Tarski-Class (X,{}) <> Tarski-Class (X,1) )
proofend;