:: Grothendieck Universes
:: by Karol P\kak
::
:: Received May 31, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FUNCT_1, RELAT_1, SETFAM_1, XBOOLE_0, SUBSET_1, TARSKI, ZFMISC_1,
NAT_1, CARD_1, ORDINAL1, CLASSES1, CARD_3, CLASSES2, CLASSES3, WELLORD1,
FINSET_1, NUMBERS, XXREAL_0, ARYTM_3, ARYTM_1, MEMBERED, ROUGHS_4;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1,
CARD_1, NUMBERS, CLASSES1, CARD_3, CLASSES2, XCMPLX_0, NAT_1, WELLORD1,
FINSET_1, MEMBERED, XXREAL_0, XXREAL_2;
constructors WELLORD2, CLASSES1, CARD_3, NUMBERS, WELLORD1, NAT_1, ORDINAL6,
XXREAL_2;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELAT_1, SUBSET_1, CARD_1, CARD_3,
CLASSES1, CLASSES2, FINSET_1, XCMPLX_0, ORDINAL6, ZFMISC_1, XXREAL_0,
MEMBERED, XXREAL_2;
requirements SUBSET, BOOLE, NUMERALS, ARITHM;
begin :: Grothendieck Universes Axioms
:: The material is an extension of the formalization used in
:: Chad E. Brown, Karol Pak,
:: A Tale of Two Set Theories, Intelligent Computer Mathematics
:: In C. Kaliszyk and E. Brady and A. Kohlhase and C. Sacerdoti Coen editors,
:: Intelligent Computer Mathematics - 12th International Conference, CICM 2019,
:: Proceedings, Vol 11617 of LNCS, pages 44-60. Springer, 2019.
reserve X,Y,Z for set,
x,y,z for object,
A,B,C for Ordinal;
definition
let X;
attr X is power-closed means
:: CLASSES3:def 1
Y in X implies bool Y in X;
end;
definition
let X;
attr X is union-closed means
:: CLASSES3:def 2
Y in X implies union Y in X;
end;
definition
let X;
attr X is FamUnion-closed means
:: CLASSES3:def 3
for Y for f being Function st
dom f = Y & rng f c= X & Y in X
holds union rng f in X;
end;
registration
cluster Tarski -> power-closed subset-closed for set;
end;
registration
cluster epsilon-transitive Tarski -> union-closed FamUnion-closed
for set;
end;
registration
cluster epsilon-transitive FamUnion-closed -> union-closed for set;
end;
registration
cluster epsilon-transitive power-closed -> subset-closed for set;
end;
definition
mode Grothendieck is epsilon-transitive power-closed FamUnion-closed set;
end;
begin :: Grothendieck Universe Operator
definition
let X be set;
mode Grothendieck of X -> Grothendieck means
:: CLASSES3:def 4
X in it;
end;
registration
let G1,G2 be Grothendieck;
cluster G1/\G2 -> epsilon-transitive power-closed FamUnion-closed;
end;
theorem :: CLASSES3:1
for G1,G2 being Grothendieck of X holds G1/\G2 is Grothendieck of X;
definition
let X be set;
func GrothendieckUniverse X -> Grothendieck of X means
:: CLASSES3:def 5
for G being Grothendieck of X holds it c= G;
end;
scheme :: CLASSES3:sch 1
ClosedUnderReplacement
{X()-> set, U() -> Grothendieck of X(),F(set) -> set}:
{F(x) where x is Element of X(): x in X()} in U()
provided
Y in X() implies F(Y) in U();
reserve U for Grothendieck;
theorem :: CLASSES3:2
for f be Function st dom f in U & rng f c= U holds rng f in U;
begin :: Set of All Sets Up To Given Rank
definition
let x be object;
func Rrank x -> epsilon-transitive set equals
:: CLASSES3:def 6
Rank the_rank_of x;
end;
theorem :: CLASSES3:3
X in Rank A iff ex B st B in A & X in bool Rank B;
theorem :: CLASSES3:4
Y in Rrank X iff ex Z st Z in X & Y in bool Rrank Z;
theorem :: CLASSES3:5 :: Theorem 2 (1)
x in X & y in Rrank x implies y in Rrank X;
theorem :: CLASSES3:6 :: Theorem 2 (2)
Y in Rrank X implies ex x st x in X & Y c= Rrank x;
theorem :: CLASSES3:7 :: Theorem 2 (3)
X c= Rrank X;
theorem :: CLASSES3:8 :: Theorem 2 (4)
X c= Rrank Y implies Rrank X c= Rrank Y;
theorem :: CLASSES3:9 :: Theorem 2 (5)
X in Rrank Y implies Rrank X in Rrank Y;
theorem :: CLASSES3:10 :: Theorem 2 (6)
X in Rrank Y or Rrank Y c= Rrank X;
theorem :: CLASSES3:11 :: Theorem 2 (7)
Rrank X in Rrank Y or Rrank Y c= Rrank X;
theorem :: CLASSES3:12
X in U & X,A are_equipotent implies A in U;
theorem :: CLASSES3:13
X in Y in U implies X in U;
theorem :: CLASSES3:14 :: Theorem 3
X in U implies Rrank X in U;
theorem :: CLASSES3:15
A in U implies Rank A in U;
begin :: Tarski vs. Grothendieck Universe
theorem :: CLASSES3:16 :: Main Lemma 1
for X st X c= U & not X in U
ex f be Function st f is one-to-one & dom f = On U & rng f = X;
theorem :: CLASSES3:17 :: Theorem 5
for U be Grothendieck holds U is Tarski;
registration
cluster epsilon-transitive power-closed FamUnion-closed -> universal for set;
cluster universal -> epsilon-transitive power-closed FamUnion-closed for set;
end;
theorem :: CLASSES3:18
for G be Grothendieck of X holds Tarski-Class X c= G;
theorem :: CLASSES3:19
for X be infinite set holds not X in Tarski-Class {X};
theorem :: CLASSES3:20
for X be infinite set holds
Tarski-Class {X} c< GrothendieckUniverse {X};
theorem :: CLASSES3:21
GrothendieckUniverse X is Universe &
for U be Universe st X in U holds GrothendieckUniverse X c= U;
theorem :: CLASSES3:22
for X be epsilon-transitive set holds
Tarski-Class X = GrothendieckUniverse X;