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

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

registration
coherence
for b1 being set st b1 is Tarski holds
b1 is subset-closed
;
end;

registration
let X be set ;
coherence 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 () = card () 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 () 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 () 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 () <> 0 & card () <> {} & card () 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 () & X c= Tarski-Class W ) ) holds
Funcs (X,()) 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 S1[ 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: S1[ 0 ] by ; Lm3: for A being Ordinal st S1[A] holds S1[ 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 S1[B] ) holds S1[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 () holds ( card (Rank A) in card () & 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 ()) c= Tarski-Class W proof end; deffunc H1( object ) -> set = the_rank_of$1;

deffunc H2( 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 ; 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 () holds card (Rank A) c= card () 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 () = card (Rank (card ())) 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 ()) or X, Rank (card ()) are_equipotent or X in Rank (card ()) ) 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 ()) 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 () 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 ()) by Th42; theorem Th44: :: CLASSES2:44 for W being set st W is epsilon-transitive holds Rank (card ()) is_Tarski-Class_of W by ; theorem :: CLASSES2:45 for W being set st W is epsilon-transitive holds Rank (card ()) = 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 coherence for b1 being set st b1 is universal holds ( b1 is epsilon-transitive & b1 is Tarski ) ; coherence for b1 being set st b1 is epsilon-transitive & b1 is Tarski holds b1 is universal ; end; registration cluster non empty universal for set ; existence ex b1 being set st ( b1 is universal & not b1 is empty ) proof end; end; definition 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; coherence 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; coherence 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 ; 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 b1 being Element of U1 holds b1 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 correctness coherence ; ; end; :: deftheorem defines FinSETS CLASSES2:def 2 : Lm5: by ORDINAL1:def 11; theorem Th62: :: CLASSES2:62 proof end; theorem Th63: :: CLASSES2:63 proof end; theorem :: CLASSES2:64 proof end; definition correctness ; end; :: deftheorem defines SETS CLASSES2:def 3 : registration let X be set ; coherence ; end; registration let X be epsilon-transitive set ; coherence 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 b1, b2 being Universe st X c= b1 & ( for Y being Universe st X c= Y holds b1 c= Y ) & X c= b2 & ( for Y being Universe st X c= Y holds b2 c= Y ) holds b1 = b2 ; existence ex b1 being Universe st ( X c= b1 & ( for Y being Universe st X c= Y holds b1 c= Y ) ) proof end; 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 & ( for Y being Universe st X c= Y holds b2 c= Y ) ) ); deffunc H3( Ordinal, set ) -> set = Tarski-Class$2;

deffunc H4( 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 b1 being set ex L being Sequence st ( b1 = 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 b1, b2 being set st ex L being Sequence st ( b1 = 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 ( b2 = 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 b1 = b2 ; proof end; end; :: deftheorem Def5 defines UNIVERSE CLASSES2:def 5 : for A being Ordinal for b2 being set holds ( b2 = UNIVERSE A iff ex L being Sequence st ( b2 = 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 H5( Ordinal) -> set = UNIVERSE$1;

Lm6: now :: thesis: ( H5( 0 ) = FinSETS & ( for A being Ordinal holds H5( succ A) = H3(A,H5(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 = H5(B) ) holds
H5(A) = H4(A,L) ) )
A1: for A being Ordinal
for x being object holds
( x = H5(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) = H3(C,L . C) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
L . C = H4(C,L | C) ) ) ) by Def5;
thus H5( 0 ) = FinSETS from :: thesis: ( ( for A being Ordinal holds H5( succ A) = H3(A,H5(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 = H5(B) ) holds
H5(A) = H4(A,L) ) )

thus for A being Ordinal holds H5( succ A) = H3(A,H5(A)) from :: 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 = H5(B) ) holds
H5(A) = H4(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 = H5(B) ) holds
H5(A) = H4(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 = H5(B) ) implies H5(A) = H4(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 = 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;
coherence
( UNIVERSE A is universal & not UNIVERSE A is empty )
proof end;
end;

theorem :: CLASSES2:65

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

Lm7:
;

theorem :: CLASSES2:67
UNIVERSE 1 = SETS by ;

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