omega is non empty epsilon-transitive epsilon-connected ordinal set
{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set
the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set
1 is non empty epsilon-transitive epsilon-connected ordinal natural Element of omega
{{},1} is non empty set
bool {} is non empty set
{{}} is non empty functional set
union {} is epsilon-transitive epsilon-connected ordinal set
F is set
{F} is non empty set
{{}} --> F is non empty Relation-like {{}} -defined {F} -valued Function-like constant V17({{}}) V18({{}},{F}) Element of bool [:{{}},{F}:]
[:{{}},{F}:] is non empty Relation-like set
bool [:{{}},{F}:] is non empty set
dom ({{}} --> F) is non empty functional Element of bool {{}}
bool {{}} is non empty set
proj2 ({{}} --> F) is non empty trivial set
proj1 ({{}} --> F) is non empty set
x is set
({{}} --> F) . {} is set
b is set
({{}} --> F) . b is set
rng ({{}} --> F) is non empty trivial Element of bool {F}
bool {F} is non empty set
the set is set
{ the set } is non empty set
F is set
proj2 {} is empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural with_non-empty_elements set
proj1 {} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V22() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set
F1() is set
F is Relation-like Function-like set
proj1 F is set
e is epsilon-transitive epsilon-connected ordinal set
F . e is set
F2(e) is set
F3(e) is set
F is set
e is set
F \/ e is set
x is Relation-like Function-like set
proj2 x is set
proj1 x is set
b is Relation-like Function-like set
proj2 b is set
proj1 b is set
c5 is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
c5 +^ a is epsilon-transitive epsilon-connected ordinal set
x is Relation-like Function-like set
proj1 x is set
proj2 x is set
y is set
z is set
x . z is set
Z is epsilon-transitive epsilon-connected ordinal set
y is epsilon-transitive epsilon-connected ordinal natural set
x . Z is set
Z is epsilon-transitive epsilon-connected ordinal set
y is epsilon-transitive epsilon-connected ordinal natural set
Z -^ y is epsilon-transitive epsilon-connected ordinal set
b . (Z -^ y) is set
y +^ (Z -^ y) is epsilon-transitive epsilon-connected ordinal set
Z is epsilon-transitive epsilon-connected ordinal set
y is epsilon-transitive epsilon-connected ordinal natural set
y is set
z is set
x . z is set
x . z is set
z is epsilon-transitive epsilon-connected ordinal natural set
z is set
b . z is set
y is epsilon-transitive epsilon-connected ordinal natural set
Z is epsilon-transitive epsilon-connected ordinal set
y +^ Z is epsilon-transitive epsilon-connected ordinal set
(y +^ Z) -^ y is epsilon-transitive epsilon-connected ordinal set
b . ((y +^ Z) -^ y) is set
x . (y +^ Z) is set
y is epsilon-transitive epsilon-connected ordinal natural set
z is epsilon-transitive epsilon-connected ordinal natural set
y +^ z is epsilon-transitive epsilon-connected ordinal natural set
F is set
{F} is non empty set
F is set
e is set
{F,e} is non empty set
{F} is non empty () set
{e} is non empty () set
{F} \/ {e} is non empty set
F is set
e is set
x is set
{F,e,x} is non empty set
{F} is non empty () set
{e,x} is non empty () set
{F} \/ {e,x} is non empty set
F is set
e is set
x is set
b is set
{F,e,x,b} is non empty set
{F} is non empty () set
{e,x,b} is non empty () set
{F} \/ {e,x,b} is non empty set
F is set
e is set
x is set
b is set
c5 is set
{F,e,x,b,c5} is non empty set
{F} is non empty () set
{e,x,b,c5} is non empty () set
{F} \/ {e,x,b,c5} is non empty set
F is set
e is set
x is set
b is set
c5 is set
a is set
{F,e,x,b,c5,a} is non empty set
{F} is non empty () set
{e,x,b,c5,a} is non empty () set
{F} \/ {e,x,b,c5,a} is non empty set
F is set
e is set
x is set
b is set
c5 is set
a is set
x is set
{F,e,x,b,c5,a,x} is non empty set
{F} is non empty () set
{e,x,b,c5,a,x} is non empty () set
{F} \/ {e,x,b,c5,a,x} is non empty set
F is set
e is set
x is set
b is set
c5 is set
a is set
x is set
y is set
{F,e,x,b,c5,a,x,y} is non empty set
{F} is non empty () set
{e,x,b,c5,a,x,y} is non empty () set
{F} \/ {e,x,b,c5,a,x,y} is non empty set
F is () set
bool F is non empty set
e is Element of bool F
x is set
b is Relation-like Function-like set
proj2 b is set
proj1 b is set
c5 is Relation-like Function-like set
proj1 c5 is set
a is set
x is set
b . x is set
c5 . x is set
x is set
c5 . x is set
b . x is set
b . x is set
b . x is set
proj2 c5 is set
F is () set
e is () set
F \/ e is set
F is set
e is set
F is set
e is set
F \/ e is set
F is set
e is () set
F /\ e is set
F is () set
e is set
F /\ e is () set
F \ e is () Element of bool F
bool F is non empty set
F is set
e is set
F /\ e is set
F is set
e is set
F \ e is Element of bool F
bool F is non empty set
F is Relation-like Function-like set
e is () set
F .: e is set
proj1 F is set
(proj1 F) /\ e is () set
b is Relation-like Function-like set
proj2 b is set
proj1 b is set
b * F is Relation-like Function-like set
proj2 (b * F) is set
proj1 (b * F) is set
F .: ((proj1 F) /\ e) is set
F is set
e is Relation-like Function-like set
e .: F is set
F is set
bool F is non empty set
bool (bool F) is non empty set
e is Element of bool (bool F)
x is Relation-like Function-like set
proj2 x is set
proj1 x is set
bool (proj1 x) is non empty Element of bool (bool (proj1 x))
bool (proj1 x) is non empty set
bool (bool (proj1 x)) is non empty set
b is set
c5 is set
the Element of e is Element of e
x " the Element of e is set
x .: (x " the Element of e) is set
c5 is Element of bool (bool (proj1 x))
bool (bool {}) is non empty set
x is Element of bool (bool {})
y is set
x is epsilon-transitive epsilon-connected ordinal set
bool x is non empty set
bool (bool x) is non empty set
succ x is non empty epsilon-transitive epsilon-connected ordinal set
bool (succ x) is non empty set
bool (bool (succ x)) is non empty set
y is Element of bool (bool (succ x))
{x} is non empty () set
bool x is non empty Element of bool (bool x)
z is set
y is set
the Element of y is Element of y
x \/ {x} is non empty set
the Element of y \ {x} is Element of bool the Element of y
bool the Element of y is non empty set
(x \/ {x}) \ {x} is Element of bool (x \/ {x})
bool (x \/ {x}) is non empty set
x \ {x} is Element of bool x
y is Element of bool (bool x)
Z is set
X1 is set
X1 \ {x} is Element of bool X1
bool X1 is non empty set
Z \/ {x} is non empty set
A is non empty set
B is set
B \ {x} is Element of bool B
bool B is non empty set
(B \ {x}) \/ {x} is non empty set
A \ {x} is Element of bool A
bool A is non empty set
Z \ {x} is Element of bool Z
bool Z is non empty set
X1 \/ {x} is non empty set
A is set
B is set
B \ {x} is Element of bool B
bool B is non empty set
A \ {x} is Element of bool A
bool A is non empty set
A \/ {x} is non empty set
(B \ {x}) \/ {x} is non empty set
B \/ {x} is non empty set
x is set
B is set
c17 is set
x is epsilon-transitive epsilon-connected ordinal set
bool x is non empty set
bool (bool x) is non empty set
y is Element of bool (bool x)
x is set
x .: x is set
y is set
x " (x .: x) is set
x " y is set
x .: (x " y) is set
y is set
F1() is set
bool F1() is non empty Element of bool (bool F1())
bool F1() is non empty set
bool (bool F1()) is non empty set
F is set
e is set
e is Element of bool (bool F1())
x is set
F1() \ x is Element of bool F1()
the Element of F1() \ x is Element of F1() \ x
{ the Element of F1() \ x} is non empty () set
x \/ { the Element of F1() \ x} is non empty set
c5 is set
b is set
F is set
union F is set
bool F is non empty Element of bool (bool F)
bool F is non empty set
bool (bool F) is non empty set
e is set
x is set
b is set
{x} is non empty () set
b \/ {x} is non empty set
union (b \/ {x}) is set
union b is set
union {x} is set
(union b) \/ (union {x}) is set
(union b) \/ x is set
c5 is set
union c5 is set
x is set
union x is set
F is () set
e is () set
[:F,e:] is Relation-like set
x is set
{x} is non empty () set
[:F,{x}:] is Relation-like set
b is Relation-like Function-like set
proj1 b is set
proj2 b is set
c5 is set
a is set
b . a is set
[a,x] is V1() set
{a,x} is non empty () set
{a} is non empty () set
{{a,x},{a}} is non empty () set
a is set
x is set
[a,x] is V1() set
{a,x} is non empty () set
{a} is non empty () set
{{a,x},{a}} is non empty () set
b . a is set
b .: F is () set
bool [:F,e:] is non empty Element of bool (bool [:F,e:])
bool [:F,e:] is non empty set
bool (bool [:F,e:]) is non empty set
x is set
union x is set
b is set
c5 is set
c5 is set
a is set
[c5,a] is V1() set
{c5,a} is non empty () set
{c5} is non empty () set
{{c5,a},{c5}} is non empty () set
{a} is non empty () set
[:F,{a}:] is Relation-like set
b is Relation-like Function-like set
proj1 b is set
proj2 b is set
c5 is set
a is set
b . a is set
{a} is non empty () set
[:F,{a}:] is Relation-like set
a is set
{a} is non empty () set
[:F,{a}:] is Relation-like set
b . a is set
b .: e is () set
c5 is set
a is set
{a} is non empty () set
[:F,{a}:] is Relation-like set
F is () set
e is () set
x is () set
[:F,e,x:] is set
[:F,e:] is Relation-like () set
[:[:F,e:],x:] is Relation-like () set
F is () set
e is () set
x is () set
b is () set
[:F,e,x,b:] is set
[:F,e,x:] is () set
[:[:F,e,x:],b:] is Relation-like () set
F is () set
bool F is non empty Element of bool (bool F)
bool F is non empty set
bool (bool F) is non empty set
e is set
bool {} is non empty Element of bool (bool {})
bool (bool {}) is non empty set
x is set
b is set
{x} is non empty () set
b \/ {x} is non empty set
bool b is non empty Element of bool (bool b)
bool b is non empty set
bool (bool b) is non empty set
c5 is set
y is set
a is set
y \/ {x} is non empty set
z is set
x is set
z \/ {x} is non empty set
c5 is set
c5 \/ {x} is non empty set
a is set
a \/ {x} is non empty set
c5 is Relation-like Function-like set
proj1 c5 is set
proj2 c5 is set
bool (b \/ {x}) is non empty set
bool (b \/ {x}) is non empty Element of bool (bool (b \/ {x}))
bool (bool (b \/ {x})) is non empty set
(bool (b \/ {x})) \ (bool b) is Element of bool (bool (b \/ {x}))
a is set
x is set
c5 . x is set
y is set
y \/ {x} is non empty set
a \ {x} is Element of bool a
bool a is non empty set
y is set
c5 . (a \ {x}) is set
y is set
y \/ {x} is non empty set
a \/ {x} is non empty set
c5 .: (bool b) is set
((bool (b \/ {x})) \ (bool b)) \/ (bool b) is non empty set
(bool (b \/ {x})) \/ (bool b) is non empty set
F is set
union F is set
bool (union F) is non empty Element of bool (bool (union F))
bool (union F) is non empty set
bool (bool (union F)) is non empty set
e is set
F is Relation-like Function-like set
proj1 F is set
proj2 F is set
F .: (proj1 F) is set
F is set
e is Relation-like Function-like set
proj2 e is set
e " F is set
e .: (e " F) is set
F is () set
e is () set
F \+\ e is set
F \ e is () set
e \ F is () set
(F \ e) \/ (e \ F) is () set
F is non empty set
bool F is non empty set
the Element of F is Element of F
{ the Element of F} is non empty () Element of bool F
F is Relation-like Function-like set
proj1 F is set
proj2 F is set
[:(proj1 F),(proj2 F):] is Relation-like set
proj2 F is set
[:(proj1 F),(proj2 F):] is Relation-like set
pr1 ((proj1 F),(proj2 F)) is Relation-like [:(proj1 F),(proj2 F):] -defined proj1 F -valued Function-like V18([:(proj1 F),(proj2 F):], proj1 F) Element of bool [:[:(proj1 F),(proj2 F):],(proj1 F):]
[:[:(proj1 F),(proj2 F):],(proj1 F):] is Relation-like set
bool [:[:(proj1 F),(proj2 F):],(proj1 F):] is non empty set
(pr1 ((proj1 F),(proj2 F))) .: F is Element of bool (proj1 F)
bool (proj1 F) is non empty set
F is set
e is set
x is set
{e} is non empty () set
x \/ {e} is non empty set
b is set
c5 is set
b is set
b is set
{e} is non empty () set
x \/ {e} is non empty set
c5 is set
c5 is set
a is set
x is set
b is set
{e} is non empty () set
x \/ {e} is non empty set
{e} is non empty () set
x \/ {e} is non empty set
b is set
e is set
F is set
e is set
x is set
{e} is non empty () set
x \/ {e} is non empty set
b is set
c5 is set
b is set
b is set
{e} is non empty () set
x \/ {e} is non empty set
c5 is set
c5 is set
a is set
x is set
b is set
{e} is non empty () set
x \/ {e} is non empty set
{e} is non empty () set
x \/ {e} is non empty set
b is set
e is set
F is set
e is set
x is set
[:e,x:] is Relation-like set
b is Relation-like Function-like set
proj1 b is set
c5 is Relation-like Function-like set
proj1 c5 is set
proj2 b is set
a is set
proj2 c5 is set
x is set
[:a,x:] is Relation-like set
y is set
z is set
b . z is set
y is set
z is set
[y,z] is V1() set
{y,z} is non empty () set
{y} is non empty () set
{{y,z},{y}} is non empty () set
z `1 is set
y is set
z is set
c5 . z is set
y is set
z is set
[y,z] is V1() set
{y,z} is non empty () set
{y} is non empty () set
{{y,z},{y}} is non empty () set
z `2 is set
y is set
z is set
y is set
[z,y] is V1() set
{z,y} is non empty () set
{z} is non empty () set
{{z,y},{z}} is non empty () set
c5 . y is set
y `2 is set
b . y is set
y `1 is set
F is set
e is set
x is set
[:e,x:] is Relation-like set
b is Relation-like Function-like set
proj1 b is set
proj2 b is set
c5 is set
[:c5,x:] is Relation-like set
a is set
x is set
b . x is set
y is set
z is set
[y,z] is V1() set
{y,z} is non empty () set
{y} is non empty () set
{{y,z},{y}} is non empty () set
x `1 is set
a is set
x is set
y is set
[x,y] is V1() set
{x,y} is non empty () set
{x} is non empty () set
{{x,y},{x}} is non empty () set
b . a is set
a `1 is set
[{},{}] is V1() set
{{},{}} is non empty functional () set
{{{},{}},{{}}} is non empty () set
{[{},{}]} is non empty Relation-like Function-like () set
F is Relation-like () set
proj1 F is set
e is Relation-like Function-like set
proj1 e is set
x is set
proj2 e is set
b is set
e . b is set
b `2 is set
[x,(b `2)] is V1() set
{x,(b `2)} is non empty () set
{x} is non empty () set
{{x,(b `2)},{x}} is non empty () set
b `1 is set
c5 is set
a is set
[c5,a] is V1() set
{c5,a} is non empty () set
{c5} is non empty () set
{{c5,a},{c5}} is non empty () set
b is set
[x,b] is V1() set
{x,b} is non empty () set
{x} is non empty () set
{{x,b},{x}} is non empty () set
e . [x,b] is set
[x,b] `1 is set
e is Relation-like Function-like () set
F is Relation-like Function-like set
e * F is Relation-like Function-like set
proj1 (e * F) is set
proj1 e is () set
F is () set
e is set
[:F,e:] is Relation-like set
bool [:F,e:] is non empty set
x is Relation-like F -defined e -valued Function-like V18(F,e) Element of bool [:F,e:]
dom x is () Element of bool F
bool F is non empty () set
F is set
e is set
F .--> e is Relation-like {F} -defined Function-like one-to-one set
{F} is non empty () set
{F} --> e is non empty Relation-like {F} -defined {e} -valued Function-like constant V17({F}) V18({F},{e}) () Element of bool [:{F},{e}:]
{e} is non empty () set
[:{F},{e}:] is non empty Relation-like () set
bool [:{F},{e}:] is non empty () set
F is Relation-like () set
proj2 F is set
e is Relation-like Function-like set
proj1 e is set
x is set
proj2 e is set
b is set
e . b is set
b `1 is set
[(b `1),x] is V1() set
{(b `1),x} is non empty () set
{(b `1)} is non empty () set
{{(b `1),x},{(b `1)}} is non empty () set
b `2 is set
c5 is set
a is set
[c5,a] is V1() set
{c5,a} is non empty () set
{c5} is non empty () set
{{c5,a},{c5}} is non empty () set
b is set
[b,x] is V1() set
{b,x} is non empty () set
{b} is non empty () set
{{b,x},{b}} is non empty () set
e . [b,x] is set
[b,x] `2 is set
F is Relation-like Function-like () set
e is set
F " e is set
proj1 F is () set
F is Relation-like Function-like () set
e is Relation-like Function-like () set
F +* e is Relation-like Function-like set
proj1 (F +* e) is set
proj1 F is () set
proj1 e is () set
(proj1 F) \/ (proj1 e) is () set
F is Relation-like Function-like set
proj1 F is set
e is set
F . e is set
proj2 F is set
F . e is set
e is set
proj2 F is set
x is set
F . x is set
F is set
e is Relation-like F -defined Function-like set
x is set
dom e is Element of bool F
bool F is non empty set
e . x is set
dom e is Element of bool F
bool F is non empty set
e . x is set
dom e is Element of bool F
bool F is non empty set
x is set
proj1 e is set
e . x is set
dom e is Element of bool F
bool F is non empty set
F is set
e is set
[:e,F:] is Relation-like set
x is set
{x} is non empty () set
[x,{x}] is V1() set
{x,{x}} is non empty () set
{{x,{x}},{x}} is non empty () set
F is set
e is Relation-like F -defined Function-like set
F is set
e is set
F is non empty set
e is non empty set
the Element of F is Element of F
the Element of e is Element of e
{ the Element of F} is non empty () set
the Element of F .--> the Element of e is Relation-like F -defined { the Element of F} -defined e -valued Function-like one-to-one () set
{ the Element of F} --> the Element of e is non empty Relation-like { the Element of F} -defined e -valued { the Element of e} -valued Function-like constant V17({ the Element of F}) V18({ the Element of F},{ the Element of e}) () Element of bool [:{ the Element of F},{ the Element of e}:]
{ the Element of e} is non empty () set
[:{ the Element of F},{ the Element of e}:] is non empty Relation-like () set
bool [:{ the Element of F},{ the Element of e}:] is non empty () set
c5 is Relation-like F -defined { the Element of F} -defined e -valued Function-like one-to-one () set
F is set
e is Relation-like () set
F |` e is Relation-like set
e is Relation-like () set
F is set
e | F is Relation-like set
e is Relation-like Function-like set
F is () set
e | F is Relation-like Function-like set
proj1 (e | F) is set
F is Relation-like () set
field F is set
proj1 F is () set
proj2 F is () set
(proj1 F) \/ (proj2 F) is () set
F is set
e is set
{e} is non empty () set
F is set
F is non trivial set
bool F is non empty set
e is set
x is set
{e,x} is non empty () set
b is Element of bool F
F is set
e is set
x is set
b is set
(F,e) --> (x,b) is set
F .--> x is Relation-like {F} -defined Function-like one-to-one () set
{F} is non empty () set
{F} --> x is non empty Relation-like {F} -defined {x} -valued Function-like constant V17({F}) V18({F},{x}) () Element of bool [:{F},{x}:]
{x} is non empty () set
[:{F},{x}:] is non empty Relation-like () set
bool [:{F},{x}:] is non empty () set
e .--> b is Relation-like {e} -defined Function-like one-to-one () set
{e} is non empty () set
{e} --> b is non empty Relation-like {e} -defined {b} -valued Function-like constant V17({e}) V18({e},{b}) () Element of bool [:{e},{b}:]
{b} is non empty () set
[:{e},{b}:] is non empty Relation-like () set
bool [:{e},{b}:] is non empty () set
(F .--> x) +* (e .--> b) is Relation-like Function-like () set
F is set
e is set
F is () set
e is Element of F
{{{}}} is non empty () set
F is non empty () set
e is set
F is () set
{F} is non empty () set
e is set
bool F is non empty () Element of bool (bool F)
bool F is non empty () set
bool (bool F) is non empty () set
e is set
e is () set
{F,e} is non empty () set
x is set
F is () set
bool F is non empty set
e is Element of bool F
x is set
e is () set
F \/ e is set
x is set
F is () () set
union F is set
e is set
{{{}}} is non empty () () set
{{}} .--> {{}} is Relation-like {{{}}} -defined Function-like one-to-one () set
{{{}}} --> {{}} is non empty Relation-like non-empty {{{}}} -defined {{{}}} -valued Function-like constant V17({{{}}}) V18({{{}}},{{{}}}) () Element of bool [:{{{}}},{{{}}}:]
[:{{{}}},{{{}}}:] is non empty Relation-like () set
bool [:{{{}}},{{{}}}:] is non empty () () set
F is Relation-like {{{}}} -defined Function-like one-to-one () set
e is set
F . e is set
F is Relation-like set
e is set
proj2 F is set
F is Relation-like Function-like () set
e is set
F . e is set
proj1 F is set
proj1 F is set
proj1 F is set
F is Relation-like () set
proj2 F is set
e is set