:: by Karol P\kak

::

:: Received May 31, 2020

:: Copyright (c) 2020-2021 Association of Mizar Users

:: deftheorem Def1 defines power-closed CLASSES3:def 1 :

for X being set holds

( X is power-closed iff for Y being set st Y in X holds

bool Y in X );

for X being set holds

( X is power-closed iff for Y being set st Y in X holds

bool Y in X );

:: deftheorem Def2 defines union-closed CLASSES3:def 2 :

for X being set holds

( X is union-closed iff for Y being set st Y in X holds

union Y in X );

for X being set holds

( X is union-closed iff for Y being set st Y in X holds

union Y in X );

:: deftheorem Def3 defines FamUnion-closed CLASSES3:def 3 :

for X being set holds

( X is FamUnion-closed iff for Y being set

for f being Function st dom f = Y & rng f c= X & Y in X holds

union (rng f) in X );

for X being set holds

( X is FamUnion-closed iff for Y being set

for f being Function st dom f = Y & rng f c= X & Y in X holds

union (rng f) in X );

registration

coherence

for b_{1} being set st b_{1} is Tarski holds

( b_{1} is power-closed & b_{1} is subset-closed )
;

end;
for b

( b

registration

coherence

for b_{1} being set st b_{1} is epsilon-transitive & b_{1} is Tarski holds

( b_{1} is union-closed & b_{1} is FamUnion-closed )

end;
for b

( b

proof end;

registration

coherence

for b_{1} being set st b_{1} is epsilon-transitive & b_{1} is FamUnion-closed holds

b_{1} is union-closed

end;
for b

b

proof end;

registration

coherence

for b_{1} being set st b_{1} is epsilon-transitive & b_{1} is power-closed holds

b_{1} is subset-closed

end;
for b

b

proof end;

:: deftheorem Def4 defines Grothendieck CLASSES3:def 4 :

for X being set

for b_{2} being Grothendieck holds

( b_{2} is Grothendieck of X iff X in b_{2} );

for X being set

for b

( b

registration

let G1, G2 be Grothendieck;

coherence

( G1 /\ G2 is epsilon-transitive & G1 /\ G2 is power-closed & G1 /\ G2 is FamUnion-closed )

end;
coherence

( G1 /\ G2 is epsilon-transitive & G1 /\ G2 is power-closed & G1 /\ G2 is FamUnion-closed )

proof end;

definition

let X be set ;

ex b_{1} being Grothendieck of X st

for G being Grothendieck of X holds b_{1} c= G

for b_{1}, b_{2} being Grothendieck of X st ( for G being Grothendieck of X holds b_{1} c= G ) & ( for G being Grothendieck of X holds b_{2} c= G ) holds

b_{1} = b_{2}
;

end;
func GrothendieckUniverse X -> Grothendieck of X means :GDef: :: CLASSES3:def 5

for G being Grothendieck of X holds it c= G;

existence for G being Grothendieck of X holds it c= G;

ex b

for G being Grothendieck of X holds b

proof end;

uniqueness for b

b

:: deftheorem GDef defines GrothendieckUniverse CLASSES3:def 5 :

for X being set

for b_{2} being Grothendieck of X holds

( b_{2} = GrothendieckUniverse X iff for G being Grothendieck of X holds b_{2} c= G );

for X being set

for b

( b

:: deftheorem defines Rrank CLASSES3:def 6 :

for x being object holds Rrank x = Rank (the_rank_of x);

for x being object holds Rrank x = Rank (the_rank_of x);

theorem Th3: :: CLASSES3:3

for X being set

for A being Ordinal holds

( X in Rank A iff ex B being Ordinal st

( B in A & X in bool (Rank B) ) )

for A being Ordinal holds

( X in Rank A iff ex B being Ordinal st

( B in A & X in bool (Rank B) ) )

proof end;

theorem :: CLASSES3:12

for X being set

for A being Ordinal

for U being Grothendieck st X in U & X,A are_equipotent holds

A in U

for A being Ordinal

for U being Grothendieck st X in U & X,A are_equipotent holds

A in U

proof end;

theorem Th16: :: CLASSES3:16

for U being Grothendieck

for X being set st X c= U & not X in U holds

ex f being Function st

( f is one-to-one & dom f = On U & rng f = X )

for X being set st X c= U & not X in U holds

ex f being Function st

( f is one-to-one & dom f = On U & rng f = X )

proof end;

registration

coherence

for b_{1} being set st b_{1} is epsilon-transitive & b_{1} is power-closed & b_{1} is FamUnion-closed holds

b_{1} is universal

for b_{1} being set st b_{1} is universal holds

( b_{1} is epsilon-transitive & b_{1} is power-closed & b_{1} is FamUnion-closed )
;

end;
for b

b

proof end;

coherence for b

( b

theorem :: CLASSES3:21

for X being set holds

( GrothendieckUniverse X is Universe & ( for U being Universe st X in U holds

GrothendieckUniverse X c= U ) )

( GrothendieckUniverse X is Universe & ( for U being Universe st X in U holds

GrothendieckUniverse X c= U ) )

proof end;