:: ZF_FUND1 semantic presentation

REAL is set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of bool REAL
bool REAL is set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set
bool NAT is non trivial non finite set
bool NAT is non trivial non finite set
VAR is non empty Element of bool NAT
bool VAR is set
{} is set
the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real V33() V34() finite finite-yielding V48() cardinal {} -element set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real V33() V34() finite finite-yielding V48() cardinal {} -element set
1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
5 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT : 5 <= b₁ } is set
{{}} is non empty trivial finite 1 -element set
V is non empty epsilon-transitive V35() V36() universal set
the Element of V is Element of V
[: the Element of V, the Element of V:] is Relation-like Element of V
V is non empty epsilon-transitive V35() V36() universal set
X is Element of V
E is Element of V
X (#) E is Relation-like set
v1 is set
m is set
m is set
[:m,v1:] is Relation-like set
n is Relation-like Function-like set
proj1 n is set
proj2 n is set
fs is set
Dn is set
[fs,Dn] is V22() set
{fs,Dn} is finite set
{fs} is non empty trivial finite 1 -element set
{{fs,Dn},{fs}} is finite V48() set
C is set
[fs,C] is V22() set
{fs,C} is finite set
{{fs,C},{fs}} is finite V48() set
[C,Dn] is V22() set
{C,Dn} is finite set
{C} is non empty trivial finite 1 -element set
{{C,Dn},{C}} is finite V48() set
[[fs,C],[C,Dn]] is V22() set
{[fs,C],[C,Dn]} is Relation-like finite set
{[fs,C]} is Relation-like Function-like constant non empty trivial finite 1 -element set
{{[fs,C],[C,Dn]},{[fs,C]}} is finite V48() set
n . [[fs,C],[C,Dn]] is set
[[fs,C],[C,Dn]] `1 is set
([[fs,C],[C,Dn]] `1) `1 is set
[[fs,C],[C,Dn]] `2 is set
([[fs,C],[C,Dn]] `2) `2 is set
[(([[fs,C],[C,Dn]] `1) `1),(([[fs,C],[C,Dn]] `2) `2)] is V22() set
{(([[fs,C],[C,Dn]] `1) `1),(([[fs,C],[C,Dn]] `2) `2)} is finite set
{(([[fs,C],[C,Dn]] `1) `1)} is non empty trivial finite 1 -element set
{{(([[fs,C],[C,Dn]] `1) `1),(([[fs,C],[C,Dn]] `2) `2)},{(([[fs,C],[C,Dn]] `1) `1)}} is finite V48() set
[fs,C] `1 is set
[([fs,C] `1),(([[fs,C],[C,Dn]] `2) `2)] is V22() set
{([fs,C] `1),(([[fs,C],[C,Dn]] `2) `2)} is finite set
{([fs,C] `1)} is non empty trivial finite 1 -element set
{{([fs,C] `1),(([[fs,C],[C,Dn]] `2) `2)},{([fs,C] `1)}} is finite V48() set
[C,Dn] `2 is set
[([fs,C] `1),([C,Dn] `2)] is V22() set
{([fs,C] `1),([C,Dn] `2)} is finite set
{{([fs,C] `1),([C,Dn] `2)},{([fs,C] `1)}} is finite V48() set
[fs,([C,Dn] `2)] is V22() set
{fs,([C,Dn] `2)} is finite set
{{fs,([C,Dn] `2)},{fs}} is finite V48() set
card (X (#) E) is epsilon-transitive epsilon-connected ordinal cardinal set
card [:m,v1:] is epsilon-transitive epsilon-connected ordinal cardinal set
n is Relation-like Function-like set
proj1 n is set
proj2 n is set
n is set
card V is non empty epsilon-transitive epsilon-connected ordinal cardinal set
v1 is set
m is set
[v1,m] is V22() set
{v1,m} is finite set
{v1} is non empty trivial finite 1 -element set
{{v1,m},{v1}} is finite V48() set
n is set
[v1,n] is V22() set
{v1,n} is finite set
{{v1,n},{v1}} is finite V48() set
[n,m] is V22() set
{n,m} is finite set
{n} is non empty trivial finite 1 -element set
{{n,m},{n}} is finite V48() set
[:NAT,VAR:] is Relation-like non trivial non finite set
bool [:NAT,VAR:] is non trivial non finite set
() is Relation-like NAT -defined VAR -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,VAR:]
V is Element of VAR
X is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
E is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal set
5 + E is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
H is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
x. H is Element of VAR
X is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
x. X is Element of VAR
E is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
x. E is Element of VAR
5 + X is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
5 + E is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
dom () is non empty Element of bool NAT
rng () is non empty Element of bool VAR
() " is Relation-like Function-like set
proj1 (() ") is set
proj2 (() ") is set
V is set
X is Element of VAR
(X) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
E is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
() . E is Element of VAR
card (X) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
x. (card (X)) is Element of VAR
x. (X) is Element of VAR
X is set
() . X is set
E is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
() . E is Element of VAR
V is set
X is set
() . V is set
() . X is set
E is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
card E is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
x. (card E) is Element of VAR
H is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
card H is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
x. (card H) is Element of VAR
5 + (card E) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
5 + (card H) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
v1 is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
card m is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
V is Element of bool VAR
(() ") .: V is set
V is finite Element of bool VAR
(V) is Element of bool NAT
(() ") .: V is finite set
X is non empty set
[:VAR,X:] is Relation-like set
bool [:VAR,X:] is set
V is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
Free V is finite Element of bool VAR
((Free V)) is finite Element of bool NAT
(() ") .: (Free V) is finite set
St (V,X) is Element of bool (VAL X)
VAL X is set
bool (VAL X) is set
Funcs (((Free V)),X) is functional non empty FUNCTION_DOMAIN of ((Free V)),X
E is set
H is set
v1 is Relation-like VAR -defined X -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,X:]
v1 * () is Relation-like NAT -defined X -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,X:]
[:NAT,X:] is Relation-like non trivial non finite set
bool [:NAT,X:] is non trivial non finite set
(v1 * ()) | ((Free V)) is Relation-like NAT -defined ((Free V)) -defined NAT -defined X -valued Function-like finite Element of bool [:NAT,X:]
dom (v1 * ()) is non empty Element of bool NAT
dom ((v1 * ()) | ((Free V))) is finite Element of bool NAT
NAT /\ ((Free V)) is finite Element of bool NAT
rng ((v1 * ()) | ((Free V))) is finite Element of bool X
bool X is set
v1 is Relation-like VAR -defined X -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,X:]
v1 * () is Relation-like NAT -defined X -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,X:]
(v1 * ()) | ((Free V)) is Relation-like NAT -defined ((Free V)) -defined NAT -defined X -valued Function-like finite Element of bool [:NAT,X:]
H is set
v1 is set
m is Relation-like VAR -defined X -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,X:]
m * () is Relation-like NAT -defined X -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,X:]
[:NAT,X:] is Relation-like non trivial non finite set
bool [:NAT,X:] is non trivial non finite set
(m * ()) | ((Free V)) is Relation-like NAT -defined ((Free V)) -defined NAT -defined X -valued Function-like finite Element of bool [:NAT,X:]
E is set
H is set
v1 is set
m is Relation-like VAR -defined X -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,X:]
m * () is Relation-like NAT -defined X -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,X:]
[:NAT,X:] is Relation-like non trivial non finite set
bool [:NAT,X:] is non trivial non finite set
(m * ()) | ((Free V)) is Relation-like NAT -defined ((Free V)) -defined NAT -defined X -valued Function-like finite Element of bool [:NAT,X:]
v1 is set
m is Relation-like VAR -defined X -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,X:]
m * () is Relation-like NAT -defined X -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,X:]
[:NAT,X:] is Relation-like non trivial non finite set
bool [:NAT,X:] is non trivial non finite set
(m * ()) | ((Free V)) is Relation-like NAT -defined ((Free V)) -defined NAT -defined X -valued Function-like finite Element of bool [:NAT,X:]
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
V is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
card V is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
x. (card V) is Element of VAR
((x. (card V))) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
V is finite Element of bool NAT
X is non empty set
[:VAR,X:] is Relation-like set
bool [:VAR,X:] is set
Funcs (V,X) is functional non empty FUNCTION_DOMAIN of V,X
E is Relation-like VAR -defined X -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,X:]
E * () is Relation-like NAT -defined X -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,X:]
[:NAT,X:] is Relation-like non trivial non finite set
bool [:NAT,X:] is non trivial non finite set
(E * ()) | V is Relation-like NAT -defined V -defined NAT -defined X -valued Function-like finite Element of bool [:NAT,X:]
dom ((E * ()) | V) is finite Element of bool V
bool V is finite V48() set
rng ((E * ()) | V) is finite Element of bool X
bool X is set
dom (E * ()) is non empty Element of bool NAT
V is non empty set
[:VAR,V:] is Relation-like set
bool [:VAR,V:] is set
X is Relation-like VAR -defined V -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,V:]
X * () is Relation-like NAT -defined V -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,V:]
[:NAT,V:] is Relation-like non trivial non finite set
bool [:NAT,V:] is non trivial non finite set
E is Element of VAR
(E) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
() . (E) is Element of VAR
(() ") . E is set
(X * ()) . (E) is Element of V
X . E is Element of V
card (E) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
x. (card (E)) is Element of VAR
x. (E) is Element of VAR
dom (X * ()) is non empty Element of bool NAT
V is set
X is finite Element of bool VAR
(X) is finite Element of bool NAT
(() ") .: X is finite set
E is set
(() ") . E is set
H is set
(() ") . H is set
H is set
(() ") . H is set
v1 is Element of VAR
(v1) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
() . V is set
E is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
card E is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
x. (card E) is Element of VAR
E is Element of VAR
(E) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
(() ") . E is set
V is Element of VAR
{V} is non empty trivial finite 1 -element Element of bool VAR
({V}) is finite Element of bool NAT
(() ") .: {V} is finite set
(V) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
{(V)} is non empty trivial finite V48() 1 -element Element of bool NAT
X is set
E is Element of VAR
(E) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
X is set
V is Element of VAR
(V) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
X is Element of VAR
{V,X} is finite Element of bool VAR
({V,X}) is finite Element of bool NAT
(() ") .: {V,X} is finite set
(X) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
{(V),(X)} is finite V48() Element of bool NAT
E is set
H is Element of VAR
(H) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
E is set
V is finite Element of bool VAR
(V) is finite Element of bool NAT
(() ") .: V is finite set
(() ") | V is Relation-like Function-like finite set
proj2 ((() ") | V) is finite set
proj1 ((() ") | V) is finite set
(proj1 (() ")) /\ V is finite Element of bool VAR
V is non empty set
[:VAR,V:] is Relation-like set
bool [:VAR,V:] is set
X is Relation-like VAR -defined V -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,V:]
X * () is Relation-like NAT -defined V -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,V:]
[:NAT,V:] is Relation-like non trivial non finite set
bool [:NAT,V:] is non trivial non finite set
E is Element of VAR
(E) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
X . E is Element of V
H is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
Free H is finite Element of bool VAR
((Free H)) is finite Element of bool NAT
(() ") .: (Free H) is finite set
(X * ()) | ((Free H)) is Relation-like NAT -defined ((Free H)) -defined NAT -defined V -valued Function-like finite Element of bool [:NAT,V:]
((X * ()) | ((Free H))) . (E) is set
dom ((X * ()) | ((Free H))) is finite Element of bool NAT
(X * ()) . (E) is Element of V
V is non empty set
[:VAR,V:] is Relation-like set
bool [:VAR,V:] is set
X is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
Free X is finite Element of bool VAR
((Free X)) is finite Element of bool NAT
(() ") .: (Free X) is finite set
St (X,V) is Element of bool (VAL V)
VAL V is set
bool (VAL V) is set
E is Relation-like VAR -defined V -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,V:]
E * () is Relation-like NAT -defined V -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,V:]
[:NAT,V:] is Relation-like non trivial non finite set
bool [:NAT,V:] is non trivial non finite set
(E * ()) | ((Free X)) is Relation-like NAT -defined ((Free X)) -defined NAT -defined V -valued Function-like finite Element of bool [:NAT,V:]
H is Relation-like VAR -defined V -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,V:]
H * () is Relation-like NAT -defined V -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,V:]
(H * ()) | ((Free X)) is Relation-like NAT -defined ((Free X)) -defined NAT -defined V -valued Function-like finite Element of bool [:NAT,V:]
v1 is Element of VAR
E . v1 is Element of V
H . v1 is Element of V
(v1) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
((H * ()) | ((Free X))) . (v1) is set
V is set
X is finite Element of bool NAT
E is non empty set
Funcs (X,E) is functional non empty FUNCTION_DOMAIN of X,E
[:VAR,E:] is Relation-like set
bool [:VAR,E:] is set
the Element of E is Element of E
[:X,E:] is Relation-like set
bool [:X,E:] is set
m is Relation-like Function-like set
proj1 m is set
proj2 m is set
v1 is Relation-like X -defined E -valued Function-like V14(X) quasi_total finite Element of bool [:X,E:]
dom v1 is finite Element of bool X
bool X is finite V48() set
m is set
v1 . m is set
rng v1 is finite Element of bool E
bool E is set
[:NAT,E:] is Relation-like non trivial non finite set
bool [:NAT,E:] is non trivial non finite set
m is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
[:VAR,NAT:] is Relation-like non trivial non finite set
bool [:VAR,NAT:] is non trivial non finite set
(() ") (#) m is Relation-like E -valued Function-like set
n is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
n * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
(n * ()) | X is Relation-like NAT -defined X -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
dom m is non empty Element of bool NAT
(dom m) /\ X is finite Element of bool NAT
fs is Relation-like Function-like set
proj1 fs is set
proj2 fs is set
fs is set
m . fs is set
v1 . fs is set
Dn is Relation-like Function-like set
proj1 Dn is set
proj2 Dn is set
id (dom ()) is Relation-like dom () -defined dom () -valued Function-like one-to-one non empty V14( dom ()) quasi_total Element of bool [:(dom ()),(dom ()):]
[:(dom ()),(dom ()):] is Relation-like set
bool [:(dom ()),(dom ()):] is set
m * (id (dom ())) is Relation-like dom () -defined E -valued Function-like Element of bool [:(dom ()),E:]
[:(dom ()),E:] is Relation-like set
bool [:(dom ()),E:] is set
() (#) (() ") is Relation-like NAT -defined Function-like set
(() (#) (() ")) (#) m is Relation-like NAT -defined E -valued Function-like set
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
X is non empty Element of bool V
E is set
H is set
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
X is non empty Element of bool V
E is set
{E} is non empty trivial finite 1 -element set
H is set
union H is set
{E,E} is finite set
union {E} is set
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
X is non empty Element of bool V
the Element of X is Element of X
0-element_of V is epsilon-transitive epsilon-connected ordinal Element of V
1-element_of V is non empty epsilon-transitive epsilon-connected ordinal Element of V
H is Element of V
{H} is non empty trivial finite 1 -element Element of V
{ {[(0-element_of V),b₁],[(1-element_of V),b₂]} where b₁, b₂ is Element of V : ( b₁ in b₂ & b₁ in {H} & b₂ in {H} ) } is set
the Element of { {[(0-element_of V),b₁],[(1-element_of V),b₂]} where b₁, b₂ is Element of V : ( b₁ in b₂ & b₁ in {H} & b₂ in {H} ) } is Element of { {[(0-element_of V),b₁],[(1-element_of V),b₂]} where b₁, b₂ is Element of V : ( b₁ in b₂ & b₁ in {H} & b₂ in {H} ) }
n is Element of V
[(0-element_of V),n] is V22() Element of V
{(0-element_of V),n} is finite set
{(0-element_of V)} is non empty trivial finite 1 -element set
{{(0-element_of V),n},{(0-element_of V)}} is finite V48() set
fs is Element of V
[(1-element_of V),fs] is V22() Element of V
{(1-element_of V),fs} is finite set
{(1-element_of V)} is non empty trivial finite 1 -element set
{{(1-element_of V),fs},{(1-element_of V)}} is finite V48() set
{[(0-element_of V),n],[(1-element_of V),fs]} is Relation-like finite Element of V
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
X is non empty Element of bool V
E is set
H is set
E \/ H is set
E \ H is Element of bool E
bool E is set
E (#) H is Relation-like set
m is Element of V
{m} is non empty trivial finite 1 -element Element of V
v1 is Element of V
{v1} is non empty trivial finite 1 -element Element of V
{ (b₁ \/ b₂) where b₁, b₂ is Element of V : ( b₁ in {m} & b₂ in {v1} ) } is set
fs is set
Dn is Element of V
C is Element of V
Dn \/ C is Element of V
m \/ v1 is Element of V
{(m \/ v1)} is non empty trivial finite 1 -element Element of V
{ (b₁ \ b₂) where b₁, b₂ is Element of V : ( b₁ in {m} & b₂ in {v1} ) } is set
Dn is set
C is Element of V
p is Element of V
C \ p is Element of V
m \ v1 is Element of V
{(m \ v1)} is non empty trivial finite 1 -element Element of V
{ (V,b₁,b₂) where b₁, b₂ is Element of V : ( b₁ in {m} & b₂ in {v1} ) } is set
C is set
p is Element of V
f is Element of V
(V,p,f) is Relation-like Element of V
(V,m,v1) is Relation-like Element of V
{(V,m,v1)} is non empty trivial finite 1 -element Element of V
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
X is non empty Element of bool V
E is set
H is set
E /\ H is set
E \ H is Element of bool E
bool E is set
E \ (E \ H) is Element of bool E
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
X is non empty Element of bool V
E is set
H is set
{E,H} is finite set
[E,H] is V22() set
{E} is non empty trivial finite 1 -element set
{{E,H},{E}} is finite V48() set
v1 is Element of V
m is Element of V
{v1,m} is finite Element of V
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
X is non empty Element of bool V
E is set
H is epsilon-transitive epsilon-connected ordinal set
v1 is epsilon-transitive epsilon-connected ordinal set
succ v1 is non empty epsilon-transitive epsilon-connected ordinal set
{v1} is non empty trivial finite 1 -element set
v1 \/ {v1} is set
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
X is non empty Element of bool V
E is finite Element of bool NAT
Funcs (E,NAT) is functional non empty FUNCTION_DOMAIN of E, NAT
Funcs ({},NAT) is functional non empty FUNCTION_DOMAIN of {} , NAT
H is set
v1 is set
Funcs (v1,NAT) is functional non empty FUNCTION_DOMAIN of v1, NAT
{H} is non empty trivial finite 1 -element set
v1 \/ {H} is set
Funcs ((v1 \/ {H}),NAT) is functional non empty FUNCTION_DOMAIN of v1 \/ {H}, NAT
m is set
n is Relation-like Function-like set
proj1 n is set
proj2 n is set
n | v1 is Relation-like Function-like set
proj2 (n | v1) is set
n | {H} is Relation-like Function-like finite set
proj1 (n | {H}) is finite set
(v1 \/ {H}) /\ {H} is finite set
(n | {H}) . H is set
[H,((n | {H}) . H)] is V22() set
{H,((n | {H}) . H)} is finite set
{{H,((n | {H}) . H)},{H}} is finite V48() set
{[H,((n | {H}) . H)]} is Relation-like Function-like constant non empty trivial finite 1 -element set
proj2 (n | {H}) is finite set
proj1 (n | v1) is set
(v1 \/ {H}) /\ v1 is set
n | (v1 \/ {H}) is Relation-like Function-like set
(n | v1) \/ (n | {H}) is Relation-like set
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
X is Element of V
E is non empty Element of bool V
H is finite Element of bool NAT
Funcs (H,X) is functional set
v1 is set
m is set
Funcs (m,X) is functional set
{v1} is non empty trivial finite 1 -element set
m \/ {v1} is set
Funcs ((m \/ {v1}),X) is functional set
{ {[b₁,b₂]} where b₁, b₂ is Element of V : ( b₁ in {v1} & b₂ in X ) } is set
Funcs ({v1},X) is functional set
C is set
p is Relation-like Function-like set
proj1 p is set
proj2 p is set
p . v1 is set
Dn is Element of V
f is Element of V
[Dn,f] is V22() Element of V
{Dn,f} is finite set
{Dn} is non empty trivial finite 1 -element set
{{Dn,f},{Dn}} is finite V48() set
{[Dn,f]} is Relation-like Function-like constant non empty trivial finite 1 -element Element of V
C is set
p is Element of V
f is Element of V
[p,f] is V22() Element of V
{p,f} is finite set
{p} is non empty trivial finite 1 -element set
{{p,f},{p}} is finite V48() set
{[p,f]} is Relation-like Function-like constant non empty trivial finite 1 -element Element of V
x is Relation-like Function-like set
proj2 x is set
{f} is non empty trivial finite 1 -element Element of V
proj1 x is set
C is Element of V
p is Element of V
{ (b₁ \/ b₂) where b₁, b₂ is Element of V : ( b₁ in C & b₂ in p ) } is set
x is set
u is Relation-like Function-like set
proj1 u is set
proj2 u is set
u | m is Relation-like Function-like set
proj2 (u | m) is set
u | {v1} is Relation-like Function-like finite set
proj2 (u | {v1}) is finite set
proj1 (u | {v1}) is finite set
(m \/ {v1}) /\ {v1} is finite set
proj1 (u | m) is set
(m \/ {v1}) /\ m is set
u | (m \/ {v1}) is Relation-like Function-like set
(u | m) \/ (u | {v1}) is Relation-like set
t is Element of V
q is Element of V
t \/ q is Element of V
x is set
u is Element of V
h is Element of V
u \/ h is Element of V
g is Relation-like Function-like set
proj1 g is set
proj2 g is set
q is Relation-like Function-like set
proj1 q is set
proj2 q is set
g \/ q is Relation-like set
t is Relation-like Function-like set
proj2 t is set
(proj2 g) \/ (proj2 q) is set
X \/ X is Element of V
proj1 t is set
Funcs ({},X) is functional set
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
X is Element of V
E is Element of V
{ (V,X,b₁) where b₁ is Element of V : b₁ in E } is set
H is non empty Element of bool V
v1 is finite Element of bool NAT
Funcs (v1,NAT) is functional non empty FUNCTION_DOMAIN of v1, NAT
{X} is non empty trivial finite 1 -element Element of V
{ (V,b₁,b₂) where b₁, b₂ is Element of V : ( b₁ in {X} & b₂ in E ) } is set
Dn is set
C is Element of V
p is Element of V
(V,C,p) is Relation-like Element of V
(V,X,p) is Relation-like Element of V
Dn is set
C is Element of V
(V,X,C) is Relation-like Element of V
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
X is non empty Element of bool V
E is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
0-element_of V is epsilon-transitive epsilon-connected ordinal Element of V
1-element_of V is non empty epsilon-transitive epsilon-connected ordinal Element of V
X is non empty Element of bool V
succ {} is non empty set
{} \/ {{}} is set
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
X is Element of V
E is Element of V
H is non empty Element of bool V
v1 is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
{v1} is non empty trivial finite V48() 1 -element Element of bool NAT
m is finite Element of bool NAT
Funcs (m,X) is functional set
m \ {v1} is finite Element of bool NAT
Funcs ((m \ {v1}),X) is functional set
{ b₁ where b₁ is Element of V : ( b₁ in Funcs ((m \ {v1}),X) & ex b₂ being set st {[v1,b₂]} \/ b₁ in E ) } is set
Funcs ({v1},X) is functional set
{ [v1,b₁] where b₁ is Element of V : b₁ in X } is set
n is Element of V
union n is Element of V
Dn is set
C is Element of V
[v1,C] is V22() Element of [:NAT,V:]
[:NAT,V:] is Relation-like non trivial non finite set
{v1,C} is finite set
{v1} is non empty trivial finite V48() 1 -element set
{{v1,C},{v1}} is finite V48() set
{[v1,C]} is Relation-like Function-like constant non empty trivial finite 1 -element set
p is Relation-like Function-like set
proj2 p is set
{C} is non empty trivial finite 1 -element Element of V
proj1 p is set
Dn is set
C is set
p is Relation-like Function-like set
proj1 p is set
proj2 p is set
p . v1 is set
[v1,(p . v1)] is V22() set
{v1,(p . v1)} is finite set
{v1} is non empty trivial finite V48() 1 -element set
{{v1,(p . v1)},{v1}} is finite V48() set
{[v1,(p . v1)]} is Relation-like Function-like constant non empty trivial finite 1 -element set
f is Element of V
[v1,f] is V22() Element of [:NAT,V:]
[:NAT,V:] is Relation-like non trivial non finite set
{v1,f} is finite set
{{v1,f},{v1}} is finite V48() set
{ { [v1,b₁] where b₁ is Element of V : b₁ in X } } is non empty trivial finite 1 -element set
Dn is Element of V
{ (b₁ \ b₂) where b₁, b₂ is Element of V : ( b₁ in E & b₂ in Dn ) } is set
f is set
x is Element of V
u is Element of V
x \ u is Element of V
x \ { [v1,b₁] where b₁ is Element of V : b₁ in X } is Element of bool x
bool x is set
h is Relation-like Function-like set
proj1 h is set
proj2 h is set
h | (m \ {v1}) is Relation-like Function-like finite set
proj1 (h | (m \ {v1})) is finite set
m /\ (m \ {v1}) is finite Element of bool NAT
m /\ m is finite Element of bool NAT
m /\ {v1} is finite Element of bool NAT
(m /\ m) \ (m /\ {v1}) is finite Element of bool NAT
h \ { [v1,b₁] where b₁ is Element of V : b₁ in X } is Relation-like Function-like Element of bool h
bool h is set
q is set
t is set
[q,t] is V22() set
{q,t} is finite set
{q} is non empty trivial finite 1 -element set
{{q,t},{q}} is finite V48() set
x is Element of V
[v1,x] is V22() Element of [:NAT,V:]
[:NAT,V:] is Relation-like non trivial non finite set
{v1,x} is finite set
{v1} is non empty trivial finite V48() 1 -element set
{{v1,x},{v1}} is finite V48() set
h . q is set
x is Element of V
[q,x] is V22() set
{q,x} is finite set
{{q,x},{q}} is finite V48() set
(h | (m \ {v1})) . q is set
proj2 (h | (m \ {v1})) is finite set
h . v1 is set
[v1,(h . v1)] is V22() set
{v1,(h . v1)} is finite set
{v1} is non empty trivial finite V48() 1 -element set
{{v1,(h . v1)},{v1}} is finite V48() set
{[v1,(h . v1)]} is Relation-like Function-like constant non empty trivial finite 1 -element set
x /\ { [v1,b₁] where b₁ is Element of V : b₁ in X } is set
t is set
x is set
[t,x] is V22() set
{t,x} is finite set
{t} is non empty trivial finite 1 -element set
{{t,x},{t}} is finite V48() set
y is Element of V
[v1,y] is V22() Element of [:NAT,V:]
[:NAT,V:] is Relation-like non trivial non finite set
{v1,y} is finite set
{{v1,y},{v1}} is finite V48() set
t is set
x is Element of V
[v1,x] is V22() Element of [:NAT,V:]
[:NAT,V:] is Relation-like non trivial non finite set
{v1,x} is finite set
{{v1,x},{v1}} is finite V48() set
{[v1,(h . v1)]} \/ (x \ { [v1,b₁] where b₁ is Element of V : b₁ in X } ) is set
q is Element of V
x is set
u is Element of V
h is set
[v1,h] is V22() set
{v1,h} is finite set
{v1} is non empty trivial finite V48() 1 -element set
{{v1,h},{v1}} is finite V48() set
{[v1,h]} is Relation-like Function-like constant non empty trivial finite 1 -element set
{[v1,h]} \/ u is set
h is set
[v1,h] is V22() set
{v1,h} is finite set
{v1} is non empty trivial finite V48() 1 -element set
{{v1,h},{v1}} is finite V48() set
{[v1,h]} is Relation-like Function-like constant non empty trivial finite 1 -element set
{[v1,h]} \/ u is set
g is Element of V
f is Element of V
g \ f is Element of V
q is Relation-like Function-like set
proj1 q is set
proj2 q is set
t is set
x is set
y is set
[x,y] is V22() set
{x,y} is finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is finite V48() set
e is Element of V
[v1,e] is V22() Element of [:NAT,V:]
[:NAT,V:] is Relation-like non trivial non finite set
{v1,e} is finite set
{{v1,e},{v1}} is finite V48() set
t is set
x is set
y is set
[x,y] is V22() set
{x,y} is finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is finite V48() set
e is Element of V
[v1,e] is V22() Element of [:NAT,V:]
[:NAT,V:] is Relation-like non trivial non finite set
{v1,e} is finite set
{{v1,e},{v1}} is finite V48() set
t is Relation-like Function-like set
proj1 t is set
proj2 t is set
t . v1 is set
x is Element of V
[v1,x] is V22() Element of [:NAT,V:]
[:NAT,V:] is Relation-like non trivial non finite set
{v1,x} is finite set
{{v1,x},{v1}} is finite V48() set
y is set
{[v1,h]} \ f is Relation-like Function-like finite Element of bool {[v1,h]}
bool {[v1,h]} is finite V48() set
u \ f is Element of V
(u \ f) \/ ({[v1,h]} \ f) is set
t is set
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
X is Element of V
E is Element of V
H is non empty Element of bool V
v1 is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
{ ({[v1,b₁]} \/ b₂) where b₁, b₂ is Element of V : ( b₁ in X & b₂ in E ) } is set
{v1} is non empty trivial finite V48() 1 -element Element of bool NAT
Funcs ({v1},X) is functional set
m is Element of V
{ (b₁ \/ b₂) where b₁, b₂ is Element of V : ( b₁ in m & b₂ in E ) } is set
Dn is set
C is Element of V
p is Element of V
C \/ p is Element of V
f is Relation-like Function-like set
proj1 f is set
proj2 f is set
f . v1 is set
x is Element of V
[v1,x] is V22() Element of [:NAT,V:]
[:NAT,V:] is Relation-like non trivial non finite set
{v1,x} is finite set
{v1} is non empty trivial finite V48() 1 -element set
{{v1,x},{v1}} is finite V48() set
{[v1,x]} is Relation-like Function-like constant non empty trivial finite 1 -element set
{[v1,x]} \/ p is set
Dn is set
C is Element of V
[v1,C] is V22() Element of [:NAT,V:]
[:NAT,V:] is Relation-like non trivial non finite set
{v1,C} is finite set
{v1} is non empty trivial finite V48() 1 -element set
{{v1,C},{v1}} is finite V48() set
{[v1,C]} is Relation-like Function-like constant non empty trivial finite 1 -element set
p is Element of V
{[v1,C]} \/ p is set
f is Relation-like Function-like set
proj2 f is set
{C} is non empty trivial finite 1 -element Element of V
proj1 f is set
x is Element of V
x \/ p is Element of V
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
X is non empty Element of bool V
E is set
H is set
v1 is set
{H} is non empty trivial finite 1 -element set
v1 \/ {H} is set
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
X is Element of V
E is non empty Element of bool V
H is set
v1 is finite Element of bool NAT
Funcs (v1,H) is functional set
m is Relation-like Function-like set
proj1 m is set
proj2 m is set
n is set
fs is set
Dn is set
[fs,Dn] is V22() set
{fs,Dn} is finite set
{fs} is non empty trivial finite 1 -element set
{{fs,Dn},{fs}} is finite V48() set
m . fs is set
[:(proj1 m),(proj2 m):] is Relation-like set
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
X is Element of V
E is Element of V
H is non empty Element of bool V
v1 is finite Element of bool NAT
Funcs (v1,X) is functional set
m is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
{ ({[m,b₁]} \/ E) where b₁ is Element of V : b₁ in X } is set
{E} is non empty trivial finite 1 -element Element of V
{ ({[m,b₁]} \/ b₂) where b₁, b₂ is Element of V : ( b₁ in X & b₂ in {E} ) } is set
C is set
p is Element of V
[m,p] is V22() Element of [:NAT,V:]
[:NAT,V:] is Relation-like non trivial non finite set
{m,p} is finite set
{m} is non empty trivial finite V48() 1 -element set
{{m,p},{m}} is finite V48() set
{[m,p]} is Relation-like Function-like constant non empty trivial finite 1 -element set
f is Element of V
{[m,p]} \/ f is set
C is set
p is Element of V
[m,p] is V22() Element of [:NAT,V:]
[:NAT,V:] is Relation-like non trivial non finite set
{m,p} is finite set
{m} is non empty trivial finite V48() 1 -element set
{{m,p},{m}} is finite V48() set
{[m,p]} is Relation-like Function-like constant non empty trivial finite 1 -element set
{[m,p]} \/ E is set
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
X is Element of V
E is Element of V
H is Element of V
v1 is non empty Element of bool V
m is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
{m} is non empty trivial finite V48() 1 -element Element of bool NAT
{ b₁ where b₁ is Element of V : ( b₁ in X & {[m,b₁]} \/ E in H ) } is set
n is finite Element of bool NAT
Funcs (n,X) is functional set
n \/ {m} is finite Element of bool NAT
Funcs ((n \/ {m}),X) is functional set
{E} is non empty trivial finite 1 -element Element of V
{ ({[m,b₁]} \/ E) where b₁ is Element of V : b₁ in X } is set
{ ({[m,b₁]} \/ E) where b₁ is Element of V : b₁ in X } /\ H is set
{ {[m,b₁]} where b₁ is Element of V : {[m,b₁]} \/ E in H } is set
C is Element of V
{ (b₁ \ b₂) where b₁, b₂ is Element of V : ( b₁ in C & b₂ in {E} ) } is set
u is Element of V
[m,u] is V22() Element of [:NAT,V:]
[:NAT,V:] is Relation-like non trivial non finite set
{m,u} is finite set
{m} is non empty trivial finite V48() 1 -element set
{{m,u},{m}} is finite V48() set
{[m,u]} is Relation-like Function-like constant non empty trivial finite 1 -element set
{[m,u]} \/ E is set
h is Relation-like Function-like set
proj1 h is set
proj2 h is set
h . m is set
u is set
h is Element of V
g is Element of V
h \ g is Element of V
q is Element of V
[m,q] is V22() Element of [:NAT,V:]
[:NAT,V:] is Relation-like non trivial non finite set
{m,q} is finite set
{m} is non empty trivial finite V48() 1 -element set
{{m,q},{m}} is finite V48() set
{[m,q]} is Relation-like Function-like constant non empty trivial finite 1 -element set
{[m,q]} \/ E is set
t is set
x is Relation-like Function-like set
proj1 x is set
proj2 x is set
{[m,q]} \ E is Relation-like Function-like finite Element of bool {[m,q]}
bool {[m,q]} is finite V48() set
E \ E is Element of V
({[m,q]} \ E) \/ (E \ E) is set
{[m,q]} \/ (E \ E) is set
{[m,q]} \/ {} is set
u is set
h is Element of V
[m,h] is V22() Element of [:NAT,V:]
[:NAT,V:] is Relation-like non trivial non finite set
{m,h} is finite set
{m} is non empty trivial finite V48() 1 -element set
{{m,h},{m}} is finite V48() set
{[m,h]} is Relation-like Function-like constant non empty trivial finite 1 -element set
{[m,h]} \/ E is set
g is Element of V
q is set
t is Relation-like Function-like set
proj1 t is set
proj2 t is set
g \ E is Element of V
{[m,h]} \ E is Relation-like Function-like finite Element of bool {[m,h]}
bool {[m,h]} is finite V48() set
E \ E is Element of V
({[m,h]} \ E) \/ (E \ E) is set
{[m,h]} \/ (E \ E) is set
{[m,h]} \/ {} is set
union { {[m,b₁]} where b₁ is Element of V : {[m,b₁]} \/ E in H } is set
union (union { {[m,b₁]} where b₁ is Element of V : {[m,b₁]} \/ E in H } ) is set
union (union (union { {[m,b₁]} where b₁ is Element of V : {[m,b₁]} \/ E in H } )) is set
h is set
g is Element of V
[m,g] is V22() Element of [:NAT,V:]
[:NAT,V:] is Relation-like non trivial non finite set
{m,g} is finite set
{m} is non empty trivial finite V48() 1 -element set
{{m,g},{m}} is finite V48() set
{[m,g]} is Relation-like Function-like constant non empty trivial finite 1 -element set
{[m,g]} \/ E is set
{{m,g},{m}} is finite V48() set
{ b₁ where b₁ is Element of V : ( b₁ in X & {[m,b₁]} \/ E in H ) } \/ {m} is set
h is set
g is set
q is set
t is set
x is Element of V
[m,x] is V22() Element of [:NAT,V:]
[:NAT,V:] is Relation-like non trivial non finite set
{m,x} is finite set
{m} is non empty trivial finite V48() 1 -element set
{{m,x},{m}} is finite V48() set
{[m,x]} is Relation-like Function-like constant non empty trivial finite 1 -element set
{[m,x]} \/ E is set
(union (union (union { {[m,b₁]} where b₁ is Element of V : {[m,b₁]} \/ E in H } ))) \ {m} is Element of bool (union (union (union { {[m,b₁]} where b₁ is Element of V : {[m,b₁]} \/ E in H } )))
bool (union (union (union { {[m,b₁]} where b₁ is Element of V : {[m,b₁]} \/ E in H } ))) is set
( { b₁ where b₁ is Element of V : ( b₁ in X & {[m,b₁]} \/ E in H ) } \/ {m}) \ {m} is Element of bool ( { b₁ where b₁ is Element of V : ( b₁ in X & {[m,b₁]} \/ E in H ) } \/ {m})
bool ( { b₁ where b₁ is Element of V : ( b₁ in X & {[m,b₁]} \/ E in H ) } \/ {m}) is set
{ b₁ where b₁ is Element of V : ( b₁ in X & {[m,b₁]} \/ E in H ) } \ {m} is Element of bool { b₁ where b₁ is Element of V : ( b₁ in X & {[m,b₁]} \/ E in H ) }
bool { b₁ where b₁ is Element of V : ( b₁ in X & {[m,b₁]} \/ E in H ) } is set
{m} \ {m} is finite Element of bool NAT
( { b₁ where b₁ is Element of V : ( b₁ in X & {[m,b₁]} \/ E in H ) } \ {m}) \/ ({m} \ {m}) is set
{ b₁ where b₁ is Element of V : ( b₁ in X & {[m,b₁]} \/ E in H ) } \/ ({m} \ {m}) is set
{ b₁ where b₁ is Element of V : ( b₁ in X & {[m,b₁]} \/ E in H ) } \/ {} is set
V is set
X is set
[V,X] is V22() set
{V,X} is finite set
{V} is non empty trivial finite 1 -element set
{{V,X},{V}} is finite V48() set
[X,X] is V22() set
{X,X} is finite set
{X} is non empty trivial finite 1 -element set
{{X,X},{X}} is finite V48() set
{[V,X],[X,X]} is Relation-like finite set
E is set
[X,E] is V22() set
{X,E} is finite set
{{X,E},{X}} is finite V48() set
{[X,E]} is Relation-like Function-like constant non empty trivial finite 1 -element set
{[V,X],[X,X]} (#) {[X,E]} is Relation-like set
[V,E] is V22() set
{V,E} is finite set
{{V,E},{V}} is finite V48() set
{[V,E],[X,E]} is Relation-like finite set
H is set
v1 is set
[H,v1] is V22() set
{H,v1} is finite set
{H} is non empty trivial finite 1 -element set
{{H,v1},{H}} is finite V48() set
m is set
[H,m] is V22() set
{H,m} is finite set
{{H,m},{H}} is finite V48() set
[m,v1] is V22() set
{m,v1} is finite set
{m} is non empty trivial finite 1 -element set
{{m,v1},{m}} is finite V48() set
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
0-element_of V is epsilon-transitive epsilon-connected ordinal Element of V
1-element_of V is non empty epsilon-transitive epsilon-connected ordinal Element of V
X is Element of V
{ {[(0-element_of V),b₁],[(1-element_of V),b₁]} where b₁ is Element of V : b₁ in X } is set
E is non empty Element of bool V
[(0-element_of V),(1-element_of V)] is V22() Element of V
{(0-element_of V),(1-element_of V)} is finite set
{(0-element_of V)} is non empty trivial finite 1 -element set
{{(0-element_of V),(1-element_of V)},{(0-element_of V)}} is finite V48() set
[(1-element_of V),(1-element_of V)] is V22() Element of V
{(1-element_of V),(1-element_of V)} is finite set
{(1-element_of V)} is non empty trivial finite 1 -element set
{{(1-element_of V),(1-element_of V)},{(1-element_of V)}} is finite V48() set
{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]} is Relation-like finite Element of V
{ {[(1-element_of V),b₁]} where b₁ is Element of V : b₁ in X } is set
{(1-element_of V)} is non empty trivial finite 1 -element Element of V
m is Element of V
{ {[b₁,b₂]} where b₁, b₂ is Element of V : ( b₁ in m & b₂ in X ) } is set
fs is set
n is Element of V
Dn is Element of V
[(1-element_of V),Dn] is V22() Element of V
{(1-element_of V),Dn} is finite set
{{(1-element_of V),Dn},{(1-element_of V)}} is finite V48() set
{[(1-element_of V),Dn]} is Relation-like Function-like constant non empty trivial finite 1 -element Element of V
n is set
fs is Element of V
Dn is Element of V
[fs,Dn] is V22() Element of V
{fs,Dn} is finite set
{fs} is non empty trivial finite 1 -element set
{{fs,Dn},{fs}} is finite V48() set
{[fs,Dn]} is Relation-like Function-like constant non empty trivial finite 1 -element Element of V
[(1-element_of V),Dn] is V22() Element of V
{(1-element_of V),Dn} is finite set
{{(1-element_of V),Dn},{(1-element_of V)}} is finite V48() set
{[(1-element_of V),Dn]} is Relation-like Function-like constant non empty trivial finite 1 -element Element of V
{{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} is non empty trivial finite V48() 1 -element Element of V
m is Element of V
{ (V,b₁,b₂) where b₁, b₂ is Element of V : ( b₁ in {{[(0-element_of V),(1-element_of V)],[(1-element_of V),(1-element_of V)]}} & b₂ in m ) } is set
C is set
Dn is Element of V
p is Element of V
[(0-element_of V),p] is V22() Element of V
{(0-element_of V),p} is finite set
{{(0-element_of V),p},{(0-element_of V)}} is finite V48() set
[(1-element_of V),p] is V22() Element of V
{(1-element_of V),p} is finite set
{{(1-element_of V),p},{(1-element_of V)}} is finite V48() set
{[(0-element_of V),p],[(1-element_of V),p]} is Relation-like finite Element of V
{[(1-element_of V),p]} is Relation-like Function-like constant non empty trivial finite 1 -element Element of V
f is Element of V
(V,Dn,f) is Relation-like Element of V
Dn is set
C is Element of V
p is Element of V
(V,C,p) is Relation-like Element of V
f is Element of V
[(1-element_of V),f] is V22() Element of V
{(1-element_of V),f} is finite set
{{(1-element_of V),f},{(1-element_of V)}} is finite V48() set
{[(1-element_of V),f]} is Relation-like Function-like constant non empty trivial finite 1 -element Element of V
[(0-element_of V),f] is V22() Element of V
{(0-element_of V),f} is finite set
{{(0-element_of V),f},{(0-element_of V)}} is finite V48() set
{[(0-element_of V),f],[(1-element_of V),f]} is Relation-like finite Element of V
V is set
X is set
E is set
[E,V] is V22() set
{E,V} is finite set
{E} is non empty trivial finite 1 -element set
{{E,V},{E}} is finite V48() set
H is set
[H,X] is V22() set
{H,X} is finite set
{H} is non empty trivial finite 1 -element set
{{H,X},{H}} is finite V48() set
{[E,V],[H,X]} is Relation-like finite set
v1 is set
[V,v1] is V22() set
{V,v1} is finite set
{V} is non empty trivial finite 1 -element set
{{V,v1},{V}} is finite V48() set
[E,v1] is V22() set
{E,v1} is finite set
{{E,v1},{E}} is finite V48() set
m is set
[X,m] is V22() set
{X,m} is finite set
{X} is non empty trivial finite 1 -element set
{{X,m},{X}} is finite V48() set
{[V,v1],[X,m]} is Relation-like finite set
{[E,V],[H,X]} (#) {[V,v1],[X,m]} is Relation-like set
[H,m] is V22() set
{H,m} is finite set
{{H,m},{H}} is finite V48() set
{[E,v1],[H,m]} is Relation-like finite set
n is set
fs is set
[n,fs] is V22() set
{n,fs} is finite set
{n} is non empty trivial finite 1 -element set
{{n,fs},{n}} is finite V48() set
Dn is set
[n,Dn] is V22() set
{n,Dn} is finite set
{{n,Dn},{n}} is finite V48() set
[Dn,fs] is V22() set
{Dn,fs} is finite set
{Dn} is non empty trivial finite 1 -element set
{{Dn,fs},{Dn}} is finite V48() set
V is set
X is set
{V,X} is finite set
E is Relation-like Function-like set
proj1 E is set
E . V is set
[V,(E . V)] is V22() set
{V,(E . V)} is finite set
{V} is non empty trivial finite 1 -element set
{{V,(E . V)},{V}} is finite V48() set
E . X is set
[X,(E . X)] is V22() set
{X,(E . X)} is finite set
{X} is non empty trivial finite 1 -element set
{{X,(E . X)},{X}} is finite V48() set
{[V,(E . V)],[X,(E . X)]} is Relation-like finite set
H is set
v1 is set
m is set
[v1,m] is V22() set
{v1,m} is finite set
{v1} is non empty trivial finite 1 -element set
{{v1,m},{v1}} is finite V48() set
H is set
E . H is set
[H,(E . H)] is V22() set
{H,(E . H)} is finite set
{H} is non empty trivial finite 1 -element set
{{H,(E . H)},{H}} is finite V48() set
E . H is set
[H,(E . H)] is V22() set
{H,(E . H)} is finite set
{H} is non empty trivial finite 1 -element set
{{H,(E . H)},{H}} is finite V48() set
E . H is set
[H,(E . H)] is V22() set
{H,(E . H)} is finite set
{H} is non empty trivial finite 1 -element set
{{H,(E . H)},{H}} is finite V48() set
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
X is non empty Element of bool V
E is non empty set
v1 is Element of VAR
m is Element of VAR
v1 '=' m is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
((v1 '=' m),E) is set
v1 'in' m is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
((v1 'in' m),E) is set
Free (v1 '=' m) is finite Element of bool VAR
{v1,m} is finite Element of bool VAR
Free (v1 'in' m) is finite Element of bool VAR
((Free (v1 '=' m))) is finite Element of bool NAT
(() ") .: (Free (v1 '=' m)) is finite set
H is Element of V
{ {[b₁,b₂]} where b₁, b₂ is Element of V : ( b₁ in ((Free (v1 '=' m))) & b₂ in H ) } is set
{v1} is non empty trivial finite 1 -element Element of bool VAR
(v1) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
p is set
f is Element of V
x is Element of V
[f,x] is V22() Element of V
{f,x} is finite set
{f} is non empty trivial finite 1 -element set
{{f,x},{f}} is finite V48() set
{[f,x]} is Relation-like Function-like constant non empty trivial finite 1 -element Element of V
[:VAR,E:] is Relation-like set
bool [:VAR,E:] is set
VAR --> x is Relation-like VAR -defined V -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,V:]
[:VAR,V:] is Relation-like set
bool [:VAR,V:] is set
{(v1)} is non empty trivial finite V48() 1 -element Element of bool NAT
u is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
u * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
[:NAT,E:] is Relation-like non trivial non finite set
bool [:NAT,E:] is non trivial non finite set
(u * ()) | ((Free (v1 '=' m))) is Relation-like NAT -defined ((Free (v1 '=' m))) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
dom ((u * ()) | ((Free (v1 '=' m)))) is finite Element of bool NAT
{f} is non empty trivial finite 1 -element Element of V
((u * ()) | ((Free (v1 '=' m)))) . f is set
[f,(((u * ()) | ((Free (v1 '=' m)))) . f)] is V22() set
{f,(((u * ()) | ((Free (v1 '=' m)))) . f)} is finite set
{{f,(((u * ()) | ((Free (v1 '=' m)))) . f)},{f}} is finite V48() set
{[f,(((u * ()) | ((Free (v1 '=' m)))) . f)]} is Relation-like Function-like constant non empty trivial finite 1 -element set
u . v1 is Element of E
[f,(u . v1)] is V22() Element of [:V,E:]
[:V,E:] is Relation-like set
{f,(u . v1)} is finite set
{{f,(u . v1)},{f}} is finite V48() set
{[f,(u . v1)]} is Relation-like Function-like constant non empty trivial finite 1 -element set
Var1 (v1 '=' m) is Element of VAR
u . (Var1 (v1 '=' m)) is Element of E
u . m is Element of E
Var2 (v1 '=' m) is Element of VAR
u . (Var2 (v1 '=' m)) is Element of E
St ((v1 '=' m),E) is Element of bool (VAL E)
VAL E is set
bool (VAL E) is set
f is set
[:VAR,E:] is Relation-like set
bool [:VAR,E:] is set
St ((v1 '=' m),E) is Element of bool (VAL E)
VAL E is set
bool (VAL E) is set
x is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
x * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
[:NAT,E:] is Relation-like non trivial non finite set
bool [:NAT,E:] is non trivial non finite set
(x * ()) | ((Free (v1 '=' m))) is Relation-like NAT -defined ((Free (v1 '=' m))) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
x . v1 is Element of E
dom ((x * ()) | ((Free (v1 '=' m)))) is finite Element of bool NAT
p is Element of V
{p} is non empty trivial finite 1 -element Element of V
((x * ()) | ((Free (v1 '=' m)))) . p is set
[p,(((x * ()) | ((Free (v1 '=' m)))) . p)] is V22() set
{p,(((x * ()) | ((Free (v1 '=' m)))) . p)} is finite set
{p} is non empty trivial finite 1 -element set
{{p,(((x * ()) | ((Free (v1 '=' m)))) . p)},{p}} is finite V48() set
{[p,(((x * ()) | ((Free (v1 '=' m)))) . p)]} is Relation-like Function-like constant non empty trivial finite 1 -element set
u is Element of V
[p,u] is V22() Element of V
{p,u} is finite set
{{p,u},{p}} is finite V48() set
{[p,u]} is Relation-like Function-like constant non empty trivial finite 1 -element Element of V
{(v1)} is non empty trivial finite V48() 1 -element Element of bool NAT
the Element of ((v1 'in' m),E) is Element of ((v1 'in' m),E)
[:VAR,E:] is Relation-like set
bool [:VAR,E:] is set
((Free (v1 'in' m))) is finite Element of bool NAT
(() ") .: (Free (v1 'in' m)) is finite set
St ((v1 'in' m),E) is Element of bool (VAL E)
VAL E is set
bool (VAL E) is set
f is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
f * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
[:NAT,E:] is Relation-like non trivial non finite set
bool [:NAT,E:] is non trivial non finite set
(f * ()) | ((Free (v1 'in' m))) is Relation-like NAT -defined ((Free (v1 'in' m))) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
Var1 (v1 'in' m) is Element of VAR
f . (Var1 (v1 'in' m)) is Element of E
Var2 (v1 'in' m) is Element of VAR
f . (Var2 (v1 'in' m)) is Element of E
f . v1 is Element of E
f . m is Element of E
(m) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
1-element_of V is non empty epsilon-transitive epsilon-connected ordinal Element of V
[(m),(1-element_of V)] is V22() Element of [:NAT,V:]
[:NAT,V:] is Relation-like non trivial non finite set
{(m),(1-element_of V)} is finite set
{(m)} is non empty trivial finite V48() 1 -element set
{{(m),(1-element_of V)},{(m)}} is finite V48() set
(v1) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
0-element_of V is epsilon-transitive epsilon-connected ordinal Element of V
[(v1),(0-element_of V)] is V22() Element of [:NAT,V:]
{(v1),(0-element_of V)} is finite set
{(v1)} is non empty trivial finite V48() 1 -element set
{{(v1),(0-element_of V)},{(v1)}} is finite V48() set
{[(v1),(0-element_of V)],[(m),(1-element_of V)]} is Relation-like finite set
((Free (v1 '=' m))) is finite Element of bool NAT
(() ") .: (Free (v1 '=' m)) is finite set
{(v1),(m)} is finite V48() Element of bool NAT
x. (m) is Element of VAR
Dn is Element of V
Funcs (((Free (v1 '=' m))),NAT) is functional non empty FUNCTION_DOMAIN of ((Free (v1 '=' m))), NAT
{[(v1),(0-element_of V)]} is Relation-like Function-like constant non empty trivial finite 1 -element set
{[(m),(1-element_of V)]} is Relation-like Function-like constant non empty trivial finite 1 -element set
x is Relation-like Function-like set
p is Relation-like Function-like set
f is Relation-like Function-like set
p \/ f is Relation-like set
proj2 x is set
proj2 p is set
proj2 f is set
(proj2 p) \/ (proj2 f) is set
{(0-element_of V)} is non empty trivial finite 1 -element Element of V
{(0-element_of V)} \/ (proj2 f) is set
{(1-element_of V)} is non empty trivial finite 1 -element Element of V
{(0-element_of V)} \/ {(1-element_of V)} is finite Element of V
{(0-element_of V),(1-element_of V)} is finite Element of V
proj1 x is set
proj1 p is set
proj1 f is set
(proj1 p) \/ (proj1 f) is set
{(v1)} is non empty trivial finite V48() 1 -element Element of bool NAT
{(v1)} \/ (proj1 f) is set
{(m)} is non empty trivial finite V48() 1 -element Element of bool NAT
{(v1)} \/ {(m)} is finite V48() Element of bool NAT
H is Element of V
{ {[(0-element_of V),b₁],[(1-element_of V),b₁]} where b₁ is Element of V : b₁ in H } is set
{ {[(0-element_of V),b₁],[(1-element_of V),b₂]} where b₁, b₂ is Element of V : ( b₁ in b₂ & b₁ in H & b₂ in H ) } is set
f is Element of V
{ (V,Dn,b₁) where b₁ is Element of V : b₁ in f } is set
h is Element of V
{ (V,Dn,b₁) where b₁ is Element of V : b₁ in h } is set
q is set
t is Element of V
(V,Dn,t) is Relation-like Element of V
x is Element of V
[(0-element_of V),x] is V22() Element of V
{(0-element_of V),x} is finite set
{(0-element_of V)} is non empty trivial finite 1 -element set
{{(0-element_of V),x},{(0-element_of V)}} is finite V48() set
[(1-element_of V),x] is V22() Element of V
{(1-element_of V),x} is finite set
{(1-element_of V)} is non empty trivial finite 1 -element set
{{(1-element_of V),x},{(1-element_of V)}} is finite V48() set
{[(0-element_of V),x],[(1-element_of V),x]} is Relation-like finite Element of V
[:VAR,E:] is Relation-like set
bool [:VAR,E:] is set
VAR --> x is Relation-like VAR -defined V -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,V:]
[:VAR,V:] is Relation-like set
bool [:VAR,V:] is set
y is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
Var1 (v1 '=' m) is Element of VAR
y . (Var1 (v1 '=' m)) is Element of E
Var2 (v1 '=' m) is Element of VAR
y . (Var2 (v1 '=' m)) is Element of E
St ((v1 '=' m),E) is Element of bool (VAL E)
VAL E is set
bool (VAL E) is set
y * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
[:NAT,E:] is Relation-like non trivial non finite set
bool [:NAT,E:] is non trivial non finite set
(y * ()) | ((Free (v1 '=' m))) is Relation-like NAT -defined ((Free (v1 '=' m))) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
((y * ()) | ((Free (v1 '=' m)))) . (m) is set
y . m is Element of E
((y * ()) | ((Free (v1 '=' m)))) . (v1) is set
y . v1 is Element of E
dom ((y * ()) | ((Free (v1 '=' m)))) is finite Element of bool NAT
[(v1),x] is V22() Element of [:NAT,V:]
{(v1),x} is finite set
{{(v1),x},{(v1)}} is finite V48() set
[(m),x] is V22() Element of [:NAT,V:]
{(m),x} is finite set
{{(m),x},{(m)}} is finite V48() set
{[(v1),x],[(m),x]} is Relation-like finite set
q is set
[:VAR,E:] is Relation-like set
bool [:VAR,E:] is set
St ((v1 '=' m),E) is Element of bool (VAL E)
VAL E is set
bool (VAL E) is set
t is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
t * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
[:NAT,E:] is Relation-like non trivial non finite set
bool [:NAT,E:] is non trivial non finite set
(t * ()) | ((Free (v1 '=' m))) is Relation-like NAT -defined ((Free (v1 '=' m))) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
t . v1 is Element of E
Var1 (v1 '=' m) is Element of VAR
t . (Var1 (v1 '=' m)) is Element of E
Var2 (v1 '=' m) is Element of VAR
t . (Var2 (v1 '=' m)) is Element of E
t . m is Element of E
((t * ()) | ((Free (v1 '=' m)))) . (m) is set
x is Element of V
[(0-element_of V),x] is V22() Element of V
{(0-element_of V),x} is finite set
{(0-element_of V)} is non empty trivial finite 1 -element set
{{(0-element_of V),x},{(0-element_of V)}} is finite V48() set
[(1-element_of V),x] is V22() Element of V
{(1-element_of V),x} is finite set
{(1-element_of V)} is non empty trivial finite 1 -element set
{{(1-element_of V),x},{(1-element_of V)}} is finite V48() set
{[(0-element_of V),x],[(1-element_of V),x]} is Relation-like finite Element of V
dom ((t * ()) | ((Free (v1 '=' m)))) is finite Element of bool NAT
((t * ()) | ((Free (v1 '=' m)))) . (v1) is set
[(v1),x] is V22() Element of [:NAT,V:]
{(v1),x} is finite set
{{(v1),x},{(v1)}} is finite V48() set
[(m),x] is V22() Element of [:NAT,V:]
{(m),x} is finite set
{{(m),x},{(m)}} is finite V48() set
{[(v1),x],[(m),x]} is Relation-like finite set
y is Element of V
(V,Dn,y) is Relation-like Element of V
t is set
x is Element of V
(V,Dn,x) is Relation-like Element of V
y is Element of V
[(0-element_of V),y] is V22() Element of V
{(0-element_of V),y} is finite set
{(0-element_of V)} is non empty trivial finite 1 -element set
{{(0-element_of V),y},{(0-element_of V)}} is finite V48() set
e is Element of V
[(1-element_of V),e] is V22() Element of V
{(1-element_of V),e} is finite set
{(1-element_of V)} is non empty trivial finite 1 -element set
{{(1-element_of V),e},{(1-element_of V)}} is finite V48() set
{[(0-element_of V),y],[(1-element_of V),e]} is Relation-like finite Element of V
[(v1),y] is V22() Element of [:NAT,V:]
{(v1),y} is finite set
{{(v1),y},{(v1)}} is finite V48() set
[(m),e] is V22() Element of [:NAT,V:]
{(m),e} is finite set
{{(m),e},{(m)}} is finite V48() set
{[(v1),y],[(m),e]} is Relation-like finite set
gg is Element of E
[:VAR,E:] is Relation-like set
bool [:VAR,E:] is set
q is Element of VAR
f is Element of E
ff is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
ff . q is Element of E
ff * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
[:NAT,E:] is Relation-like non trivial non finite set
bool [:NAT,E:] is non trivial non finite set
((Free (v1 'in' m))) is finite Element of bool NAT
(() ") .: (Free (v1 'in' m)) is finite set
(ff * ()) | ((Free (v1 'in' m))) is Relation-like NAT -defined ((Free (v1 'in' m))) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
((ff * ()) | ((Free (v1 'in' m)))) . (m) is set
ff . m is Element of E
((ff * ()) | ((Free (v1 'in' m)))) . (v1) is set
ff . v1 is Element of E
Var1 (v1 'in' m) is Element of VAR
ff . (Var1 (v1 'in' m)) is Element of E
Var2 (v1 'in' m) is Element of VAR
ff . (Var2 (v1 'in' m)) is Element of E
St ((v1 'in' m),E) is Element of bool (VAL E)
VAL E is set
bool (VAL E) is set
dom ((ff * ()) | ((Free (v1 'in' m)))) is finite Element of bool NAT
q is set
[:VAR,E:] is Relation-like set
bool [:VAR,E:] is set
((Free (v1 'in' m))) is finite Element of bool NAT
(() ") .: (Free (v1 'in' m)) is finite set
St ((v1 'in' m),E) is Element of bool (VAL E)
VAL E is set
bool (VAL E) is set
t is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
t * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
[:NAT,E:] is Relation-like non trivial non finite set
bool [:NAT,E:] is non trivial non finite set
(t * ()) | ((Free (v1 'in' m))) is Relation-like NAT -defined ((Free (v1 'in' m))) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
t . m is Element of E
t . v1 is Element of E
Var1 (v1 'in' m) is Element of VAR
t . (Var1 (v1 'in' m)) is Element of E
Var2 (v1 'in' m) is Element of VAR
t . (Var2 (v1 'in' m)) is Element of E
y is Element of V
x is Element of V
[(0-element_of V),y] is V22() Element of V
{(0-element_of V),y} is finite set
{(0-element_of V)} is non empty trivial finite 1 -element set
{{(0-element_of V),y},{(0-element_of V)}} is finite V48() set
[(1-element_of V),x] is V22() Element of V
{(1-element_of V),x} is finite set
{(1-element_of V)} is non empty trivial finite 1 -element set
{{(1-element_of V),x},{(1-element_of V)}} is finite V48() set
{[(0-element_of V),y],[(1-element_of V),x]} is Relation-like finite Element of V
((t * ()) | ((Free (v1 'in' m)))) . (m) is set
dom ((t * ()) | ((Free (v1 'in' m)))) is finite Element of bool NAT
((t * ()) | ((Free (v1 'in' m)))) . (v1) is set
[(v1),y] is V22() Element of [:NAT,V:]
{(v1),y} is finite set
{{(v1),y},{(v1)}} is finite V48() set
[(m),x] is V22() Element of [:NAT,V:]
{(m),x} is finite set
{{(m),x},{(m)}} is finite V48() set
{[(v1),y],[(m),x]} is Relation-like finite set
e is Element of V
(V,Dn,e) is Relation-like Element of V
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
X is non empty Element of bool V
E is non empty set
v1 is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
(v1,E) is set
'not' v1 is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
(('not' v1),E) is set
Free v1 is finite Element of bool VAR
((Free v1)) is finite Element of bool NAT
(() ") .: (Free v1) is finite set
Free ('not' v1) is finite Element of bool VAR
((Free ('not' v1))) is finite Element of bool NAT
(() ") .: (Free ('not' v1)) is finite set
n is set
[:VAR,E:] is Relation-like set
bool [:VAR,E:] is set
St (('not' v1),E) is Element of bool (VAL E)
VAL E is set
bool (VAL E) is set
fs is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
fs * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
[:NAT,E:] is Relation-like non trivial non finite set
bool [:NAT,E:] is non trivial non finite set
(fs * ()) | ((Free v1)) is Relation-like NAT -defined ((Free v1)) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
Funcs (((Free v1)),E) is functional non empty FUNCTION_DOMAIN of ((Free v1)),E
St (v1,E) is Element of bool (VAL E)
Dn is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
Dn * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
(Dn * ()) | ((Free v1)) is Relation-like NAT -defined ((Free v1)) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
fs is Relation-like Function-like set
proj1 fs is set
proj2 fs is set
Dn is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
Dn * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
(Dn * ()) | ((Free v1)) is Relation-like NAT -defined ((Free v1)) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
St (v1,E) is Element of bool (VAL E)
(Funcs (((Free v1)),E)) \ (v1,E) is functional Element of bool (Funcs (((Free v1)),E))
bool (Funcs (((Free v1)),E)) is set
H is Element of V
Funcs (((Free v1)),H) is functional set
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
X is non empty Element of bool V
E is non empty set
v1 is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
(v1,E) is set
m is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
(m,E) is set
v1 '&' m is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
((v1 '&' m),E) is set
Free v1 is finite Element of bool VAR
((Free v1)) is finite Element of bool NAT
(() ") .: (Free v1) is finite set
Free m is finite Element of bool VAR
((Free m)) is finite Element of bool NAT
(() ") .: (Free m) is finite set
((Free m)) \ ((Free v1)) is finite Element of bool NAT
H is Element of V
Funcs ((((Free m)) \ ((Free v1))),H) is functional set
((Free v1)) \ ((Free m)) is finite Element of bool NAT
Funcs ((((Free v1)) \ ((Free m))),H) is functional set
Dn is Element of V
p is Element of V
{ (b₁ \/ b₂) where b₁, b₂ is Element of V : ( b₁ in Dn & b₂ in p ) } is set
C is Element of V
f is Element of V
{ (b₁ \/ b₂) where b₁, b₂ is Element of V : ( b₁ in C & b₂ in f ) } is set
h is set
{ (b₁ \/ b₂) where b₁, b₂ is Element of V : ( b₁ in Dn & b₂ in p ) } /\ { (b₁ \/ b₂) where b₁, b₂ is Element of V : ( b₁ in C & b₂ in f ) } is set
g is Element of V
q is Element of V
g \/ q is Element of V
t is Element of V
x is Element of V
t \/ x is Element of V
[:VAR,E:] is Relation-like set
bool [:VAR,E:] is set
St (m,E) is Element of bool (VAL E)
VAL E is set
bool (VAL E) is set
y is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
y * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
[:NAT,E:] is Relation-like non trivial non finite set
bool [:NAT,E:] is non trivial non finite set
(y * ()) | ((Free m)) is Relation-like NAT -defined ((Free m)) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
e is Relation-like Function-like set
proj1 e is set
proj2 e is set
St (v1,E) is Element of bool (VAL E)
f is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
f * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
(f * ()) | ((Free v1)) is Relation-like NAT -defined ((Free v1)) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
dom ((f * ()) | ((Free v1))) is finite Element of bool NAT
((f * ()) | ((Free v1))) \/ e is Relation-like set
gg is Relation-like Function-like set
proj2 gg is set
rng ((f * ()) | ((Free v1))) is finite Element of bool E
bool E is set
(rng ((f * ()) | ((Free v1)))) \/ (proj2 e) is set
proj1 gg is set
((Free v1)) \/ (((Free m)) \ ((Free v1))) is finite Element of bool NAT
((Free v1)) \/ ((Free m)) is finite Element of bool NAT
Funcs ((((Free v1)) \/ ((Free m))),E) is functional non empty FUNCTION_DOMAIN of ((Free v1)) \/ ((Free m)),E
ff is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
ff * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
(ff * ()) | (((Free v1)) \/ ((Free m))) is Relation-like NAT -defined ((Free v1)) \/ ((Free m)) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
(ff * ()) | ((Free v1)) is Relation-like NAT -defined ((Free v1)) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
dom ((ff * ()) | ((Free v1))) is finite Element of bool NAT
q is set
(ff * ()) | ((Free m)) is Relation-like NAT -defined ((Free m)) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
((ff * ()) | ((Free v1))) \/ ((ff * ()) | ((Free m))) is Relation-like NAT -defined E -valued finite Element of bool [:NAT,E:]
((ff * ()) | ((Free v1))) . q is set
((ff * ()) | (((Free v1)) \/ ((Free m)))) . q is set
((f * ()) | ((Free v1))) . q is set
dom ((ff * ()) | ((Free m))) is finite Element of bool NAT
dom ((y * ()) | ((Free m))) is finite Element of bool NAT
q is set
((ff * ()) | ((Free m))) . q is set
((ff * ()) | (((Free v1)) \/ ((Free m)))) . q is set
((y * ()) | ((Free m))) . q is set
St ((v1 '&' m),E) is Element of bool (VAL E)
(Free v1) \/ (Free m) is finite Element of bool VAR
(((Free v1) \/ (Free m))) is finite Element of bool NAT
(() ") .: ((Free v1) \/ (Free m)) is finite set
(ff * ()) | (((Free v1) \/ (Free m))) is Relation-like NAT -defined (((Free v1) \/ (Free m))) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
Free (v1 '&' m) is finite Element of bool VAR
((Free (v1 '&' m))) is finite Element of bool NAT
(() ") .: (Free (v1 '&' m)) is finite set
(ff * ()) | ((Free (v1 '&' m))) is Relation-like NAT -defined ((Free (v1 '&' m))) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
h is set
g is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
g * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
(g * ()) | ((Free (v1 '&' m))) is Relation-like NAT -defined ((Free (v1 '&' m))) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
(g * ()) | ((Free m)) is Relation-like NAT -defined ((Free m)) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
(g * ()) | (((Free v1)) \ ((Free m))) is Relation-like NAT -defined ((Free v1)) \ ((Free m)) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
[:(((Free v1)) \ ((Free m))),E:] is Relation-like set
bool [:(((Free v1)) \ ((Free m))),E:] is set
((Free m)) \/ ((Free v1)) is finite Element of bool NAT
(g * ()) | (((Free m)) \/ ((Free v1))) is Relation-like NAT -defined ((Free m)) \/ ((Free v1)) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
((Free m)) \/ (((Free v1)) \ ((Free m))) is finite Element of bool NAT
(g * ()) | (((Free m)) \/ (((Free v1)) \ ((Free m)))) is Relation-like NAT -defined ((Free m)) \/ (((Free v1)) \ ((Free m))) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
((g * ()) | ((Free m))) \/ ((g * ()) | (((Free v1)) \ ((Free m)))) is Relation-like NAT -defined E -valued finite Element of bool [:NAT,E:]
q is Element of V
t is Element of V
q \/ t is Element of V
(g * ()) | ((Free v1)) is Relation-like NAT -defined ((Free v1)) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
(g * ()) | (((Free m)) \ ((Free v1))) is Relation-like NAT -defined ((Free m)) \ ((Free v1)) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
[:(((Free m)) \ ((Free v1))),E:] is Relation-like set
bool [:(((Free m)) \ ((Free v1))),E:] is set
(g * ()) | (((Free v1)) \/ ((Free m))) is Relation-like NAT -defined ((Free v1)) \/ ((Free m)) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
(g * ()) | (((Free v1)) \/ (((Free m)) \ ((Free v1)))) is Relation-like NAT -defined ((Free v1)) \/ (((Free m)) \ ((Free v1))) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
((g * ()) | ((Free v1))) \/ ((g * ()) | (((Free m)) \ ((Free v1)))) is Relation-like NAT -defined E -valued finite Element of bool [:NAT,E:]
x is Element of V
y is Element of V
x \/ y is Element of V
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
X is non empty Element of bool V
E is non empty set
H is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
(H,E) is set
v1 is Element of VAR
All (v1,H) is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
((All (v1,H)),E) is set
Free H is finite Element of bool VAR
{v1} is non empty trivial finite 1 -element Element of bool VAR
(Free H) \ {v1} is finite Element of bool VAR
Free (All (v1,H)) is finite Element of bool VAR
m is set
[:VAR,E:] is Relation-like set
bool [:VAR,E:] is set
((Free (All (v1,H)))) is finite Element of bool NAT
(() ") .: (Free (All (v1,H))) is finite set
St ((All (v1,H)),E) is Element of bool (VAL E)
VAL E is set
bool (VAL E) is set
n is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
n * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
[:NAT,E:] is Relation-like non trivial non finite set
bool [:NAT,E:] is non trivial non finite set
(n * ()) | ((Free (All (v1,H)))) is Relation-like NAT -defined ((Free (All (v1,H)))) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
St (H,E) is Element of bool (VAL E)
m is set
[:VAR,E:] is Relation-like set
bool [:VAR,E:] is set
((Free H)) is finite Element of bool NAT
(() ") .: (Free H) is finite set
St (H,E) is Element of bool (VAL E)
VAL E is set
bool (VAL E) is set
n is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
n * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
[:NAT,E:] is Relation-like non trivial non finite set
bool [:NAT,E:] is non trivial non finite set
(n * ()) | ((Free H)) is Relation-like NAT -defined ((Free H)) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
fs is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
Dn is Element of VAR
n . Dn is Element of E
fs . Dn is Element of E
St ((All (v1,H)),E) is Element of bool (VAL E)
Free H is finite Element of bool VAR
(v1) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
((Free H)) is finite Element of bool NAT
(() ") .: (Free H) is finite set
'not' H is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
(('not' H),E) is set
Funcs (((Free H)),E) is functional non empty FUNCTION_DOMAIN of ((Free H)),E
Dn is set
[:VAR,E:] is Relation-like set
bool [:VAR,E:] is set
Free ('not' H) is finite Element of bool VAR
((Free ('not' H))) is finite Element of bool NAT
(() ") .: (Free ('not' H)) is finite set
St (('not' H),E) is Element of bool (VAL E)
VAL E is set
bool (VAL E) is set
C is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
C * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
[:NAT,E:] is Relation-like non trivial non finite set
bool [:NAT,E:] is non trivial non finite set
(C * ()) | ((Free ('not' H))) is Relation-like NAT -defined ((Free ('not' H))) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
{(v1)} is non empty trivial finite V48() 1 -element Element of bool NAT
((Free H)) \ {(v1)} is finite Element of bool NAT
{v1} is non empty trivial finite 1 -element Element of bool VAR
({v1}) is finite Element of bool NAT
(() ") .: {v1} is finite set
((Free H)) \ ({v1}) is finite Element of bool NAT
(Free H) \ {v1} is finite Element of bool VAR
(((Free H) \ {v1})) is finite Element of bool NAT
(() ") .: ((Free H) \ {v1}) is finite set
Free (All (v1,H)) is finite Element of bool VAR
((Free (All (v1,H)))) is finite Element of bool NAT
(() ") .: (Free (All (v1,H))) is finite set
m is Element of V
Funcs ((((Free H)) \ {(v1)}),m) is functional set
Dn is Element of V
{ b₁ where b₁ is Element of V : ( b₁ in Funcs ((((Free H)) \ {(v1)}),m) & ex b₂ being set st {[(v1),b₂]} \/ b₁ in Dn ) } is set
((Free H) \ {v1}) \/ {v1} is finite Element of bool VAR
(((Free H) \ {v1})) \/ ({v1}) is finite Element of bool NAT
(((Free H) \ {v1})) \/ {(v1)} is finite Element of bool NAT
(Funcs ((((Free H)) \ {(v1)}),m)) \ { b₁ where b₁ is Element of V : ( b₁ in Funcs ((((Free H)) \ {(v1)}),m) & ex b₂ being set st {[(v1),b₂]} \/ b₁ in Dn ) } is functional Element of bool (Funcs ((((Free H)) \ {(v1)}),m))
bool (Funcs ((((Free H)) \ {(v1)}),m)) is set
p is set
f is Relation-like Function-like set
proj1 f is set
proj2 f is set
[:VAR,E:] is Relation-like set
bool [:VAR,E:] is set
x is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
x * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
[:NAT,E:] is Relation-like non trivial non finite set
bool [:NAT,E:] is non trivial non finite set
(x * ()) | (((Free H)) \ {(v1)}) is Relation-like NAT -defined ((Free H)) \ {(v1)} -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
St ((All (v1,H)),E) is Element of bool (VAL E)
VAL E is set
bool (VAL E) is set
St (H,E) is Element of bool (VAL E)
u is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
u * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
(u * ()) | ((Free (All (v1,H)))) is Relation-like NAT -defined ((Free (All (v1,H)))) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
(u * ()) | (((Free H)) \ {(v1)}) is Relation-like NAT -defined ((Free H)) \ {(v1)} -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
St (('not' H),E) is Element of bool (VAL E)
Free ('not' H) is finite Element of bool VAR
((Free ('not' H))) is finite Element of bool NAT
(() ") .: (Free ('not' H)) is finite set
(u * ()) | ((Free ('not' H))) is Relation-like NAT -defined ((Free ('not' H))) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
(((Free H)) \ {(v1)}) \/ {(v1)} is finite Element of bool NAT
(u * ()) | ((((Free H)) \ {(v1)}) \/ {(v1)}) is Relation-like NAT -defined (((Free H)) \ {(v1)}) \/ {(v1)} -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
(u * ()) | {(v1)} is Relation-like NAT -defined {(v1)} -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
((u * ()) | (((Free H)) \ {(v1)})) \/ ((u * ()) | {(v1)}) is Relation-like NAT -defined E -valued finite Element of bool [:NAT,E:]
dom ((u * ()) | {(v1)}) is finite Element of bool NAT
((u * ()) | {(v1)}) . (v1) is set
[(v1),(((u * ()) | {(v1)}) . (v1))] is V22() set
{(v1),(((u * ()) | {(v1)}) . (v1))} is finite set
{(v1)} is non empty trivial finite V48() 1 -element set
{{(v1),(((u * ()) | {(v1)}) . (v1))},{(v1)}} is finite V48() set
{[(v1),(((u * ()) | {(v1)}) . (v1))]} is Relation-like Function-like constant non empty trivial finite 1 -element set
h is Element of V
{[(v1),(((u * ()) | {(v1)}) . (v1))]} \/ h is set
u is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
u * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
(u * ()) | (((Free H)) \ {(v1)}) is Relation-like NAT -defined ((Free H)) \ {(v1)} -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
dom ((u * ()) | (((Free H)) \ {(v1)})) is finite Element of bool (((Free H)) \ {(v1)})
bool (((Free H)) \ {(v1)}) is finite V48() set
dom ((x * ()) | (((Free H)) \ {(v1)})) is finite Element of bool (((Free H)) \ {(v1)})
h is set
g is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
card g is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
x. (card g) is Element of VAR
((x. (card g))) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
((u * ()) | (((Free H)) \ {(v1)})) . h is set
(u * ()) . h is set
u . (x. (card g)) is Element of E
x . (x. (card g)) is Element of E
(x * ()) . h is set
((x * ()) | (((Free H)) \ {(v1)})) . h is set
p is set
[:VAR,E:] is Relation-like set
bool [:VAR,E:] is set
St ((All (v1,H)),E) is Element of bool (VAL E)
VAL E is set
bool (VAL E) is set
f is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
f * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
[:NAT,E:] is Relation-like non trivial non finite set
bool [:NAT,E:] is non trivial non finite set
(f * ()) | ((Free (All (v1,H)))) is Relation-like NAT -defined ((Free (All (v1,H)))) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
Free ('not' H) is finite Element of bool VAR
((Free ('not' H))) is finite Element of bool NAT
(() ") .: (Free ('not' H)) is finite set
x is Element of V
u is set
[(v1),u] is V22() set
{(v1),u} is finite set
{(v1)} is non empty trivial finite V48() 1 -element set
{{(v1),u},{(v1)}} is finite V48() set
{[(v1),u]} is Relation-like Function-like constant non empty trivial finite 1 -element set
{[(v1),u]} \/ x is set
h is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
h * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
(h * ()) | ((Free H)) is Relation-like NAT -defined ((Free H)) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
(h * ()) | (((Free H)) \ {(v1)}) is Relation-like NAT -defined ((Free H)) \ {(v1)} -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
dom ((h * ()) | (((Free H)) \ {(v1)})) is finite Element of bool (((Free H)) \ {(v1)})
bool (((Free H)) \ {(v1)}) is finite V48() set
(f * ()) | (((Free H)) \ {(v1)}) is Relation-like NAT -defined ((Free H)) \ {(v1)} -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
dom ((f * ()) | (((Free H)) \ {(v1)})) is finite Element of bool (((Free H)) \ {(v1)})
q is set
((h * ()) | (((Free H)) \ {(v1)})) . q is set
((h * ()) | ((Free H))) . q is set
((f * ()) | (((Free H)) \ {(v1)})) . q is set
St (('not' H),E) is Element of bool (VAL E)
g is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
g * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
(g * ()) | ((Free ('not' H))) is Relation-like NAT -defined ((Free ('not' H))) -defined NAT -defined E -valued Function-like finite Element of bool [:NAT,E:]
St (H,E) is Element of bool (VAL E)
u is Element of V
h is set
[(v1),h] is V22() set
{(v1),h} is finite set
{{(v1),h},{(v1)}} is finite V48() set
{[(v1),h]} is Relation-like Function-like constant non empty trivial finite 1 -element set
{[(v1),h]} \/ u is set
Free H is finite Element of bool VAR
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
X is non empty Element of bool V
E is non empty set
H is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
(H,E) is set
v1 is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
(v1,E) is set
'not' v1 is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
(('not' v1),E) is set
v1 is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
(v1,E) is set
m is Element of VAR
All (m,v1) is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
((All (m,v1)),E) is set
v1 is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
(v1,E) is set
m is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
(m,E) is set
v1 '&' m is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
((v1 '&' m),E) is set
v1 is Element of VAR
m is Element of VAR
v1 '=' m is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
((v1 '=' m),E) is set
n is Element of VAR
fs is Element of VAR
n 'in' fs is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
((n 'in' fs),E) is set
V is non empty epsilon-transitive V35() V36() universal set
bool V is set
X is non empty Element of bool V
E is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
0-element_of V is epsilon-transitive epsilon-connected ordinal Element of V
1-element_of V is non empty epsilon-transitive epsilon-connected ordinal Element of V
V is set
X is set
[V,X] is V22() set
{V,X} is finite set
{V} is non empty trivial finite 1 -element set
{{V,X},{V}} is finite V48() set
[X,X] is V22() set
{X,X} is finite set
{X} is non empty trivial finite 1 -element set
{{X,X},{X}} is finite V48() set
{[V,X],[X,X]} is Relation-like finite set
E is set
[X,E] is V22() set
{X,E} is finite set
{{X,E},{X}} is finite V48() set
{[X,E]} is Relation-like Function-like constant non empty trivial finite 1 -element set
{[V,X],[X,X]} (#) {[X,E]} is Relation-like set
[V,E] is V22() set
{V,E} is finite set
{{V,E},{V}} is finite V48() set
{[V,E],[X,E]} is Relation-like finite set
V is set
X is set
E is set
[E,V] is V22() set
{E,V} is finite set
{E} is non empty trivial finite 1 -element set
{{E,V},{E}} is finite V48() set
H is set
[H,X] is V22() set
{H,X} is finite set
{H} is non empty trivial finite 1 -element set
{{H,X},{H}} is finite V48() set
{[E,V],[H,X]} is Relation-like finite set
v1 is set
[V,v1] is V22() set
{V,v1} is finite set
{V} is non empty trivial finite 1 -element set
{{V,v1},{V}} is finite V48() set
m is set
[X,m] is V22() set
{X,m} is finite set
{X} is non empty trivial finite 1 -element set
{{X,m},{X}} is finite V48() set
{[V,v1],[X,m]} is Relation-like finite set
{[E,V],[H,X]} (#) {[V,v1],[X,m]} is Relation-like set
[E,v1] is V22() set
{E,v1} is finite set
{{E,v1},{E}} is finite V48() set
[H,m] is V22() set
{H,m} is finite set
{{H,m},{H}} is finite V48() set
{[E,v1],[H,m]} is Relation-like finite set
V is Element of VAR
{V} is non empty trivial finite 1 -element Element of bool VAR
({V}) is finite Element of bool NAT
(() ") .: {V} is finite set
(V) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
{(V)} is non empty trivial finite V48() 1 -element Element of bool NAT
X is Element of VAR
E is Element of VAR
{X,E} is finite Element of bool VAR
({X,E}) is finite Element of bool NAT
(() ") .: {X,E} is finite set
(X) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
(E) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
{(X),(E)} is finite V48() Element of bool NAT
E is Relation-like Function-like set
proj1 E is set
V is set
X is set
{V,X} is finite set
E . V is set
[V,(E . V)] is V22() set
{V,(E . V)} is finite set
{V} is non empty trivial finite 1 -element set
{{V,(E . V)},{V}} is finite V48() set
E . X is set
[X,(E . X)] is V22() set
{X,(E . X)} is finite set
{X} is non empty trivial finite 1 -element set
{{X,(E . X)},{X}} is finite V48() set
{[V,(E . V)],[X,(E . X)]} is Relation-like finite set
m is Relation-like Function-like set
H is set
m . H is set
[H,(m . H)] is V22() set
{H,(m . H)} is finite set
{H} is non empty trivial finite 1 -element set
{{H,(m . H)},{H}} is finite V48() set
v1 is set
m . v1 is set
[v1,(m . v1)] is V22() set
{v1,(m . v1)} is finite set
{v1} is non empty trivial finite 1 -element set
{{v1,(m . v1)},{v1}} is finite V48() set
{[H,(m . H)],[v1,(m . v1)]} is Relation-like finite set
proj1 m is set
{H,v1} is finite set
V is finite Element of bool VAR
(V) is finite Element of bool NAT
(() ") .: V is finite set
V is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
card V is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
x. (card V) is Element of VAR
((x. (card V))) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
X is non empty set
[:VAR,X:] is Relation-like set
bool [:VAR,X:] is set
v1 is non empty set
[:VAR,v1:] is Relation-like set
bool [:VAR,v1:] is set
fs is non empty set
[:VAR,fs:] is Relation-like set
bool [:VAR,fs:] is set
C is non empty set
[:VAR,C:] is Relation-like set
bool [:VAR,C:] is set
V is finite Element of bool NAT
E is Relation-like VAR -defined X -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,X:]
E * () is Relation-like NAT -defined X -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,X:]
[:NAT,X:] is Relation-like non trivial non finite set
bool [:NAT,X:] is non trivial non finite set
(E * ()) | V is Relation-like NAT -defined V -defined NAT -defined X -valued Function-like finite Element of bool [:NAT,X:]
dom ((E * ()) | V) is finite Element of bool V
bool V is finite V48() set
m is Relation-like VAR -defined v1 -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,v1:]
m * () is Relation-like NAT -defined v1 -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,v1:]
[:NAT,v1:] is Relation-like non trivial non finite set
bool [:NAT,v1:] is non trivial non finite set
H is finite Element of bool NAT
(m * ()) | H is Relation-like NAT -defined H -defined NAT -defined v1 -valued Function-like finite Element of bool [:NAT,v1:]
rng ((m * ()) | H) is finite Element of bool v1
bool v1 is set
Dn is Relation-like VAR -defined fs -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,fs:]
Dn * () is Relation-like NAT -defined fs -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,fs:]
[:NAT,fs:] is Relation-like non trivial non finite set
bool [:NAT,fs:] is non trivial non finite set
n is finite Element of bool NAT
(Dn * ()) | n is Relation-like NAT -defined n -defined NAT -defined fs -valued Function-like finite Element of bool [:NAT,fs:]
Funcs (n,fs) is functional non empty FUNCTION_DOMAIN of n,fs
p is Relation-like VAR -defined C -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,C:]
p * () is Relation-like NAT -defined C -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,C:]
[:NAT,C:] is Relation-like non trivial non finite set
bool [:NAT,C:] is non trivial non finite set
dom (p * ()) is non empty Element of bool NAT
E is non empty set
[:VAR,E:] is Relation-like set
bool [:VAR,E:] is set
V is Element of VAR
(V) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
() . (V) is Element of VAR
X is Element of VAR
(() ") . X is set
(X) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
H is Relation-like VAR -defined E -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,E:]
H * () is Relation-like NAT -defined E -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,E:]
[:NAT,E:] is Relation-like non trivial non finite set
bool [:NAT,E:] is non trivial non finite set
v1 is Element of VAR
(v1) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
(H * ()) . (v1) is Element of E
H . v1 is Element of E
V is set
X is finite Element of bool VAR
(X) is finite Element of bool NAT
(() ") .: X is finite set
v1 is Element of VAR
H is finite Element of bool VAR
E is set
(v1) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
(H) is finite Element of bool NAT
(() ") .: H is finite set
V is finite Element of bool VAR
X is finite Element of bool VAR
V \/ X is finite Element of bool VAR
((V \/ X)) is finite Element of bool NAT
(() ") .: (V \/ X) is finite set
(V) is finite Element of bool NAT
(() ") .: V is finite set
(X) is finite Element of bool NAT
(() ") .: X is finite set
(V) \/ (X) is finite Element of bool NAT
E is finite Element of bool VAR
H is finite Element of bool VAR
E \ H is finite Element of bool VAR
((E \ H)) is finite Element of bool NAT
(() ") .: (E \ H) is finite set
(E) is finite Element of bool NAT
(() ") .: E is finite set
(H) is finite Element of bool NAT
(() ") .: H is finite set
(E) \ (H) is finite Element of bool NAT
V is non empty set
[:VAR,V:] is Relation-like set
bool [:VAR,V:] is set
E is Element of VAR
H is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
Free H is finite Element of bool VAR
X is Relation-like VAR -defined V -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,V:]
X * () is Relation-like NAT -defined V -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,V:]
[:NAT,V:] is Relation-like non trivial non finite set
bool [:NAT,V:] is non trivial non finite set
((Free H)) is finite Element of bool NAT
(() ") .: (Free H) is finite set
(X * ()) | ((Free H)) is Relation-like NAT -defined ((Free H)) -defined NAT -defined V -valued Function-like finite Element of bool [:NAT,V:]
(E) is epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal Element of NAT
((X * ()) | ((Free H))) . (E) is set
X . E is Element of V
V is non empty set
[:VAR,V:] is Relation-like set
bool [:VAR,V:] is set
E is Relation-like VAR -defined V -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,V:]
E * () is Relation-like NAT -defined V -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,V:]
[:NAT,V:] is Relation-like non trivial non finite set
bool [:NAT,V:] is non trivial non finite set
X is Relation-like NAT -defined NAT -valued Function-like V52() ZF-formula-like M8( NAT )
Free X is finite Element of bool VAR
((Free X)) is finite Element of bool NAT
(() ") .: (Free X) is finite set
(E * ()) | ((Free X)) is Relation-like NAT -defined ((Free X)) -defined NAT -defined V -valued Function-like finite Element of bool [:NAT,V:]
H is Relation-like VAR -defined V -valued Function-like non empty V14( VAR ) quasi_total Element of bool [:VAR,V:]
H * () is Relation-like NAT -defined V -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,V:]
(H * ()) | ((Free X)) is Relation-like NAT -defined ((Free X)) -defined NAT -defined V -valued Function-like finite Element of bool [:NAT,V:]
St (X,V) is Element of bool (VAL V)
VAL V is set
bool (VAL V) is set
V is set
X is finite Element of bool NAT
E is non empty set
Funcs (X,E) is functional non empty FUNCTION_DOMAIN of X,E
[:VAR,E:] is Relation-like set
bool [:VAR,E:] is set