:: 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 b₁ being set st b₁ is Tarski holds
( b₁ is power-closed & b₁ is subset-closed ) ;

end;

registration

cluster epsilon-transitive Tarski -> union-closed FamUnion-closed for set ;

coherence
for b₁ being set st b₁ is epsilon-transitive & b₁ is Tarski holds
( b₁ is union-closed & b₁ is FamUnion-closed )

proof end;

end;

registration

cluster epsilon-transitive FamUnion-closed -> union-closed for set ;

coherence
for b₁ being set st b₁ is epsilon-transitive & b₁ is FamUnion-closed holds
b₁ is union-closed

proof end;

end;

registration

cluster epsilon-transitive power-closed -> subset-closed for set ;

coherence
for b₁ being set st b₁ is epsilon-transitive & b₁ is power-closed holds
b₁ 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 b₁ being Grothendieck st X in b₁

proof end;

end;

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

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 b₁ being Grothendieck of X st
for G being Grothendieck of X holds b₁ c= G

proof end;

uniqueness
for b₁, b₂ being Grothendieck of X st ( for G being Grothendieck of X holds b₁ c= G ) & ( for G being Grothendieck of X holds b₂ c= G ) holds
b₁ = b₂ ;

end;

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

scheme :: CLASSES3:sch 1
ClosedUnderReplacement{ F₁() -> set , F₂() -> Grothendieck of F₁(), F₃( set ) -> set } :

{ F₃(x) where x is Element of F₁() : x in F₁() } in F₂()

provided

A1: for Y being set st Y in F₁() holds
F₃(Y) in F₂()

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 b₁ being set st b₁ is epsilon-transitive & b₁ is power-closed & b₁ is FamUnion-closed holds
b₁ is universal

proof end;

cluster universal -> epsilon-transitive power-closed FamUnion-closed for set ;

coherence
for b₁ being set st b₁ is universal holds
( b₁ is epsilon-transitive & b₁ is power-closed & b₁ 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;