The abstract of the Mizar article:

Tarski's Classes and Ranks

by

Grzegorz Bancerek

Received March 23, 1990

MML identifier: CLASSES1

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, TARSKI, SETFAM_1, BOOLE, CARD_1, ORDINAL1, ORDINAL2,
      RELAT_1, MCART_1, CLASSES1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
      NUMBERS, NAT_1, ORDINAL1, MCART_1, ORDINAL2, CARD_1;
 constructors SETFAM_1, NAT_1, MCART_1, WELLORD2, CARD_1, MEMBERED, XBOOLE_0;
 clusters SUBSET_1, ORDINAL1, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
 requirements NUMERALS, SUBSET, BOOLE;


begin

 reserve W,X,Y,Z for set,
         f,g for Function,
         a,x,y,z for set;

definition let B be set;
 attr B is subset-closed means
:: CLASSES1:def 1
 for X,Y holds X in B & Y c= X implies Y in B;
end;

definition let B be set;
 attr B is being_Tarski-Class means
:: CLASSES1:def 2
  B is subset-closed &
       (for X holds X in B implies bool X in B) &
       (for X holds X c= B implies X,B are_equipotent or X in B);
  synonym B is_Tarski-Class;
end;

definition let A,B be set;
 pred B is_Tarski-Class_of A means
:: CLASSES1:def 3
 A in B & B is_Tarski-Class;
end;

definition let A be set;
 func Tarski-Class A -> set means
:: CLASSES1:def 4
 it is_Tarski-Class_of A &
     for D being set st D is_Tarski-Class_of A holds it c= D;
end;

definition let A be set;
 cluster Tarski-Class A -> non empty;
end;

canceled;

theorem :: CLASSES1:2
   W is_Tarski-Class iff
   W is subset-closed &
   (for X st X in W holds bool X in W) &
   (for X st X c= W & Card X <` Card W holds X in W);

canceled 2;

theorem :: CLASSES1:5
  X in Tarski-Class X;

theorem :: CLASSES1:6
  Y in Tarski-Class X & Z c= Y implies Z in Tarski-Class X;

theorem :: CLASSES1:7
  Y in Tarski-Class X implies bool Y in Tarski-Class X;

theorem :: CLASSES1:8
  Y c= Tarski-Class X implies
      Y,Tarski-Class X are_equipotent or Y in Tarski-Class X;

theorem :: CLASSES1:9
    Y c= Tarski-Class X & Card Y <` Card Tarski-Class X implies
   Y in Tarski-Class X;

 reserve u,v for Element of Tarski-Class(X),
         A,B,C for Ordinal,
         L,L1 for T-Sequence;

definition let X,A;
 func Tarski-Class(X,A) means
:: CLASSES1:def 5

   ex L st it = last L & dom L = succ A & L.{} = { X } &
    (for C st succ C in succ A holds
     L.succ C = { u : ex v st v in L.C & u c= v } \/
                { bool v : v in L.C } \/
                bool(L.C) /\ Tarski-Class X) &
      for C st C in succ A & C <> {} & C is_limit_ordinal
             holds L.C = (union rng(L|C)) /\ Tarski-Class X;
end;

definition let X,A;
 redefine func Tarski-Class(X,A) -> Subset of Tarski-Class X;
end;

theorem :: CLASSES1:10
   Tarski-Class(X,{}) = { X };

theorem :: CLASSES1:11
   Tarski-Class(X,succ A) =
      { u : ex v st v in Tarski-Class(X,A) & u c= v } \/
      { bool v : v in Tarski-Class(X,A) } \/
      bool Tarski-Class(X,A) /\ Tarski-Class X;

theorem :: CLASSES1:12
  A <> {} & A is_limit_ordinal implies
      Tarski-Class(X,A) = { u : ex B st B in A & u in Tarski-Class(X,B) };

theorem :: CLASSES1:13
  Y in Tarski-Class(X,succ A) iff
   Y c= Tarski-Class(X,A) & Y in Tarski-Class X or
   ex Z st Z in Tarski-Class(X,A) & (Y c= Z or Y = bool Z);

theorem :: CLASSES1:14
   Y c= Z & Z in Tarski-Class(X,A) implies Y in Tarski-Class(X,succ A);

theorem :: CLASSES1:15
   Y in Tarski-Class(X,A) implies bool Y in Tarski-Class(X,succ A);

theorem :: CLASSES1:16
  A <> {} & A is_limit_ordinal implies
   (x in Tarski-Class(X,A) iff ex B st B in A & x in Tarski-Class(X,B));

theorem :: CLASSES1:17
    A <> {} & A is_limit_ordinal & Y in Tarski-Class(X,A) &
   (Z c= Y or Z = bool Y) implies Z in Tarski-Class(X,A);

theorem :: CLASSES1:18
  Tarski-Class(X,A) c= Tarski-Class(X,succ A);

theorem :: CLASSES1:19
  A c= B implies Tarski-Class(X,A) c= Tarski-Class(X,B);

theorem :: CLASSES1:20
  ex A st Tarski-Class(X,A) = Tarski-Class(X,succ A);

theorem :: CLASSES1:21
  Tarski-Class(X,A) = Tarski-Class(X,succ A) implies
   Tarski-Class(X,A) = Tarski-Class X;

theorem :: CLASSES1:22
  ex A st Tarski-Class(X,A) = Tarski-Class X;

theorem :: CLASSES1:23
    ex A st Tarski-Class(X,A) = Tarski-Class X &
    for B st B in A holds Tarski-Class(X,B) <> Tarski-Class X;

theorem :: CLASSES1:24
    Y <> X & Y in Tarski-Class X implies
   ex A st not Y in Tarski-Class(X,A) & Y in Tarski-Class(X,succ A);

theorem :: CLASSES1:25
  X is epsilon-transitive implies
   for A st A <> {} holds Tarski-Class(X,A) is epsilon-transitive;

theorem :: CLASSES1:26
    Tarski-Class(X,{}) in Tarski-Class(X,one) &
   Tarski-Class(X,{}) <> Tarski-Class(X,one);

theorem :: CLASSES1:27
  X is epsilon-transitive implies Tarski-Class X is epsilon-transitive;

theorem :: CLASSES1:28
  Y in Tarski-Class X implies Card Y <` Card Tarski-Class X;

theorem :: CLASSES1:29
  Y in Tarski-Class X implies not Y,Tarski-Class X are_equipotent;

theorem :: CLASSES1:30
  x in Tarski-Class X & y in Tarski-Class X implies
   {x} in Tarski-Class X & {x,y} in Tarski-Class X;

theorem :: CLASSES1:31
  x in Tarski-Class X & y in Tarski-Class X implies [x,y] in
 Tarski-Class X;

theorem :: CLASSES1:32
   Y c= Tarski-Class X & Z c= Tarski-Class X implies [:Y,Z:] c= Tarski-Class X;

definition let A;
 func Rank(A) means
:: CLASSES1:def 6

   ex L st it = last L & dom L = succ A & L.{} = {} &
    (for C st succ C in succ A holds L.succ C = bool(L.C)) &
     for C st C in succ A & C <> {} & C is_limit_ordinal
           holds L.C = union rng(L|C);
end;

theorem :: CLASSES1:33
   Rank {} = {};

theorem :: CLASSES1:34
   Rank succ A = bool Rank A;

theorem :: CLASSES1:35
  A <> {} & A is_limit_ordinal implies
   for x holds x in Rank A iff ex B st B in A & x in Rank B;

theorem :: CLASSES1:36
  X c= Rank A iff X in Rank succ A;

theorem :: CLASSES1:37
  Rank A is epsilon-transitive;

theorem :: CLASSES1:38
  X in Rank A implies X c= Rank A;

theorem :: CLASSES1:39
    Rank A c= Rank succ A;

theorem :: CLASSES1:40
  union Rank A c= Rank A;

theorem :: CLASSES1:41
    X in Rank A implies union X in Rank A;

theorem :: CLASSES1:42
  A in B iff Rank A in Rank B;

theorem :: CLASSES1:43
  A c= B iff Rank A c= Rank B;

theorem :: CLASSES1:44
  A c= Rank A;

theorem :: CLASSES1:45
    for A,X st X in Rank A holds
  not X,Rank A are_equipotent & Card X <` Card Rank A;

theorem :: CLASSES1:46
    X c= Rank A iff bool X c= Rank succ A;

theorem :: CLASSES1:47
  X c= Y & Y in Rank A implies X in Rank A;

theorem :: CLASSES1:48
  X in Rank A iff bool X in Rank succ A;

theorem :: CLASSES1:49
  x in Rank A iff {x} in Rank succ A;

theorem :: CLASSES1:50
  x in Rank A & y in Rank A iff {x,y} in Rank succ A;

theorem :: CLASSES1:51
   x in Rank A & y in Rank A iff [x,y] in Rank succ succ A;

theorem :: CLASSES1:52
  X is epsilon-transitive &
  Rank A /\ Tarski-Class X = Rank succ A /\ Tarski-Class X implies
   Tarski-Class X c= Rank A;

theorem :: CLASSES1:53
  X is epsilon-transitive implies ex A st Tarski-Class X c= Rank A;

theorem :: CLASSES1:54
  X is epsilon-transitive implies union X c= X;

theorem :: CLASSES1:55
  X is epsilon-transitive & Y is epsilon-transitive implies
  X \/ Y is epsilon-transitive;

theorem :: CLASSES1:56
    X is epsilon-transitive & Y is epsilon-transitive implies
   X /\ Y is epsilon-transitive;

 reserve k,n for Nat;

definition let X;
 func the_transitive-closure_of X -> set means
:: CLASSES1:def 7

  x in it iff ex f,n st x in f.n & dom f = NAT & f.0 = X &
   for k holds f.(k+1) = union(f.k);
end;

canceled;

theorem :: CLASSES1:58
  the_transitive-closure_of X is epsilon-transitive;

theorem :: CLASSES1:59
  X c= the_transitive-closure_of X;

theorem :: CLASSES1:60
  X c= Y & Y is epsilon-transitive implies
  the_transitive-closure_of X c= Y;

theorem :: CLASSES1:61
  (for Z st X c= Z & Z is epsilon-transitive holds Y c= Z) & X c= Y &
   Y is epsilon-transitive implies the_transitive-closure_of X = Y;

theorem :: CLASSES1:62
  X is epsilon-transitive implies the_transitive-closure_of X = X;

theorem :: CLASSES1:63
   the_transitive-closure_of {} = {};

theorem :: CLASSES1:64
   the_transitive-closure_of A = A;

theorem :: CLASSES1:65
 X c= Y implies the_transitive-closure_of X c= the_transitive-closure_of Y;

theorem :: CLASSES1:66
   the_transitive-closure_of the_transitive-closure_of X =
   the_transitive-closure_of X;

theorem :: CLASSES1:67
   the_transitive-closure_of (X \/ Y) =
   the_transitive-closure_of X \/ the_transitive-closure_of Y;

theorem :: CLASSES1:68
   the_transitive-closure_of (X /\ Y) c=
   the_transitive-closure_of X /\ the_transitive-closure_of Y;

theorem :: CLASSES1:69
  ex A st X c= Rank A;

definition let X;
 func the_rank_of X -> Ordinal means
:: CLASSES1:def 8
   X c= Rank it & for B st X c= Rank B holds it c= B;
end;

canceled;

theorem :: CLASSES1:71
  the_rank_of bool X = succ the_rank_of X;

theorem :: CLASSES1:72
   the_rank_of Rank A = A;

theorem :: CLASSES1:73
  X c= Rank A iff the_rank_of X c= A;

theorem :: CLASSES1:74
  X in Rank A iff the_rank_of X in A;

theorem :: CLASSES1:75
   X c= Y implies the_rank_of X c= the_rank_of Y;

theorem :: CLASSES1:76
  X in Y implies the_rank_of X in the_rank_of Y;

theorem :: CLASSES1:77
  the_rank_of X c= A iff for Y st Y in X holds the_rank_of Y in A;

theorem :: CLASSES1:78
  A c= the_rank_of X iff for B st B in A ex Y st Y in
 X & B c= the_rank_of Y;

theorem :: CLASSES1:79
   the_rank_of X = {} iff X = {};

theorem :: CLASSES1:80
  the_rank_of X = succ A implies ex Y st Y in X & the_rank_of Y = A;

theorem :: CLASSES1:81
   the_rank_of A = A;

theorem :: CLASSES1:82
    the_rank_of Tarski-Class X <> {} &
   the_rank_of Tarski-Class X is_limit_ordinal;