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