CLASSES2

:: Universal Classes
::  by Bogdan Nowak and Grzegorz Bancerek
::
:: Received April 10, 1990
:: Copyright (c) 1990-2026 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;
 definitions TARSKI, CLASSES1, XBOOLE_0;
 equalities TARSKI, ORDINAL1;
 expansions TARSKI, ORDINAL1, CLASSES1, XBOOLE_0;
 theorems TARSKI, ZFMISC_1, SETFAM_1, ORDINAL1, WELLORD2, ORDINAL2, ORDINAL3,
      FUNCT_1, FUNCT_2, CARD_1, CLASSES1, CARD_2, FRAENKEL, CARD_3, RELAT_1,
      XBOOLE_1;
 schemes FUNCT_1, PARTFUN1, CARD_3, ORDINAL1, ORDINAL2, XBOOLE_0, CARD_2;

begin

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

Lm1: Tarski-Class X is Tarski
proof
  Tarski-Class X is_Tarski-Class_of X by CLASSES1:def 4;
  hence thesis;
end;

registration
  cluster Tarski -> subset-closed for set;
  coherence;
end;

registration
  let X be set;
  cluster Tarski-Class X -> Tarski;
  coherence by Lm1;
end;

theorem Th1:
  W is subset-closed & X in W implies not X,W are_equipotent & card X in card W
proof
  assume
A1: W is subset-closed;
  assume
A2: X in W;
  bool X c= W
  by A1,A2;
  then
A3: card bool X c= card W by CARD_1:11;
A4: card X in card bool X by CARD_1:14;
  then card X in card W by A3;
  then card X <> card W;
  hence thesis by A4,A3,CARD_1:5;
end;

theorem Th2:
  W is Tarski & x in W & y in W implies {x} in W & {x,y} in W
proof
  defpred C[object] means $1 = {};
  assume that
A1: W is Tarski and
A2: x in W and
A3: y in W;
A4: {x} c= bool x by ZFMISC_1:68;
  bool x in W by A1,A2;
  hence {x} in W by A1,A4,CLASSES1:def 1;
  then
A5: bool {x} in W by A1;
  deffunc g(object) = x;
  deffunc f(object) = y;
  consider f such that
A6: dom f = {{},{x}} &
for z being object st z in {{},{x}} holds (C[z] implies f.z =
  f(z)) & (not C[z] implies f.z = g(z)) from PARTFUN1:sch 1;
  {x,y} c= rng f
  proof
    let z be object;
A7: {} in {{},{x}} by TARSKI:def 2;
A8: {x} in {{},{x}} by TARSKI:def 2;
    assume z in {x,y};
    then z = x or z = y by TARSKI:def 2;
    then f.{} = z or f.{x} = z by A6,A7,A8;
    hence thesis by A6,A7,A8,FUNCT_1:def 3;
  end;
  then
A9: card {x,y} c= card {{},{x}} by A6,CARD_1:12;
A10: {x,y} c= W
  by A2,A3,TARSKI:def 2;
  bool {x} = {{},{x}} by ZFMISC_1:24;
  then card {{},{x}} in card W by A1,A5,Th1;
  then card {x,y} in card W by A9,ORDINAL1:12;
  hence thesis by A1,A10,CLASSES1:1;
end;

theorem Th3:
  W is Tarski & x in W & y in W implies [x,y] in W
proof
  assume
A1: W is Tarski;
  assume that
A2: x in W and
A3: y in W;
A4: {x} in W by A1,A2,Th2;
  {x,y} in W by A1,A2,A3,Th2;
  hence thesis by A1,A4,Th2;
end;

theorem Th4:
  W is Tarski & X in W implies Tarski-Class X c= W
proof
  assume that
A1: W is Tarski and
A2: X in W;
  reconsider D = W as non empty set by A2;
  D is_Tarski-Class_of X by A1,A2;
  hence thesis by CLASSES1:def 4;
end;

theorem Th5:
  W is Tarski & A in W implies succ A in W & A c= W
proof
  assume that
A1: for X,Y st X in W & Y c= X holds Y in W and
A2: for X st X in W holds bool X in W and
  for X st X c= W holds X,W are_equipotent or X in W and
A3: A in W;
  bool A in W by A2,A3;
  hence succ A in W by A1,ORDINAL2:3;
  let x be object;
  assume
A4: x in A;
  then reconsider B = x as Ordinal;
  B c= A by A4,ORDINAL1:def 2;
  hence thesis by A1,A3;
end;

theorem
  A in Tarski-Class W implies succ A in Tarski-Class W & A c=
  Tarski-Class W by Th5;

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

theorem
  X is epsilon-transitive & X in Tarski-Class W implies X c=
  Tarski-Class W by Th7;

theorem Th9:
  W is Tarski implies On W = card W
proof
  assume
A1: W is Tarski;
  now
    let X;
    assume
A2: X in On W;
    hence X is Ordinal by ORDINAL1:def 9;
    reconsider A = X as Ordinal by A2,ORDINAL1:def 9;
A3: X in W by A2,ORDINAL1:def 9;
    thus X c= On W
    proof
      let x be object;
      assume
A4:   x in X;
      then x in A;
      then reconsider B = x as Ordinal;
      B c= A by A4,ORDINAL1:def 2;
      then B in W by A1,A3,CLASSES1:def 1;
      hence thesis by ORDINAL1:def 9;
    end;
  end;
  then reconsider ON = On W as epsilon-transitive epsilon-connected set
   by ORDINAL1:19;
A5: now
    assume ON in W;
    then ON in ON by ORDINAL1:def 9;
    hence contradiction;
  end;
  ON c= W by ORDINAL2:7;
  then
A6: ON,W are_equipotent or ON in W by A1;
  now
    let A;
    assume that
A7: A,ON are_equipotent and
A8: not ON c= A;
    A in ON by A8,ORDINAL1:16;
    then A in W by ORDINAL1:def 9;
    hence contradiction by A1,A6,A5,A7,Th1,WELLORD2:15;
  end;
  then reconsider ON as Cardinal by CARD_1:def 1;
  ON = card ON;
  hence thesis by A6,A5,CARD_1:5;
end;

theorem
  On Tarski-Class W = card Tarski-Class W by Th9;

theorem Th11:
  W is Tarski & X in W implies card X in W
proof
  assume that
A1: W is Tarski and
A2: X in W;
A3: card W = On W by A1,Th9;
  card X in card W by A1,A2,Th1;
  hence thesis by A3,ORDINAL1:def 9;
end;

theorem
  X in Tarski-Class W implies card X in Tarski-Class W by Th11;

theorem Th13:
  W is Tarski & x in card W implies x in W
proof
  assume
A1: W is Tarski;
  assume x in card W;
  then x in On W by A1,Th9;
  hence thesis by ORDINAL1:def 9;
end;

theorem
  x in card Tarski-Class W implies x in Tarski-Class W by Th13;

theorem
  W is Tarski & m in card W implies m in W
proof
  assume
A1: W is Tarski;
  assume m in card W;
  then m in On W by A1,Th9;
  hence thesis by ORDINAL1:def 9;
end;

theorem
  m in card Tarski-Class W implies m in Tarski-Class W
proof
  assume m in card Tarski-Class W;
  then m in On Tarski-Class W by Th9;
  hence thesis by ORDINAL1:def 9;
end;

theorem
  W is Tarski & m in W implies m c= W by Th5;

theorem
  m in Tarski-Class W implies m c= Tarski-Class W by Th5;

theorem Th19:
  W is Tarski implies card W is limit_ordinal
proof
  assume
A1: W is Tarski;
  now
    let A;
    assume A in card W;
    then A in W by A1,Th13;
    then succ A in W by A1,Th5;
    then succ A in On W by ORDINAL1:def 9;
    hence succ A in card W by A1,Th9;
  end;
  hence thesis by ORDINAL1:28;
end;

theorem
  W is Tarski & W <> {} implies card W <> 0 & card W <> {} & card W is
  limit_ordinal by Th19;

theorem Th21:
  card Tarski-Class W <> 0 & card Tarski-Class W <> {} & card
  Tarski-Class W is limit_ordinal
proof
  thus card Tarski-Class W <> 0;
  thus card Tarski-Class W <> {};
  now
    let A;
    assume A in card Tarski-Class W;
    then A in Tarski-Class W by Th13;
    then succ A in Tarski-Class W by Th5;
    then succ A in On Tarski-Class W by ORDINAL1:def 9;
    hence succ A in card Tarski-Class W by Th9;
  end;
  hence thesis by ORDINAL1:28;
end;

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

theorem Th22:
  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
proof
  assume
A1: W is Tarski;
  assume that
A2: X in W & W is epsilon-transitive or X in W & X c= W or card X in
  card W & X c= W;
A3: card X in card W by A1,A2,Th1;
  let x be object;
  assume
A4: x in Funcs(X,W);
  then consider f such that
A5: x = f and
A6: dom f = X and
A7: rng f c= W by FUNCT_2:def 2;
A8: X c= W by A2;
A9: f c= W
  proof
    let y be object;
    assume
A10: y in f;
    then consider y1,y2 being object such that
A11: [y1,y2] = y by RELAT_1:def 1;
A12: y1 in dom f by A10,A11,FUNCT_1:1;
    y2 = f.y1 by A10,A11,FUNCT_1:1;
    then y2 in rng f by A12,FUNCT_1:def 3;
    hence thesis by A1,A8,A6,A7,A11,A12,Th3;
  end;
  card f = card X by A4,A5,CARD_2:3;
  hence thesis by A1,A3,A5,A9,CLASSES1:1;
end;

theorem
  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
proof
  assume that
A1: 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;
A2: card X in card Tarski-Class W by A1,CLASSES1:24;
  let x be object;
  assume
A3: x in Funcs(X,Tarski-Class W);
  then consider f such that
A4: x = f and
A5: dom f = X and
A6: rng f c= Tarski-Class W by FUNCT_2:def 2;
  W is epsilon-transitive implies Tarski-Class W is epsilon-transitive by
CLASSES1:23;
  then
A7: X c= Tarski-Class W by A1;
A8: f c= Tarski-Class W
  proof
    let y be object;
    assume
A9: y in f;
    then consider y1,y2 being object such that
A10: [y1,y2] = y by RELAT_1:def 1;
A11: y1 in dom f by A9,A10,FUNCT_1:1;
    y2 = f.y1 by A9,A10,FUNCT_1:1;
    then y2 in rng f by A11,FUNCT_1:def 3;
    hence thesis by A7,A5,A6,A10,A11,CLASSES1:27;
  end;
  card f = card X by A3,A4,CARD_2:3;
  hence thesis by A2,A4,A8,CLASSES1:6;
end;

theorem Th24:
  dom L is limit_ordinal & (for A st A in dom L holds L.A = Rank A)
  implies Rank dom L = Union L
proof
  assume that
A1: dom L is limit_ordinal and
A2: for A st A in dom L holds L.A = Rank A;
A3: union rng L = Union L by CARD_3:def 4;
  now
    thus Rank dom L c= Union L
    proof
      let x be object;
      assume x in Rank dom L;
      then consider A such that
A5:   A in dom L and
A6:   x in Rank A by A1,CLASSES1:31;
      L.A = Rank A by A2,A5;
      then Rank A in rng L by A5,FUNCT_1:def 3;
      hence thesis by A3,A6,TARSKI:def 4;
    end;
    thus Union L c= Rank dom L
    proof
      let x be object;
      assume x in Union L;
      then consider X such that
A7:   x in X and
A8:   X in rng L by A3,TARSKI:def 4;
      consider y being object such that
A9:   y in dom L and
A10:  X = L.y by A8,FUNCT_1:def 3;
      reconsider y as Ordinal by A9;
      X = Rank y by A2,A9,A10;
      hence thesis by A1,A7,A9,CLASSES1:31;
    end;
  end;
  hence thesis;
end;

defpred PQ[Ordinal] means W is Tarski & $1 in On W implies card Rank $1 in
card W & Rank $1 in W;

Lm2: PQ[0] by Th9,CLASSES1:29,ORDINAL1:def 9;

Lm3: PQ[A] implies PQ[succ A]
proof
  assume
A1: PQ[A];
A2: A in succ A by ORDINAL1:6;
  let W;
  assume that
A3: W is Tarski and
A4: succ A in On W;
  card W = On W by A3,Th9;
  then A in On W by A4,A2,ORDINAL1:10;
  then Rank A in W by A1,A3;
  then
A5: bool Rank A in W by A3;
  Rank succ A = bool Rank A by CLASSES1:30;
  hence thesis by A3,A5,Th1;
end;

Lm4: A <> 0 & A is limit_ordinal & (for B st B in A holds PQ[B]) implies PQ[A]
proof
  deffunc f(Ordinal) = Rank $1;
  assume that
 A <> 0 and
A2: A is limit_ordinal and
A3: for B st B in A holds PQ[B];
  let W;
  assume that
A4: W is Tarski and
A5: A in On W;
  consider L such that
A6: dom L = A & for B st B in A holds L.B = f(B) from ORDINAL2:sch 2;
  deffunc g(object) = card bool (L.$1);
  consider F such that
A7: dom F = A & for x being set st x in A holds F.x = g(x)
from CARD_3:sch 1;
A8: product F c= Funcs(A,W)
  proof
    let x be object;
    assume x in product F;
    then consider f such that
A9: x = f and
A10: dom f = dom F and
A11: for x being object st x in dom F holds f.x in F.x by CARD_3:def 5;
    rng f c= W
    proof
A12:  A in W by A5,ORDINAL1:def 9;
      let z be object;
      assume z in rng f;
      then consider y being object such that
A13:  y in dom f and
A14:  z = f.y by FUNCT_1:def 3;
      reconsider y as Ordinal by A7,A10,A13;
A15:  f.y in F.y by A10,A11,A13;
      y c= A by A7,A10,A13,ORDINAL1:def 2;
      then y in W by A4,A12,CLASSES1:def 1;
      then
A16:  y in On W by ORDINAL1:def 9;
      L.y = Rank y by A6,A7,A10,A13;
      then L.y in W by A3,A4,A7,A10,A13,A16;
      then bool (L.y) in W by A4;
      then
A17:  card bool (L.y) in W by A4,Th11;
      F.y = card bool (L.y) by A7,A10,A13;
      then F.y c= W by A4,A17,Th5;
      hence thesis by A14,A15;
    end;
    hence thesis by A7,A9,A10,FUNCT_2:def 2;
  end;
A18: Product F = card product F by CARD_3:def 8;
A19: A in W by A5,ORDINAL1:def 9;
  then A c= W by A4,Th5;
  then Funcs(A,W) c= W by A4,A19,Th22;
  then product F c= W by A8;
  then
A20: Product F c= card W by A18,CARD_1:11;
A21: for x being object st x in dom Card L holds (Card L).x in F.x
  proof
    let x be object;
A22: card (L.x) in card bool (L.x) by CARD_1:14;
    assume x in dom Card L;
    then
A23: x in dom L by CARD_3:def 2;
    then F.x = card bool (L.x) by A6,A7;
    hence thesis by A23,A22,CARD_3:def 2;
  end;
  dom Card L = dom L by CARD_3:def 2;
  then
A24: Sum Card L in Product F by A6,A7,A21,CARD_3:41;
A25: Rank A c= W
  proof
    let x be object;
    assume x in Rank A;
    then consider B such that
A26: B in A and
A27: x in Rank B by A2,CLASSES1:31;
    B c= A by A26,ORDINAL1:def 2;
    then B in W by A4,A19,CLASSES1:def 1;
    then B in On W by ORDINAL1:def 9;
    then Rank B c= W by A3,A4,A26,Th7;
    hence thesis by A27;
  end;
A28: Rank A = Union L by A2,A6,Th24;
  hence card Rank A in card W by A24,A20,CARD_3:39,ORDINAL1:12;
  card Rank A in Product F by A28,A24,CARD_3:39,ORDINAL1:12;
  hence thesis by A4,A20,A25,CLASSES1:1;
end;

theorem Th25:
  W is Tarski & A in On W implies card Rank A in card W & Rank A in W
proof
  PQ[B] from ORDINAL2:sch 1(Lm2,Lm3,Lm4);
  hence thesis;
end;

theorem
  A in On Tarski-Class W implies card Rank A in card Tarski-Class W &
  Rank A in Tarski-Class W by Th25;

theorem Th27:
  W is Tarski implies Rank card W c= W
proof
  assume
A1: W is Tarski;
  now
    thus thesis
    proof
A3:   card W is limit_ordinal by A1,Th19;
      let x be object;
      assume x in Rank card W;
      then consider A such that
A4:   A in card W and
A5:   x in Rank A by A3,CLASSES1:31;
      A in On W by A1,A4,Th9;
      then Rank A c= W by A1,Th7,Th25;
      hence thesis by A5;
    end;
  end;
  hence thesis;
end;

theorem Th28:
  Rank card Tarski-Class W c= Tarski-Class W
proof
A1: card Tarski-Class W is limit_ordinal by Th21;
  let x be object;
  assume x in Rank card Tarski-Class W;
  then consider A such that
A2: A in card Tarski-Class W and
A3: x in Rank A by A1,CLASSES1:31;
  A in On Tarski-Class W by A2,Th9;
  then Rank A c= Tarski-Class W by Th7,Th25;
  hence thesis by A3;
end;

deffunc f(object) = the_rank_of $1;
deffunc g(set) = card bool $1;

theorem Th29:
  W is Tarski & W is epsilon-transitive & X in W implies the_rank_of X in W
proof
  assume that
A1: W is Tarski and
A2: W is epsilon-transitive;
A3: On W = card W by A1,Th9;
  defpred P[Ordinal] means ex X st $1 = the_rank_of X & X in W & not $1 in W;
  assume that
A4: X in W and
A5: not the_rank_of X in W;
A6: ex A st P[A] by A4,A5;
  consider A such that
A7: P[A] and
A8: for B st P[B] holds A c= B from ORDINAL1:sch 1(A6);
  consider X such that
A9: A = the_rank_of X and
A10: X in W and
A11: not A in W by A7;
  defpred P[object] means ex Y st Y in X & $1 = the_rank_of Y;
  consider LL being set such that
A12: for x being object holds x in LL iff x in On W & P[x]
from XBOOLE_0:sch 1;
  consider ff being Cardinal-Function such that
A13: dom ff = LL & for x st x in LL holds ff.x = g(x) from CARD_3:sch 1;
A14: LL c= On W
  by A12;
A15: product ff c= Funcs(LL,W)
  proof
    let x be object;
    assume x in product ff;
    then consider g such that
A16: x = g and
A17: dom g = dom ff and
A18: for x being object st x in dom ff holds g.x in ff.x by CARD_3:def 5;
    rng g c= W
    proof
      let y be object;
      assume y in rng g;
      then consider x being object such that
A19:  x in dom g and
A20:  y = g.x by FUNCT_1:def 3;
      reconsider x as set by TARSKI:1;
A21:  ff.x = card bool x by A13,A17,A19;
      x in W by A14,A13,A17,A19,ORDINAL1:def 9;
      then bool x in W by A1;
      then card bool x in W by A1,Th11;
      then
A22:  card bool x c= W by A1,Th5;
      y in ff.x by A17,A18,A19,A20;
      hence thesis by A21,A22;
    end;
    hence thesis by A13,A16,A17,FUNCT_2:def 2;
  end;
  now
    let Z;
    assume Z in union LL;
    then consider Y such that
A23: Z in Y and
A24: Y in LL by TARSKI:def 4;
    Y in On W by A12,A24;
    then reconsider Y as Ordinal by ORDINAL1:def 9;
A25: Y c= union LL by A24,ZFMISC_1:74;
A26: Z in Y by A23;
    hence Z is Ordinal;
    reconsider A = Z as Ordinal by A26;
    A c= Y by A23,ORDINAL1:def 2;
    hence Z c= union LL by A25;
  end;
  then reconsider ULL = union LL as epsilon-transitive epsilon-connected set
by ORDINAL1:19;
A27: dom Card id LL = dom id LL by CARD_3:def 2;
A28: dom id LL = LL by RELAT_1:45;
  now
    let x be object;
    assume
A29: x in dom Card id LL;
    then
A30: (Card id LL).x = card ((id LL).x) by A27,CARD_3:def 2;
A31: (id LL).x = x by A28,A27,A29,FUNCT_1:18;
    reconsider xx=x as set by TARSKI:1;
    ff.x = card bool xx by A13,A28,A27,A29;
    hence (Card id LL).x in ff.x by A31,A30,CARD_1:14;
  end;
  then
A32: Sum Card id LL in Product ff by A13,A28,A27,CARD_3:41;
  Union id LL = union rng id LL by CARD_3:def 4
    .= ULL by RELAT_1:45;
  then
A33: card ULL in Product ff by A32,CARD_3:39,ORDINAL1:12;
  consider f such that
A34: dom f = X & for x being object st x in X holds f.x = f(x)
from FUNCT_1:sch 3;
  LL c= rng f
  proof
    let x be object;
    assume x in LL;
    then consider Y such that
A35: Y in X and
A36: x = the_rank_of Y by A12;
    f.Y = x by A34,A35,A36;
    hence thesis by A34,A35,FUNCT_1:def 3;
  end;
  then
A37: card LL c= card X by A34,CARD_1:12;
  card X in card W by A1,A10,Th1;
  then card LL <> card W by A37,ORDINAL1:12;
  then
A38: not LL,W are_equipotent by CARD_1:5;
A39: card product ff = Product ff by CARD_3:def 8;
A40: X c= W by A2,A10;
  X c= Rank card W
  proof
    let x be object;
            reconsider xx=x as set by TARSKI:1;
    assume
A41: x in X;
    then not A c= the_rank_of xx by A9,CLASSES1:68,ORDINAL1:5;
    then the_rank_of xx in W by A8,A40,A41;
    then the_rank_of xx in card W by A3,ORDINAL1:def 9;
    then
A42: Rank the_rank_of xx in Rank card W by CLASSES1:36;
    xx c= Rank the_rank_of xx by CLASSES1:def 9;
    hence thesis by A42,CLASSES1:41;
  end;
  then
A43: A c= On W by A9,A3,CLASSES1:65;
  On W c= ULL
  proof
    let x be object;
    assume
A44: x in On W;
    then reconsider B = x as Ordinal by ORDINAL1:def 9;
    now
      assume
A45:  for Y st Y in X holds the_rank_of Y c= B;
      X c= Rank succ B
      proof
        let y be object;
         reconsider yy=y as set by TARSKI:1;
        assume y in X;
        then the_rank_of yy c= B by A45;
        then the_rank_of yy in succ B by ORDINAL1:22;
        hence thesis by CLASSES1:66;
      end;
      then
A46:  A c= succ B by A9,CLASSES1:65;
      B in W by A44,ORDINAL1:def 9;
      then succ B in W by A1,Th5;
      hence contradiction by A1,A11,A46,CLASSES1:def 1;
    end;
    then consider Y such that
A47: Y in X and
A48: not the_rank_of Y c= B;
    the_rank_of Y in A by A9,A47,CLASSES1:68;
    then the_rank_of Y in LL by A43,A12,A47;
    then
A49: the_rank_of Y c= ULL by ZFMISC_1:74;
    B in the_rank_of Y by A48,ORDINAL1:16;
    hence thesis by A49;
  end;
  then
A50: card On W c= card ULL by CARD_1:11;
  On W c= W by ORDINAL2:7;
  then LL c= W by A14;
  then LL in W by A1,A38;
  then Funcs(LL,W) c= W by A1,A2,Th22;
  then product ff c= W by A15;
  then
A51: Product ff c= card W by A39,CARD_1:11;
  On W = card W by A1,Th9;
  hence contradiction by A33,A51,A50,CARD_1:4;
end;

theorem Th30:
  W is Tarski & W is epsilon-transitive implies W c= Rank card W
proof
  assume that
A1: W is Tarski and
A2: W is epsilon-transitive;
  let x be object;
            reconsider xx=x as set by TARSKI:1;
  assume x in W;
  then the_rank_of xx in W by A1,A2,Th29;
  then
A3: the_rank_of xx in On W by ORDINAL1:def 9;
  On W = card W by A1,Th9;
  then
A4: Rank the_rank_of xx in Rank card W by A3,CLASSES1:36;
  xx c= Rank the_rank_of xx by CLASSES1:def 9;
  hence thesis by A4,CLASSES1:41;
end;

theorem Th31:
  W is Tarski & W is epsilon-transitive implies Rank card W = W
by Th27,Th30;

theorem
  W is Tarski & A in On W implies card Rank A c= card W
proof
  assume that
A1: W is Tarski and
A2: A in On W;
  card Rank A in card W by A1,A2,Th25;
  hence thesis by CARD_1:3;
end;

theorem
  A in On Tarski-Class W implies card Rank A c= card Tarski-Class W
proof
  assume A in On Tarski-Class W;
  then card Rank A in card Tarski-Class W by Th25;
  hence thesis by CARD_1:3;
end;

theorem Th34:
  W is Tarski implies card W = card Rank card W
proof
  assume W is Tarski;
  then
A1: card Rank card W c= card W by Th27,CARD_1:11;
  card card W c= card Rank card W by CARD_1:11,CLASSES1:38;
  hence thesis by A1;
end;

theorem
  card Tarski-Class W = card Rank card Tarski-Class W by Th34;

theorem Th36:
  W is Tarski & X c= Rank card W implies X,Rank card W
  are_equipotent or X in Rank card W
proof
  assume that
A1: W is Tarski and
A2: X c= Rank card W and
A3: not X,Rank card W are_equipotent;
  defpred P[object] means ex Y st Y in X & $1 = the_rank_of Y;
  consider LL being set such that
A4: for x being object holds x in LL iff x in On W & P[x] from XBOOLE_0:sch 1;
  consider ff being Cardinal-Function such that
A5: dom ff = LL & for x st x in LL holds ff.x = g(x) from CARD_3:sch 1;
A6: LL c= On W
  by A4;
A7: product ff c= Funcs(LL,W)
  proof
    let x be object;
    assume x in product ff;
    then consider g such that
A8: x = g and
A9: dom g = dom ff and
A10: for x being object st x in dom ff holds g.x in ff.x by CARD_3:def 5;
    rng g c= W
    proof
      let y be object;
      assume y in rng g;
      then consider x being object such that
A11:  x in dom g and
A12:  y = g.x by FUNCT_1:def 3;
      reconsider x as set by TARSKI:1;
A13:  ff.x = card bool x by A5,A9,A11;
      x in W by A6,A5,A9,A11,ORDINAL1:def 9;
      then bool x in W by A1;
      then card bool x in W by A1,Th11;
      then
A14:  card bool x c= W by A1,Th5;
      y in ff.x by A9,A10,A11,A12;
      hence thesis by A13,A14;
    end;
    hence thesis by A5,A8,A9,FUNCT_2:def 2;
  end;
A15: card W = card Rank card W by A1,Th34;
  then
A16: card X <> card W by A3,CARD_1:5;
  On W c= W by ORDINAL2:7;
  then
A17: LL c= W by A6;
  now
    let Z;
    assume Z in union LL;
    then consider Y such that
A18: Z in Y and
A19: Y in LL by TARSKI:def 4;
    Y in On W by A4,A19;
    then reconsider Y as Ordinal by ORDINAL1:def 9;
A20: Y c= union LL by A19,ZFMISC_1:74;
A21: Z in Y by A18;
    hence Z is Ordinal;
    reconsider A = Z as Ordinal by A21;
    A c= Y by A18,ORDINAL1:def 2;
    hence Z c= union LL by A20;
  end;
  then reconsider ULL = union LL as epsilon-transitive epsilon-connected set
by ORDINAL1:19;
A22: dom Card id LL = dom id LL by CARD_3:def 2;
A23: dom id LL = LL by RELAT_1:45;
  now
    let x be object;
    assume
A24: x in dom Card id LL;
    then
A25: (Card id LL).x = card ((id LL).x) by A22,CARD_3:def 2;
A26: (id LL).x = x by A23,A22,A24,FUNCT_1:18;
    reconsider xx=x as set by TARSKI:1;
    ff.x = card bool xx by A5,A23,A22,A24;
    hence (Card id LL).x in ff.x by A26,A25,CARD_1:14;
  end;
  then
A27: Sum Card id LL in Product ff by A5,A23,A22,CARD_3:41;
  consider f such that
A28: dom f = X &
for x being object st x in X holds f.x = f(x) from FUNCT_1:sch 3;
  LL c= rng f
  proof
    let x be object;
    assume x in LL;
    then consider Y such that
A29: Y in X and
A30: x = the_rank_of Y by A4;
    f.Y = x by A28,A29,A30;
    hence thesis by A28,A29,FUNCT_1:def 3;
  end;
  then
A31: card LL c= card X by A28,CARD_1:12;
A32: card product ff = Product ff by CARD_3:def 8;
  card X c= card W by A2,A15,CARD_1:11;
  then card X in card W by A16,CARD_1:3;
  then card LL <> card W by A31,ORDINAL1:12;
  then not LL,W are_equipotent by CARD_1:5;
  then LL in W by A1,A17;
  then Funcs(LL,W) c= W by A1,A17,Th22;
  then product ff c= W by A7;
  then
A33: Product ff c= card W by A32,CARD_1:11;
A34: card W is limit_ordinal by A1,Th19;
A35: card W = On W by A1,Th9;
  X c= Rank succ ULL
  proof
    let x be object;
            reconsider xx=x as set by TARSKI:1;
    defpred P[Ordinal] means $1 in card W & xx c= Rank $1;
    assume
A36: x in X;
    then
A37: f.x = the_rank_of xx by A28;
    consider A such that
A38: A in card W and
A39: x in Rank A by A2,A34,A36,CLASSES1:31;
    P[A] by A38,A39,ORDINAL1:def 2;
    then
A40: ex A st P[A];
    consider A such that
A41: P[A] and
A42: for B st P[B] holds A c= B from ORDINAL1:sch 1(A40);
    now
      let B;
      assume xx c= Rank B;
      then A c= card W & card W c= B or A c= B by A41,A42,ORDINAL1:16;
      hence A c= B;
    end;
    then A = the_rank_of xx by A41,CLASSES1:def 9;
    then f.x in LL by A4,A35,A36,A37,A41;
    then the_rank_of xx c= ULL by A37,ZFMISC_1:74;
    then
A43: Rank the_rank_of xx c= Rank ULL by CLASSES1:37;
    xx c= Rank the_rank_of xx by CLASSES1:def 9;
    then xx c= Rank ULL by A43;
    hence thesis by CLASSES1:32;
  end;
  then
A44: X in Rank succ succ ULL by CLASSES1:32;
  Union id LL = union rng id LL by CARD_3:def 4
    .= ULL by RELAT_1:45;
  then card ULL in card W by A27,A33,CARD_3:39,ORDINAL1:12;
  then
A45: ULL <> On W by A35;
  union card W = card W by A34;
  then ULL c= On W by A6,A35,ZFMISC_1:77;
  then ULL c< On W by A45;
  then ULL in card W by A35,ORDINAL1:11;
  then succ ULL in card W by A34,ORDINAL1:28;
  then succ succ ULL in card W by A34,ORDINAL1:28;
  hence thesis by A34,A44,CLASSES1:31;
end;

theorem
  X c= Rank card Tarski-Class W implies X,Rank card Tarski-Class W
  are_equipotent or X in Rank card Tarski-Class W by Th36;

theorem Th38:
  W is Tarski implies Rank card W is Tarski
proof
  assume
A1: W is Tarski;
  set B = Rank card W;
  thus for X,Y holds X in B & Y c= X implies Y in B by CLASSES1:41;
  now
A2: card W is limit_ordinal by A1,Th19;
    thus for X holds X in B implies bool X in B
    proof
      let X;
      assume X in B;
      then consider A such that
A4:   A in card W and
A5:   X in Rank A by A2,CLASSES1:31;
A6:   bool X in Rank succ A by A5,CLASSES1:42;
      succ A in card W by A2,A4,ORDINAL1:28;
      hence thesis by A2,A6,CLASSES1:31;
    end;
  end;
  hence thesis by A1,Th36;
end;

theorem
  Rank card Tarski-Class W is Tarski by Th38;

theorem Th40:
  X is epsilon-transitive & A in the_rank_of X implies
  ex Y st Y in X & the_rank_of Y = A
proof
  assume that
A1: X is epsilon-transitive and
A2: A in the_rank_of X;
  defpred P[Ordinal] means ex Y st A in $1 & Y in X & the_rank_of Y = $1;
  assume
A3: not thesis;
A4: ex B st P[B]
  proof
    assume
A5: for B,Y st A in B & Y in X holds the_rank_of Y <> B;
    X c= Rank A
    proof
      let x be object;
      reconsider xx=x as set by TARSKI:1;
      assume
A6:   x in X;
      then
A7:   the_rank_of xx <> A by A3;
      the_rank_of xx c= A by A5,A6,ORDINAL1:16;
      then the_rank_of xx c< A by A7;
      then the_rank_of xx in A by ORDINAL1:11;
      hence thesis by CLASSES1:66;
    end;
    then the_rank_of X c= A by CLASSES1:65;
    hence contradiction by A2,ORDINAL1:5;
  end;
  consider B such that
A8: P[B] and
A9: for C st P[C] holds B c= C from ORDINAL1:sch 1(A4);
  consider Y such that
A10: A in B and
A11: Y in X and
A12: the_rank_of Y = B by A8;
  Y c= Rank A
  proof
    let x be object;
            reconsider xx=x as set by TARSKI:1;
A13: Y c= X by A1,A11;
    assume
A14: x in Y;
    then the_rank_of xx in B by A12,CLASSES1:68;
    then not A in the_rank_of xx by A9,A14,A13,ORDINAL1:5;
    then
A15: the_rank_of xx c= A by ORDINAL1:16;
    the_rank_of xx <> A by A3,A14,A13;
    then the_rank_of xx c< A by A15;
    then the_rank_of xx in A by ORDINAL1:11;
    hence thesis by CLASSES1:66;
  end;
  then the_rank_of Y c= A by CLASSES1:65;
  hence contradiction by A10,A12,ORDINAL1:5;
end;

theorem Th41:
  X is epsilon-transitive implies card the_rank_of X c= card X
proof
  consider f such that
A1: dom f = X &
for x being object st x in X holds f.x = f(x) from FUNCT_1:sch 3;
  assume
A2: X is epsilon-transitive;
  the_rank_of X c= rng f
  proof
    let x be object;
    assume
A3: x in the_rank_of X;
    then reconsider x9 = x as Ordinal;
    consider Y such that
A4: Y in X and
A5: the_rank_of Y = x9 by A2,A3,Th40;
    f.Y = x by A1,A4,A5;
    hence thesis by A1,A4,FUNCT_1:def 3;
  end;
  hence thesis by A1,CARD_1:12;
end;

theorem Th42:
  W is Tarski & X is epsilon-transitive & X in W implies X in Rank card W
proof
  assume
A1: W is Tarski;
  assume
A2: X is epsilon-transitive;
  assume X in W;
  then card X in card W by A1,Th1;
  then
A3: card the_rank_of X in card W by A2,Th41,ORDINAL1:12;
  card card W = card W;
  then the_rank_of X in card W by A3,CARD_3:43;
  then
A4: Rank the_rank_of X in Rank card W by CLASSES1:36;
  X c= Rank the_rank_of X by CLASSES1:def 9;
  hence thesis by A4,CLASSES1:41;
end;

theorem
  X is epsilon-transitive & X in Tarski-Class W implies X in Rank card
  Tarski-Class W by Th42;

theorem Th44:
  W is epsilon-transitive implies Rank card Tarski-Class W is_Tarski-Class_of W
by CLASSES1:2,Th38,Th42;

theorem
  W is epsilon-transitive implies Rank card Tarski-Class W = Tarski-Class W
proof
  assume W is epsilon-transitive;
  then Rank card Tarski-Class W is_Tarski-Class_of W by Th44;
  hence Rank card Tarski-Class W c= Tarski-Class W & Tarski-Class W c= Rank
  card Tarski-Class W by Th28,CLASSES1:def 4;
end;

definition
  let IT be set;
  attr IT is universal means

  IT is epsilon-transitive & IT is Tarski;
end;

registration
  cluster universal -> epsilon-transitive Tarski for set;
  coherence;
  cluster epsilon-transitive Tarski -> universal for set;
  coherence;
end;

registration
  cluster universal non empty for set;
  existence
  proof
    set X = the set;
    take V = Tarski-Class the_transitive-closure_of X;
    thus V is epsilon-transitive by CLASSES1:23;
    thus thesis;
  end;
end;

definition
  mode Universe is universal non empty set;
end;

reserve U1,U2,U for Universe;

theorem Th46:
  On U is Ordinal
proof
  On U = card U by Th9;
  hence thesis;
end;

theorem Th47:
  X is epsilon-transitive implies Tarski-Class X is universal
by CLASSES1:23;

theorem
  Tarski-Class U is Universe by Th47;

registration
  let U;
  cluster On U -> ordinal;
  coherence by Th46;
  cluster Tarski-Class U -> universal;
  coherence by Th47;
end;

theorem Th49:
  Tarski-Class A is universal
by CLASSES1:23;

registration
  let A;
  cluster Tarski-Class A -> universal;
  coherence by Th49;
end;

theorem Th50:
  U = Rank On U
proof
  card U = On U by Th9;
  hence thesis by Th31;
end;

theorem Th51:
  On U <> {} & On U is limit_ordinal
proof
  card U = On U by Th9;
  hence thesis by Th19;
end;

theorem
  U1 in U2 or U1 = U2 or U2 in U1
proof
A1: On U1 in On U2 or On U1 = On U2 or On U2 in On U1 by ORDINAL1:14;
A2: U2 = Rank On U2 by Th50;
  U1 = Rank On U1 by Th50;
  hence thesis by A1,A2,CLASSES1:36;
end;

theorem Th53:
  U1 c= U2 or U2 in U1
proof
A1: On U1 c= On U2 or On U2 in On U1 by ORDINAL1:16;
A2: U2 = Rank On U2 by Th50;
  U1 = Rank On U1 by Th50;
  hence thesis by A1,A2,CLASSES1:36,37;
end;

theorem Th54:
  U1,U2 are_c=-comparable
proof
A1: On U1 c= On U2 or On U2 c= On U1;
A2: U2 = Rank On U2 by Th50;
  U1 = Rank On U1 by Th50;
  hence U1 c= U2 or U2 c= U1 by A1,A2,CLASSES1:37;
end;

theorem
  U1 \/ U2 is Universe & U1 /\ U2 is Universe
proof
  U1,U2 are_c=-comparable by Th54;
  then U1 c= U2 or U2 c= U1;
  hence thesis by XBOOLE_1:12,28;
end;

theorem Th56:
  {} in U
proof
  {} c= the Element of U;
  hence thesis by CLASSES1:def 1;
end;

theorem
  x in U implies {x} in U by Th2;

theorem
  x in U & y in U implies {x,y} in U & [x,y] in U by Th2,Th3;

theorem Th59:
  X in U implies bool X in U & union X in U & meet X in U
proof
  assume
A1: X in U;
  hence bool X in U by CLASSES1:def 2;
  U = Rank On U by Th50;
  hence
A2: union X in U by A1,CLASSES1:35;
  meet X c= union X by SETFAM_1:2;
  hence thesis by A2,CLASSES1:def 1;
end;

theorem Th60:
  X in U & Y in U implies X \/ Y in U & X /\ Y in U & X \ Y in U & X \+\ Y in U
proof
  assume that
A1: X in U and
A2: Y in U;
A3: union {X,Y} = X \/ Y by ZFMISC_1:75;
A4: meet {X,Y} = X /\ Y by SETFAM_1:11;
  {X,Y} in U by A1,A2,Th2;
  hence
A5: X \/ Y in U & X /\ Y in U by A3,A4,Th59;
  X \+\ Y = (X \/ Y)\(X /\ Y) by XBOOLE_1:101;
  hence thesis by A1,A5,CLASSES1:def 1;
end;

theorem Th61:
  X in U & Y in U implies [:X,Y:] in U & Funcs(X,Y) in U
proof
  assume that
A1: X in U and
A2: Y in U;
  X \/ Y in U by A1,A2,Th60;
  then bool(X \/ Y) in U by Th59;
  then
A3: bool bool(X \/ Y) in U by Th59;
  [:X,Y:] c= bool bool(X \/ Y) by ZFMISC_1:86;
  hence [:X,Y:] in U by A3,CLASSES1:def 1;
  then
A4: bool [:X,Y:] in U by Th59;
  Funcs(X,Y) c= bool [:X,Y:] by FRAENKEL:2;
  hence thesis by A4,CLASSES1:def 1;
end;

reserve u,v for Element of U;

registration
  let U1;
  cluster non empty for Element of U1;
  existence
  proof
    {} in U1 by Th56;
    then reconsider x = bool {} as Element of U1 by Th59;
    take x;
    thus thesis;
  end;
end;

definition
  let U,u;
  redefine func {u} -> Element of U;  :: redefines { (TARSKI, definition)
  coherence by Th2;
  redefine func bool u -> Element of U;  :: redefines bool (ZFMISC_1, definition)
  coherence by Th59;
  redefine func union u -> Element of U;  :: redefines union (TARSKI, definition)
  coherence by Th59;
  redefine func meet u -> Element of U;  :: redefines meet (SETFAM_1, definition)
  coherence by Th59;
  let v;
  redefine func {u,v} -> Element of U;  :: redefines { (TARSKI, definition)
  coherence by Th2;
  redefine func [u,v] -> Element of U;  :: redefines [ (TARSKI, definition)
  coherence by Th3;
  redefine func u \/ v -> Element of U;  :: redefines \/ (XBOOLE_0, definition)
  coherence by Th60;
  redefine func u /\ v -> Element of U;  :: redefines /\ (XBOOLE_0, definition)
  coherence by Th60;
  redefine func u \ v -> Element of U;  :: redefines \ (XBOOLE_0, definition)
  coherence by Th60;
  redefine func u \+\ v -> Element of U;  :: redefines \+\ (XBOOLE_0, definition)
  coherence by Th60;
  redefine func [:u,v:] -> Element of U;  :: redefines [: (ZFMISC_1, definition)
  coherence by Th61;
  redefine func Funcs(u,v) -> Element of U;  :: redefines Funcs (FUNCT_2, definition)
  coherence by Th61;
end;

definition
  func FinSETS -> Universe equals
  Tarski-Class {};
  correctness;
end;

Lm5: omega is limit_ordinal by ORDINAL1:def 11;

theorem Th62:
  card Rank omega = card omega
proof
  deffunc h(Ordinal) = Rank $1;
  consider L such that
A1: dom L = omega & for A st A in omega holds L.A = h(A) from ORDINAL2:
  sch 2;
  now
    let X,Y;
    assume X in rng L;
    then consider x being object such that
A2: x in dom L and
A3: X = L.x by FUNCT_1:def 3;
    assume Y in rng L;
    then consider y being object such that
A4: y in dom L and
A5: Y = L.y by FUNCT_1:def 3;
    reconsider x,y as Ordinal by A2,A4;
A6: Y = Rank y by A1,A4,A5;
A7: x c= y or y c= x;
    X = Rank x by A1,A2,A3;
    then X c= Y or Y c= X by A6,A7,CLASSES1:37;
    hence X,Y are_c=-comparable;
  end;
  then
A8: rng L is c=-linear;
A9: card omega c= card Rank omega by CARD_1:11,CLASSES1:38;
A10: now
    let X;
    assume X in rng L;
    then consider x being object such that
A11: x in dom L and
A12: X = L.x by FUNCT_1:def 3;
    reconsider x as Ordinal by A11;
    X = Rank x by A1,A11,A12;
    hence card X in card omega by A1,A11,CARD_2:67,CARD_3:42;
  end;
  Rank omega = Union L by A1,Lm5,Th24
    .= union rng L by CARD_3:def 4;
  then card Rank omega c= card omega by A8,A10,CARD_3:46;
  hence thesis by A9;
end;

theorem Th63:
  Rank omega is Tarski
proof
  thus X in Rank omega & Y c= X implies Y in Rank omega by CLASSES1:41;
  thus X in Rank omega implies bool X in Rank omega
  proof
    assume X in Rank omega;
    then consider A such that
A1: A in omega and
A2: X in Rank A by Lm5,CLASSES1:31;
A3: bool X in Rank succ A by A2,CLASSES1:42;
    succ A in omega by A1,Lm5,ORDINAL1:28;
    hence thesis by A3,Lm5,CLASSES1:31;
  end;
  thus X c= Rank omega implies X,Rank omega are_equipotent or X in Rank omega
  proof
A4: 0 in omega;
    defpred P[object,object] means the_rank_of $2 c= the_rank_of $1;
    assume that
A5: X c= Rank omega and
A6: not X,Rank omega are_equipotent and
A7: not X in Rank omega;
A8: card X <> card omega by A6,Th62,CARD_1:5;
    card X c= card omega by A5,Th62,CARD_1:11;
    then card X in omega by A8,CARD_1:3;
    then reconsider X as finite set;
A9: for x,y being object holds P[x,y] or P[y,x];
A10: for x,y,z being object st P[x,y] & P[y,z] holds P[x,z] by XBOOLE_1:1;
    omega c= Rank omega by CLASSES1:38;
    then
A11: X <> {} by A7,A4;
    consider x being object such that
A12: x in X &
     for y being object st y in X holds P[x,y] from CARD_2:sch 2(A11,A9,A10);
    set A = the_rank_of x;
    for Y st Y in X holds the_rank_of Y in succ A by A12,ORDINAL1:22;
    then
A13: the_rank_of X c= succ A by CLASSES1:69;
    A in omega by A5,A12,CLASSES1:66;
    then succ A in omega by Lm5,ORDINAL1:28;
    then the_rank_of X in omega by A13,ORDINAL1:12;
    hence thesis by A7,CLASSES1:66;
  end;
end;

theorem
  FinSETS = Rank omega
proof
A1: omega c= Rank omega by CLASSES1:38;
  then reconsider M = Rank omega as non empty set;
  0 in omega;
  then M is_Tarski-Class_of {} by A1,Th63;
  hence FinSETS c= Rank omega by CLASSES1:def 4;
A2: {} in On FinSETS by Th51,ORDINAL3:8;
A3: FinSETS = Rank On FinSETS by Th50;
  On FinSETS is limit_ordinal by Th51;
  then omega c= On FinSETS by A2,ORDINAL1:def 11;
  hence thesis by A3,CLASSES1:37;
end;

definition
  func SETS -> Universe equals
  Tarski-Class FinSETS;
  correctness;
end;

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

registration
  let X be epsilon-transitive set;
  cluster Tarski-Class X -> epsilon-transitive;
  coherence by CLASSES1:23;
end;

definition
  let X be set;
  func Universe_closure X -> Universe means
  :Def4:
  X c= it & for Y being Universe st X c= Y holds it c= Y;
  uniqueness;
  existence
  proof
    per cases;
    suppose
      Rank the_rank_of X is Universe;
      then reconsider R = Rank the_rank_of X as Universe;
      take R;
      thus X c= R by CLASSES1:def 9;
      let Y be Universe;
      assume X c= Y;
      then the_rank_of X c= the_rank_of Y by CLASSES1:67;
      then
A1:   R c= Rank the_rank_of Y by CLASSES1:37;
A2:   Rank card Y = Y by Th31;
      then the_rank_of Y c= card Y by CLASSES1:def 9;
      then Rank the_rank_of Y c= Y by A2,CLASSES1:37;
      hence thesis by A1;
    end;
    suppose
A3:   Rank the_rank_of X is not Universe;
      take R = Tarski-Class Rank the_rank_of X;
A4:   Rank the_rank_of X in R by CLASSES1:2;
      X c= Rank the_rank_of X by CLASSES1:def 9;
      then X in R by A4,CLASSES1:def 1;
      hence X c= R by ORDINAL1:def 2;
      let Y be Universe;
      assume X c= Y;
      then
A5:   the_rank_of X c= the_rank_of Y by CLASSES1:67;
A6:   Rank card Y = Y by Th31;
      then
A7:   the_rank_of Y c= card Y by CLASSES1:def 9;
      Y c= Rank the_rank_of Y by CLASSES1:def 9;
      then card Y c= the_rank_of Y by A6,CLASSES1:37;
      then card Y = the_rank_of Y by A7;
      then the_rank_of X c< card Y by A3,A5,A6;
      then the_rank_of X in card Y by ORDINAL1:11;
      then Rank the_rank_of X in Y by A6,CLASSES1:36;
      then Y is_Tarski-Class_of Rank the_rank_of X;
      hence thesis by CLASSES1:def 4;
    end;
  end;
end;

deffunc C(Ordinal,set) = Tarski-Class $2;
deffunc D(Ordinal,Sequence) = Universe_closure Union $2;

definition
  mode FinSet is Element of FinSETS;
  mode Set is Element of SETS;
  let A;
  func UNIVERSE A -> set means
  : Def5:
  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);
  correctness
  proof
    (ex x being object,
   L st x = last L & dom L = succ A & L.0 = FinSETS & (for C st
succ C in succ A holds L.succ C = C(C,L.C)) & for C st C in succ A & C <> 0 &
C is limit_ordinal holds L.C = D(C,L|C) ) & for x1,x2 being set st (ex L st x1
= last L & dom L = succ A & L.0 = FinSETS & (for C st succ C in succ A holds L
.succ C = C(C,L.C)) & for C st C in succ A & C <> 0 & C is limit_ordinal holds
L.C = D(C,L|C) ) & (ex L st x2 = last L & dom L = succ A & L.0 = FinSETS & (
for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C in succ A & C
<> 0 & C is limit_ordinal holds L.C = D(C,L|C) ) holds x1 = x2 from ORDINAL2:
    sch 7;
   hence thesis;
  end;
end;

deffunc u(Ordinal) = UNIVERSE $1;

Lm6: now
A1: for A for x being object
  holds x = u(A) iff ex L st x = last L & dom L = succ A & L.0 =
FinSETS & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C in
  succ A & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C) by Def5;
  thus u(0) = FinSETS from ORDINAL2:sch 8(A1);
  thus for A holds u(succ A) = C(A,u(A)) from ORDINAL2:sch 9(A1);
  let A,L;
  assume that
A2: A <> 0 & A is limit_ordinal and
A3: dom L = A and
A4: for B st B in A holds L.B = u(B);
  thus u(A) = D(A,L) from ORDINAL2:sch 10(A1,A2,A3,A4);
end;

registration
  let A;
  cluster UNIVERSE A -> universal non empty;
  coherence
  proof
    defpred P[Ordinal] means UNIVERSE $1 is Universe;
A1: P[B] implies P[succ B]
    proof
      assume P[B];
      then reconsider UU = UNIVERSE B as Universe;
      UNIVERSE succ B = Tarski-Class UU by Lm6;
      hence thesis;
    end;
A2: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B]
    holds P[A]
    proof
      let A such that
A3:   A <> 0 and
A4:   A is limit_ordinal and
      for B st B in A holds P[B];
      consider L such that
A5:   dom L = A & for B st B in A holds L.B = u(B) from ORDINAL2:sch 2;
      UNIVERSE A = Universe_closure Union L by A3,A4,A5,Lm6
        .= Universe_closure union rng L by CARD_3:def 4;
      hence thesis;
    end;
A6: P[0] by Lm6;
    for A holds P[A] from ORDINAL2:sch 1(A6,A1,A2);
    hence thesis;
  end;
end;

theorem
  UNIVERSE {} = FinSETS by Lm6;

theorem
  UNIVERSE succ A = Tarski-Class UNIVERSE A by Lm6;

Lm7: 1 = succ 0;

theorem
  UNIVERSE 1 = SETS by Lm6,Lm7;

theorem
  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 by Lm6;

theorem
  FinSETS c= U & Tarski-Class {} c= U & UNIVERSE {} c= U
proof
A1: On U c= Rank On U by CLASSES1:38;
A2: Rank On U = U by Th50;
  {} in On U by Th51,ORDINAL3:8;
  hence thesis by A2,A1,Lm6,Th4;
end;

theorem Th70:
  A in B iff UNIVERSE A in UNIVERSE B
proof
  defpred P[Ordinal] means for A st A in $1 holds UNIVERSE A in UNIVERSE $1;
A1: for B st P[B] holds P[succ B]
  proof
    let B such that
A2: P[B];
    let A;
    assume
A3: A in succ B;
    A c< B iff A c= B & A <> B;
    then A in B or A = B by A3,ORDINAL1:11,22;
    then
A4: UNIVERSE A in UNIVERSE B or UNIVERSE A = UNIVERSE B by A2;
    UNIVERSE succ B = Tarski-Class UNIVERSE B by Lm6;
    then UNIVERSE B in UNIVERSE succ B by CLASSES1:2;
    hence thesis by A4,ORDINAL1:10;
  end;
A5: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B]
  holds P[A]
  proof
    let B;
    assume that
A6: B <> 0 and
A7: B is limit_ordinal and
    for C st C in B for A st A in C holds UNIVERSE A in UNIVERSE C;
    let A;
    consider L such that
A8: dom L = B & for C st C in B holds L.C = u(C) from ORDINAL2:sch 2;
    assume A in B;
    then
A9: succ A in B by A7,ORDINAL1:28;
    then L.succ A = UNIVERSE succ A by A8;
    then UNIVERSE succ A in rng L by A9,A8,FUNCT_1:def 3;
    then
A10: UNIVERSE succ A c= union rng L by ZFMISC_1:74;
    UNIVERSE B = Universe_closure Union L by A6,A7,A8,Lm6
      .= Universe_closure union rng L by CARD_3:def 4;
    then union rng L c= UNIVERSE B by Def4;
    then
A11: UNIVERSE succ A c= UNIVERSE B by A10;
A12: UNIVERSE A in Tarski-Class UNIVERSE A by CLASSES1:2;
    UNIVERSE succ A = Tarski-Class UNIVERSE A by Lm6;
    hence thesis by A12,A11;
  end;
A13: P[0];
A14: for B holds P[B] from ORDINAL2:sch 1(A13,A1,A5);
  hence A in B implies UNIVERSE A in UNIVERSE B;
  assume that
A15: UNIVERSE A in UNIVERSE B and
A16: not A in B;
  B in A or B = A by A16,ORDINAL1:16;
  hence contradiction by A14,A15;
end;

theorem
  UNIVERSE A = UNIVERSE B implies A = B
proof
  assume that
A1: UNIVERSE A = UNIVERSE B and
A2: A <> B;
  A in B or B in A by A2,ORDINAL1:14;
  then UNIVERSE A in UNIVERSE B or UNIVERSE B in UNIVERSE A by Th70;
  hence contradiction by A1;
end;

theorem
  A c= B iff UNIVERSE A c= UNIVERSE B
proof
  thus A c= B implies UNIVERSE A c= UNIVERSE B
  proof
    assume
A1: A c= B;
    assume not UNIVERSE A c= UNIVERSE B;
    then UNIVERSE B in UNIVERSE A by Th53;
    then B in A by Th70;
    hence contradiction by A1,ORDINAL1:5;
  end;
  assume
A2: UNIVERSE A c= UNIVERSE B;
  assume not A c= B;
  then B in A by ORDINAL1:16;
  then UNIVERSE B in UNIVERSE A by Th70;
  hence contradiction by A2,ORDINAL1:5;
end;

reserve u,v for Element of Tarski-Class(X);

theorem
  Tarski-Class(X,{}) in Tarski-Class(X,1) &
  Tarski-Class(X,{}) <> Tarski-Class(X,1)
proof
  deffunc F(Ordinal) = Tarski-Class(X,$1);
  deffunc C(Ordinal,set) = { u : ex v st v in $2 & u c= v } \/
  { bool v : v in $2 } \/ bool $2 /\ Tarski-Class X;
  deffunc D(Ordinal,Sequence) = (union rng $2) /\ Tarski-Class X;
A1: for A for x being object holds x = F(A) iff
  ex L st x = last L & dom L = succ A & L.0 = { X } &
  (for C st succ C in succ A holds L.succ C = C(C,L.C)) &
  for C st C in succ A & C <> 0 & C is limit_ordinal
  holds L.C = D(C,L|C) by CLASSES1:def 5;
A2: F(0) = { X } from ORDINAL2:sch 8(A1);
  then X in Tarski-Class(X,{}) by TARSKI:def 1;
  then
A3: bool X in Tarski-Class X by CLASSES1:4;
 { X } c= bool X
  proof
    let x be object;
    assume x in { X };
then  x = X by TARSKI:def 1;
    hence thesis by ZFMISC_1:def 1;
  end;
then  1 = succ 0 & { X } in Tarski-Class X by A3,CLASSES1:3;
  thus
then A4: Tarski-Class(X,{}) in Tarski-Class(X,1) by A2,CLASSES1:10;
  assume Tarski-Class(X,{}) = Tarski-Class(X,1);
  hence contradiction by A4;
end;