The abstract of the Mizar article:

Universal Classes

by

Bogdan Nowak, and

Grzegorz Bancerek

Received April 10, 1990

MML identifier: CLASSES2

[ Mizar article, MML identifier index ]

environ

 vocabulary CARD_1, ORDINAL1, FUNCT_1, CLASSES1, TARSKI, BOOLE, RELAT_1,
      ORDINAL2, CARD_3, FUNCT_2, PROB_1, RLVECT_1, ZF_LANG, ZFMISC_1, SETFAM_1,
      FINSET_1, CLASSES2, HAHNBAN;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NAT_1, WELLORD2, FINSET_1,
      SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, ORDINAL1, ORDINAL2, CARD_1,
      CLASSES1, PROB_1, CARD_3;
 constructors WELLORD2, PROB_1, CLASSES1, CARD_3, XCMPLX_0, MEMBERED, PARTFUN1,
      RELAT_2, XBOOLE_0;
 clusters ORDINAL1, CARD_1, CLASSES1, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1,
      FUNCT_2, PARTFUN1, XBOOLE_0, ORDINAL2;
 requirements SUBSET, BOOLE;


begin

 reserve m for Cardinal,
         n for Nat,
         A,B,C for Ordinal,
         x,y,z,X,Y,Z,W for set,
         f for Function;

definition
 cluster being_Tarski-Class -> subset-closed set;
end;

definition let X be set;
  cluster Tarski-Class X -> being_Tarski-Class;
end;

theorem :: CLASSES2:1
  W is subset-closed & X in W implies
      not X,W are_equipotent & Card X <` Card W;

canceled;

theorem :: CLASSES2:3
  W is_Tarski-Class & x in W & y in W implies {x} in W & {x,y} in W;

theorem :: CLASSES2:4
  W is_Tarski-Class & x in W & y in W implies [x,y] in W;

theorem :: CLASSES2:5
  W is_Tarski-Class & X in W implies Tarski-Class X c= W;

scheme TC {P[set]}:
 for X holds P[Tarski-Class X] provided
 for X st X is_Tarski-Class holds P[X];

theorem :: CLASSES2:6
  W is_Tarski-Class & A in W implies succ A in W & A c= W;

theorem :: CLASSES2:7
   A in Tarski-Class W implies succ A in Tarski-Class W &
   A c= Tarski-Class W;

theorem :: CLASSES2:8
  W is subset-closed & X is epsilon-transitive & X in W implies X c= W;

theorem :: CLASSES2:9
   X is epsilon-transitive & X in Tarski-Class W implies X c= Tarski-Class W;

theorem :: CLASSES2:10
  W is_Tarski-Class implies On W = Card W;

theorem :: CLASSES2:11
  On Tarski-Class W = Card Tarski-Class W;

theorem :: CLASSES2:12
  W is_Tarski-Class & X in W implies Card X in W;

theorem :: CLASSES2:13
    X in Tarski-Class W implies Card X in Tarski-Class W;

theorem :: CLASSES2:14
  W is_Tarski-Class & x in Card W implies x in W;

theorem :: CLASSES2:15
   x in Card Tarski-Class W implies x in Tarski-Class W;

theorem :: CLASSES2:16
    W is_Tarski-Class & m <` Card W implies m in W;

theorem :: CLASSES2:17
    m <` Card Tarski-Class W implies m in Tarski-Class W;

theorem :: CLASSES2:18
   W is_Tarski-Class & m in W implies m c= W;

theorem :: CLASSES2:19
    m in Tarski-Class W implies m c= Tarski-Class W;

theorem :: CLASSES2:20
  W is_Tarski-Class implies Card W is_limit_ordinal;

theorem :: CLASSES2:21
  W is_Tarski-Class & W <> {} implies Card W <> 0 & Card W <> {} &
    Card W is_limit_ordinal;

theorem :: CLASSES2:22
  Card Tarski-Class W <> 0 & Card Tarski-Class W <> {} &
    Card Tarski-Class W is_limit_ordinal;

 reserve f,g for Function,
         L,L1 for T-Sequence,
         F for Cardinal-Function;

theorem :: CLASSES2:23
  W is_Tarski-Class &
  (X in W & W is epsilon-transitive or X in W & X c= W or
   Card X <` Card W & X c= W) implies Funcs(X,W) c= W;

theorem :: CLASSES2:24
    X in Tarski-Class W & W is epsilon-transitive or
  X in Tarski-Class W & X c= Tarski-Class W or
   Card X <` Card Tarski-Class W & X c= Tarski-Class W
    implies Funcs(X,Tarski-Class W) c= Tarski-Class W;

theorem :: CLASSES2:25
  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:26
  W is_Tarski-Class & A in On W implies Card Rank A <` Card W & Rank A in W;

theorem :: CLASSES2:27
   A in On Tarski-Class W implies
   Card Rank A <` Card Tarski-Class W & Rank A in Tarski-Class W;

theorem :: CLASSES2:28
  W is_Tarski-Class implies Rank Card W c= W;

theorem :: CLASSES2:29
  Rank Card Tarski-Class W c= Tarski-Class W;

theorem :: CLASSES2:30
 W is_Tarski-Class & W is epsilon-transitive & X in W implies
 the_rank_of X in W;

theorem :: CLASSES2:31
  W is_Tarski-Class & W is epsilon-transitive implies W c= Rank Card W;

theorem :: CLASSES2:32
  W is_Tarski-Class & W is epsilon-transitive implies Rank Card W = W;

theorem :: CLASSES2:33
    W is_Tarski-Class & A in On W implies Card Rank A <=` Card W;

theorem :: CLASSES2:34
    A in On Tarski-Class W implies Card Rank A <=` Card Tarski-Class W;

theorem :: CLASSES2:35
  W is_Tarski-Class implies Card W = Card Rank Card W;

theorem :: CLASSES2:36
  Card Tarski-Class W = Card Rank Card Tarski-Class W;

theorem :: CLASSES2:37
  W is_Tarski-Class & X c= Rank Card W implies
   X,Rank Card W are_equipotent or X in Rank Card W;

theorem :: CLASSES2:38
    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:39
  W is_Tarski-Class implies Rank Card W is_Tarski-Class;

theorem :: CLASSES2:40
  Rank Card Tarski-Class W is_Tarski-Class;

theorem :: CLASSES2:41
  X is epsilon-transitive & A in the_rank_of X implies
   ex Y st Y in X & the_rank_of Y = A;

theorem :: CLASSES2:42
  X is epsilon-transitive implies Card the_rank_of X <=` Card X;

theorem :: CLASSES2:43
  W is_Tarski-Class & X is epsilon-transitive & X in W implies
   X in Rank Card W;

theorem :: CLASSES2:44
   X is epsilon-transitive & X in Tarski-Class W implies
   X in Rank Card Tarski-Class W;

theorem :: CLASSES2:45
  W is epsilon-transitive implies
   Rank Card Tarski-Class W is_Tarski-Class_of W;

theorem :: CLASSES2:46
    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-Class;
 end;

 definition
  cluster universal -> epsilon-transitive being_Tarski-Class set;
  cluster epsilon-transitive being_Tarski-Class -> universal set;
 end;

 definition
  cluster universal non empty set;
 end;

definition
  mode Universe is universal non empty set;
end;

 reserve U1,U2,U3,Universum for Universe;

canceled 3;

theorem :: CLASSES2:50
  On Universum is Ordinal;

theorem :: CLASSES2:51
  X is epsilon-transitive implies Tarski-Class X is universal;

theorem :: CLASSES2:52
   Tarski-Class Universum is Universe;

 definition let Universum;
   cluster On Universum -> ordinal;
   cluster Tarski-Class Universum -> universal;
 end;

theorem :: CLASSES2:53
  Tarski-Class A is universal;

 definition let A;
   cluster Tarski-Class A -> universal;
 end;

theorem :: CLASSES2:54
  Universum = Rank On Universum;

theorem :: CLASSES2:55
  On Universum <> {} & On Universum is_limit_ordinal;

theorem :: CLASSES2:56
    U1 in U2 or U1 = U2 or U2 in U1;

theorem :: CLASSES2:57
  U1 c= U2 or U2 in U1;

theorem :: CLASSES2:58
  U1,U2 are_c=-comparable;

theorem :: CLASSES2:59
  U1 in U2 & U2 in U3 implies U1 in U3;

canceled;

theorem :: CLASSES2:61
   U1 \/ U2 is Universe & U1 /\ U2 is Universe;

theorem :: CLASSES2:62
 {} in Universum;

theorem :: CLASSES2:63
  x in Universum implies {x} in Universum;

theorem :: CLASSES2:64
  x in Universum & y in Universum implies {x,y} in Universum & [x,y] in
 Universum;

theorem :: CLASSES2:65
 X in Universum implies
   bool X in Universum & union X in Universum & meet X in Universum;

theorem :: CLASSES2:66
 X in Universum & Y in Universum implies
   X \/ Y in Universum & X /\ Y in Universum &
   X \ Y in Universum & X \+\ Y in Universum;

theorem :: CLASSES2:67
 X in Universum & Y in Universum implies
   [:X,Y:] in Universum & Funcs(X,Y) in Universum;

 reserve u,v for Element of Universum;

 definition let U1;
  cluster non empty Element of U1;
 end;

 definition let Universum,u;
  redefine
   func {u} -> Element of Universum;
   func bool u -> non empty Element of Universum;
   func union u -> Element of Universum;
   func meet u -> Element of Universum;
   let v;
   func {u,v} -> Element of Universum;
   func [u,v] -> Element of Universum;
   func u \/ v -> Element of Universum;
   func u /\ v -> Element of Universum;
   func u \ v -> Element of Universum;
   func u \+\ v -> Element of Universum;
   func [:u,v:] -> Element of Universum;
   func Funcs(u,v) -> Element of Universum;
 end;

 definition
  func FinSETS -> Universe equals
:: CLASSES2:def 2
     Tarski-Class {};
 end;

canceled;

theorem :: CLASSES2:69
  Card Rank omega = Card omega;

theorem :: CLASSES2:70
  Rank omega is_Tarski-Class;

theorem :: CLASSES2:71
   FinSETS = Rank omega;

 definition
  func SETS -> Universe equals
:: CLASSES2:def 3
     Tarski-Class FinSETS;
 end;

definition
 let X be set;
 cluster the_transitive-closure_of X -> epsilon-transitive;
end;

definition
 let X be epsilon-transitive set;
 cluster Tarski-Class X -> epsilon-transitive;
end;

definition
 let A be Ordinal;
 cluster Rank A -> 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 means
:: CLASSES2:def 5
   ex L st it = last L & dom L = succ A & L.{} = 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 <> {} & C is_limit_ordinal
           holds L.C = Universe_closure Union(L|C);
end;

definition let A;
  cluster UNIVERSE A -> universal non empty;
 end;

canceled 3;

theorem :: CLASSES2:75
   UNIVERSE {} = FinSETS;

theorem :: CLASSES2:76
   UNIVERSE succ A = Tarski-Class UNIVERSE A;

theorem :: CLASSES2:77
   UNIVERSE one = SETS;

theorem :: CLASSES2:78
   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:79
    FinSETS c= Universum & Tarski-Class {} c= Universum &
   UNIVERSE {} c= Universum;

theorem :: CLASSES2:80
  A in B iff UNIVERSE A in UNIVERSE B;

theorem :: CLASSES2:81
    UNIVERSE A = UNIVERSE B implies A = B;

theorem :: CLASSES2:82
    A c= B iff UNIVERSE A c= UNIVERSE B;