:: CLASSES2 semantic presentation

K97() is set

bool K97() is non empty set

bool omega is non empty non finite set

X is set
Tarski-Class X is non empty set
X is set
X is set
Tarski-Class X is non empty set
X is set

x is set

bool x is non empty Element of bool (bool x)
bool x is non empty set
bool (bool x) is non empty set
B is set

X is set
x is set
{x} is non empty trivial 1 -element set
B is set
{x,B} is non empty set
bool x is non empty Element of bool (bool x)
bool x is non empty set
bool (bool x) is non empty set
bool {x} is non empty Element of bool ()
bool {x} is non empty set
bool () is non empty set
{{},{x}} is non empty set

dom A is set
rng A is set
L is set
A . {} is set
A . {x} is set

L is set

X is set
x is set
B is set
[x,B] is set
{x,B} is non empty set
{x} is non empty trivial 1 -element set
{{x,B},{x}} is non empty set
X is set
x is set

B is non empty set

{X} is non empty trivial 1 -element set
X \/ {X} is non empty set
x is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
B is set

x is set

{X} is non empty trivial 1 -element set
X \/ {X} is non empty set
X is set
x is set
B is set
X is set
x is set

X is set
On X is set

x is set
A is set

X is set

On () is set

X is set
x is set

On X is set
X is set
x is set

X is set

x is set
On X is set
X is set
x is set

x is set

On x is set

x is set

On () is set
x is set

x is set

X is set

{x} is non empty trivial 1 -element set
x \/ {x} is non empty set
On X is set

X is set

X is set

{x} is non empty trivial 1 -element set
x \/ {x} is non empty set
On () is set
X is set

x is set

Funcs (x,X) is set
B is set

dom A is set
rng A is set
L is set
x is set
y is set
[x,y] is set
{x,y} is non empty set
{x} is non empty trivial 1 -element set
{{x,y},{x}} is non empty set
A . x is set

X is set

x is set

Funcs (X,()) is non empty FUNCTION_DOMAIN of X, Tarski-Class x
B is set

dom A is set
rng A is set
L is set
x is set
y is set
[x,y] is set
{x,y} is non empty set
{x} is non empty trivial 1 -element set
{{x,y},{x}} is non empty set
A . x is set

Union X is set
rng X is set
union (rng X) is set
x is set

X . B is set
x is set
B is set
A is set
X . A is set

X is set
On X is set

{X} is non empty trivial 1 -element set
X \/ {X} is non empty set

x is set
On x is set

bool (Rank X) is non empty Element of bool (bool (Rank X))
bool (Rank X) is non empty set
bool (bool (Rank X)) is non empty set

x is set
On x is set

dom A is set
product A is set
Funcs (X,x) is set
L is set

dom x is set
rng x is set
y is set
A is set
x . A is set

x . A is set
A . A is set
B . A is set

bool (B . A) is non empty Element of bool (bool (B . A))
bool (B . A) is non empty set
bool (bool (B . A)) is non empty set
card (bool (B . A)) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

dom (Card B) is set
L is set
(Card B) . L is set
A . L is set
B . L is set

bool (B . L) is non empty Element of bool (bool (B . L))
bool (B . L) is non empty set
bool (bool (B . L)) is non empty set
card (bool (B . L)) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

L is set

Union B is set

x is set
On x is set

x is set

On () is set

X is set

x is set

On X is set
X is set

x is set

On () is set
X is set
x is set

On X is set

A is set

A is set

L is set

dom x is set
y is set
product x is set
Funcs (L,X) is set
y is set

dom A is set
rng A is set
A is set
B is set
A . B is set
x . B is set
bool B is non empty Element of bool (bool B)
bool B is non empty set
bool (bool B) is non empty set

y is set
union L is set
A is set

dom (Card (id L)) is set
dom (id L) is set
A is set
(Card (id L)) . A is set
(id L) . A is set

x . A is set
bool A is non empty Element of bool (bool A)
bool A is non empty set
bool (bool A) is non empty set

Union (id L) is set
rng (id L) is set
union (rng (id L)) is set

dom A is set
rng A is set
A is set
B is set

A . B is set

A is set

A is set

{B} is non empty trivial 1 -element set
B \/ {B} is non empty set

Y is set

Y is set

Y is set

X is set

x is set

On X is set

X is set

x is set
On x is set

x is set

On () is set

X is set

X is set

X is set

x is set
On X is set
B is set

dom A is set
L is set
product A is set
Funcs (B,X) is set
L is set

dom x is set
rng x is set
y is set
A is set
x . A is set
A . A is set
bool A is non empty Element of bool (bool A)
bool A is non empty set
bool (bool A) is non empty set

L is set
union B is set
x is set

dom (Card (id B)) is set
dom (id B) is set
x is set
(Card (id B)) . x is set
(id B) . x is set

A . x is set
bool x is non empty Element of bool (bool x)
bool x is non empty set
bool (bool x) is non empty set

dom x is set
rng x is set
y is set
A is set

x . A is set

{L} is non empty trivial 1 -element set
L \/ {L} is non empty set

y is set
x . y is set

{(succ L)} is non empty trivial 1 -element set
(succ L) \/ {(succ L)} is non empty set
Rank (succ (succ L)) is epsilon-transitive set
Union (id B) is set
rng (id B) is set
union (rng (id B)) is set

X is set
x is set

X is set

B is set
A is set
B is set
bool B is non empty Element of bool (bool B)
bool B is non empty set
bool (bool B) is non empty set

{A} is non empty trivial 1 -element set
A \/ {A} is non empty set

B is set
bool B is non empty Element of bool (bool B)
bool B is non empty set
bool (bool B) is non empty set
A is set
X is set

x is set

B is set

A is set

A is set

L is set

X is set

dom x is set
rng x is set
B is set

L is set

x . L is set
X is set

x is set

X is set
x is set

X is set

X is set

X is set
X is set
the set is set

Tarski-Class () is non empty subset-closed Tarski set
x is non empty subset-closed Tarski set

On X is set

X is set

On X is set

X \/ x is non empty set
X /\ x is set

the Element of X is Element of X
X is set

{X} is non empty trivial 1 -element set
X is set

x is set
{X,x} is non empty set
[X,x] is set
{X} is non empty trivial 1 -element set
{{X,x},{X}} is non empty set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
union X is set
meet X is set

X is set
x is set
X \/ x is set
X /\ x is set
X \ x is Element of bool X
bool X is non empty set
X \+\ x is set
X \ x is set
x \ X is set
(X \ x) \/ (x \ X) is set

{X,x} is non empty set
union {X,x} is set
meet {X,x} is set
(X \/ x) \ (X /\ x) is Element of bool (X \/ x)
bool (X \/ x) is non empty set
X is set
x is set
[:X,x:] is set
Funcs (X,x) is set

X \/ x is set
bool (X \/ x) is non empty Element of bool (bool (X \/ x))
bool (X \/ x) is non empty set
bool (bool (X \/ x)) is non empty set
bool (bool (X \/ x)) is non empty Element of bool (bool (bool (X \/ x)))
bool (bool (X \/ x)) is non empty set
bool (bool (bool (X \/ x))) is non empty set
bool [:X,x:] is non empty Element of bool (bool [:X,x:])
bool [:X,x:] is non empty set
bool (bool [:X,x:]) is non empty set

bool {} is non empty Element of bool ()
bool {} is non empty set
bool () is non empty set
x is Element of X

x is Element of X
{x} is non empty trivial 1 -element set
bool x is non empty set
union x is set
meet x is set
B is Element of X
{x,B} is non empty set
[x,B] is set
{{x,B},{x}} is non empty set
x \/ B is set
x /\ B is set
x \ B is set
x \+\ B is set
B \ x is set
(x \ B) \/ (B \ x) is set
[:x,B:] is set
Funcs (x,B) is set

() is non empty epsilon-transitive subset-closed Tarski () set

x is set
rng X is set
A is set
X . A is set
B is set
L is set
X . L is set

x is set
B is set
X . B is set

Union X is set
union (rng X) is set
X is set
x is set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set

{x} is non empty trivial 1 -element set
x \/ {x} is non empty set

X is set

A is set

B is set

A is set

B is set

L is set

x is finite set
B is set

L is set

{()} is non empty trivial 1 -element set
() \/ {()} is non empty set

X is non empty set

Rank (On ()) is epsilon-transitive set

() is non empty epsilon-transitive subset-closed Tarski () set
X is set

X is set

{X} is non empty trivial 1 -element set
X \/ {X} is non empty set
x is set

(X) is set

{X} is non empty trivial 1 -element set
X \/ {X} is non empty set
A is set

last L is set

{B} is non empty trivial 1 -element set
B \/ {B} is non empty set
L . {} is set
(B) is set
({}) is set

(X) is set
Union x is set
(()) is non empty epsilon-transitive subset-closed Tarski () set

(X) is set

(x) is set

{x} is non empty trivial 1 -element set
x \/ {x} is non empty set
((succ x)) is set

(x) is set

Union B is set
(()) is non empty epsilon-transitive subset-closed Tarski () set
rng B is set
union (rng B) is set
((union (rng B))) is non empty epsilon-transitive subset-closed Tarski () set

{X} is non empty trivial 1 -element set
X \/ {X} is non empty set
((succ X)) is non empty epsilon-transitive subset-closed Tarski () set
(X) is non empty epsilon-transitive subset-closed Tarski () set

is non empty trivial 1 -element set
0 \/ is non empty set
(1) is non empty epsilon-transitive subset-closed Tarski () set

(X) is non empty epsilon-transitive subset-closed Tarski () set
Union x is set
(()) is non empty epsilon-transitive subset-closed Tarski () set

(X) is non empty epsilon-transitive subset-closed Tarski () set

(x) is non empty epsilon-transitive subset-closed Tarski () set

(B) is non empty epsilon-transitive subset-closed Tarski () set

{B} is non empty trivial 1 -element set
B \/ {B} is non empty set
((succ B)) is non empty epsilon-transitive subset-closed Tarski () set

(A) is non empty epsilon-transitive subset-closed Tarski () set

(B) is non empty epsilon-transitive subset-closed Tarski () set

(A) is non empty epsilon-transitive subset-closed Tarski () set

{A} is non empty trivial 1 -element set
A \/ {A} is non empty set
L . (succ A) is set
((succ A)) is non empty epsilon-transitive subset-closed Tarski () set
rng L is set
union (rng L) is set
Union L is set
(()) is non empty epsilon-transitive subset-closed Tarski () set
((union (rng L))) is non empty epsilon-transitive subset-closed Tarski () set

(B) is non empty epsilon-transitive subset-closed Tarski () set

(X) is non empty epsilon-transitive subset-closed Tarski () set

(x) is non empty epsilon-transitive subset-closed Tarski () set

(X) is non empty epsilon-transitive subset-closed Tarski () set

(x) is non empty epsilon-transitive subset-closed Tarski () set
X is set
Tarski-Class (X,{}) is Element of bool ()

bool () is non empty set
Tarski-Class (X,1) is Element of bool ()
{ b1 where b1 is Element of Tarski-Class X : ex b2 being Element of Tarski-Class X st
( b2 in a2 & b1 c= b2 )
}
is set

{ (bool b1) where b1 is Element of Tarski-Class X : b1 in a2 } is set
{ b1 where b1 is Element of Tarski-Class X : ex b2 being Element of Tarski-Class X st
( b2 in a2 & b1 c= b2 )
}
\/ { (bool b1) where b1 is Element of Tarski-Class X : b1 in a2 } is set

{X} is non empty trivial 1 -element set
B is set

Tarski-Class (X,x) is Element of bool ()

{x} is non empty trivial 1 -element set
x \/ {x} is non empty set
L is set

last x is set

{A} is non empty trivial 1 -element set
A \/ {A} is non empty set
x . {} is set
Tarski-Class (X,A) is Element of bool ()
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
x is set