:: ZF_FUND2 semantic presentation

REAL is set

bool NAT is non trivial V35() set
bool NAT is non trivial V35() set
VAR is non empty Element of bool NAT

is non trivial V35() set
bool is non trivial V35() set
{} is set

x. 0 is Element of VAR
x. 1 is Element of VAR

x. 2 is Element of VAR
{(),(x. 1),(x. 2)} is V35() set

x. 3 is Element of VAR

x. 4 is Element of VAR

L is non empty set
[:VAR,L:] is set
bool [:VAR,L:] is set

Free W is V35() Element of bool VAR

{ b1 where b1 is Element of L : L,ksi / ((),b1) |= W } is set
bool L is set
l is set
u is Element of L

((x. 2) 'in' ()) => ((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. 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 / ((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. 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. 2) 'in' (x. 1))))) is V35() Element of bool VAR
Free (((x. 2) 'in' ()) => ((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. 2) 'in' (x. 1)))) \ {(x. 2)} is V35() Element of bool VAR
Free ((x. 2) 'in' ()) is V35() Element of bool VAR
Free ((x. 2) 'in' (x. 1)) is V35() Element of bool VAR
(Free ((x. 2) 'in' ())) \/ (Free ((x. 2) 'in' (x. 1))) is V35() Element of bool VAR
((Free ((x. 2) 'in' ())) \/ (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. 2),(x. 1)} is V35() set
((Free ((x. 2) 'in' ())) \/ {(x. 2),(x. 1)}) \ {(x. 2)} is V35() Element of bool ((Free ((x. 2) 'in' ())) \/ {(x. 2),(x. 1)})
bool ((Free ((x. 2) 'in' ())) \/ {(x. 2),(x. 1)}) is V35() V39() set
{(x. 2),()} is V35() set
{(x. 2),()} \/ {(x. 2),(x. 1)} is V35() set
({(x. 2),()} \/ {(x. 2),(x. 1)}) \ {(x. 2)} is V35() Element of bool ({(x. 2),()} \/ {(x. 2),(x. 1)})
bool ({(x. 2),()} \/ {(x. 2),(x. 1)}) is V35() V39() set
{(x. 2),()} \ {(x. 2)} is V35() Element of bool {(x. 2),()}
bool {(x. 2),()} 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. 2)}) \/ ({(x. 2),(x. 1)} \ {(x. 2)}) is V35() set
{(x. 1)} is non empty trivial V35() 1 -element set
({(x. 2),()} \ {(x. 2)}) \/ {(x. 1)} is V35() set
{()} is non empty trivial V35() 1 -element set
{()} \/ {(x. 1)} is V35() set
{(),(x. 1)} is V35() set
{ b1 where b1 is Element of W : W,(ksi / ((x. 1),L)) / ((),b1) |= All ((x. 2),(((x. 2) 'in' ()) => ((x. 2) 'in' (x. 1)))) } is set
u1 is set
u2 is Element of W
(ksi / ((x. 1),L)) / ((),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)) / ((),u2)) / ((x. 2),a) is Relation-like VAR -defined W -valued Function-like quasi_total Element of bool [:VAR,W:]
(((ksi / ((x. 1),L)) / ((),u2)) / ((x. 2),a)) . (x. 2) is Element of W
(((ksi / ((x. 1),L)) / ((),u2)) / ((x. 2),a)) . (x. 1) is Element of W
((ksi / ((x. 1),L)) / ((),u2)) . (x. 1) is Element of W
(ksi / ((x. 1),L)) . (x. 1) is Element of W
((ksi / ((x. 1),L)) / ((),u2)) . () is Element of W
(((ksi / ((x. 1),L)) / ((),u2)) / ((x. 2),a)) . () 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)) / ((),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)) / ((),u2)) / ((x. 2),i) is Relation-like VAR -defined W -valued Function-like quasi_total Element of bool [:VAR,W:]
(((ksi / ((x. 1),L)) / ((),u2)) / ((x. 2),i)) . (x. 2) is Element of W
((ksi / ((x. 1),L)) / ((),u2)) . () is Element of W
(((ksi / ((x. 1),L)) / ((),u2)) / ((x. 2),i)) . () is Element of W
(((ksi / ((x. 1),L)) / ((),u2)) / ((x. 2),i)) . (x. 1) is Element of W
((ksi / ((x. 1),L)) / ((),u2)) . (x. 1) is Element of W

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

Union L is non empty Element of bool W
bool W is set
lambda is set
bool lambda is set

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

u1 is Element of L . l

((All ((x. 2),(((x. 2) 'in' ()) => ((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
() /\ (bool lambda) is Element of bool W
l is non empty set
u is Element of l

u1 is set
L . u1 is set

L . u2 is 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

L . a is non empty Element of W
u .: (dom u) is set

L . u1 is non empty Element of W
u2 is set
i is Element of l
u . i is set

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
() /\ ((bool lambda) /\ (bool lambda)) is Element of bool W
lambda is set

l is set
L . l is set

L . u1 is non empty Element of W
u2 is set

variables_in W is non empty Element of bool VAR
Free W is V35() Element of bool VAR

All ((x. 4),(W <=> ((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
Ex ((),(All ((x. 4),(W <=> ((x. 4) '=' ()))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((),(All ((x. 4),(W <=> ((x. 4) '=' ()))))))) 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

[:L,L:] is set
bool [:L,L:] is set
lambda is Element of VAR
W / ((),lambda) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
Free (W / ((),lambda)) is V35() Element of bool VAR
(W / ((),lambda)) <=> ((x. 4) '=' ()) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
All ((x. 4),((W / ((),lambda)) <=> ((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
Ex ((),(All ((x. 4),((W / ((),lambda)) <=> ((x. 4) '=' ()))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((),(All ((x. 4),((W / ((),lambda)) <=> ((x. 4) '=' ()))))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
def_func' ((W / ((),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)) / ((),(((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)) / ((),(((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))) / ((),(((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 / ((),lambda)),ksi)) . l is set

All ((x. 4),(W <=> ((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
Ex ((),(All ((x. 4),(W <=> ((x. 4) '=' ()))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((),(All ((x. 4),(W <=> ((x. 4) '=' ()))))))) 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

[: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)) / ((),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)) / ((),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)) / ((),l)) / ((x. 4),i)) . (x. 4) is Element of L
(((ksi / ((x. 3), the Element of L)) / ((),l)) / ((x. 4),i)) . () is Element of L
((ksi / ((x. 3), the Element of L)) / ((),l)) . () is Element of L
a is Element of L

variables_in W is non empty Element of bool VAR
Free W is V35() Element of bool VAR
L is Element of VAR

(W / ((),L)) / ((x. 4),()) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
ksi is Element of VAR

((x. 3) 'in' ksi) '&' ((W / ((),L)) / ((x. 4),())) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
Ex ((x. 3),(((x. 3) 'in' ksi) '&' ((W / ((),L)) / ((x. 4),())))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
Free (Ex ((x. 3),(((x. 3) 'in' ksi) '&' ((W / ((),L)) / ((x. 4),()))))) is V35() Element of bool VAR
Free (((x. 3) 'in' ksi) '&' ((W / ((),L)) / ((x. 4),()))) is V35() Element of bool VAR
{(x. 3)} is non empty trivial V35() 1 -element set
(Free (((x. 3) 'in' ksi) '&' ((W / ((),L)) / ((x. 4),())))) \ {(x. 3)} is V35() Element of bool VAR
Free ((x. 3) 'in' ksi) is V35() Element of bool VAR
Free ((W / ((),L)) / ((x. 4),())) is V35() Element of bool VAR
(Free ((x. 3) 'in' ksi)) \/ (Free ((W / ((),L)) / ((x. 4),()))) is V35() Element of bool VAR
((Free ((x. 3) 'in' ksi)) \/ (Free ((W / ((),L)) / ((x. 4),())))) \ {(x. 3)} is V35() Element of bool VAR
{(x. 3),ksi} is V35() set
{(x. 3),ksi} \/ (Free ((W / ((),L)) / ((x. 4),()))) is V35() set
({(x. 3),ksi} \/ (Free ((W / ((),L)) / ((x. 4),())))) \ {(x. 3)} is V35() Element of bool ({(x. 3),ksi} \/ (Free ((W / ((),L)) / ((x. 4),()))))
bool ({(x. 3),ksi} \/ (Free ((W / ((),L)) / ((x. 4),())))) 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 / ((),L)) / ((x. 4),()))) \ {(x. 3)} is V35() Element of bool VAR
({(x. 3),ksi} \ {(x. 3)}) \/ ((Free ((W / ((),L)) / ((x. 4),()))) \ {(x. 3)}) is V35() set
Free (W / ((),L)) is V35() Element of bool VAR
{()} is non empty trivial V35() 1 -element set
(Free W) \ {()} is V35() Element of bool VAR
{L} is non empty trivial V35() 1 -element set
((Free W) \ {()}) \/ {L} is V35() set
{()} is non empty trivial V35() 1 -element set
variables_in (W / ((),L)) is non empty Element of bool VAR
{(x. 4)} is non empty trivial V35() 1 -element set
(Free (W / ((),L))) \ {(x. 4)} is V35() Element of bool VAR
((Free (W / ((),L))) \ {(x. 4)}) \/ {()} is V35() set
(Free W) \ {()} is V35() Element of bool VAR
{L} is non empty trivial V35() 1 -element set
((Free W) \ {()}) \/ {L} is V35() set
W is non empty epsilon-transitive V33() V34() universal set

Union L is non empty Element of bool W
bool W is set
[:VAR,():] is set
bool [:VAR,():] is set

Free lambda is V35() Element of bool VAR

lambda <=> ((x. 4) '=' ()) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
All ((x. 4),(lambda <=> ((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
Ex ((),(All ((x. 4),(lambda <=> ((x. 4) '=' ()))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((),(All ((x. 4),(lambda <=> ((x. 4) '=' ()))))))) 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

x. (u + 5) is Element of VAR
lambda / ((),(x. (u + 5))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

(lambda / ((),(x. (u + 5)))) <=> ((x. 4) '=' ()) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
All ((x. 4),((lambda / ((),(x. (u + 5)))) <=> ((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
Ex ((),(All ((x. 4),((lambda / ((),(x. (u + 5)))) <=> ((x. 4) '=' ()))))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((),(All ((x. 4),((lambda / ((),(x. (u + 5)))) <=> ((x. 4) '=' ()))))))) 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 [:(),():]
[:(),():] is set
bool [:(),():] is set
def_func' ((lambda / ((),(x. (u + 5)))),l) is Relation-like Union L -defined Union L -valued Function-like quasi_total Element of bool [:(),():]
i is Element of Union L

a is set
L . a is set

L . i is 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

L . b is non empty Element of W

dom l is Element of bool VAR

rng l is Element of bool ()
bool () is set
l .: (dom l) is Element of bool ()

i .: (rng l) is set

Free (lambda / ((),(x. (u + 5)))) is V35() Element of bool VAR
i is set
i .: i is set

L . i is non empty Element of W
b is set
e is Element of Union L
i . e is set

L . e is non empty Element of W
i is Element of Union L
i . i is set

L . i is non empty Element of W

variables_in (lambda / ((),(x. (u + 5)))) is non empty Element of bool VAR
(def_func' (lambda,l)) .: i is Element of bool ()
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

L . (i \/ b) is non empty Element of W

[:(On W),(On W):] is set
bool [:(On W),(On W):] is set
(lambda / ((),(x. (u + 5)))) / ((x. 4),()) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

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

L . v is non empty Element of W

x. (u + 10) is Element of VAR
{()} is non empty trivial V35() 1 -element set
(variables_in lambda) \ {()} 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. (u + 5)))) / ((x. 4),())) 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. (u + 5)))) / ((x. 4),())))) is Relation-like NAT -defined NAT -valued Function-like V43() ZF-formula-like M7( NAT )

[:VAR,(L . a1):] is set
bool [:VAR,(L . a1):] is set

v . (x. 4) is Element of L . a1
v / ((),(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 / ((),(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. (u + 5))} is set
variables_in ((lambda / ((),(x. (u + 5)))) / ((x. 4),())) is non empty Element of bool VAR
{(x. 4)} is non empty trivial V35() 1 -element set
(variables_in (lambda / ((),(x. (u + 5))))) \ {(x. 4)} is Element of bool VAR
((variables_in (lambda / ((),(x. (u + 5))))) \ {(x. 4)}) \/ {()} is set
((Ex ((x. 3),(((x. 3) 'in' (x. (u + 10))) '&' ((lambda / ((),(x. (u + 5)))) / ((x. 4),()))))),(L . a1),((v / ((),(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. (u + 5)))) / ((x. 4),()))))) is V35() Element of bool VAR
u1 is set
dom (def_func' (lambda,l)) is Element of bool ()
m1 is set
(def_func' (lambda,l)) . m1 is set
u9 is Element of Union L

(def_func' (lambda,l)) . u9 is Element of Union L
(l / ((x. 3),u9)) / ((),((def_func' (lambda,l)) . u9)) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,():]
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)) / ((),m2) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]
() ! ((v / ((x. 3),u2)) / ((),m2)) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,():]
(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,():]
((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))) / ((),((def_func' (lambda,l)) . u9)) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,():]
((l / ((x. 3),u9)) / ((),((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,():]
((v / ((x. 3),u2)) / ((),m2)) / ((x. (u + 10)),mu) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]
((v / ((),(v . (x. 4)))) / ((x. (u + 10)),mu)) . (x. (u + 10)) is Element of L . a1
((v / ((),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((),m2) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]
(((v / ((),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((),m2)) . (x. (u + 10)) is Element of L . a1
(((v / ((),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((),m2)) / ((x. 3),u2) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]
((((v / ((),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((),m2)) / ((x. 3),u2)) . (x. 3) is Element of L . a1
((((v / ((),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((),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)) / ((),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 / ((),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((),b1) |= Ex ((x. 3),(((x. 3) 'in' (x. (u + 10))) '&' ((lambda / ((),(x. (u + 5)))) / ((x. 4),())))) } is set
u1 is set
{ b1 where b1 is Element of L . a1 : L . a1,((v / ((),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((),b1) |= Ex ((x. 3),(((x. 3) 'in' (x. (u + 10))) '&' ((lambda / ((),(x. (u + 5)))) / ((x. 4),())))) } is set
m1 is Element of L . a1
((v / ((),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((),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 / ((),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((),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)) / ((),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)) / ((),m1) is Relation-like VAR -defined L . a1 -valued Function-like quasi_total Element of bool [:VAR,(L . a1):]
((v / ((x. 3),m2)) / ((),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

u9 is Element of Union L
(l / ((x. 3),u2)) / ((),u9) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,():]
((l / ((x. 3),u2)) / ((),u9)) / ((x. 4),u9) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,():]
(l / ((x. 3),u2)) / ((x. 4),u9) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,():]
((l / ((x. 3),u2)) / ((x. 4),u9)) / ((),u9) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,():]
((l / ((x. 3),u2)) / ((),u9)) . () is Element of Union L
() ! ((v / ((x. 3),m2)) / ((),m1)) is Relation-like VAR -defined Union L -valued Function-like quasi_total Element of bool [:VAR,():]
(def_func' (lambda,l)) . u2 is Element of Union L
((v / ((),(v . (x. 4)))) / ((x. (u + 10)),mu)) . (x. (u + 10)) is Element of L . a1
(((v / ((),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((),m1)) . (x. (u + 10)) is Element of L . a1
dom (def_func' (lambda,l)) is Element of bool ()
((((v / ((),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((),m1)) / ((x. 3),m2)) . (x. 3) is Element of L . a1
((((v / ((),(v . (x. 4)))) / ((x. (u + 10)),mu)) / ((),m1)) / ((x. 3),m2)) . (x. (u + 10)) is Element of L . a1
Free (Ex ((x. 3),(((x. 3) 'in' (x. (u + 10))) '&' ((lambda / ((),(x. (u + 5)))) / ((x. 4),()))))) is V35() Element of bool VAR
lambda is set

l is set
L . l is set

L . u1 is non empty Element of W
u2 is set

Free lambda is V35() Element of bool VAR

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

[:NAT,L:] is non trivial V35() set
bool [:NAT,L:] is non trivial V35() set

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

((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

((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

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

(W,L,ksi) is Element of bool L
bool L is set

[: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 / ((),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 / ((),u1)) * decode is Relation-like NAT -defined L -valued Function-like Element of bool [:NAT,L:]
((ksi / ((),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 * 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

St (W,L) is Element of bool (VAL L)
VAL L is set
bool (VAL L) is set
(ksi / ((),u1)) * decode is Relation-like NAT -defined L -valued Function-like Element of bool [:NAT,L:]
((ksi / ((),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 * decode) | (code (Free W)) is Relation-like NAT -defined L -valued Function-like V35() Element of bool [:NAT,L:]

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

W is non empty epsilon-transitive V33() V34() universal set
bool W is set
L is non empty Element of bool W

lambda is non empty set
[:VAR,lambda:] is set
bool [:VAR,lambda:] is set

(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 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 * 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
() | (code (Free ksi)) is Relation-like NAT -defined lambda -valued Function-like V35() Element of bool [:NAT,lambda:]

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

Union L is non empty Element of bool W
bool W is set
ksi is set

lambda is set
L . lambda is set

L . u is non empty Element of W
u1 is set

Free ksi is V35() Element of bool VAR

ksi is set
union ksi is set
ksi is set
lambda is set
{ksi,lambda} is V35() 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

dom ksi is set
ksi . 0 is set
rng ksi is set

ksi . l is set

ksi . (l + 1) is set

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

u1 is set
L . u1 is set

l is set
u is set
ksi . u is set

ksi . u1 is set

ksi . u is set
L . (ksi . u) is set

ksi . (u + 1) is set
L . (ksi . (u + 1)) is set

L . u1 is non empty Element of W
u2 is set
L . u2 is set

{ 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

ksi . u is set

ksi . (u + 1) is set

L . u1 is non empty Element of W
L . u2 is non empty Element of W

u2 is set
ksi . u2 is set

ksi . (i + 1) is set

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

ksi . i is set
L . (ksi . i) is set

L . a is non empty Element of W

rng L is V68() set
Union (L | l) is set
u1 is set

u2 is set
(L | l) . u2 is set
L . u2 is set

(dom L) /\ l is set

i is set
ksi . i is set

ksi . i is set

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

ksi . i is set
L . (ksi . i) is set

L . a is non empty Element of W

ksi . (i + 1) is set
L . (ksi . (i + 1)) is set
ksi is set