:: Universal Classes :: by Bogdan Nowak and Grzegorz Bancerek :: :: Received April 10, 1990 :: Copyright (c) 1990-2016 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 CARD_1, ORDINAL1, FUNCT_1, CLASSES1, TARSKI, ZFMISC_1, XBOOLE_0, RELAT_1, CARD_3, FUNCT_2, SUBSET_1, SETFAM_1, FINSET_1, ORDINAL2, CLASSES2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, FINSET_1, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, ORDINAL2, CLASSES1, CARD_3; constructors SETFAM_1, WELLORD2, ORDINAL2, CLASSES1, CARD_3, NUMBERS, FUNCT_2, XTUPLE_0; registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, CARD_1, CLASSES1; requirements SUBSET, BOOLE, NUMERALS; begin reserve m for Cardinal, A,B,C for Ordinal, x,y,z,X,Y,Z,W for set, f for Function; registration cluster Tarski -> subset-closed for set; end; registration let X be set; cluster Tarski-Class X -> Tarski; end; theorem :: CLASSES2:1 W is subset-closed & X in W implies not X,W are_equipotent & card X in card W ; theorem :: CLASSES2:2 W is Tarski & x in W & y in W implies {x} in W & {x,y} in W; theorem :: CLASSES2:3 W is Tarski & x in W & y in W implies [x,y] in W; theorem :: CLASSES2:4 W is Tarski & X in W implies Tarski-Class X c= W; theorem :: CLASSES2:5 W is Tarski & A in W implies succ A in W & A c= W; theorem :: CLASSES2:6 A in Tarski-Class W implies succ A in Tarski-Class W & A c= Tarski-Class W; theorem :: CLASSES2:7 W is subset-closed & X is epsilon-transitive & X in W implies X c= W; theorem :: CLASSES2:8 X is epsilon-transitive & X in Tarski-Class W implies X c= Tarski-Class W; theorem :: CLASSES2:9 W is Tarski implies On W = card W; theorem :: CLASSES2:10 On Tarski-Class W = card Tarski-Class W; theorem :: CLASSES2:11 W is Tarski & X in W implies card X in W; theorem :: CLASSES2:12 X in Tarski-Class W implies card X in Tarski-Class W; theorem :: CLASSES2:13 W is Tarski & x in card W implies x in W; theorem :: CLASSES2:14 x in card Tarski-Class W implies x in Tarski-Class W; theorem :: CLASSES2:15 W is Tarski & m in card W implies m in W; theorem :: CLASSES2:16 m in card Tarski-Class W implies m in Tarski-Class W; theorem :: CLASSES2:17 W is Tarski & m in W implies m c= W; theorem :: CLASSES2:18 m in Tarski-Class W implies m c= Tarski-Class W; theorem :: CLASSES2:19 W is Tarski implies card W is limit_ordinal; theorem :: CLASSES2:20 W is Tarski & W <> {} implies card W <> 0 & card W <> {} & card W is limit_ordinal; theorem :: CLASSES2:21 card Tarski-Class W <> 0 & card Tarski-Class W <> {} & card Tarski-Class W is limit_ordinal; reserve f,g for Function, L for Sequence, F for Cardinal-Function; theorem :: CLASSES2:22 W is Tarski & (X in W & W is epsilon-transitive or X in W & X c= W or card X in card W & X c= W) implies Funcs(X,W) c= W; theorem :: CLASSES2:23 X in Tarski-Class W & W is epsilon-transitive or X in Tarski-Class W & X c= Tarski-Class W or card X in card Tarski-Class W & X c= Tarski-Class W implies Funcs(X,Tarski-Class W) c= Tarski-Class W; theorem :: CLASSES2:24 dom L is limit_ordinal & (for A st A in dom L holds L.A = Rank A ) implies Rank dom L = Union L; theorem :: CLASSES2:25 W is Tarski & A in On W implies card Rank A in card W & Rank A in W; theorem :: CLASSES2:26 A in On Tarski-Class W implies card Rank A in card Tarski-Class W & Rank A in Tarski-Class W; theorem :: CLASSES2:27 W is Tarski implies Rank card W c= W; theorem :: CLASSES2:28 Rank card Tarski-Class W c= Tarski-Class W; theorem :: CLASSES2:29 W is Tarski & W is epsilon-transitive & X in W implies the_rank_of X in W; theorem :: CLASSES2:30 W is Tarski & W is epsilon-transitive implies W c= Rank card W; theorem :: CLASSES2:31 W is Tarski & W is epsilon-transitive implies Rank card W = W; theorem :: CLASSES2:32 W is Tarski & A in On W implies card Rank A c= card W; theorem :: CLASSES2:33 A in On Tarski-Class W implies card Rank A c= card Tarski-Class W; theorem :: CLASSES2:34 W is Tarski implies card W = card Rank card W; theorem :: CLASSES2:35 card Tarski-Class W = card Rank card Tarski-Class W; theorem :: CLASSES2:36 W is Tarski & X c= Rank card W implies X,Rank card W are_equipotent or X in Rank card W; theorem :: CLASSES2:37 X c= Rank card Tarski-Class W implies X,Rank card Tarski-Class W are_equipotent or X in Rank card Tarski-Class W; theorem :: CLASSES2:38 W is Tarski implies Rank card W is Tarski; theorem :: CLASSES2:39 Rank card Tarski-Class W is Tarski; theorem :: CLASSES2:40 X is epsilon-transitive & A in the_rank_of X implies ex Y st Y in X & the_rank_of Y = A; theorem :: CLASSES2:41 X is epsilon-transitive implies card the_rank_of X c= card X; theorem :: CLASSES2:42 W is Tarski & X is epsilon-transitive & X in W implies X in Rank card W; theorem :: CLASSES2:43 X is epsilon-transitive & X in Tarski-Class W implies X in Rank card Tarski-Class W; theorem :: CLASSES2:44 W is epsilon-transitive implies Rank card Tarski-Class W is_Tarski-Class_of W ; theorem :: CLASSES2:45 W is epsilon-transitive implies Rank card Tarski-Class W = Tarski-Class W; definition let IT be set; attr IT is universal means :: CLASSES2:def 1 IT is epsilon-transitive & IT is Tarski; end; registration cluster universal -> epsilon-transitive Tarski for set; cluster epsilon-transitive Tarski -> universal for set; end; registration cluster universal non empty for set; end; definition mode Universe is universal non empty set; end; reserve U1,U2,U for Universe; theorem :: CLASSES2:46 On U is Ordinal; theorem :: CLASSES2:47 X is epsilon-transitive implies Tarski-Class X is universal; theorem :: CLASSES2:48 Tarski-Class U is Universe; registration let U; cluster On U -> ordinal; cluster Tarski-Class U -> universal; end; theorem :: CLASSES2:49 Tarski-Class A is universal; registration let A; cluster Tarski-Class A -> universal; end; theorem :: CLASSES2:50 U = Rank On U; theorem :: CLASSES2:51 On U <> {} & On U is limit_ordinal; theorem :: CLASSES2:52 U1 in U2 or U1 = U2 or U2 in U1; theorem :: CLASSES2:53 U1 c= U2 or U2 in U1; theorem :: CLASSES2:54 U1,U2 are_c=-comparable; theorem :: CLASSES2:55 U1 \/ U2 is Universe & U1 /\ U2 is Universe; theorem :: CLASSES2:56 {} in U; theorem :: CLASSES2:57 x in U implies {x} in U; theorem :: CLASSES2:58 x in U & y in U implies {x,y} in U & [x,y] in U; theorem :: CLASSES2:59 X in U implies bool X in U & union X in U & meet X in U; theorem :: CLASSES2:60 X in U & Y in U implies X \/ Y in U & X /\ Y in U & X \ Y in U & X \+\ Y in U ; theorem :: CLASSES2:61 X in U & Y in U implies [:X,Y:] in U & Funcs(X,Y) in U; reserve u,v for Element of U; registration let U1; cluster non empty for Element of U1; end; definition let U,u; redefine func {u} -> Element of U; redefine func bool u -> Element of U; redefine func union u -> Element of U; redefine func meet u -> Element of U; let v; redefine func {u,v} -> Element of U; redefine func [u,v] -> Element of U; redefine func u \/ v -> Element of U; redefine func u /\ v -> Element of U; redefine func u \ v -> Element of U; redefine func u \+\ v -> Element of U; redefine func [:u,v:] -> Element of U; redefine func Funcs(u,v) -> Element of U; end; definition func FinSETS -> Universe equals :: CLASSES2:def 2 Tarski-Class {}; end; theorem :: CLASSES2:62 card Rank omega = card omega; theorem :: CLASSES2:63 Rank omega is Tarski; theorem :: CLASSES2:64 FinSETS = Rank omega; definition func SETS -> Universe equals :: CLASSES2:def 3 Tarski-Class FinSETS; end; registration let X be set; cluster the_transitive-closure_of X -> epsilon-transitive; end; registration let X be epsilon-transitive set; cluster Tarski-Class X -> epsilon-transitive; end; definition let X be set; func Universe_closure X -> Universe means :: CLASSES2:def 4 X c= it & for Y being Universe st X c= Y holds it c= Y; end; definition mode FinSet is Element of FinSETS; mode Set is Element of SETS; let A; func UNIVERSE A -> set means :: CLASSES2:def 5 ex L st it = last L & dom L = succ A & L.0 = FinSETS & (for C st succ C in succ A holds L.succ C = Tarski-Class(L.C)) & for C st C in succ A & C <> 0 & C is limit_ordinal holds L.C = Universe_closure Union(L|C); end; registration let A; cluster UNIVERSE A -> universal non empty; end; theorem :: CLASSES2:65 UNIVERSE {} = FinSETS; theorem :: CLASSES2:66 UNIVERSE succ A = Tarski-Class UNIVERSE A; theorem :: CLASSES2:67 UNIVERSE 1 = SETS; theorem :: CLASSES2:68 A <> {} & A is limit_ordinal & dom L = A & (for B st B in A holds L.B = UNIVERSE B) implies UNIVERSE A = Universe_closure Union L; theorem :: CLASSES2:69 FinSETS c= U & Tarski-Class {} c= U & UNIVERSE {} c= U; theorem :: CLASSES2:70 A in B iff UNIVERSE A in UNIVERSE B; theorem :: CLASSES2:71 UNIVERSE A = UNIVERSE B implies A = B; theorem :: CLASSES2:72 A c= B iff UNIVERSE A c= UNIVERSE B; reserve u,v for Element of Tarski-Class(X); theorem :: CLASSES2:73 Tarski-Class(X,{}) in Tarski-Class(X,1) & Tarski-Class(X,{}) <> Tarski-Class(X,1);