:: CLASSES2 semantic presentation

K97() is set

K101() is non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of bool K97()

bool K97() is non empty set

omega is non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set

bool omega is non empty non finite set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional finite cardinal {} -element set

the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional finite cardinal {} -element set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional finite cardinal {} -element set

1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal Element of K101()

union {} is epsilon-transitive epsilon-connected ordinal set

card {} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional finite cardinal {} -element set

card omega is non empty epsilon-transitive epsilon-connected ordinal non finite cardinal set

Rank {} is epsilon-transitive 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

card X is epsilon-transitive epsilon-connected ordinal cardinal set

x is set

card x is epsilon-transitive epsilon-connected ordinal cardinal 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

card (bool x) is non empty epsilon-transitive epsilon-connected ordinal cardinal 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})

bool {x} is non empty set

bool (bool {x}) is non empty set

{{},{x}} is non empty set

A is Relation-like Function-like set

dom A is set

rng A is set

L is set

A . {} is set

A . {x} is set

card {x,B} is non empty epsilon-transitive epsilon-connected ordinal cardinal set

card {{},{x}} is non empty epsilon-transitive epsilon-connected ordinal cardinal set

L is set

card X is epsilon-transitive epsilon-connected ordinal cardinal 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

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

B is non empty set

X is epsilon-transitive epsilon-connected ordinal set

succ X is non empty epsilon-transitive epsilon-connected ordinal 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

A is epsilon-transitive epsilon-connected ordinal set

X is epsilon-transitive epsilon-connected ordinal set

x is set

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

succ X is non empty epsilon-transitive epsilon-connected ordinal 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

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

X is set

On X is set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

x is set

A is set

B is epsilon-transitive epsilon-connected ordinal set

L is epsilon-transitive epsilon-connected ordinal set

x is epsilon-transitive epsilon-connected ordinal set

B is epsilon-transitive epsilon-connected ordinal set

B is epsilon-transitive epsilon-connected ordinal cardinal set

card B is epsilon-transitive epsilon-connected ordinal cardinal set

X is set

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

On (Tarski-Class X) is set

card (Tarski-Class X) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

X is set

x is set

card x is epsilon-transitive epsilon-connected ordinal cardinal set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

On X is set

X is set

x is set

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

card X is epsilon-transitive epsilon-connected ordinal cardinal set

X is set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

x is set

On X is set

X is set

x is set

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

card (Tarski-Class x) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

X is epsilon-transitive epsilon-connected ordinal cardinal set

x is set

card x is epsilon-transitive epsilon-connected ordinal cardinal set

On x is set

X is epsilon-transitive epsilon-connected ordinal cardinal set

x is set

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

card (Tarski-Class x) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

On (Tarski-Class x) is set

x is set

X is epsilon-transitive epsilon-connected ordinal cardinal set

X is epsilon-transitive epsilon-connected ordinal cardinal set

x is set

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

X is set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

x is epsilon-transitive epsilon-connected ordinal set

succ x is non empty epsilon-transitive epsilon-connected ordinal set

{x} is non empty trivial 1 -element set

x \/ {x} is non empty set

On X is set

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional finite cardinal {} -element Element of K101()

X is set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

X is set

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

card (Tarski-Class X) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

x is epsilon-transitive epsilon-connected ordinal set

succ x is non empty epsilon-transitive epsilon-connected ordinal set

{x} is non empty trivial 1 -element set

x \/ {x} is non empty set

On (Tarski-Class X) is set

X is set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

x is set

card x is epsilon-transitive epsilon-connected ordinal cardinal set

Funcs (x,X) is set

B is set

A is Relation-like Function-like 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

card A is epsilon-transitive epsilon-connected ordinal cardinal set

X is set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

x is set

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

card (Tarski-Class x) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

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

B is set

A is Relation-like Function-like 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

card A is epsilon-transitive epsilon-connected ordinal cardinal set

X is Relation-like T-Sequence-like Function-like set

dom X is epsilon-transitive epsilon-connected ordinal set

Rank (dom X) is epsilon-transitive set

Union X is set

rng X is set

union (rng X) is set

x is set

B is epsilon-transitive epsilon-connected ordinal set

Rank B is epsilon-transitive set

X . B is set

x is set

B is set

A is set

X . A is set

L is epsilon-transitive epsilon-connected ordinal set

Rank L is epsilon-transitive set

card (Rank {}) is epsilon-transitive epsilon-connected ordinal cardinal set

X is set

On X is set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

X is epsilon-transitive epsilon-connected ordinal set

Rank X is epsilon-transitive set

card (Rank X) is epsilon-transitive epsilon-connected ordinal cardinal set

succ X is non empty epsilon-transitive epsilon-connected ordinal set

{X} is non empty trivial 1 -element set

X \/ {X} is non empty set

Rank (succ X) is epsilon-transitive set

card (Rank (succ X)) is epsilon-transitive epsilon-connected ordinal cardinal set

x is set

On x is set

card x is epsilon-transitive epsilon-connected ordinal cardinal 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 epsilon-transitive epsilon-connected ordinal set

Rank X is epsilon-transitive set

card (Rank X) is epsilon-transitive epsilon-connected ordinal cardinal set

x is set

On x is set

card x is epsilon-transitive epsilon-connected ordinal cardinal set

B is Relation-like T-Sequence-like Function-like set

dom B is epsilon-transitive epsilon-connected ordinal set

A is Relation-like Function-like Cardinal-yielding set

dom A is set

product A is set

Funcs (X,x) is set

L is set

x is Relation-like Function-like set

dom x is set

rng x is set

y is set

A is set

x . A is set

A is epsilon-transitive epsilon-connected ordinal set

x . A is set

A . A is set

B . A is set

Rank A is epsilon-transitive 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

Product A is epsilon-transitive epsilon-connected ordinal cardinal set

card (product A) is epsilon-transitive epsilon-connected ordinal cardinal set

Card B is Relation-like Function-like Cardinal-yielding set

dom (Card B) is set

L is set

(Card B) . L is set

A . L is set

B . L is set

card (B . L) is epsilon-transitive epsilon-connected ordinal cardinal 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

Sum (Card B) is epsilon-transitive epsilon-connected ordinal cardinal set

L is set

x is epsilon-transitive epsilon-connected ordinal set

Rank x is epsilon-transitive set

Union B is set

X is epsilon-transitive epsilon-connected ordinal set

Rank X is epsilon-transitive set

card (Rank X) is epsilon-transitive epsilon-connected ordinal cardinal set

x is set

On x is set

card x is epsilon-transitive epsilon-connected ordinal cardinal set

X is epsilon-transitive epsilon-connected ordinal set

x is set

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

On (Tarski-Class x) is set

Rank X is epsilon-transitive set

card (Rank X) is epsilon-transitive epsilon-connected ordinal cardinal set

card (Tarski-Class x) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

X is set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

Rank (card X) is epsilon-transitive set

x is set

B is epsilon-transitive epsilon-connected ordinal set

Rank B is epsilon-transitive set

On X is set

X is set

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

card (Tarski-Class X) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

Rank (card (Tarski-Class X)) is epsilon-transitive set

x is set

B is epsilon-transitive epsilon-connected ordinal set

Rank B is epsilon-transitive set

On (Tarski-Class X) is set

X is set

x is set

the_rank_of x is epsilon-transitive epsilon-connected ordinal set

On X is set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

B is epsilon-transitive epsilon-connected ordinal set

A is set

the_rank_of A is epsilon-transitive epsilon-connected ordinal set

A is set

the_rank_of A is epsilon-transitive epsilon-connected ordinal set

L is set

x is Relation-like Function-like Cardinal-yielding set

dom x is set

y is set

product x is set

Funcs (L,X) is set

y is set

A is Relation-like Function-like 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

card (bool B) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

y is set

union L is set

A is set

A is epsilon-transitive epsilon-connected ordinal set

B is epsilon-transitive epsilon-connected ordinal set

id L is Relation-like Function-like one-to-one set

Card (id L) is Relation-like Function-like Cardinal-yielding 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

card ((id L) . A) is epsilon-transitive epsilon-connected ordinal cardinal 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

card (bool A) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

Sum (Card (id L)) is epsilon-transitive epsilon-connected ordinal cardinal set

Product x is epsilon-transitive epsilon-connected ordinal cardinal set

Union (id L) is set

rng (id L) is set

union (rng (id L)) is set

y is epsilon-transitive epsilon-connected ordinal set

card y is epsilon-transitive epsilon-connected ordinal cardinal set

A is Relation-like Function-like set

dom A is set

rng A is set

A is set

B is set

the_rank_of B is epsilon-transitive epsilon-connected ordinal set

A . B is set

card L is epsilon-transitive epsilon-connected ordinal cardinal set

card A is epsilon-transitive epsilon-connected ordinal cardinal set

card (product x) is epsilon-transitive epsilon-connected ordinal cardinal set

Rank (card X) is epsilon-transitive set

A is set

the_rank_of A is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of A) is epsilon-transitive set

A is set

B is epsilon-transitive epsilon-connected ordinal set

succ B is non empty epsilon-transitive epsilon-connected ordinal set

{B} is non empty trivial 1 -element set

B \/ {B} is non empty set

Rank (succ B) is epsilon-transitive set

Y is set

the_rank_of Y is epsilon-transitive epsilon-connected ordinal set

Y is set

the_rank_of Y is epsilon-transitive epsilon-connected ordinal set

Y is set

the_rank_of Y is epsilon-transitive epsilon-connected ordinal set

card (On X) is epsilon-transitive epsilon-connected ordinal cardinal set

X is set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

Rank (card X) is epsilon-transitive set

x is set

the_rank_of x is epsilon-transitive epsilon-connected ordinal set

On X is set

Rank (the_rank_of x) is epsilon-transitive set

X is set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

Rank (card X) is epsilon-transitive set

X is epsilon-transitive epsilon-connected ordinal set

Rank X is epsilon-transitive set

card (Rank X) is epsilon-transitive epsilon-connected ordinal cardinal set

x is set

On x is set

card x is epsilon-transitive epsilon-connected ordinal cardinal set

X is epsilon-transitive epsilon-connected ordinal set

Rank X is epsilon-transitive set

card (Rank X) is epsilon-transitive epsilon-connected ordinal cardinal set

x is set

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

On (Tarski-Class x) is set

card (Tarski-Class x) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

X is set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

Rank (card X) is epsilon-transitive set

card (Rank (card X)) is epsilon-transitive epsilon-connected ordinal cardinal set

card (card X) is epsilon-transitive epsilon-connected ordinal cardinal set

X is set

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

card (Tarski-Class X) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

Rank (card (Tarski-Class X)) is epsilon-transitive set

card (Rank (card (Tarski-Class X))) is epsilon-transitive epsilon-connected ordinal cardinal set

X is set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

Rank (card X) is epsilon-transitive set

x is set

On X is set

B is set

A is Relation-like Function-like Cardinal-yielding set

dom A is set

L is set

product A is set

Funcs (B,X) is set

L is set

x is Relation-like Function-like 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

card (bool A) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

card (Rank (card X)) is epsilon-transitive epsilon-connected ordinal cardinal set

card x is epsilon-transitive epsilon-connected ordinal cardinal set

L is set

union B is set

x is set

y is epsilon-transitive epsilon-connected ordinal set

A is epsilon-transitive epsilon-connected ordinal set

id B is Relation-like Function-like one-to-one set

Card (id B) is Relation-like Function-like Cardinal-yielding 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

card ((id B) . x) is epsilon-transitive epsilon-connected ordinal cardinal 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

card (bool x) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

Sum (Card (id B)) is epsilon-transitive epsilon-connected ordinal cardinal set

Product A is epsilon-transitive epsilon-connected ordinal cardinal set

x is Relation-like Function-like set

dom x is set

rng x is set

y is set

A is set

the_rank_of A is epsilon-transitive epsilon-connected ordinal set

x . A is set

card B is epsilon-transitive epsilon-connected ordinal cardinal set

card (product A) is epsilon-transitive epsilon-connected ordinal cardinal set

L is epsilon-transitive epsilon-connected ordinal set

succ L is non empty epsilon-transitive epsilon-connected ordinal set

{L} is non empty trivial 1 -element set

L \/ {L} is non empty set

Rank (succ L) is epsilon-transitive set

y is set

x . y is set

the_rank_of y is epsilon-transitive epsilon-connected ordinal set

A is epsilon-transitive epsilon-connected ordinal set

Rank A is epsilon-transitive set

A is epsilon-transitive epsilon-connected ordinal set

Rank A is epsilon-transitive set

B is epsilon-transitive epsilon-connected ordinal set

Rank B is epsilon-transitive set

Rank (the_rank_of y) is epsilon-transitive set

Rank L is epsilon-transitive set

succ (succ L) is non empty epsilon-transitive epsilon-connected ordinal 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

card L is epsilon-transitive epsilon-connected ordinal cardinal set

union (card X) is epsilon-transitive epsilon-connected ordinal set

X is set

x is set

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

card (Tarski-Class x) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

Rank (card (Tarski-Class x)) is epsilon-transitive set

X is set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

Rank (card X) is epsilon-transitive 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 epsilon-transitive epsilon-connected ordinal set

Rank A is epsilon-transitive set

succ A is non empty epsilon-transitive epsilon-connected ordinal set

{A} is non empty trivial 1 -element set

A \/ {A} is non empty set

Rank (succ A) is epsilon-transitive 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

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

card (Tarski-Class X) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

Rank (card (Tarski-Class X)) is epsilon-transitive set

X is epsilon-transitive epsilon-connected ordinal set

x is set

the_rank_of x is epsilon-transitive epsilon-connected ordinal set

Rank X is epsilon-transitive set

B is set

the_rank_of B is epsilon-transitive epsilon-connected ordinal set

B is epsilon-transitive epsilon-connected ordinal set

A is set

the_rank_of A is epsilon-transitive epsilon-connected ordinal set

A is set

the_rank_of A is epsilon-transitive epsilon-connected ordinal set

Rank X is epsilon-transitive set

L is set

the_rank_of L is epsilon-transitive epsilon-connected ordinal set

X is set

the_rank_of X is epsilon-transitive epsilon-connected ordinal set

card (the_rank_of X) is epsilon-transitive epsilon-connected ordinal cardinal set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

x is Relation-like Function-like set

dom x is set

rng x is set

B is set

A is epsilon-transitive epsilon-connected ordinal set

L is set

the_rank_of L is epsilon-transitive epsilon-connected ordinal set

x . L is set

X is set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

Rank (card X) is epsilon-transitive set

x is set

card x is epsilon-transitive epsilon-connected ordinal cardinal set

the_rank_of x is epsilon-transitive epsilon-connected ordinal set

card (the_rank_of x) is epsilon-transitive epsilon-connected ordinal cardinal set

card (card X) is epsilon-transitive epsilon-connected ordinal cardinal set

Rank (the_rank_of x) is epsilon-transitive set

X is set

x is set

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

card (Tarski-Class x) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

Rank (card (Tarski-Class x)) is epsilon-transitive set

X is set

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

card (Tarski-Class X) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

Rank (card (Tarski-Class X)) is epsilon-transitive set

X is set

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

card (Tarski-Class X) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

Rank (card (Tarski-Class X)) is epsilon-transitive set

X is set

X is set

the set is set

the_transitive-closure_of the set is set

Tarski-Class (the_transitive-closure_of the set ) is non empty subset-closed Tarski set

x is non empty subset-closed Tarski set

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

On X is set

card X is non empty epsilon-transitive epsilon-connected ordinal cardinal set

X is set

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

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

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

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

On X is set

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

X is epsilon-transitive epsilon-connected ordinal set

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

X is epsilon-transitive epsilon-connected ordinal set

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

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

On X is epsilon-transitive epsilon-connected ordinal set

Rank (On X) is epsilon-transitive set

card X is non empty epsilon-transitive epsilon-connected ordinal cardinal set

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

On X is epsilon-transitive epsilon-connected ordinal set

card X is non empty epsilon-transitive epsilon-connected ordinal cardinal set

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

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

On X is epsilon-transitive epsilon-connected ordinal set

On x is epsilon-transitive epsilon-connected ordinal set

Rank (On x) is epsilon-transitive set

Rank (On X) is epsilon-transitive set

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

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

On X is epsilon-transitive epsilon-connected ordinal set

On x is epsilon-transitive epsilon-connected ordinal set

Rank (On x) is epsilon-transitive set

Rank (On X) is epsilon-transitive set

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

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

On X is epsilon-transitive epsilon-connected ordinal set

On x is epsilon-transitive epsilon-connected ordinal set

Rank (On x) is epsilon-transitive set

Rank (On X) is epsilon-transitive set

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

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

X \/ x is non empty set

X /\ x is set

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

the Element of X is Element of X

X is set

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

{X} is non empty trivial 1 -element set

X is set

B is non empty epsilon-transitive subset-closed Tarski () 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 non empty epsilon-transitive subset-closed Tarski () set

On x is epsilon-transitive epsilon-connected ordinal set

Rank (On x) is epsilon-transitive 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

B is non empty epsilon-transitive subset-closed Tarski () 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

B is non empty epsilon-transitive subset-closed Tarski () 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

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

bool {} is non empty Element of bool (bool {})

bool {} is non empty set

bool (bool {}) is non empty set

x is Element of X

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

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

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

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

Rank omega is epsilon-transitive set

card (Rank omega) is epsilon-transitive epsilon-connected ordinal cardinal set

X is Relation-like T-Sequence-like Function-like set

dom X is epsilon-transitive epsilon-connected ordinal 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

y is epsilon-transitive epsilon-connected ordinal set

Rank y is epsilon-transitive set

x is epsilon-transitive epsilon-connected ordinal set

Rank x is epsilon-transitive set

x is set

B is set

X . B is set

A is epsilon-transitive epsilon-connected ordinal set

Rank A is epsilon-transitive set

card x is epsilon-transitive epsilon-connected ordinal cardinal 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 epsilon-transitive epsilon-connected ordinal set

Rank x is epsilon-transitive set

succ x is non empty epsilon-transitive epsilon-connected ordinal set

{x} is non empty trivial 1 -element set

x \/ {x} is non empty set

Rank (succ x) is epsilon-transitive set

X is set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

A is set

the_rank_of A is epsilon-transitive epsilon-connected ordinal set

B is set

the_rank_of B is epsilon-transitive epsilon-connected ordinal set

A is set

the_rank_of A is epsilon-transitive epsilon-connected ordinal set

B is set

the_rank_of B is epsilon-transitive epsilon-connected ordinal set

L is set

the_rank_of L is epsilon-transitive epsilon-connected ordinal set

x is finite set

B is set

the_rank_of B is epsilon-transitive epsilon-connected ordinal set

L is set

the_rank_of L is epsilon-transitive epsilon-connected ordinal set

succ (the_rank_of B) is non empty epsilon-transitive epsilon-connected ordinal set

{(the_rank_of B)} is non empty trivial 1 -element set

(the_rank_of B) \/ {(the_rank_of B)} is non empty set

the_rank_of x is epsilon-transitive epsilon-connected ordinal set

X is non empty set

On () is epsilon-transitive epsilon-connected ordinal set

Rank (On ()) is epsilon-transitive set

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

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

X is set

the_transitive-closure_of X is set

X is epsilon-transitive set

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

X is set

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

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

the_rank_of X is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of X) is epsilon-transitive set

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

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

the_rank_of B is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of B) is epsilon-transitive set

card B is non empty epsilon-transitive epsilon-connected ordinal cardinal set

Rank (card B) is epsilon-transitive set

the_rank_of X is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of X) is epsilon-transitive set

Tarski-Class (Rank (the_rank_of 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

the_rank_of B is epsilon-transitive epsilon-connected ordinal set

card B is non empty epsilon-transitive epsilon-connected ordinal cardinal set

Rank (card B) is epsilon-transitive set

Rank (the_rank_of B) is epsilon-transitive set

the_rank_of X is epsilon-transitive epsilon-connected ordinal set

Rank (the_rank_of X) is epsilon-transitive set

X is epsilon-transitive epsilon-connected ordinal set

succ X is non empty epsilon-transitive epsilon-connected ordinal set

{X} is non empty trivial 1 -element set

X \/ {X} is non empty set

x is set

X is epsilon-transitive epsilon-connected ordinal set

(X) is set

succ X is non empty epsilon-transitive epsilon-connected ordinal set

{X} is non empty trivial 1 -element set

X \/ {X} is non empty set

A is set

L is Relation-like T-Sequence-like Function-like set

last L is set

dom L is epsilon-transitive epsilon-connected ordinal set

B is epsilon-transitive epsilon-connected ordinal set

succ B is non empty epsilon-transitive epsilon-connected ordinal 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 epsilon-transitive epsilon-connected ordinal set

x is Relation-like T-Sequence-like Function-like set

dom x is epsilon-transitive epsilon-connected ordinal set

(X) is set

Union x is set

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

X is epsilon-transitive epsilon-connected ordinal set

(X) is set

x is epsilon-transitive epsilon-connected ordinal set

(x) is set

succ x is non empty epsilon-transitive epsilon-connected ordinal set

{x} is non empty trivial 1 -element set

x \/ {x} is non empty set

((succ x)) is set

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

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

x is epsilon-transitive epsilon-connected ordinal set

(x) is set

B is Relation-like T-Sequence-like Function-like set

dom B is epsilon-transitive epsilon-connected ordinal set

Union B is set

((Union B)) 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 epsilon-transitive epsilon-connected ordinal set

succ X is non empty epsilon-transitive epsilon-connected ordinal 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

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

succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal set

{0} is non empty trivial 1 -element set

0 \/ {0} is non empty set

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

X is epsilon-transitive epsilon-connected ordinal set

x is Relation-like T-Sequence-like Function-like set

dom x is epsilon-transitive epsilon-connected ordinal set

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

Union x is set

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

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

On X is epsilon-transitive epsilon-connected ordinal set

Rank (On X) is epsilon-transitive set

X is epsilon-transitive epsilon-connected ordinal set

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

x is epsilon-transitive epsilon-connected ordinal set

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

B is epsilon-transitive epsilon-connected ordinal set

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

succ B is non empty epsilon-transitive epsilon-connected ordinal 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 epsilon-transitive epsilon-connected ordinal set

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

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

B is epsilon-transitive epsilon-connected ordinal set

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

A is epsilon-transitive epsilon-connected ordinal set

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

L is Relation-like T-Sequence-like Function-like set

dom L is epsilon-transitive epsilon-connected ordinal set

succ A is non empty epsilon-transitive epsilon-connected ordinal 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

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

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

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

B is epsilon-transitive epsilon-connected ordinal set

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

X is epsilon-transitive epsilon-connected ordinal set

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

x is epsilon-transitive epsilon-connected ordinal set

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

X is epsilon-transitive epsilon-connected ordinal set

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

x is epsilon-transitive epsilon-connected ordinal set

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

X is set

Tarski-Class (X,{}) is Element of bool (Tarski-Class X)

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

bool (Tarski-Class X) is non empty set

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

{ b

( b

{ (bool b

{ b

( b

{X} is non empty trivial 1 -element set

B is set

x is epsilon-transitive epsilon-connected ordinal set

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

succ x is non empty epsilon-transitive epsilon-connected ordinal set

{x} is non empty trivial 1 -element set

x \/ {x} is non empty set

L is set

x is Relation-like T-Sequence-like Function-like set

last x is set

dom x is epsilon-transitive epsilon-connected ordinal set

A is epsilon-transitive epsilon-connected ordinal set

succ A is non empty epsilon-transitive epsilon-connected ordinal 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 (Tarski-Class X)

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