:: ZF_FUND1 semantic presentation

REAL is 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

{} is set

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

v1 is set
m is set
m is set
[:m,v1:] is Relation-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],[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

proj1 n is set
proj2 n is set
n 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
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

bool is non trivial non finite set

V is Element of VAR

x. H is Element of VAR

x. X is Element of VAR

x. E is Element of VAR

dom () is non empty Element of bool NAT
rng () is non empty Element of bool VAR

proj1 (() ") is set
proj2 (() ") is set
V is set
X is Element of VAR

() . E is Element of VAR

x. (card (X)) is Element of VAR
x. (X) is Element of VAR
X is set
() . X is set

() . E is Element of VAR
V is set
X is set
() . V is set
() . X is set

x. (card E) is Element of VAR

x. (card H) is Element of VAR

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

bool [:VAR,X:] is set

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

[: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 * ()) | ((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

[: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

[: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

[: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

x. (card V) is Element of VAR

V is finite Element of bool NAT
X is non empty set

bool [:VAR,X:] is set
Funcs (V,X) is functional non empty FUNCTION_DOMAIN of V,X

[:NAT,X:] is Relation-like non trivial non finite set
bool [:NAT,X:] is non trivial non finite set

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

bool [:VAR,V:] is set

[: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 Element of VAR
(() ") . E is set
(X * ()) . (E) is Element of V
X . E is Element of V

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

() . V is set

x. (card E) is Element of VAR
E is Element of VAR

(() ") . 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 non empty trivial finite V48() 1 -element Element of bool NAT
X is set
E is Element of VAR

X is set
V is Element of VAR

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

{(V),(X)} is finite V48() Element of bool NAT
E is set
H is Element of VAR

E is set
V is finite Element of bool VAR
(V) is finite Element of bool NAT
(() ") .: V is 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

bool [:VAR,V:] is set

[:NAT,V:] is Relation-like non trivial non finite set
bool [:NAT,V:] is non trivial non finite set
E is Element of VAR

X . E is Element of V

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

bool [:VAR,V:] is set

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

[: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 * ()) | ((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

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

bool [:VAR,E:] is set
the Element of E is Element of E
[:X,E:] is Relation-like set
bool [:X,E:] is set

proj1 m is set
proj2 m is set

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

bool is non trivial non finite set

dom m is non empty Element of bool NAT
(dom m) /\ X is finite Element of bool NAT

proj1 fs is set
proj2 fs is set
fs is set
m . fs is set
v1 . fs is 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

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

H is Element of V
{H} is non empty trivial finite 1 -element Element of V
{ {[(),b1],[(),b2]} where b1, b2 is Element of V : ( b1 in b2 & b1 in {H} & b2 in {H} ) } is set
the Element of { {[(),b1],[(),b2]} where b1, b2 is Element of V : ( b1 in b2 & b1 in {H} & b2 in {H} ) } is Element of { {[(),b1],[(),b2]} where b1, b2 is Element of V : ( b1 in b2 & b1 in {H} & b2 in {H} ) }
n is Element of V
[(),n] is V22() Element of V
{(),n} is finite set
{()} is non empty trivial finite 1 -element set
{{(),n},{()}} is finite V48() set
fs is Element of V
[(),fs] is V22() Element of V
{(),fs} is finite set
{()} is non empty trivial finite 1 -element set
{{(),fs},{()}} is finite V48() set
{[(),n],[(),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

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
{ (b1 \/ b2) where b1, b2 is Element of V : ( b1 in {m} & b2 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
{ (b1 \ b2) where b1, b2 is Element of V : ( b1 in {m} & b2 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,b1,b2) where b1, b2 is Element of V : ( b1 in {m} & b2 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

{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

proj1 n is set
proj2 n is set

proj2 (n | v1) is 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
{ {[b1,b2]} where b1, b2 is Element of V : ( b1 in {v1} & b2 in X ) } is set
Funcs ({v1},X) is functional set
C is 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

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

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
{ (b1 \/ b2) where b1, b2 is Element of V : ( b1 in C & b2 in p ) } is set
x is set

proj1 u is set
proj2 u is set

proj2 (u | m) is 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

proj1 g is set
proj2 g is set

proj1 q is set
proj2 q is set

proj2 t is set
() \/ () 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,b1) where b1 is Element of V : b1 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,b1,b2) where b1, b2 is Element of V : ( b1 in {X} & b2 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

V is non empty epsilon-transitive V35() V36() universal set
bool V is set

X is non empty Element of bool V
succ {} is non empty 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 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
{ b1 where b1 is Element of V : ( b1 in Funcs ((m \ {v1}),X) & ex b2 being set st {[v1,b2]} \/ b1 in E ) } is set
Funcs ({v1},X) is functional set
{ [v1,b1] where b1 is Element of V : b1 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

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

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

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,b1] where b1 is Element of V : b1 in X } } is non empty trivial finite 1 -element set
Dn is Element of V
{ (b1 \ b2) where b1, b2 is Element of V : ( b1 in E & b2 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,b1] where b1 is Element of V : b1 in X } is Element of bool x
bool x is 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,b1] where b1 is Element of V : b1 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

x /\ { [v1,b1] where b1 is Element of V : b1 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,b1] where b1 is Element of V : b1 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]} \/ 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]} \/ u is set
g is Element of V
f is Element of V
g \ f is Element of V

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

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,b1]} \/ b2) where b1, b2 is Element of V : ( b1 in X & b2 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
{ (b1 \/ b2) where b1, b2 is Element of V : ( b1 in m & b2 in E ) } is set
Dn is set
C is Element of V
p is Element of V
C \/ p is Element of V

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]} \/ 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

p is Element of V
{[v1,C]} \/ p is 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

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
[:(),():] 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,b1]} \/ E) where b1 is Element of V : b1 in X } is set
{E} is non empty trivial finite 1 -element Element of V
{ ({[m,b1]} \/ b2) where b1, b2 is Element of V : ( b1 in X & b2 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

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]} \/ 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 non empty trivial finite V48() 1 -element Element of bool NAT
{ b1 where b1 is Element of V : ( b1 in X & {[m,b1]} \/ 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,b1]} \/ E) where b1 is Element of V : b1 in X } is set
{ ({[m,b1]} \/ E) where b1 is Element of V : b1 in X } /\ H is set
{ {[m,b1]} where b1 is Element of V : {[m,b1]} \/ E in H } is set
C is Element of V
{ (b1 \ b2) where b1, b2 is Element of V : ( b1 in C & b2 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]} \/ E is 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]} \/ E is set
t is set

proj1 x is set
proj2 x is set

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]} \/ E is set
g is Element of V
q is set

proj1 t is set
proj2 t is set
g \ E is Element of V

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,b1]} where b1 is Element of V : {[m,b1]} \/ E in H } is set
union (union { {[m,b1]} where b1 is Element of V : {[m,b1]} \/ E in H } ) is set
union (union (union { {[m,b1]} where b1 is Element of V : {[m,b1]} \/ 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]} \/ E is set
{{m,g},{m}} is finite V48() set
{ b1 where b1 is Element of V : ( b1 in X & {[m,b1]} \/ 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]} \/ E is set
(union (union (union { {[m,b1]} where b1 is Element of V : {[m,b1]} \/ E in H } ))) \ {m} is Element of bool (union (union (union { {[m,b1]} where b1 is Element of V : {[m,b1]} \/ E in H } )))
bool (union (union (union { {[m,b1]} where b1 is Element of V : {[m,b1]} \/ E in H } ))) is set
( { b1 where b1 is Element of V : ( b1 in X & {[m,b1]} \/ E in H ) } \/ {m}) \ {m} is Element of bool ( { b1 where b1 is Element of V : ( b1 in X & {[m,b1]} \/ E in H ) } \/ {m})
bool ( { b1 where b1 is Element of V : ( b1 in X & {[m,b1]} \/ E in H ) } \/ {m}) is set
{ b1 where b1 is Element of V : ( b1 in X & {[m,b1]} \/ E in H ) } \ {m} is Element of bool { b1 where b1 is Element of V : ( b1 in X & {[m,b1]} \/ E in H ) }
bool { b1 where b1 is Element of V : ( b1 in X & {[m,b1]} \/ E in H ) } is set

( { b1 where b1 is Element of V : ( b1 in X & {[m,b1]} \/ E in H ) } \ {m}) \/ ({m} \ {m}) is set
{ b1 where b1 is Element of V : ( b1 in X & {[m,b1]} \/ E in H ) } \/ ({m} \ {m}) is set
{ b1 where b1 is Element of V : ( b1 in X & {[m,b1]} \/ 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

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

X is Element of V
{ {[(),b1],[(),b1]} where b1 is Element of V : b1 in X } is set
E is non empty Element of bool V
[(),()] is V22() Element of V
{(),()} is finite set
{()} is non empty trivial finite 1 -element set
{{(),()},{()}} is finite V48() set
[(),()] is V22() Element of V
{(),()} is finite set
{()} is non empty trivial finite 1 -element set
{{(),()},{()}} is finite V48() set
{[(),()],[(),()]} is Relation-like finite Element of V
{ {[(),b1]} where b1 is Element of V : b1 in X } is set
{()} is non empty trivial finite 1 -element Element of V
m is Element of V
{ {[b1,b2]} where b1, b2 is Element of V : ( b1 in m & b2 in X ) } is set
fs is set
n is Element of V
Dn is Element of V
[(),Dn] is V22() Element of V
{(),Dn} is finite set
{{(),Dn},{()}} is finite V48() set

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

[(),Dn] is V22() Element of V
{(),Dn} is finite set
{{(),Dn},{()}} is finite V48() set

{{[(),()],[(),()]}} is non empty trivial finite V48() 1 -element Element of V
m is Element of V
{ (V,b1,b2) where b1, b2 is Element of V : ( b1 in {{[(),()],[(),()]}} & b2 in m ) } is set
C is set
Dn is Element of V
p is Element of V
[(),p] is V22() Element of V
{(),p} is finite set
{{(),p},{()}} is finite V48() set
[(),p] is V22() Element of V
{(),p} is finite set
{{(),p},{()}} is finite V48() set
{[(),p],[(),p]} is Relation-like finite 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
[(),f] is V22() Element of V
{(),f} is finite set
{{(),f},{()}} is finite V48() set

[(),f] is V22() Element of V
{(),f} is finite set
{{(),f},{()}} is finite V48() set
{[(),f],[(),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

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),E) is set

((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
{ {[b1,b2]} where b1, b2 is Element of V : ( b1 in ((Free (v1 '=' m))) & b2 in H ) } is set
{v1} is non empty trivial finite 1 -element Element of bool VAR

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

bool [:VAR,E:] is set

bool [:VAR,V:] is set
{(v1)} is non empty trivial finite V48() 1 -element Element of bool NAT