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

Tarski's Classes and Ranks

by
Grzegorz Bancerek

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;
```