REAL is set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal V35() cardinal limit_cardinal Element of bool REAL
bool REAL is set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal V35() cardinal limit_cardinal set
bool NAT is non trivial V35() set
bool NAT is non trivial V35() set
VAR is non empty Element of bool NAT
bool VAR is set
[:NAT,VAR:] is non trivial V35() set
bool [:NAT,VAR:] is non trivial V35() set
{} is set
the Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real V28() V29() V35() V39() cardinal {} -element set is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real V28() V29() V35() V39() cardinal {} -element set
1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive V28() V29() V35() cardinal Element of NAT
0 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
card NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal V35() cardinal set
the_axiom_of_pairs is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
the_axiom_of_unions is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
the_axiom_of_infinity is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
the_axiom_of_power_sets is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
x. 0 is Element of VAR
x. 1 is Element of VAR
2 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive V28() V29() V35() cardinal Element of NAT
x. 2 is Element of VAR
{(x. 0),(x. 1),(x. 2)} is V35() set
3 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive V28() V29() V35() cardinal Element of NAT
x. 3 is Element of VAR
4 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive V28() V29() V35() cardinal Element of NAT
x. 4 is Element of VAR
(x. 4) '=' (x. 0) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
decode is Relation-like NAT -defined VAR -valued Function-like quasi_total Element of bool [:NAT,VAR:]
decode " is Relation-like Function-like set
L is non empty set
[:VAR,L:] is set
bool [:VAR,L:] is set
W is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
Free W is V35() Element of bool VAR
ksi is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]
{ b1 where b1 is Element of L : L,ksi / ((x. 0),b1) |= W } is set
bool L is set
l is set
u is Element of L
ksi / ((x. 0),u) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]
(x. 2) 'in' (x. 0) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
(x. 2) 'in' (x. 1) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
W is non empty set
[:VAR,W:] is set
bool [:VAR,W:] is set
L is Element of W
bool L is set
W /\ (bool L) is set
ksi is Relation-like VAR -defined W -valued Function-like quasi_total Element of bool [:VAR,W:]
ksi / ((x. 1),L) is Relation-like VAR -defined W -valued Function-like quasi_total Element of bool [:VAR,W:]
((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),W,(ksi / ((x. 1),L))) is Element of bool W
bool W is set
Free (All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))) is V35() Element of bool VAR
Free (((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))) is V35() Element of bool VAR
{(x. 2)} is non empty trivial V35() 1 -element set
(Free (((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)))) \ {(x. 2)} is V35() Element of bool VAR
Free ((x. 2) 'in' (x. 0)) is V35() Element of bool VAR
Free ((x. 2) 'in' (x. 1)) is V35() Element of bool VAR
(Free ((x. 2) 'in' (x. 0))) \/ (Free ((x. 2) 'in' (x. 1))) is V35() Element of bool VAR
((Free ((x. 2) 'in' (x. 0))) \/ (Free ((x. 2) 'in' (x. 1)))) \ {(x. 2)} is V35() Element of bool VAR
{(x. 2),(x. 1)} is V35() set
(Free ((x. 2) 'in' (x. 0))) \/ {(x. 2),(x. 1)} is V35() set
((Free ((x. 2) 'in' (x. 0))) \/ {(x. 2),(x. 1)}) \ {(x. 2)} is V35() Element of bool ((Free ((x. 2) 'in' (x. 0))) \/ {(x. 2),(x. 1)})
bool ((Free ((x. 2) 'in' (x. 0))) \/ {(x. 2),(x. 1)}) is V35() V39() set
{(x. 2),(x. 0)} is V35() set
{(x. 2),(x. 0)} \/ {(x. 2),(x. 1)} is V35() set
({(x. 2),(x. 0)} \/ {(x. 2),(x. 1)}) \ {(x. 2)} is V35() Element of bool ({(x. 2),(x. 0)} \/ {(x. 2),(x. 1)})
bool ({(x. 2),(x. 0)} \/ {(x. 2),(x. 1)}) is V35() V39() set
{(x. 2),(x. 0)} \ {(x. 2)} is V35() Element of bool {(x. 2),(x. 0)}
bool {(x. 2),(x. 0)} is V35() V39() set
{(x. 2),(x. 1)} \ {(x. 2)} is V35() Element of bool {(x. 2),(x. 1)}
bool {(x. 2),(x. 1)} is V35() V39() set
({(x. 2),(x. 0)} \ {(x. 2)}) \/ ({(x. 2),(x. 1)} \ {(x. 2)}) is V35() set
{(x. 1)} is non empty trivial V35() 1 -element set
({(x. 2),(x. 0)} \ {(x. 2)}) \/ {(x. 1)} is V35() set
{(x. 0)} is non empty trivial V35() 1 -element set
{(x. 0)} \/ {(x. 1)} is V35() set
{(x. 0),(x. 1)} is V35() set
{ b1 where b1 is Element of W : W,(ksi / ((x. 1),L)) / ((x. 0),b1) |= All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)))) } is set
u1 is set
u2 is Element of W
(ksi / ((x. 1),L)) / ((x. 0),u2) is Relation-like VAR -defined W -valued Function-like quasi_total Element of bool [:VAR,W:]
i is set
a is Element of W
((ksi / ((x. 1),L)) / ((x. 0),u2)) / ((x. 2),a) is Relation-like VAR -defined W -valued Function-like quasi_total Element of bool [:VAR,W:]
(((ksi / ((x. 1),L)) / ((x. 0),u2)) / ((x. 2),a)) . (x. 2) is Element of W
(((ksi / ((x. 1),L)) / ((x. 0),u2)) / ((x. 2),a)) . (x. 1) is Element of W
((ksi / ((x. 1),L)) / ((x. 0),u2)) . (x. 1) is Element of W
(ksi / ((x. 1),L)) . (x. 1) is Element of W
((ksi / ((x. 1),L)) / ((x. 0),u2)) . (x. 0) is Element of W
(((ksi / ((x. 1),L)) / ((x. 0),u2)) / ((x. 2),a)) . (x. 0) is Element of W
u1 is set
(ksi / ((x. 1),L)) . (x. 1) is Element of W
u2 is Element of W
(ksi / ((x. 1),L)) / ((x. 0),u2) is Relation-like VAR -defined W -valued Function-like quasi_total Element of bool [:VAR,W:]
i is Element of W
((ksi / ((x. 1),L)) / ((x. 0),u2)) / ((x. 2),i) is Relation-like VAR -defined W -valued Function-like quasi_total Element of bool [:VAR,W:]
(((ksi / ((x. 1),L)) / ((x. 0),u2)) / ((x. 2),i)) . (x. 2) is Element of W
((ksi / ((x. 1),L)) / ((x. 0),u2)) . (x. 0) is Element of W
(((ksi / ((x. 1),L)) / ((x. 0),u2)) / ((x. 2),i)) . (x. 0) is Element of W
(((ksi / ((x. 1),L)) / ((x. 0),u2)) / ((x. 2),i)) . (x. 1) is Element of W
((ksi / ((x. 1),L)) / ((x. 0),u2)) . (x. 1) is Element of W
W is Relation-like Function-like set
Union W is set
dom W is set
L is set
rng W is set
union (rng W) is set
ksi is set
lambda is set
W . lambda is set
W is non empty epsilon-transitive V33() V34() universal set
L is Relation-like non-empty W -valued Function-like T-Sequence-like DOMAIN-yielding set
Union L is non empty Element of bool W
bool W is set
lambda is set
bool lambda is set
l is epsilon-transitive epsilon-connected ordinal Element of W
L . l is non empty Element of W
(L . l) /\ (bool lambda) is set
[:VAR,(L . l):] is set
bool [:VAR,(L . l):] is set
the Relation-like VAR -defined L . l -valued Function-like quasi_total Element of bool [:VAR,(L . l):] is Relation-like VAR -defined L . l -valued Function-like quasi_total Element of bool [:VAR,(L . l):]
u1 is Element of L . l
the Relation-like VAR -defined L . l -valued Function-like quasi_total Element of bool [:VAR,(L . l):] / ((x. 1),u1) is Relation-like VAR -defined L . l -valued Function-like quasi_total Element of bool [:VAR,(L . l):]
((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(L . l),( the Relation-like VAR -defined L . l -valued Function-like quasi_total Element of bool [:VAR,(L . l):] / ((x. 1),u1))) is Element of bool (L . l)
bool (L . l) is set
lambda is set
bool lambda is set
(Union L) /\ (bool lambda) is Element of bool W
l is non empty set
u is Element of l
dom L is epsilon-transitive epsilon-connected ordinal set
u1 is set
L . u1 is set
On W is non empty epsilon-transitive epsilon-connected ordinal set
u2 is epsilon-transitive epsilon-connected ordinal Element of W
L . u2 is set
u is Relation-like Function-like set
dom u is set
rng u is set
u1 is set
u2 is set
u . u2 is set
i is Element of l
u . i is set
a is epsilon-transitive epsilon-connected ordinal Element of W
L . a is non empty Element of W
u .: (dom u) is set
card l is non empty epsilon-transitive epsilon-connected ordinal cardinal set
card W is non empty epsilon-transitive epsilon-connected ordinal cardinal set
card (rng u) is epsilon-transitive epsilon-connected ordinal cardinal set
sup (rng u) is epsilon-transitive epsilon-connected ordinal set
u1 is epsilon-transitive epsilon-connected ordinal Element of W
L . u1 is non empty Element of W
u2 is set
i is Element of l
u . i is set
a is epsilon-transitive epsilon-connected ordinal Element of W
L . a is non empty Element of W
(L . u1) /\ (bool lambda) is set
l /\ (bool lambda) is set
(bool lambda) /\ (bool lambda) is set
(Union L) /\ ((bool lambda) /\ (bool lambda)) is Element of bool W
lambda is set
dom L is epsilon-transitive epsilon-connected ordinal set
l is set
L . l is set
u is epsilon-transitive epsilon-connected ordinal set
On W is non empty epsilon-transitive epsilon-connected ordinal set
u1 is epsilon-transitive epsilon-connected ordinal Element of W
L . u1 is non empty Element of W
u2 is set
W is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
variables_in W is non empty Element of bool VAR
Free W is V35() Element of bool VAR
W <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
All ((x. 4),(W <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(W <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(W <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
L is non empty set
[:VAR,L:] is set
bool [:VAR,L:] is set
ksi is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]
def_func' (W,ksi) is Relation-like L -defined L -valued Function-like quasi_total Element of bool [:L,L:]
[:L,L:] is set
bool [:L,L:] is set
lambda is Element of VAR
W / ((x. 0),lambda) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
Free (W / ((x. 0),lambda)) is V35() Element of bool VAR
(W / ((x. 0),lambda)) <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
All ((x. 4),((W / ((x. 0),lambda)) <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),((W / ((x. 0),lambda)) <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),((W / ((x. 0),lambda)) <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
def_func' ((W / ((x. 0),lambda)),ksi) is Relation-like L -defined L -valued Function-like quasi_total Element of bool [:L,L:]
l is Element of L
ksi / ((x. 3),l) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]
u is Element of L
u2 is Element of L
(ksi / ((x. 3),l)) / ((x. 4),u2) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]
u1 is Element of L
((ksi / ((x. 3),l)) / ((x. 4),u2)) . lambda is Element of L
((ksi / ((x. 3),l)) / ((x. 4),u2)) / ((x. 0),(((ksi / ((x. 3),l)) / ((x. 4),u2)) . lambda)) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]
((ksi / ((x. 3),l)) / ((x. 4),u2)) . lambda is Element of L
((ksi / ((x. 3),l)) / ((x. 4),u2)) / ((x. 0),(((ksi / ((x. 3),l)) / ((x. 4),u2)) . lambda)) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]
l is set
u is Element of L
(def_func' (W,ksi)) . u is Element of L
ksi / ((x. 3),u) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]
(ksi / ((x. 3),u)) / ((x. 4),((def_func' (W,ksi)) . u)) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]
((ksi / ((x. 3),u)) / ((x. 4),((def_func' (W,ksi)) . u))) . lambda is Element of L
((ksi / ((x. 3),u)) / ((x. 4),((def_func' (W,ksi)) . u))) / ((x. 0),(((ksi / ((x. 3),u)) / ((x. 4),((def_func' (W,ksi)) . u))) . lambda)) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]
(def_func' (W,ksi)) . l is set
(def_func' ((W / ((x. 0),lambda)),ksi)) . l is set
W is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
W <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
All ((x. 4),(W <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(W <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(W <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
Free W is V35() Element of bool VAR
L is non empty set
[:VAR,L:] is set
bool [:VAR,L:] is set
ksi is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]
def_func' (W,ksi) is Relation-like L -defined L -valued Function-like quasi_total Element of bool [:L,L:]
[:L,L:] is set
bool [:L,L:] is set
the Element of L is Element of L
ksi / ((x. 3), the Element of L) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]
l is Element of L
(ksi / ((x. 3), the Element of L)) / ((x. 0),l) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]
u is Element of L
(def_func' (W,ksi)) .: u is Element of bool L
bool L is set
the Element of (def_func' (W,ksi)) .: u is Element of (def_func' (W,ksi)) .: u
dom (def_func' (W,ksi)) is Element of bool L
u2 is set
(def_func' (W,ksi)) . u2 is set
i is Element of L
((ksi / ((x. 3), the Element of L)) / ((x. 0),l)) / ((x. 4),i) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]
(((ksi / ((x. 3), the Element of L)) / ((x. 0),l)) / ((x. 4),i)) . (x. 4) is Element of L
(((ksi / ((x. 3), the Element of L)) / ((x. 0),l)) / ((x. 4),i)) . (x. 0) is Element of L
((ksi / ((x. 3), the Element of L)) / ((x. 0),l)) . (x. 0) is Element of L
a is Element of L
W is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
variables_in W is non empty Element of bool VAR
Free W is V35() Element of bool VAR
L is Element of VAR
W / ((x. 0),L) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
(W / ((x. 0),L)) / ((x. 4),(x. 0)) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
ksi is Element of VAR
(x. 3) 'in' ksi is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
((x. 3) 'in' ksi) '&' ((W / ((x. 0),L)) / ((x. 4),(x. 0))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
Ex ((x. 3),(((x. 3) 'in' ksi) '&' ((W / ((x. 0),L)) / ((x. 4),(x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
Free (Ex ((x. 3),(((x. 3) 'in' ksi) '&' ((W / ((x. 0),L)) / ((x. 4),(x. 0)))))) is V35() Element of bool VAR
Free (((x. 3) 'in' ksi) '&' ((W / ((x. 0),L)) / ((x. 4),(x. 0)))) is V35() Element of bool VAR
{(x. 3)} is non empty trivial V35() 1 -element set
(Free (((x. 3) 'in' ksi) '&' ((W / ((x. 0),L)) / ((x. 4),(x. 0))))) \ {(x. 3)} is V35() Element of bool VAR
Free ((x. 3) 'in' ksi) is V35() Element of bool VAR
Free ((W / ((x. 0),L)) / ((x. 4),(x. 0))) is V35() Element of bool VAR
(Free ((x. 3) 'in' ksi)) \/ (Free ((W / ((x. 0),L)) / ((x. 4),(x. 0)))) is V35() Element of bool VAR
((Free ((x. 3) 'in' ksi)) \/ (Free ((W / ((x. 0),L)) / ((x. 4),(x. 0))))) \ {(x. 3)} is V35() Element of bool VAR
{(x. 3),ksi} is V35() set
{(x. 3),ksi} \/ (Free ((W / ((x. 0),L)) / ((x. 4),(x. 0)))) is V35() set
({(x. 3),ksi} \/ (Free ((W / ((x. 0),L)) / ((x. 4),(x. 0))))) \ {(x. 3)} is V35() Element of bool ({(x. 3),ksi} \/ (Free ((W / ((x. 0),L)) / ((x. 4),(x. 0)))))
bool ({(x. 3),ksi} \/ (Free ((W / ((x. 0),L)) / ((x. 4),(x. 0))))) is V35() V39() set
{(x. 3),ksi} \ {(x. 3)} is V35() Element of bool {(x. 3),ksi}
bool {(x. 3),ksi} is V35() V39() set
(Free ((W / ((x. 0),L)) / ((x. 4),(x. 0)))) \ {(x. 3)} is V35() Element of bool VAR
({(x. 3),ksi} \ {(x. 3)}) \/ ((Free ((W / ((x. 0),L)) / ((x. 4),(x. 0)))) \ {(x. 3)}) is V35() set
Free (W / ((x. 0),L)) is V35() Element of bool VAR
{(x. 0)} is non empty trivial V35() 1 -element set
(Free W) \ {(x. 0)} is V35() Element of bool VAR
{L} is non empty trivial V35() 1 -element set
((Free W) \ {(x. 0)}) \/ {L} is V35() set
{(x. 0)} is non empty trivial V35() 1 -element set
variables_in (W / ((x. 0),L)) is non empty Element of bool VAR
{(x. 4)} is non empty trivial V35() 1 -element set
(Free (W / ((x. 0),L))) \ {(x. 4)} is V35() Element of bool VAR
((Free (W / ((x. 0),L))) \ {(x. 4)}) \/ {(x. 0)} is V35() set
(Free W) \ {(x. 0)} is V35() Element of bool VAR
{L} is non empty trivial V35() 1 -element set
((Free W) \ {(x. 0)}) \/ {L} is V35() set
W is non empty epsilon-transitive V33() V34() universal set
L is Relation-like non-empty W -valued Function-like T-Sequence-like DOMAIN-yielding set
Union L is non empty Element of bool W
bool W is set
[:VAR,(Union L):] is set
bool [:VAR,(Union L):] is set
lambda is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
Free lambda is V35() Element of bool VAR
l is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]
lambda <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
All ((x. 4),(lambda <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),(lambda <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(lambda <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
variables_in lambda is non empty Element of bool VAR
u is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
5 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive V28() V29() V35() cardinal Element of NAT
u + 5 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
x. (u + 5) is Element of VAR
lambda / ((x. 0),(x. (u + 5))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
u + 0 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
(lambda / ((x. 0),(x. (u + 5)))) <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
All ((x. 4),((lambda / ((x. 0),(x. (u + 5)))) <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
Ex ((x. 0),(All ((x. 4),((lambda / ((x. 0),(x. (u + 5)))) <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),((lambda / ((x. 0),(x. (u + 5)))) <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
def_func' (lambda,l) is Relation-like Union L -defined Union L -valued Function-like quasi_total Element of bool [:(Union L),(Union L):]
[:(Union L),(Union L):] is set
bool [:(Union L),(Union L):] is set
def_func' ((lambda / ((x. 0),(x. (u + 5)))),l) is Relation-like Union L -defined Union L -valued Function-like quasi_total Element of bool [:(Union L),(Union L):]
i is Element of Union L
dom L is epsilon-transitive epsilon-connected ordinal set
a is set
L . a is set
On W is non empty epsilon-transitive epsilon-connected ordinal set
i is epsilon-transitive epsilon-connected ordinal Element of W
L . i is set
i is Relation-like Function-like set
dom i is set
rng i is set
a is set
i is set
i . i is set
i is Element of Union L
i . i is set
b is epsilon-transitive epsilon-connected ordinal Element of W
L . b is non empty Element of W
card VAR is non empty epsilon-transitive epsilon-connected ordinal cardinal set
card W is non empty epsilon-transitive epsilon-connected ordinal cardinal set
dom l is Element of bool VAR
card (dom l) is epsilon-transitive epsilon-connected ordinal cardinal set
rng l is Element of bool (Union L)
bool (Union L) is set
l .: (dom l) is Element of bool (Union L)
card (rng l) is epsilon-transitive epsilon-connected ordinal cardinal set
i .: (rng l) is set
card (i .: (rng l)) is epsilon-transitive epsilon-connected ordinal cardinal set
sup (i .: (rng l)) is epsilon-transitive epsilon-connected ordinal set
Free (lambda / ((x. 0),(x. (u + 5)))) is V35() Element of bool VAR
i is set
i .: i is set
sup (i .: i) is epsilon-transitive epsilon-connected ordinal set
i is epsilon-transitive epsilon-connected ordinal Element of W
L . i is non empty Element of W
b is set
e is Element of Union L
i . e is set
e is epsilon-transitive epsilon-connected ordinal Element of W
L . e is non empty Element of W
i is Element of Union L
i . i is set
i is epsilon-transitive epsilon-connected ordinal Element of W
L . i is non empty Element of W
card i is epsilon-transitive epsilon-connected ordinal cardinal set
variables_in (lambda / ((x. 0),(x. (u + 5)))) is non empty Element of bool VAR
(def_func' (lambda,l)) .: i is Element of bool (Union L)
i .: ((def_func' (lambda,l)) .: i) is set
card (i .: ((def_func' (lambda,l)) .: i)) is epsilon-transitive epsilon-connected ordinal cardinal set
card ((def_func' (lambda,l)) .: i) is epsilon-transitive epsilon-connected ordinal cardinal set
sup (i .: ((def_func' (lambda,l)) .: i)) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal Element of W
i \/ b is epsilon-transitive epsilon-connected ordinal Element of W
a is epsilon-transitive epsilon-connected ordinal Element of W
(i \/ b) \/ a is epsilon-transitive epsilon-connected ordinal Element of W
L . (i \/ b) is non empty Element of W
On W is non empty epsilon-transitive epsilon-connected ordinal set
[:(On W),(On W):] is set
bool [:(On W),(On W):] is set
(lambda / ((x. 0),(x. (u + 5)))) / ((x. 4),(x. 0)) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
phi is Relation-like On W -defined On W -valued Function-like T-Sequence-like quasi_total Ordinal-yielding Element of bool [:(On W),(On W):]
a1 is epsilon-transitive epsilon-connected ordinal Element of W
phi . a1 is epsilon-transitive epsilon-connected ordinal Element of W
L . a1 is non empty Element of W
x is set
q is set
l . q is set
mu is Element of VAR
l . mu is Element of Union L
i . (l . mu) is set
v is epsilon-transitive epsilon-connected ordinal Element of W
L . v is non empty Element of W
10 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive V28() V29() V35() cardinal Element of NAT
u + 10 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
x. (u + 10) is Element of VAR
{(x. 0)} is non empty trivial V35() 1 -element set
(variables_in lambda) \ {(x. 0)} is Element of bool VAR
(x. 3) 'in' (x. (u + 10)) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
((x. 3) 'in' (x. (u + 10))) '&' ((lambda / ((x. 0),(x. (u + 5)))) / ((x. 4),(x. 0))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
Ex ((x. 3),(((x. 3) 'in' (x. (u + 10))) '&' ((lambda / ((x. 0),(x. (u + 5)))) / ((x. 4),(x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
10 + u is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
[:VAR,(L . a1):] is set
bool [:VAR,(L . a1):] is set
v is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]
v . (x. 4) is Element of L . a1
v / ((x. 0),(v . (x. 4))) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]
mu is Element of L . a1
(v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]
{(x. (u + 5))} is non empty trivial V35() 1 -element set
((variables_in lambda) \ {(x. 0)}) \/ {(x. (u + 5))} is set
variables_in ((lambda / ((x. 0),(x. (u + 5)))) / ((x. 4),(x. 0))) is non empty Element of bool VAR
{(x. 4)} is non empty trivial V35() 1 -element set
(variables_in (lambda / ((x. 0),(x. (u + 5))))) \ {(x. 4)} is Element of bool VAR
((variables_in (lambda / ((x. 0),(x. (u + 5))))) \ {(x. 4)}) \/ {(x. 0)} is set
((Ex ((x. 3),(((x. 3) 'in' (x. (u + 10))) '&' ((lambda / ((x. 0),(x. (u + 5)))) / ((x. 4),(x. 0)))))),(L . a1),((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu))) is Element of bool (L . a1)
bool (L . a1) is set
Free (Ex ((x. 3),(((x. 3) 'in' (x. (u + 10))) '&' ((lambda / ((x. 0),(x. (u + 5)))) / ((x. 4),(x. 0)))))) is V35() Element of bool VAR
u1 is set
dom (def_func' (lambda,l)) is Element of bool (Union L)
m1 is set
(def_func' (lambda,l)) . m1 is set
u9 is Element of Union L
l / ((x. 3),u9) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]
(def_func' (lambda,l)) . u9 is Element of Union L
(l / ((x. 3),u9)) / ((x. 0),((def_func' (lambda,l)) . u9)) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]
u2 is Element of L . a1
v / ((x. 3),u2) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]
m2 is Element of L . a1
(v / ((x. 3),u2)) / ((x. 0),m2) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]
(Union L) ! ((v / ((x. 3),u2)) / ((x. 0),m2)) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]
(l / ((x. 3),u9)) / ((x. 4),((def_func' (lambda,l)) . u9)) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]
((l / ((x. 3),u9)) / ((x. 4),((def_func' (lambda,l)) . u9))) . (x. 4) is Element of Union L
((l / ((x. 3),u9)) / ((x. 4),((def_func' (lambda,l)) . u9))) / ((x. 0),((def_func' (lambda,l)) . u9)) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]
((l / ((x. 3),u9)) / ((x. 0),((def_func' (lambda,l)) . u9))) / ((x. 4),((def_func' (lambda,l)) . u9)) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]
((v / ((x. 3),u2)) / ((x. 0),m2)) / ((x. (u + 10)),mu) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]
((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) . (x. (u + 10)) is Element of L . a1
((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((x. 0),m2) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]
(((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((x. 0),m2)) . (x. (u + 10)) is Element of L . a1
(((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((x. 0),m2)) / ((x. 3),u2) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]
((((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((x. 0),m2)) / ((x. 3),u2)) . (x. 3) is Element of L . a1
((((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((x. 0),m2)) / ((x. 3),u2)) . (x. (u + 10)) is Element of L . a1
v / ((x. (u + 10)),mu) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]
(v / ((x. (u + 10)),mu)) / ((x. 0),m2) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]
{ b1 where b1 is Element of L . a1 : L . a1,((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((x. 0),b1) |= Ex ((x. 3),(((x. 3) 'in' (x. (u + 10))) '&' ((lambda / ((x. 0),(x. (u + 5)))) / ((x. 4),(x. 0))))) } is set
u1 is set
{ b1 where b1 is Element of L . a1 : L . a1,((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((x. 0),b1) |= Ex ((x. 3),(((x. 3) 'in' (x. (u + 10))) '&' ((lambda / ((x. 0),(x. (u + 5)))) / ((x. 4),(x. 0))))) } is set
m1 is Element of L . a1
((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((x. 0),m1) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]
m2 is Element of L . a1
(((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]
v / ((x. (u + 10)),mu) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]
(v / ((x. (u + 10)),mu)) / ((x. 0),m1) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]
v / ((x. 3),m2) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]
(v / ((x. 3),m2)) / ((x. 0),m1) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]
((v / ((x. 3),m2)) / ((x. 0),m1)) / ((x. (u + 10)),mu) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]
u2 is Element of Union L
l / ((x. 3),u2) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]
u9 is Element of Union L
(l / ((x. 3),u2)) / ((x. 0),u9) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]
((l / ((x. 3),u2)) / ((x. 0),u9)) / ((x. 4),u9) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]
(l / ((x. 3),u2)) / ((x. 4),u9) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]
((l / ((x. 3),u2)) / ((x. 4),u9)) / ((x. 0),u9) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]
((l / ((x. 3),u2)) / ((x. 0),u9)) . (x. 0) is Element of Union L
(Union L) ! ((v / ((x. 3),m2)) / ((x. 0),m1)) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,(Union L):]
(def_func' (lambda,l)) . u2 is Element of Union L
((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) . (x. (u + 10)) is Element of L . a1
(((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((x. 0),m1)) . (x. (u + 10)) is Element of L . a1
dom (def_func' (lambda,l)) is Element of bool (Union L)
((((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2)) . (x. 3) is Element of L . a1
((((v / ((x. 0),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((x. 0),m1)) / ((x. 3),m2)) . (x. (u + 10)) is Element of L . a1
Free (Ex ((x. 3),(((x. 3) 'in' (x. (u + 10))) '&' ((lambda / ((x. 0),(x. (u + 5)))) / ((x. 4),(x. 0)))))) is V35() Element of bool VAR
lambda is set
dom L is epsilon-transitive epsilon-connected ordinal set
l is set
L . l is set
u is epsilon-transitive epsilon-connected ordinal set
u1 is epsilon-transitive epsilon-connected ordinal Element of W
L . u1 is non empty Element of W
u2 is set
lambda is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
Free lambda is V35() Element of bool VAR
the_axiom_of_substitution_for lambda is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
W is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
Free W is V35() Element of bool VAR
code (Free W) is V35() Element of bool NAT
L is non empty set
[:VAR,L:] is set
bool [:VAR,L:] is set
ksi is Element of L
lambda is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]
lambda * decode is Relation-like NAT -defined L -valued Function-like Element of bool [:NAT,L:]
[:NAT,L:] is non trivial V35() set
bool [:NAT,L:] is non trivial V35() set
l is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
x. l is Element of VAR
[l,ksi] is set
{l,ksi} is V35() set
{l} is non empty trivial V35() V39() 1 -element set
{{l,ksi},{l}} is V35() V39() set
{[l,ksi]} is Function-like non empty trivial V35() 1 -element set
(code (Free W)) \ {l} is V35() Element of bool NAT
(lambda * decode) | ((code (Free W)) \ {l}) is Relation-like NAT -defined L -valued Function-like V35() Element of bool [:NAT,L:]
{[l,ksi]} \/ ((lambda * decode) | ((code (Free W)) \ {l})) is V35() set
lambda / ((x. l),ksi) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]
(lambda / ((x. l),ksi)) * decode is Relation-like NAT -defined L -valued Function-like Element of bool [:NAT,L:]
((lambda / ((x. l),ksi)) * decode) | (code (Free W)) is Relation-like NAT -defined L -valued Function-like V35() Element of bool [:NAT,L:]
((lambda / ((x. l),ksi)) * decode) | {l} is Relation-like NAT -defined L -valued Function-like V35() Element of bool [:NAT,L:]
dom (((lambda / ((x. l),ksi)) * decode) | {l}) is V35() Element of bool NAT
dom ((lambda / ((x. l),ksi)) * decode) is Element of bool NAT
(dom ((lambda / ((x. l),ksi)) * decode)) /\ {l} is V35() Element of bool NAT
NAT /\ {l} is V35() set
(((lambda / ((x. l),ksi)) * decode) | {l}) . l is set
[l,((((lambda / ((x. l),ksi)) * decode) | {l}) . l)] is set
{l,((((lambda / ((x. l),ksi)) * decode) | {l}) . l)} is V35() set
{{l,((((lambda / ((x. l),ksi)) * decode) | {l}) . l)},{l}} is V35() V39() set
{[l,((((lambda / ((x. l),ksi)) * decode) | {l}) . l)]} is Function-like non empty trivial V35() 1 -element set
((lambda / ((x. l),ksi)) * decode) . l is set
[l,(((lambda / ((x. l),ksi)) * decode) . l)] is set
{l,(((lambda / ((x. l),ksi)) * decode) . l)} is V35() set
{{l,(((lambda / ((x. l),ksi)) * decode) . l)},{l}} is V35() V39() set
{[l,(((lambda / ((x. l),ksi)) * decode) . l)]} is Function-like non empty trivial V35() 1 -element set
x". (x. l) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
((lambda / ((x. l),ksi)) * decode) . (x". (x. l)) is set
[l,(((lambda / ((x. l),ksi)) * decode) . (x". (x. l)))] is set
{l,(((lambda / ((x. l),ksi)) * decode) . (x". (x. l)))} is V35() set
{{l,(((lambda / ((x. l),ksi)) * decode) . (x". (x. l)))},{l}} is V35() V39() set
{[l,(((lambda / ((x. l),ksi)) * decode) . (x". (x. l)))]} is Function-like non empty trivial V35() 1 -element set
(lambda / ((x. l),ksi)) . (x. l) is Element of L
[l,((lambda / ((x. l),ksi)) . (x. l))] is set
{l,((lambda / ((x. l),ksi)) . (x. l))} is V35() set
{{l,((lambda / ((x. l),ksi)) . (x. l))},{l}} is V35() V39() set
{[l,((lambda / ((x. l),ksi)) . (x. l))]} is Function-like non empty trivial V35() 1 -element set
dom ((lambda * decode) | ((code (Free W)) \ {l})) is V35() Element of bool NAT
dom (lambda * decode) is Element of bool NAT
(dom (lambda * decode)) /\ ((code (Free W)) \ {l}) is V35() Element of bool NAT
NAT /\ ((code (Free W)) \ {l}) is V35() Element of bool NAT
(dom ((lambda / ((x. l),ksi)) * decode)) /\ ((code (Free W)) \ {l}) is V35() Element of bool NAT
((lambda / ((x. l),ksi)) * decode) | ((code (Free W)) \ {l}) is Relation-like NAT -defined L -valued Function-like V35() Element of bool [:NAT,L:]
dom (((lambda / ((x. l),ksi)) * decode) | ((code (Free W)) \ {l})) is V35() Element of bool NAT
i is set
a is Element of VAR
x". a is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
((lambda * decode) | ((code (Free W)) \ {l})) . i is set
(lambda * decode) . i is set
lambda . a is Element of L
(lambda / ((x. l),ksi)) . a is Element of L
((lambda / ((x. l),ksi)) * decode) . i is set
(((lambda / ((x. l),ksi)) * decode) | ((code (Free W)) \ {l})) . i is set
{l} \/ ((code (Free W)) \ {l}) is V35() set
((lambda / ((x. l),ksi)) * decode) | ({l} \/ ((code (Free W)) \ {l})) is Relation-like NAT -defined L -valued Function-like V35() Element of bool [:NAT,L:]
{{}} is non empty trivial V35() 1 -element set
W is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
Free W is V35() Element of bool VAR
code (Free W) is V35() Element of bool NAT
(code (Free W)) \ {{}} is V35() Element of bool NAT
L is non empty set
[:VAR,L:] is set
bool [:VAR,L:] is set
Diagram (W,L) is set
ksi is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]
(W,L,ksi) is Element of bool L
bool L is set
ksi * decode is Relation-like NAT -defined L -valued Function-like Element of bool [:NAT,L:]
[:NAT,L:] is non trivial V35() set
bool [:NAT,L:] is non trivial V35() set
(ksi * decode) | ((code (Free W)) \ {{}}) is Relation-like NAT -defined L -valued Function-like V35() Element of bool [:NAT,L:]
{ b1 where b1 is Element of L : {[{},b1]} \/ ((ksi * decode) | ((code (Free W)) \ {{}})) in Diagram (W,L) } is set
{ b1 where b1 is Element of L : L,ksi / ((x. 0),b1) |= W } is set
u is set
u1 is Element of L
[{},u1] is set
{{},u1} is V35() set
{{{},u1},{{}}} is V35() V39() set
{[{},u1]} is Function-like non empty trivial V35() 1 -element set
{[{},u1]} \/ ((ksi * decode) | ((code (Free W)) \ {{}})) is V35() set
ksi / ((x. 0),u1) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]
(ksi / ((x. 0),u1)) * decode is Relation-like NAT -defined L -valued Function-like Element of bool [:NAT,L:]
((ksi / ((x. 0),u1)) * decode) | (code (Free W)) is Relation-like NAT -defined L -valued Function-like V35() Element of bool [:NAT,L:]
St (W,L) is Element of bool (VAL L)
VAL L is set
bool (VAL L) is set
u2 is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]
u2 * decode is Relation-like NAT -defined L -valued Function-like Element of bool [:NAT,L:]
(u2 * decode) | (code (Free W)) is Relation-like NAT -defined L -valued Function-like V35() Element of bool [:NAT,L:]
u is set
u1 is Element of L
ksi / ((x. 0),u1) is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]
St (W,L) is Element of bool (VAL L)
VAL L is set
bool (VAL L) is set
(ksi / ((x. 0),u1)) * decode is Relation-like NAT -defined L -valued Function-like Element of bool [:NAT,L:]
((ksi / ((x. 0),u1)) * decode) | (code (Free W)) is Relation-like NAT -defined L -valued Function-like V35() Element of bool [:NAT,L:]
[{},u1] is set
{{},u1} is V35() set
{{{},u1},{{}}} is V35() V39() set
{[{},u1]} is Function-like non empty trivial V35() 1 -element set
{[{},u1]} \/ ((ksi * decode) | ((code (Free W)) \ {{}})) is V35() set
the Element of { b1 where b1 is Element of L : {[{},b1]} \/ ((ksi * decode) | ((code (Free W)) \ {{}})) in Diagram (W,L) } is Element of { b1 where b1 is Element of L : {[{},b1]} \/ ((ksi * decode) | ((code (Free W)) \ {{}})) in Diagram (W,L) }
u1 is Element of L
[{},u1] is set
{{},u1} is V35() set
{{{},u1},{{}}} is V35() V39() set
{[{},u1]} is Function-like non empty trivial V35() 1 -element set
{[{},u1]} \/ ((ksi * decode) | ((code (Free W)) \ {{}})) is V35() set
St (W,L) is Element of bool (VAL L)
VAL L is set
bool (VAL L) is set
u2 is Relation-like VAR -defined L -valued Function-like quasi_total Element of bool [:VAR,L:]
u2 * decode is Relation-like NAT -defined L -valued Function-like Element of bool [:NAT,L:]
(u2 * decode) | (code (Free W)) is Relation-like NAT -defined L -valued Function-like V35() Element of bool [:NAT,L:]
i is Relation-like Function-like set
dom i is set
dom (u2 * decode) is Element of bool NAT
(dom (u2 * decode)) /\ (code (Free W)) is V35() Element of bool NAT
a is Element of VAR
x". a is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
W is non empty epsilon-transitive V33() V34() universal set
bool W is set
L is non empty Element of bool W
ksi is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
lambda is non empty set
[:VAR,lambda:] is set
bool [:VAR,lambda:] is set
l is Relation-like VAR -defined lambda -valued Function-like quasi_total Element of bool [:VAR,lambda:]
(ksi,lambda,l) is Element of bool lambda
bool lambda is set
Free ksi is V35() Element of bool VAR
Free ksi is V35() Element of bool VAR
code (Free ksi) is V35() Element of bool NAT
u1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
{u1} is non empty trivial V35() V39() 1 -element set
(code (Free ksi)) \ {u1} is V35() Element of bool NAT
Diagram (ksi,lambda) is set
i is Element of W
((code (Free ksi)) \ {u1}) \/ {u1} is V35() set
u is Element of W
Funcs ((((code (Free ksi)) \ {u1}) \/ {u1}),u) is set
a is set
St (ksi,lambda) is Element of bool (VAL lambda)
VAL lambda is set
bool (VAL lambda) is set
Funcs ((code (Free ksi)),u) is set
i is Relation-like VAR -defined lambda -valued Function-like quasi_total Element of bool [:VAR,lambda:]
i * decode is Relation-like NAT -defined lambda -valued Function-like Element of bool [:NAT,lambda:]
[:NAT,lambda:] is non trivial V35() set
bool [:NAT,lambda:] is non trivial V35() set
(i * decode) | (code (Free ksi)) is Relation-like NAT -defined lambda -valued Function-like V35() Element of bool [:NAT,lambda:]
x". (x. 0) is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
l * decode is Relation-like NAT -defined lambda -valued Function-like Element of bool [:NAT,lambda:]
[:NAT,lambda:] is non trivial V35() set
bool [:NAT,lambda:] is non trivial V35() set
(l * decode) | ((code (Free ksi)) \ {u1}) is Relation-like NAT -defined lambda -valued Function-like V35() Element of bool [:NAT,lambda:]
Funcs (((code (Free ksi)) \ {u1}),u) is set
a is Element of W
{ b1 where b1 is Element of lambda : {[u1,b1]} \/ a in i } is set
{ b1 where b1 is Element of W : ( b1 in u & {[u1,b1]} \/ a in i ) } is set
b is set
e is Element of W
[u1,e] is set
{u1,e} is V35() set
{{u1,e},{u1}} is V35() V39() set
{[u1,e]} is Function-like non empty trivial V35() 1 -element set
{[u1,e]} \/ a is set
b is set
e is Element of lambda
[u1,e] is set
{u1,e} is V35() set
{{u1,e},{u1}} is V35() V39() set
{[u1,e]} is Function-like non empty trivial V35() 1 -element set
{[u1,e]} \/ a is set
e is Element of W
Free ksi is V35() Element of bool VAR
W is non empty epsilon-transitive V33() V34() universal set
L is Relation-like non-empty W -valued Function-like T-Sequence-like DOMAIN-yielding set
Union L is non empty Element of bool W
bool W is set
ksi is set
dom L is epsilon-transitive epsilon-connected ordinal set
lambda is set
L . lambda is set
l is epsilon-transitive epsilon-connected ordinal set
On W is non empty epsilon-transitive epsilon-connected ordinal set
u is epsilon-transitive epsilon-connected ordinal Element of W
L . u is non empty Element of W
u1 is set
ksi is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
Free ksi is V35() Element of bool VAR
the_axiom_of_substitution_for ksi is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
ksi is set
union ksi is set
ksi is set
lambda is set
{ksi,lambda} is V35() set
card W is non empty epsilon-transitive epsilon-connected ordinal cardinal set
{ b1 where b1 is Element of W : L . a2 in L . b1 } is set
inf { b1 where b1 is Element of W : L . a2 in L . b1 } is epsilon-transitive epsilon-connected ordinal set
0-element_of W is epsilon-transitive epsilon-connected ordinal Element of W
ksi is Relation-like Function-like set
dom ksi is set
ksi . 0 is set
rng ksi is set
card (rng ksi) is epsilon-transitive epsilon-connected ordinal cardinal set
card NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal V35() cardinal set
sup (rng ksi) is epsilon-transitive epsilon-connected ordinal set
On W is non empty epsilon-transitive epsilon-connected ordinal set
l is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
ksi . l is set
l + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
ksi . (l + 1) is set
u is epsilon-transitive epsilon-connected ordinal Element of W
L . u is non empty Element of W
{ b1 where b1 is Element of W : L . u in L . b1 } is set
inf { b1 where b1 is Element of W : L . u in L . b1 } is epsilon-transitive epsilon-connected ordinal set
dom L is epsilon-transitive epsilon-connected ordinal set
u1 is set
L . u1 is set
u2 is epsilon-transitive epsilon-connected ordinal Element of W
l is set
u is set
ksi . u is set
u1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
ksi . u1 is set
u is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
ksi . u is set
L . (ksi . u) is set
u + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
ksi . (u + 1) is set
L . (ksi . (u + 1)) is set
dom L is epsilon-transitive epsilon-connected ordinal set
u1 is epsilon-transitive epsilon-connected ordinal Element of W
L . u1 is non empty Element of W
u2 is set
L . u2 is set
i is epsilon-transitive epsilon-connected ordinal Element of W
{ b1 where b1 is Element of W : L . u1 in L . b1 } is set
{ b1 where b1 is Element of W : L . (ksi . u) in L . b1 } is set
inf { b1 where b1 is Element of W : L . (ksi . u) in L . b1 } is epsilon-transitive epsilon-connected ordinal set
a is Element of W
L . a is set
u is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
ksi . u is set
u + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
ksi . (u + 1) is set
u1 is epsilon-transitive epsilon-connected ordinal Element of W
u2 is epsilon-transitive epsilon-connected ordinal Element of W
L . u1 is non empty Element of W
L . u2 is non empty Element of W
l is epsilon-transitive epsilon-connected ordinal Element of W
union l is epsilon-transitive epsilon-connected ordinal Element of W
u is epsilon-transitive epsilon-connected ordinal set
u1 is epsilon-transitive epsilon-connected ordinal set
u2 is set
ksi . u2 is set
i is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
i + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
ksi . (i + 1) is set
a is epsilon-transitive epsilon-connected ordinal Element of W
{ (L . (ksi . b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT : verum } is set
union { (L . (ksi . b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT : verum } is set
L . l is non empty Element of W
u1 is set
u2 is set
i is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
ksi . i is set
L . (ksi . i) is set
a is epsilon-transitive epsilon-connected ordinal Element of W
L . a is non empty Element of W
L | l is Relation-like rng L -valued Function-like T-Sequence-like set
rng L is V68() set
Union (L | l) is set
u1 is set
dom (L | l) is epsilon-transitive epsilon-connected ordinal set
u2 is set
(L | l) . u2 is set
L . u2 is set
dom L is epsilon-transitive epsilon-connected ordinal set
(dom L) /\ l is set
i is epsilon-transitive epsilon-connected ordinal Element of W
a is epsilon-transitive epsilon-connected ordinal set
i is set
ksi . i is set
i is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
ksi . i is set
b is epsilon-transitive epsilon-connected ordinal Element of W
L . i is non empty Element of W
L . b is non empty Element of W
L . (ksi . i) is set
L . (sup (rng ksi)) is set
u is set
u1 is set
u2 is set
i is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
ksi . i is set
L . (ksi . i) is set
a is epsilon-transitive epsilon-connected ordinal Element of W
L . a is non empty Element of W
i + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V28() V29() V35() cardinal Element of NAT
ksi . (i + 1) is set
L . (ksi . (i + 1)) is set
ksi is set