Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Universal Classes

by
Bogdan Nowak, and
Grzegorz Bancerek

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;

```