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)
{ 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
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