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

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

the Element of { {[(0-element_of V),b

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

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

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

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

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

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

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

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

Funcs ({v1},X) is functional set

{ [v1,b

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

Dn is Element of V

{ (b

f is set

x is Element of V

u is Element of V

x \ u is Element of V

x \ { [v1,b

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

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

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

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

{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

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} is non empty trivial finite 1 -element Element of V

{ ({[m,b

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

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

{ ({[m,b

{ {[m,b

C is Element of V

{ (b

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

union (union { {[m,b

union (union (union { {[m,b

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

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

bool (union (union (union { {[m,b

( { b

bool ( { b

{ b

bool { b

{m} \ {m} is finite Element of bool NAT

( { b

{ b

{ b

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

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

{(1-element_of V)} is non empty trivial finite 1 -element Element of V

m is Element of V

{ {[b

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

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

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