:: Grothendieck Universes
:: by Karol P\kak
::
:: Received May 31, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users


definition
let X be set ;
attr X is power-closed means :Def1: :: CLASSES3:def 1
 for Y being set st Y in X holds
bool Y in X;
end;

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

definition
let X be set ;
attr X is union-closed means :Def2: :: CLASSES3:def 2
 for Y being set st Y in X holds
union Y in X;
end;

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

definition
let X be set ;
attr X is FamUnion-closed means :Def3: :: CLASSES3:def 3
 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;
end;

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

registration
cluster Tarski -> subset-closed power-closed for set ;
coherence
for b1 being set st b1 is Tarski holds
( b1 is power-closed & b1 is subset-closed ) ;
end;

registration
cluster epsilon-transitive Tarski -> union-closed FamUnion-closed for set ;
coherence
for b1 being set st b1 is epsilon-transitive & b1 is Tarski holds
( b1 is union-closed & b1 is FamUnion-closed )
proof end;
end;

registration
cluster epsilon-transitive FamUnion-closed -> union-closed for set ;
coherence
for b1 being set st b1 is epsilon-transitive & b1 is FamUnion-closed holds
b1 is union-closed
proof end;
end;

registration
cluster epsilon-transitive power-closed -> subset-closed for set ;
coherence
for b1 being set st b1 is epsilon-transitive & b1 is power-closed holds
b1 is subset-closed
proof end;
end;

definition
mode Grothendieck is epsilon-transitive power-closed FamUnion-closed set ;
end;

definition
let X be set ;
mode Grothendieck of X -> Grothendieck means :Def4: :: CLASSES3:def 4
X in it;
existence
ex b1 being Grothendieck st X in b1
proof end;
end;

:: deftheorem Def4 defines Grothendieck CLASSES3:def 4 :
for X being set
for b2 being Grothendieck holds
( b2 is Grothendieck of X iff X in b2 );

registration
let G1, G2 be Grothendieck;
cluster G1 /\ G2 -> epsilon-transitive power-closed FamUnion-closed ;
coherence
( G1 /\ G2 is epsilon-transitive & G1 /\ G2 is power-closed & G1 /\ G2 is FamUnion-closed )
proof end;
end;

theorem Th1: :: CLASSES3:1
for X being set
for G1, G2 being Grothendieck of X holds G1 /\ G2 is Grothendieck of X
proof end;

definition
let X be set ;
func GrothendieckUniverse X -> Grothendieck of X means :GDef: :: CLASSES3:def 5
 for G being Grothendieck of X holds it c= G;
existence
ex b1 being Grothendieck of X st
for G being Grothendieck of X holds b1 c= G
proof end;
uniqueness
for b1, b2 being Grothendieck of X st ( for G being Grothendieck of X holds b1 c= G ) & ( for G being Grothendieck of X holds b2 c= G ) holds
b1 = b2 ;
end;

:: deftheorem GDef defines GrothendieckUniverse CLASSES3:def 5 :
for X being set
for b2 being Grothendieck of X holds
( b2 = GrothendieckUniverse X iff for G being Grothendieck of X holds b2 c= G );

scheme :: CLASSES3:sch 1
ClosedUnderReplacement{ F1() -> set , F2() -> Grothendieck of F1(), F3( set ) -> set } :
{ F3(x) where x is Element of F1() : x in F1() } in F2()
provided
A1: for Y being set st Y in F1() holds
F3(Y) in F2()
proof end;

theorem Th2: :: CLASSES3:2
for U being Grothendieck
for f being Function st dom f in U & rng f c= U holds
rng f in U
proof end;

definition
let x be object ;
func Rrank x -> epsilon-transitive set equals :: CLASSES3:def 6
 Rank (the_rank_of x);
coherence
Rank (the_rank_of x) is epsilon-transitive set ;
end;

:: deftheorem defines Rrank CLASSES3:def 6 :
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) ) )
proof end;

theorem Th4: :: CLASSES3:4
for X, Y being set holds
( Y in Rrank X iff ex Z being set st
( Z in X & Y in bool (Rrank Z) ) )
proof end;

theorem :: CLASSES3:5
for X being set
for x, y being object st x in X & y in Rrank x holds
y in Rrank X
proof end;

theorem :: CLASSES3:6
for X, Y being set st Y in Rrank X holds
ex x being object st
( x in X & Y c= Rrank x )
proof end;

theorem :: CLASSES3:7
for X being set holds X c= Rrank X by CLASSES1:def 9;

theorem :: CLASSES3:8
for X, Y being set st X c= Rrank Y holds
Rrank X c= Rrank Y
proof end;

theorem :: CLASSES3:9
for X, Y being set st X in Rrank Y holds
Rrank X in Rrank Y
proof end;

theorem :: CLASSES3:10
for X, Y being set holds
( X in Rrank Y or Rrank Y c= Rrank X )
proof end;

theorem :: CLASSES3:11
for X, Y being set holds
( Rrank X in Rrank Y or Rrank Y c= Rrank X )
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
proof end;

theorem Th13: :: CLASSES3:13
for X, Y being set
for U being Grothendieck st X in Y & Y in U holds
X in U
proof end;

theorem Th14: :: CLASSES3:14
for X being set
for U being Grothendieck st X in U holds
Rrank X in U
proof end;

theorem :: CLASSES3:15
for A being Ordinal
for U being Grothendieck st A in U holds
Rank 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 )
proof end;

theorem Th17: :: CLASSES3:17
for U being Grothendieck holds U is Tarski
proof end;

registration
cluster epsilon-transitive power-closed FamUnion-closed -> universal for set ;
coherence
for b1 being set st b1 is epsilon-transitive & b1 is power-closed & b1 is FamUnion-closed holds
b1 is universal
proof end;
cluster universal -> epsilon-transitive power-closed FamUnion-closed for set ;
coherence
for b1 being set st b1 is universal holds
( b1 is epsilon-transitive & b1 is power-closed & b1 is FamUnion-closed ) ;
end;

theorem Th18: :: CLASSES3:18
for X being set
for G being Grothendieck of X holds Tarski-Class X c= G
proof end;

theorem Th19: :: CLASSES3:19
for X being infinite set holds not X in Tarski-Class {X}
proof end;

theorem :: CLASSES3:20
for X being infinite set holds Tarski-Class {X} c< GrothendieckUniverse {X}
proof end;

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 ) )
proof end;

theorem :: CLASSES3:22
for X being epsilon-transitive set holds Tarski-Class X = GrothendieckUniverse X
proof end;