:: GOEDELCP semantic presentation

REAL is set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable Element of bool REAL
bool REAL is non empty set
COMPLEX is set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable set
bool omega is non empty set
bool NAT is non empty set
K357() is set
1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
{} is set
the empty Relation-like non-empty empty-yielding functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() V35() finite finite-yielding V42() FinSequence-like FinSequence-membered countable set is empty Relation-like non-empty empty-yielding functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() V35() finite finite-yielding V42() FinSequence-like FinSequence-membered countable set
0 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
[0,0] is V7() set
{0,0} is finite countable set
{0} is finite countable set
{{0,0},{0}} is finite V42() countable set
<*[0,0]*> is non empty Relation-like NAT -defined Function-like finite V45(1) FinSequence-like FinSubsequence-like countable set
[1,0] is V7() set
{1,0} is finite countable set
{1} is finite countable set
{{1,0},{1}} is finite V42() countable set
<*[1,0]*> is non empty Relation-like NAT -defined Function-like finite V45(1) FinSequence-like FinSubsequence-like countable set
[2,0] is V7() set
{2,0} is finite countable set
{2} is finite countable set
{{2,0},{2}} is finite V42() countable set
<*[2,0]*> is non empty Relation-like NAT -defined Function-like finite V45(1) FinSequence-like FinSubsequence-like countable set
[3,0] is V7() set
{3,0} is finite countable set
{3} is finite countable set
{{3,0},{3}} is finite V42() countable set
<*[3,0]*> is non empty Relation-like NAT -defined Function-like finite V45(1) FinSequence-like FinSubsequence-like countable set
Seg 1 is non empty finite V45(1) countable Element of bool NAT
[:NAT,NAT:] is non empty Relation-like REAL -defined REAL -valued Element of bool [:REAL,REAL:]
[:REAL,REAL:] is Relation-like set
bool [:REAL,REAL:] is non empty set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
p is Consistent Element of bool (CQC-WFF Al)
X is Element of CQC-WFF Al
'not' X is Element of CQC-WFF Al
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
X is Element of CQC-WFF Al
'not' X is Element of CQC-WFF Al
<*X*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
p is Element of CQC-WFF Al
('not' X) 'or' p is Element of CQC-WFF Al
<*(('not' X) 'or' p)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y ^ <*(('not' X) 'or' p)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y ^ <*X*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*('not' X)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y ^ <*('not' X)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(Y ^ <*('not' X)*>) ^ <*X*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Ant ((Y ^ <*('not' X)*>) ^ <*X*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Ant (Y ^ <*X*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Suc (Y ^ <*X*>) is Element of CQC-WFF Al
Suc ((Y ^ <*('not' X)*>) ^ <*X*>) is Element of CQC-WFF Al
(Y ^ <*('not' X)*>) ^ <*('not' X)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Ant ((Y ^ <*('not' X)*>) ^ <*('not' X)*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Suc ((Y ^ <*('not' X)*>) ^ <*('not' X)*>) is Element of CQC-WFF Al
len Y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(len Y) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(Ant ((Y ^ <*('not' X)*>) ^ <*('not' X)*>)) . ((len Y) + 1) is set
len <*('not' X)*> is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(len Y) + (len <*('not' X)*>) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
len (Ant ((Y ^ <*('not' X)*>) ^ <*('not' X)*>)) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
dom (Ant ((Y ^ <*('not' X)*>) ^ <*('not' X)*>)) is finite countable Element of bool NAT
0 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
len ((Y ^ <*('not' X)*>) ^ <*('not' X)*>) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
'not' (Suc ((Y ^ <*('not' X)*>) ^ <*X*>)) is Element of CQC-WFF Al
<*('not' (Suc ((Y ^ <*('not' X)*>) ^ <*X*>)))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(Ant ((Y ^ <*('not' X)*>) ^ <*X*>)) ^ <*('not' (Suc ((Y ^ <*('not' X)*>) ^ <*X*>)))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(Ant ((Y ^ <*('not' X)*>) ^ <*X*>)) ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(Y ^ <*p*>) ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Ant ((Y ^ <*p*>) ^ <*p*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Suc ((Y ^ <*p*>) ^ <*p*>) is Element of CQC-WFF Al
(Ant ((Y ^ <*p*>) ^ <*p*>)) . ((len Y) + 1) is set
len <*p*> is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(len Y) + (len <*p*>) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
len (Ant ((Y ^ <*p*>) ^ <*p*>)) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
dom (Ant ((Y ^ <*p*>) ^ <*p*>)) is finite countable Element of bool NAT
(Y ^ <*(('not' X) 'or' p)*>) ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
'not' ('not' X) is Element of CQC-WFF Al
'not' p is Element of CQC-WFF Al
('not' ('not' X)) '&' ('not' p) is Element of CQC-WFF Al
'not' (('not' ('not' X)) '&' ('not' p)) is Element of CQC-WFF Al
<*('not' (('not' ('not' X)) '&' ('not' p)))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y ^ <*('not' (('not' ('not' X)) '&' ('not' p)))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(Y ^ <*('not' (('not' ('not' X)) '&' ('not' p)))*>) ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*('not' p)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y ^ <*('not' p)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*(('not' ('not' X)) '&' ('not' p))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(Y ^ <*('not' p)*>) ^ <*(('not' ('not' X)) '&' ('not' p))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Suc ((Y ^ <*('not' p)*>) ^ <*(('not' ('not' X)) '&' ('not' p))*>) is Element of CQC-WFF Al
Ant ((Y ^ <*('not' p)*>) ^ <*(('not' ('not' X)) '&' ('not' p))*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*('not' ('not' X))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(Ant ((Y ^ <*('not' p)*>) ^ <*(('not' ('not' X)) '&' ('not' p))*>)) ^ <*('not' ('not' X))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(Ant ((Y ^ <*('not' p)*>) ^ <*(('not' ('not' X)) '&' ('not' p))*>)) ^ <*('not' p)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Ant ((Ant ((Y ^ <*('not' p)*>) ^ <*(('not' ('not' X)) '&' ('not' p))*>)) ^ <*('not' ('not' X))*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Suc ((Ant ((Y ^ <*('not' p)*>) ^ <*(('not' ('not' X)) '&' ('not' p))*>)) ^ <*('not' ('not' X))*>) is Element of CQC-WFF Al
Ant ((Ant ((Y ^ <*('not' p)*>) ^ <*(('not' ('not' X)) '&' ('not' p))*>)) ^ <*('not' p)*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Suc ((Ant ((Y ^ <*('not' p)*>) ^ <*(('not' ('not' X)) '&' ('not' p))*>)) ^ <*('not' p)*>) is Element of CQC-WFF Al
(Ant ((Y ^ <*('not' p)*>) ^ <*(('not' ('not' X)) '&' ('not' p))*>)) ^ <*(('not' ('not' X)) '&' ('not' p))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
len (Y ^ <*(('not' X) 'or' p)*>) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Ant (Y ^ <*(('not' X) 'or' p)*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(Ant (Y ^ <*(('not' X) 'or' p)*>)) ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
X is Element of bool (CQC-WFF Al)
p is Element of CQC-WFF Al
Y is Element of bound_QC-variables Al
Ex (Y,p) is Element of CQC-WFF Al
<*(Ex (Y,p))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
J is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng J is finite countable Element of bool (CQC-WFF Al)
J ^ <*(Ex (Y,p))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
'not' (Ex (Y,p)) is Element of CQC-WFF Al
v is Element of bound_QC-variables Al
p . (Y,v) is Element of CQC-WFF Al
('not' (Ex (Y,p))) 'or' (p . (Y,v)) is Element of CQC-WFF Al
<*(('not' (Ex (Y,p))) 'or' (p . (Y,v)))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
CY is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng CY is finite countable Element of bool (CQC-WFF Al)
CY ^ <*(('not' (Ex (Y,p))) 'or' (p . (Y,v)))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
J ^ CY is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(J ^ CY) ^ <*(Ex (Y,p))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(J ^ CY) ^ <*(('not' (Ex (Y,p))) 'or' (p . (Y,v)))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*(p . (Y,v))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(J ^ CY) ^ <*(p . (Y,v))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng (J ^ CY) is finite countable Element of bool (CQC-WFF Al)
(rng J) \/ (rng CY) is finite countable Element of bool (CQC-WFF Al)
J is Element of bound_QC-variables Al
p . (Y,J) is Element of CQC-WFF Al
<*(p . (Y,J))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
v is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng v is finite countable Element of bool (CQC-WFF Al)
v ^ <*(p . (Y,J))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*(Ex (Y,p))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
v ^ <*(Ex (Y,p))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-pred_symbols Al is set
HCar Al is non empty set
K354((HCar Al)) is set
p is Consistent Element of bool (CQC-WFF Al)
X is Element of CQC-WFF Al
Y is Relation-like QC-pred_symbols Al -defined K354((HCar Al)) -valued Function-like V32( QC-pred_symbols Al,K354((HCar Al))) Henkin_interpretation of p
valH Al is Relation-like bound_QC-variables Al -defined HCar Al -valued Function-like V32( bound_QC-variables Al, HCar Al) Element of Valuations_in (Al,(HCar Al))
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
Valuations_in (Al,(HCar Al)) is non empty M5( bound_QC-variables Al, HCar Al)
'not' X is Element of CQC-WFF Al
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
X is Element of CQC-WFF Al
<*X*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
p is Element of CQC-WFF Al
<*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
X '&' p is Element of CQC-WFF Al
<*(X '&' p)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y ^ <*X*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y ^ <*(X '&' p)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Ant (Y ^ <*X*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Suc (Y ^ <*X*>) is Element of CQC-WFF Al
Suc (Y ^ <*p*>) is Element of CQC-WFF Al
Ant (Y ^ <*p*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
X is Element of bool (CQC-WFF Al)
p is Element of CQC-WFF Al
Y is Element of CQC-WFF Al
p '&' Y is Element of CQC-WFF Al
<*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
J is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng J is finite countable Element of bool (CQC-WFF Al)
J ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*Y*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
v is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng v is finite countable Element of bool (CQC-WFF Al)
v ^ <*Y*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
J ^ v is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(J ^ v) ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(J ^ v) ^ <*Y*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*(p '&' Y)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(J ^ v) ^ <*(p '&' Y)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng (J ^ v) is finite countable Element of bool (CQC-WFF Al)
(rng J) \/ (rng v) is finite countable Element of bool (CQC-WFF Al)
<*(p '&' Y)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
J is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng J is finite countable Element of bool (CQC-WFF Al)
J ^ <*(p '&' Y)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
J ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*Y*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
J ^ <*Y*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-pred_symbols Al is set
HCar Al is non empty set
K354((HCar Al)) is set
Y is Consistent Element of bool (CQC-WFF Al)
X is Element of CQC-WFF Al
J is Relation-like QC-pred_symbols Al -defined K354((HCar Al)) -valued Function-like V32( QC-pred_symbols Al,K354((HCar Al))) Henkin_interpretation of Y
valH Al is Relation-like bound_QC-variables Al -defined HCar Al -valued Function-like V32( bound_QC-variables Al, HCar Al) Element of Valuations_in (Al,(HCar Al))
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
Valuations_in (Al,(HCar Al)) is non empty M5( bound_QC-variables Al, HCar Al)
p is Element of CQC-WFF Al
X '&' p is Element of CQC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-pred_symbols Al is set
HCar Al is non empty set
K354((HCar Al)) is set
valH Al is Relation-like bound_QC-variables Al -defined HCar Al -valued Function-like V32( bound_QC-variables Al, HCar Al) Element of Valuations_in (Al,(HCar Al))
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
Valuations_in (Al,(HCar Al)) is non empty M5( bound_QC-variables Al, HCar Al)
X is Consistent Element of bool (CQC-WFF Al)
p is Relation-like QC-pred_symbols Al -defined K354((HCar Al)) -valued Function-like V32( QC-pred_symbols Al,K354((HCar Al))) Henkin_interpretation of X
VERUM Al is Element of CQC-WFF Al
Y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Y -ary_QC-pred_symbols Al is Element of bool (QC-pred_symbols Al)
bool (QC-pred_symbols Al) is non empty set
v is Element of Y -ary_QC-pred_symbols Al
J is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like finite V45(Y) FinSequence-like FinSubsequence-like countable FinSequence of QC-variables Al
v ! J is Element of CQC-WFF Al
CY is Element of CQC-WFF Al
'not' CY is Element of CQC-WFF Al
CY is Element of CQC-WFF Al
c₉ is Element of CQC-WFF Al
CY '&' c₉ is Element of CQC-WFF Al
Y is Element of CQC-WFF Al
QuantNbr Y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Y is Element of CQC-WFF Al
QuantNbr Y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
QC-pred_symbols Al is set
X is Element of CQC-WFF Al
p is Element of bound_QC-variables Al
Ex (p,X) is Element of CQC-WFF Al
Y is non empty set
K354(Y) is set
Valuations_in (Al,Y) is non empty M5( bound_QC-variables Al,Y)
J is Relation-like QC-pred_symbols Al -defined K354(Y) -valued Function-like V32( QC-pred_symbols Al,K354(Y)) interpretation of Al,Y
v is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
'not' X is Element of CQC-WFF Al
All (p,('not' X)) is Element of CQC-WFF Al
'not' (All (p,('not' X))) is Element of CQC-WFF Al
CY is Element of Y
p | CY is Relation-like bound_QC-variables Al -defined Y -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),Y:]
[:(bound_QC-variables Al),Y:] is Relation-like set
bool [:(bound_QC-variables Al),Y:] is non empty set
v . (p | CY) is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
CY is Element of Y
p | CY is Relation-like bound_QC-variables Al -defined Y -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),Y:]
[:(bound_QC-variables Al),Y:] is Relation-like set
bool [:(bound_QC-variables Al),Y:] is non empty set
v . (p | CY) is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
CY is Element of Y
p | CY is Relation-like bound_QC-variables Al -defined Y -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),Y:]
[:(bound_QC-variables Al),Y:] is Relation-like set
bool [:(bound_QC-variables Al),Y:] is non empty set
v . (p | CY) is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
CY is Element of Y
p | CY is Relation-like bound_QC-variables Al -defined Y -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),Y:]
v . (p | CY) is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
c₉ is Element of Y
p | c₉ is Relation-like bound_QC-variables Al -defined Y -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),Y:]
v . (p | c₉) is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-pred_symbols Al is set
HCar Al is non empty set
K354((HCar Al)) is set
valH Al is Relation-like bound_QC-variables Al -defined HCar Al -valued Function-like V32( bound_QC-variables Al, HCar Al) Element of Valuations_in (Al,(HCar Al))
Valuations_in (Al,(HCar Al)) is non empty M5( bound_QC-variables Al, HCar Al)
X is Element of CQC-WFF Al
p is Element of bound_QC-variables Al
Ex (p,X) is Element of CQC-WFF Al
Y is Consistent Element of bool (CQC-WFF Al)
J is Relation-like QC-pred_symbols Al -defined K354((HCar Al)) -valued Function-like V32( QC-pred_symbols Al,K354((HCar Al))) Henkin_interpretation of Y
v is Element of HCar Al
p | v is Relation-like bound_QC-variables Al -defined HCar Al -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),(HCar Al):]
[:(bound_QC-variables Al),(HCar Al):] is Relation-like set
bool [:(bound_QC-variables Al),(HCar Al):] is non empty set
(valH Al) . (p | v) is Relation-like bound_QC-variables Al -defined HCar Al -valued Function-like V32( bound_QC-variables Al, HCar Al) Element of Valuations_in (Al,(HCar Al))
id (bound_QC-variables Al) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -valued Element of K131((bound_QC-variables Al),(bound_QC-variables Al))
K131((bound_QC-variables Al),(bound_QC-variables Al)) is set
rng (valH Al) is Element of bool (HCar Al)
bool (HCar Al) is non empty set
dom (valH Al) is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
CY is set
(valH Al) . CY is set
CY is Element of bound_QC-variables Al
X . (p,CY) is Element of CQC-WFF Al
v is Element of bound_QC-variables Al
X . (p,v) is Element of CQC-WFF Al
(valH Al) . v is set
CY is Element of HCar Al
p | CY is Relation-like bound_QC-variables Al -defined HCar Al -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),(HCar Al):]
[:(bound_QC-variables Al),(HCar Al):] is Relation-like set
bool [:(bound_QC-variables Al),(HCar Al):] is non empty set
(valH Al) . (p | CY) is Relation-like bound_QC-variables Al -defined HCar Al -valued Function-like V32( bound_QC-variables Al, HCar Al) Element of Valuations_in (Al,(HCar Al))
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
QC-pred_symbols Al is set
X is Element of CQC-WFF Al
'not' X is Element of CQC-WFF Al
p is Element of bound_QC-variables Al
Ex (p,('not' X)) is Element of CQC-WFF Al
'not' (Ex (p,('not' X))) is Element of CQC-WFF Al
All (p,X) is Element of CQC-WFF Al
Y is non empty set
K354(Y) is set
Valuations_in (Al,Y) is non empty M5( bound_QC-variables Al,Y)
J is Relation-like QC-pred_symbols Al -defined K354(Y) -valued Function-like V32( QC-pred_symbols Al,K354(Y)) interpretation of Al,Y
v is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
CY is Element of Y
p | CY is Relation-like bound_QC-variables Al -defined Y -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),Y:]
[:(bound_QC-variables Al),Y:] is Relation-like set
bool [:(bound_QC-variables Al),Y:] is non empty set
v . (p | CY) is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
CY is Element of Y
p | CY is Relation-like bound_QC-variables Al -defined Y -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),Y:]
[:(bound_QC-variables Al),Y:] is Relation-like set
bool [:(bound_QC-variables Al),Y:] is non empty set
v . (p | CY) is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
CY is Element of Y
p | CY is Relation-like bound_QC-variables Al -defined Y -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),Y:]
[:(bound_QC-variables Al),Y:] is Relation-like set
bool [:(bound_QC-variables Al),Y:] is non empty set
v . (p | CY) is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
CY is Element of Y
p | CY is Relation-like bound_QC-variables Al -defined Y -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),Y:]
[:(bound_QC-variables Al),Y:] is Relation-like set
bool [:(bound_QC-variables Al),Y:] is non empty set
v . (p | CY) is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
CY is Element of Y
p | CY is Relation-like bound_QC-variables Al -defined Y -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),Y:]
v . (p | CY) is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
c₉ is Element of Y
p | c₉ is Relation-like bound_QC-variables Al -defined Y -valued Function-like finite countable Element of bool [:(bound_QC-variables Al),Y:]
v . (p | c₉) is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
X is Element of bool (CQC-WFF Al)
p is Element of CQC-WFF Al
'not' p is Element of CQC-WFF Al
Y is Element of bound_QC-variables Al
Ex (Y,('not' p)) is Element of CQC-WFF Al
'not' (Ex (Y,('not' p))) is Element of CQC-WFF Al
All (Y,p) is Element of CQC-WFF Al
<*('not' (Ex (Y,('not' p))))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
J is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng J is finite countable Element of bool (CQC-WFF Al)
J ^ <*('not' (Ex (Y,('not' p))))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*(All (Y,p))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
J ^ <*(All (Y,p))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*(All (Y,p))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
J is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng J is finite countable Element of bool (CQC-WFF Al)
J ^ <*(All (Y,p))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*('not' (Ex (Y,('not' p))))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
J ^ <*('not' (Ex (Y,('not' p))))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
X is Element of CQC-WFF Al
QuantNbr X is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(QuantNbr X) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
p is Element of bound_QC-variables Al
Ex (p,X) is Element of CQC-WFF Al
QuantNbr (Ex (p,X)) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
'not' X is Element of CQC-WFF Al
All (p,('not' X)) is Element of CQC-WFF Al
'not' (All (p,('not' X))) is Element of CQC-WFF Al
QuantNbr ('not' (All (p,('not' X)))) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
QuantNbr (All (p,('not' X))) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
QuantNbr ('not' X) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(QuantNbr ('not' X)) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
X is Element of CQC-WFF Al
QuantNbr X is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
p is Element of bound_QC-variables Al
Y is Element of bound_QC-variables Al
X . (p,Y) is Element of CQC-WFF Al
QuantNbr (X . (p,Y)) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Sbst (p,Y) is finite countable Element of vSUB Al
vSUB Al is set
[X,(Sbst (p,Y))] is V7() Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty set
CQC-Sub-WFF Al is Element of bool (QC-Sub-WFF Al)
bool (QC-Sub-WFF Al) is non empty set
{X,(Sbst (p,Y))} is finite countable set
{X} is finite countable set
{{X,(Sbst (p,Y))},{X}} is finite V42() countable set
CQC_Sub [X,(Sbst (p,Y))] is Element of CQC-WFF Al
QuantNbr (CQC_Sub [X,(Sbst (p,Y))]) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-pred_symbols Al is set
HCar Al is non empty set
K354((HCar Al)) is set
valH Al is Relation-like bound_QC-variables Al -defined HCar Al -valued Function-like V32( bound_QC-variables Al, HCar Al) Element of Valuations_in (Al,(HCar Al))
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
Valuations_in (Al,(HCar Al)) is non empty M5( bound_QC-variables Al, HCar Al)
X is Consistent Element of bool (CQC-WFF Al)
p is Relation-like QC-pred_symbols Al -defined K354((HCar Al)) -valued Function-like V32( QC-pred_symbols Al,K354((HCar Al))) Henkin_interpretation of X
Y is Element of CQC-WFF Al
QuantNbr Y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
J is Element of CQC-WFF Al
v is Element of bound_QC-variables Al
CY is Element of CQC-WFF Al
All (v,CY) is Element of CQC-WFF Al
v is Element of bound_QC-variables Al
CY is Element of CQC-WFF Al
All (v,CY) is Element of CQC-WFF Al
QuantNbr J is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
QuantNbr CY is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(QuantNbr CY) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of J,Y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of J,Y
len the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of J,Y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of J,Y . 0 is set
c₉ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of J,Y . c₉ is set
c₉ + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of J,Y . (c₉ + 1) is set
y is Element of CQC-WFF Al
QuantNbr y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
'not' CY is Element of CQC-WFF Al
Ex (v,('not' CY)) is Element of CQC-WFF Al
c₁₂ is Element of bound_QC-variables Al
('not' CY) . (v,c₁₂) is Element of CQC-WFF Al
QuantNbr ('not' CY) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
QuantNbr (('not' CY) . (v,c₁₂)) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
c₁₂ is Element of bound_QC-variables Al
('not' CY) . (v,c₁₂) is Element of CQC-WFF Al
QuantNbr (('not' CY) . (v,c₁₂)) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
'not' (Ex (v,('not' CY))) is Element of CQC-WFF Al
0 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
y is Element of QC-WFF Al
c₁₂ is Element of QC-WFF Al
f1 is Element of CQC-WFF Al
QuantNbr f1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
f1 is Element of CQC-WFF Al
QuantNbr f1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
k1 is Element of CQC-WFF Al
k1 is Element of CQC-WFF Al
'not' f1 is Element of CQC-WFF Al
QuantNbr k1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
K is Element of QC-WFF Al
K is Element of QC-WFF Al
f1 '&' K is Element of QC-WFF Al
r1 is Element of CQC-WFF Al
QuantNbr r1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(QuantNbr f1) + (QuantNbr r1) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
1 - 1 is ext-real V30() V35() set
(QuantNbr r1) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
((QuantNbr r1) + 1) - 1 is ext-real V30() V35() set
K is Element of QC-WFF Al
K '&' f1 is Element of QC-WFF Al
r1 is Element of CQC-WFF Al
QuantNbr r1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(QuantNbr f1) + (QuantNbr r1) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
K is Element of bound_QC-variables Al
All (K,f1) is Element of CQC-WFF Al
(QuantNbr f1) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
K is Element of CQC-WFF Al
QuantNbr K is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
r1 is Element of CQC-WFF Al
QuantNbr r1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
L is Element of CQC-WFF Al
QuantNbr L is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
c₁₂ is Element of CQC-WFF Al
QuantNbr c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
f1 is Element of CQC-WFF Al
QuantNbr f1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
k1 is Element of CQC-WFF Al
QuantNbr k1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of J,Y . (len the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of J,Y) is set
c₉ is Element of CQC-WFF Al
QuantNbr c₉ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-pred_symbols Al is set
HCar Al is non empty set
K354((HCar Al)) is set
valH Al is Relation-like bound_QC-variables Al -defined HCar Al -valued Function-like V32( bound_QC-variables Al, HCar Al) Element of Valuations_in (Al,(HCar Al))
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
Valuations_in (Al,(HCar Al)) is non empty M5( bound_QC-variables Al, HCar Al)
X is Consistent Element of bool (CQC-WFF Al)
p is Relation-like QC-pred_symbols Al -defined K354((HCar Al)) -valued Function-like V32( QC-pred_symbols Al,K354((HCar Al))) Henkin_interpretation of X
Y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Y + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
J is Element of CQC-WFF Al
QuantNbr J is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
v is Element of CQC-WFF Al
QuantNbr v is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of v,J is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of v,J
len the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of v,J is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of v,J . 0 is set
CY is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of v,J . CY is set
CY + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of v,J . (CY + 1) is set
p is Element of CQC-WFF Al
0 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
p is Element of QC-WFF Al
y is Element of QC-WFF Al
c₁₂ is Element of CQC-WFF Al
QuantNbr c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
c₁₂ is Element of CQC-WFF Al
QuantNbr c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
f1 is Element of CQC-WFF Al
k1 is Element of CQC-WFF Al
'not' c₁₂ is Element of CQC-WFF Al
QuantNbr k1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
k1 is Element of QC-WFF Al
k1 is Element of QC-WFF Al
c₁₂ '&' k1 is Element of QC-WFF Al
K is Element of CQC-WFF Al
QuantNbr K is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(QuantNbr c₁₂) + (QuantNbr K) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
1 + (QuantNbr K) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(QuantNbr K) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
- 1 is ext-real non positive V30() V35() set
((QuantNbr K) + 1) + (- 1) is ext-real V30() V35() set
(Y + 1) + (- 1) is ext-real V30() V35() set
k1 is Element of QC-WFF Al
k1 '&' c₁₂ is Element of QC-WFF Al
K is Element of CQC-WFF Al
QuantNbr K is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(QuantNbr c₁₂) + (QuantNbr K) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
1 + (QuantNbr K) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
(QuantNbr K) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
((QuantNbr K) + 1) + (- 1) is ext-real V30() V35() set
k1 is Element of bound_QC-variables Al
All (k1,c₁₂) is Element of CQC-WFF Al
(QuantNbr c₁₂) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
QuantNbr ('not' c₁₂) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Ex (k1,('not' c₁₂)) is Element of CQC-WFF Al
K is Element of bound_QC-variables Al
('not' c₁₂) . (k1,K) is Element of CQC-WFF Al
QuantNbr (('not' c₁₂) . (k1,K)) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
K is Element of bound_QC-variables Al
('not' c₁₂) . (k1,K) is Element of CQC-WFF Al
QuantNbr (('not' c₁₂) . (k1,K)) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
'not' (Ex (k1,('not' c₁₂))) is Element of CQC-WFF Al
k1 is Element of CQC-WFF Al
QuantNbr k1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
K is Element of CQC-WFF Al
QuantNbr K is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
r1 is Element of CQC-WFF Al
QuantNbr r1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
L is Element of CQC-WFF Al
QuantNbr L is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
y is Element of CQC-WFF Al
QuantNbr y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
f1 is Element of CQC-WFF Al
QuantNbr f1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of v,J . (len the Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable PATH of v,J) is set
CY is Element of CQC-WFF Al
QuantNbr CY is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-pred_symbols Al is set
HCar Al is non empty set
K354((HCar Al)) is set
valH Al is Relation-like bound_QC-variables Al -defined HCar Al -valued Function-like V32( bound_QC-variables Al, HCar Al) Element of Valuations_in (Al,(HCar Al))
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
Valuations_in (Al,(HCar Al)) is non empty M5( bound_QC-variables Al, HCar Al)
X is Consistent Element of bool (CQC-WFF Al)
p is Relation-like QC-pred_symbols Al -defined K354((HCar Al)) -valued Function-like V32( QC-pred_symbols Al,K354((HCar Al))) Henkin_interpretation of X
Y is Element of CQC-WFF Al
QuantNbr Y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
J is Element of CQC-WFF Al
QuantNbr J is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Y + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Al is QC-alphabet
QC-WFF Al is non empty set
QC-symbols Al is non empty set
[:NAT,(QC-symbols Al):] is non empty Relation-like set
[:NAT,(QC-symbols Al):] * is non empty functional FinSequence-membered set
bool ([:NAT,(QC-symbols Al):] *) is non empty set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
X is set
p is set
p is Element of bool (CQC-WFF Al)
Y is set
J is set
v is Element of bound_QC-variables Al
CY is Element of CQC-WFF Al
Ex (v,CY) is Element of CQC-WFF Al
X is Element of bool (CQC-WFF Al)
p is Element of bool (CQC-WFF Al)
Y is set
J is Element of bound_QC-variables Al
v is Element of CQC-WFF Al
Ex (J,v) is Element of CQC-WFF Al
J is Element of bound_QC-variables Al
v is Element of CQC-WFF Al
Ex (J,v) is Element of CQC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
Al is QC-alphabet
(Al) is Element of bool (CQC-WFF Al)
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
the Element of bound_QC-variables Al is Element of bound_QC-variables Al
the Element of CQC-WFF Al is Element of CQC-WFF Al
Ex ( the Element of bound_QC-variables Al, the Element of CQC-WFF Al) is Element of CQC-WFF Al
Al is non empty set
[:NAT,Al:] is non empty Relation-like set
bool [:NAT,Al:] is non empty set
X is Relation-like NAT -defined Al -valued Function-like V32( NAT ,Al) Element of bool [:NAT,Al:]
rng X is Element of bool Al
bool Al is non empty set
dom X is countable Element of bool NAT
Al is QC-alphabet
QC-WFF Al is non empty set
X is Element of QC-WFF Al
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
p is Element of bound_QC-variables Al
J is Element of QC-WFF Al
Ex (p,J) is Element of QC-WFF Al
Y is Element of bound_QC-variables Al
v is Element of QC-WFF Al
Ex (Y,v) is Element of QC-WFF Al
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
X is Element of CQC-WFF Al
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
p is Element of bound_QC-variables Al
Y is Element of QC-WFF Al
Ex (p,Y) is Element of QC-WFF Al
'not' Y is Element of QC-WFF Al
All (p,('not' Y)) is Element of QC-WFF Al
'not' (All (p,('not' Y))) is Element of QC-WFF Al
J is Element of bound_QC-variables Al
p is Element of CQC-WFF Al
Ex (J,p) is Element of CQC-WFF Al
v is Element of bound_QC-variables Al
Y is Element of CQC-WFF Al
Ex (v,Y) is Element of CQC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
[:NAT,(CQC-WFF Al):] is non empty Relation-like set
bool [:NAT,(CQC-WFF Al):] is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
X is Relation-like NAT -defined CQC-WFF Al -valued Function-like V32( NAT , CQC-WFF Al) Element of bool [:NAT,(CQC-WFF Al):]
p is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
X . p is Element of CQC-WFF Al
Y is Element of CQC-WFF Al
(Al,Y) is Element of bound_QC-variables Al
J is Element of CQC-WFF Al
(Al,J) is Element of bound_QC-variables Al
Y is Element of bound_QC-variables Al
J is Element of bound_QC-variables Al
v is Element of CQC-WFF Al
(Al,v) is Element of bound_QC-variables Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
[:NAT,(CQC-WFF Al):] is non empty Relation-like set
bool [:NAT,(CQC-WFF Al):] is non empty set
X is Relation-like NAT -defined CQC-WFF Al -valued Function-like V32( NAT , CQC-WFF Al) Element of bool [:NAT,(CQC-WFF Al):]
p is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
X . p is Element of CQC-WFF Al
Y is Element of CQC-WFF Al
(Al,Y) is Element of CQC-WFF Al
J is Element of CQC-WFF Al
(Al,J) is Element of CQC-WFF Al
Y is Element of CQC-WFF Al
J is Element of CQC-WFF Al
v is Element of CQC-WFF Al
(Al,v) is Element of CQC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
X is Element of bool (CQC-WFF Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X } is set
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
bool (bound_QC-variables Al) is non empty set
Y is set
J is set
v is Element of CQC-WFF Al
still_not-bound_in v is Element of bool (bound_QC-variables Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
X is Element of bool (CQC-WFF Al)
p is Element of CQC-WFF Al
Y is set
<*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng <*p*> is non empty finite countable Element of bool (CQC-WFF Al)
{p} is finite countable Element of bool (CQC-WFF Al)
<*> (CQC-WFF Al) is empty proper Relation-like non-empty empty-yielding NAT -defined CQC-WFF Al -valued Function-like functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() V35() finite finite-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable FinSequence of CQC-WFF Al
[:NAT,(CQC-WFF Al):] is non empty Relation-like set
(<*> (CQC-WFF Al)) ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
((<*> (CQC-WFF Al)) ^ <*p*>) ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*p*> ^ <*p*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1 + 1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
X is Element of CQC-WFF Al
p is Element of bound_QC-variables Al
Ex (p,X) is Element of CQC-WFF Al
(Al,(Ex (p,X))) is Element of bound_QC-variables Al
(Al,(Ex (p,X))) is Element of CQC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
VERUM Al is Element of CQC-WFF Al
X is Element of bool (CQC-WFF Al)
<*> (CQC-WFF Al) is empty proper Relation-like non-empty empty-yielding NAT -defined CQC-WFF Al -valued Function-like functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() V35() finite finite-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable FinSequence of CQC-WFF Al
[:NAT,(CQC-WFF Al):] is non empty Relation-like set
rng (<*> (CQC-WFF Al)) is empty proper Relation-like non-empty empty-yielding functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() V35() finite finite-yielding V42() FinSequence-like FinSequence-membered countable Element of bool (CQC-WFF Al)
<*(VERUM Al)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(<*> (CQC-WFF Al)) ^ <*(VERUM Al)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
VERUM Al is Element of CQC-WFF Al
'not' (VERUM Al) is Element of CQC-WFF Al
X is Element of bool (CQC-WFF Al)
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
X is Element of CQC-WFF Al
<*X*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
p is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
len p is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
p ^ <*X*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Ant p is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(Ant p) ^ Y is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Suc p is Element of CQC-WFF Al
<*(Suc p)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
((Ant p) ^ Y) ^ <*(Suc p)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(((Ant p) ^ Y) ^ <*(Suc p)*>) ^ <*X*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Ant (p ^ <*X*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Ant ((((Ant p) ^ Y) ^ <*(Suc p)*>) ^ <*X*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Suc (p ^ <*X*>) is Element of CQC-WFF Al
Suc ((((Ant p) ^ Y) ^ <*(Suc p)*>) ^ <*X*>) is Element of CQC-WFF Al
Al is QC-alphabet
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
X is Element of CQC-WFF Al
{X} is finite countable Element of bool (CQC-WFF Al)
bool (CQC-WFF Al) is non empty set
(Al,{X}) is Element of bool (bound_QC-variables Al)
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
bool (bound_QC-variables Al) is non empty set
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {X} } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {X} } is set
still_not-bound_in X is Element of bool (bound_QC-variables Al)
p is set
Y is set
J is Element of CQC-WFF Al
still_not-bound_in J is Element of bool (bound_QC-variables Al)
p is set
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
X is Element of bool (CQC-WFF Al)
(Al,X) is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X } is set
p is Element of bool (CQC-WFF Al)
X \/ p is Element of bool (CQC-WFF Al)
(Al,(X \/ p)) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X \/ p } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X \/ p } is set
(Al,p) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in p } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in p } is set
(Al,X) \/ (Al,p) is Element of bool (bound_QC-variables Al)
J is set
v is set
CY is Element of CQC-WFF Al
still_not-bound_in CY is Element of bool (bound_QC-variables Al)
Y is set
J is set
v is Element of CQC-WFF Al
still_not-bound_in v is Element of bool (bound_QC-variables Al)
J is set
v is Element of CQC-WFF Al
still_not-bound_in v is Element of bool (bound_QC-variables Al)
Al is QC-alphabet
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
bool (bound_QC-variables Al) is non empty set
X is Element of bool (bound_QC-variables Al)
p is set
Y is set
p is set
Y is Element of bound_QC-variables Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
X is Element of bool (CQC-WFF Al)
(Al,X) is Element of bool (bound_QC-variables Al)
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
bool (bound_QC-variables Al) is non empty set
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X } is set
p is Element of bool (CQC-WFF Al)
(Al,p) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in p } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in p } is set
J is set
v is set
CY is Element of CQC-WFF Al
still_not-bound_in CY is Element of bool (bound_QC-variables Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
X is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng X is finite countable Element of bool (CQC-WFF Al)
bool (CQC-WFF Al) is non empty set
(Al,(rng X)) is Element of bool (bound_QC-variables Al)
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
bool (bound_QC-variables Al) is non empty set
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in rng X } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in rng X } is set
still_not-bound_in X is Element of bool (bound_QC-variables Al)
Y is set
J is set
v is Element of CQC-WFF Al
still_not-bound_in v is Element of bool (bound_QC-variables Al)
dom X is finite countable Element of bool NAT
CY is set
X . CY is set
Y is set
J is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
v is Element of CQC-WFF Al
X . J is set
still_not-bound_in v is Element of bool (bound_QC-variables Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
X is Consistent Element of bool (CQC-WFF Al)
(Al,X) is Element of bool (bound_QC-variables Al)
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
bool (bound_QC-variables Al) is non empty set
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X } is set
(Al) is Element of bool (CQC-WFF Al)
p is Relation-like Function-like set
dom p is set
rng p is set
[:NAT,(CQC-WFF Al):] is non empty Relation-like set
bool [:NAT,(CQC-WFF Al):] is non empty set
Y is Relation-like NAT -defined CQC-WFF Al -valued Function-like V32( NAT , CQC-WFF Al) Element of bool [:NAT,(CQC-WFF Al):]
QC-symbols Al is non empty set
[:(CQC-WFF Al),(bool (bound_QC-variables Al)):] is non empty Relation-like set
J is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
J + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Y . (J + 1) is Element of CQC-WFF Al
{(Y . (J + 1))} is finite countable Element of bool (CQC-WFF Al)
(Al,{(Y . (J + 1))}) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {(Y . (J + 1))} } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {(Y . (J + 1))} } is set
'not' (Y . (J + 1)) is Element of CQC-WFF Al
(Al,Y,(J + 1)) is Element of CQC-WFF Al
(Al,Y,(J + 1)) is Element of bound_QC-variables Al
v is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
v `2 is set
c<sub>9</sub> is set
p is set
[c<sub>9</sub>,p] is V7() set
{c<sub>9</sub>,p} is finite countable set
{c<sub>9</sub>} is finite countable set
{{c<sub>9</sub>,p},{c<sub>9</sub>}} is finite V42() countable set
CY is Element of bool (bound_QC-variables Al)
CY \/ (Al,{(Y . (J + 1))}) is Element of bool (bound_QC-variables Al)
{ b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in CY \/ (Al,{(Y . (J + 1))}) } is set
Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in CY \/ (Al,{(Y . (J + 1))}) } is Element of QC-symbols Al
x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in CY \/ (Al,{(Y . (J + 1))}) } ) is Element of bound_QC-variables Al
(Al,Y,(J + 1)) . ((Al,Y,(J + 1)),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in CY \/ (Al,{(Y . (J + 1))}) } ))) is Element of CQC-WFF Al
('not' (Y . (J + 1))) 'or' ((Al,Y,(J + 1)) . ((Al,Y,(J + 1)),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in CY \/ (Al,{(Y . (J + 1))}) } )))) is Element of CQC-WFF Al
still_not-bound_in (('not' (Y . (J + 1))) 'or' ((Al,Y,(J + 1)) . ((Al,Y,(J + 1)),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in CY \/ (Al,{(Y . (J + 1))}) } ))))) is Element of bool (bound_QC-variables Al)
CY \/ (still_not-bound_in (('not' (Y . (J + 1))) 'or' ((Al,Y,(J + 1)) . ((Al,Y,(J + 1)),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in CY \/ (Al,{(Y . (J + 1))}) } )))))) is Element of bool (bound_QC-variables Al)
[(('not' (Y . (J + 1))) 'or' ((Al,Y,(J + 1)) . ((Al,Y,(J + 1)),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in CY \/ (Al,{(Y . (J + 1))}) } ))))),(CY \/ (still_not-bound_in (('not' (Y . (J + 1))) 'or' ((Al,Y,(J + 1)) . ((Al,Y,(J + 1)),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in CY \/ (Al,{(Y . (J + 1))}) } )))))))] is V7() Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
{(('not' (Y . (J + 1))) 'or' ((Al,Y,(J + 1)) . ((Al,Y,(J + 1)),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in CY \/ (Al,{(Y . (J + 1))}) } ))))),(CY \/ (still_not-bound_in (('not' (Y . (J + 1))) 'or' ((Al,Y,(J + 1)) . ((Al,Y,(J + 1)),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in CY \/ (Al,{(Y . (J + 1))}) } )))))))} is finite countable set
{(('not' (Y . (J + 1))) 'or' ((Al,Y,(J + 1)) . ((Al,Y,(J + 1)),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in CY \/ (Al,{(Y . (J + 1))}) } )))))} is finite countable set
{{(('not' (Y . (J + 1))) 'or' ((Al,Y,(J + 1)) . ((Al,Y,(J + 1)),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in CY \/ (Al,{(Y . (J + 1))}) } ))))),(CY \/ (still_not-bound_in (('not' (Y . (J + 1))) 'or' ((Al,Y,(J + 1)) . ((Al,Y,(J + 1)),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in CY \/ (Al,{(Y . (J + 1))}) } )))))))},{(('not' (Y . (J + 1))) 'or' ((Al,Y,(J + 1)) . ((Al,Y,(J + 1)),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in CY \/ (Al,{(Y . (J + 1))}) } )))))}} is finite V42() countable set
Y . 0 is Element of CQC-WFF Al
'not' (Y . 0) is Element of CQC-WFF Al
(Al,Y,0) is Element of CQC-WFF Al
(Al,Y,0) is Element of bound_QC-variables Al
{(Y . 0)} is finite countable Element of bool (CQC-WFF Al)
X \/ {(Y . 0)} is Element of bool (CQC-WFF Al)
(Al,(X \/ {(Y . 0)})) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in X \/ {(Y . 0)} } is set
union { (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in X \/ {(Y . 0)} } is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,(X \/ {(Y . 0)})) } is set
Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,(X \/ {(Y . 0)})) } is Element of QC-symbols Al
x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,(X \/ {(Y . 0)})) } ) is Element of bound_QC-variables Al
(Al,Y,0) . ((Al,Y,0),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,(X \/ {(Y . 0)})) } ))) is Element of CQC-WFF Al
('not' (Y . 0)) 'or' ((Al,Y,0) . ((Al,Y,0),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,(X \/ {(Y . 0)})) } )))) is Element of CQC-WFF Al
{(('not' (Y . 0)) 'or' ((Al,Y,0) . ((Al,Y,0),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,(X \/ {(Y . 0)})) } )))))} is finite countable Element of bool (CQC-WFF Al)
X \/ {(('not' (Y . 0)) 'or' ((Al,Y,0) . ((Al,Y,0),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,(X \/ {(Y . 0)})) } )))))} is Element of bool (CQC-WFF Al)
(Al,(X \/ {(('not' (Y . 0)) 'or' ((Al,Y,0) . ((Al,Y,0),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,(X \/ {(Y . 0)})) } )))))})) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in X \/ {(('not' (Y . 0)) 'or' ((Al,Y,0) . ((Al,Y,0),(x. (Al -one_in { b<sub>1</sub> where b<sub>2</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,(X \/ {(Y . 0)})) } )))))} } is set
union { (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in X \/ {(('not' (Y . 0)) 'or' ((Al,Y,0) . ((Al,Y,0),(x. (Al -one_in { b<sub>1</sub> where b<sub>2</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,(X \/ {(Y . 0)})) } )))))} } is set
[(('not' (Y . 0)) 'or' ((Al,Y,0) . ((Al,Y,0),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,(X \/ {(Y . 0)})) } ))))),(Al,(X \/ {(('not' (Y . 0)) 'or' ((Al,Y,0) . ((Al,Y,0),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,(X \/ {(Y . 0)})) } )))))}))] is V7() Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
{(('not' (Y . 0)) 'or' ((Al,Y,0) . ((Al,Y,0),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,(X \/ {(Y . 0)})) } ))))),(Al,(X \/ {(('not' (Y . 0)) 'or' ((Al,Y,0) . ((Al,Y,0),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,(X \/ {(Y . 0)})) } )))))}))} is finite countable set
{(('not' (Y . 0)) 'or' ((Al,Y,0) . ((Al,Y,0),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,(X \/ {(Y . 0)})) } )))))} is finite countable set
{{(('not' (Y . 0)) 'or' ((Al,Y,0) . ((Al,Y,0),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,(X \/ {(Y . 0)})) } ))))),(Al,(X \/ {(('not' (Y . 0)) 'or' ((Al,Y,0) . ((Al,Y,0),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,(X \/ {(Y . 0)})) } )))))}))},{(('not' (Y . 0)) 'or' ((Al,Y,0) . ((Al,Y,0),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,(X \/ {(Y . 0)})) } )))))}} is finite V42() countable set
[:NAT,[:(CQC-WFF Al),(bool (bound_QC-variables Al)):]:] is non empty Relation-like set
bool [:NAT,[:(CQC-WFF Al),(bool (bound_QC-variables Al)):]:] is non empty set
J is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
v is Relation-like NAT -defined [:(CQC-WFF Al),(bool (bound_QC-variables Al)):] -valued Function-like V32( NAT ,[:(CQC-WFF Al),(bool (bound_QC-variables Al)):]) Element of bool [:NAT,[:(CQC-WFF Al),(bool (bound_QC-variables Al)):]:]
v . 0 is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
{ ((v . b<sub>1</sub>) `1) where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : verum } is set
X \/ { ((v . b₁) `1) where b<sub>1</sub> is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : verum } is set
CY is set
c<sub>9</sub> is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
v . c<sub>9</sub> is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
(v . c<sub>9</sub>) `1 is set
p is set
y is set
[p,y] is V7() set
{p,y} is finite countable set
{p} is finite countable set
{{p,y},{p}} is finite V42() countable set
c₉ is Element of bound_QC-variables Al
p is Element of CQC-WFF Al
Ex (c₉,p) is Element of CQC-WFF Al
dom Y is countable Element of bool NAT
y is set
Y . y is set
c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Y . c₁₂ is Element of CQC-WFF Al
f1 is Element of CQC-WFF Al
(Al,f1) is Element of bound_QC-variables Al
(Al,f1) is Element of CQC-WFF Al
(Al,Y,c₁₂) is Element of bound_QC-variables Al
(Al,Y,c₁₂) is Element of CQC-WFF Al
v . c₁₂ is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
(v . c₁₂) `1 is set
CY is Element of bool (CQC-WFF Al)
{f1} is finite countable Element of bool (CQC-WFF Al)
X \/ {f1} is Element of bool (CQC-WFF Al)
(Al,(X \/ {f1})) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in X \/ {f1} } is set
union { (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in X \/ {f1} } is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,(X \/ {f1})) } is set
Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,(X \/ {f1})) } is Element of QC-symbols Al
x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,(X \/ {f1})) } ) is Element of bound_QC-variables Al
'not' f1 is Element of CQC-WFF Al
k1 is Element of bound_QC-variables Al
(Al,Y,c<sub>12</sub>) . ((Al,Y,c<sub>12</sub>),k1) is Element of CQC-WFF Al
('not' f1) 'or' ((Al,Y,c<sub>12</sub>) . ((Al,Y,c<sub>12</sub>),k1)) is Element of CQC-WFF Al
'not' (Ex (c<sub>9</sub>,p)) is Element of CQC-WFF Al
p . (c<sub>9</sub>,k1) is Element of CQC-WFF Al
('not' (Ex (c<sub>9</sub>,p))) 'or' (p . (c<sub>9</sub>,k1)) is Element of CQC-WFF Al
k1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() set
k1 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
k1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
v . k1 is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
(v . k1) `2 is set
(Al,{f1}) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {f1} } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {f1} } is set
(Al,{f1}) \/ ((v . k1) `2) is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,{f1}) \/ ((v . k1) `2) } is set
Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in (Al,{f1}) \/ ((v . k1) `2) } is Element of QC-symbols Al
x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,{f1}) \/ ((v . k1) `2) } ) is Element of bound_QC-variables Al
L is Element of bound_QC-variables Al
(Al,Y,c₁₂) . ((Al,Y,c₁₂),L) is Element of CQC-WFF Al
('not' f1) 'or' ((Al,Y,c₁₂) . ((Al,Y,c₁₂),L)) is Element of CQC-WFF Al
p1 is Element of bool (bound_QC-variables Al)
s is Element of bool (bound_QC-variables Al)
p1 \/ (Al,{f1}) is Element of bool (bound_QC-variables Al)
{ b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in s } is set
Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in s } is Element of QC-symbols Al
x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in s } ) is Element of bound_QC-variables Al
(Al,Y,c₁₂) . ((Al,Y,c₁₂),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in s } ))) is Element of CQC-WFF Al
('not' f1) 'or' ((Al,Y,c₁₂) . ((Al,Y,c₁₂),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in s } )))) is Element of CQC-WFF Al
still_not-bound_in (('not' f1) 'or' ((Al,Y,c₁₂) . ((Al,Y,c₁₂),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in s } ))))) is Element of bool (bound_QC-variables Al)
p1 \/ (still_not-bound_in (('not' f1) 'or' ((Al,Y,c₁₂) . ((Al,Y,c₁₂),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in s } )))))) is Element of bool (bound_QC-variables Al)
[(('not' f1) 'or' ((Al,Y,c₁₂) . ((Al,Y,c₁₂),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in s } ))))),(p1 \/ (still_not-bound_in (('not' f1) 'or' ((Al,Y,c₁₂) . ((Al,Y,c₁₂),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in s } )))))))] is V7() Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
{(('not' f1) 'or' ((Al,Y,c₁₂) . ((Al,Y,c₁₂),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in s } ))))),(p1 \/ (still_not-bound_in (('not' f1) 'or' ((Al,Y,c₁₂) . ((Al,Y,c₁₂),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in s } )))))))} is finite countable set
{(('not' f1) 'or' ((Al,Y,c₁₂) . ((Al,Y,c₁₂),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in s } )))))} is finite countable set
{{(('not' f1) 'or' ((Al,Y,c₁₂) . ((Al,Y,c₁₂),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in s } ))))),(p1 \/ (still_not-bound_in (('not' f1) 'or' ((Al,Y,c₁₂) . ((Al,Y,c₁₂),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in s } )))))))},{(('not' f1) 'or' ((Al,Y,c₁₂) . ((Al,Y,c₁₂),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in s } )))))}} is finite V42() countable set
p . (c₉,L) is Element of CQC-WFF Al
('not' (Ex (c₉,p))) 'or' (p . (c₉,L)) is Element of CQC-WFF Al
k1 is Element of bound_QC-variables Al
p . (c₉,k1) is Element of CQC-WFF Al
('not' (Ex (c₉,p))) 'or' (p . (c₉,k1)) is Element of CQC-WFF Al
k1 is Element of bound_QC-variables Al
p . (c₉,k1) is Element of CQC-WFF Al
('not' (Ex (c₉,p))) 'or' (p . (c₉,k1)) is Element of CQC-WFF Al
{ ((v . b₁) `1) where b<sub>1</sub> is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : b<sub>1</sub> in a<sub>1</sub> } is set
X \/ { ((v . b<sub>1</sub>) `1) where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : b₁ in a₁ } is set
c₉ is Relation-like Function-like set
dom c₉ is set
rng c₉ is set
union (rng c₉) is set
p is set
c₉ . 0 is set
{ ((v . b₁) `1) where b<sub>1</sub> is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : b<sub>1</sub> in 0 } is set
X \/ { ((v . b<sub>1</sub>) `1) where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : b₁ in 0 } is set
y is set
c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
v . c₁₂ is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
(v . c₁₂) `1 is set
y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
v . y is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
(v . y) `1 is set
y + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
{ ((v . b₁) `1) where b<sub>1</sub> is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : b<sub>1</sub> in y + 1 } is set
c<sub>9</sub> . (y + 1) is set
X \/ { ((v . b<sub>1</sub>) `1) where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : b₁ in y + 1 } is set
p is set
y is set
c₁₂ is set
c₉ . c₁₂ is set
f1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
{ ((v . b₁) `1) where b<sub>1</sub> is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : b<sub>1</sub> in f1 } is set
X \/ { ((v . b<sub>1</sub>) `1) where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : b₁ in f1 } is set
k1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
v . k1 is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
(v . k1) `1 is set
p is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
c<sub>9</sub> . p is set
y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
c<sub>9</sub> . y is set
{ ((v . b<sub>1</sub>) `1) where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : b₁ in p } is set
X \/ { ((v . b₁) `1) where b<sub>1</sub> is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : b<sub>1</sub> in p } is set
{ ((v . b<sub>1</sub>) `1) where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : b₁ in y } is set
X \/ { ((v . b₁) `1) where b<sub>1</sub> is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : b<sub>1</sub> in y } is set
c<sub>12</sub> is set
f1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
v . f1 is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
(v . f1) `1 is set
p is set
y is set
c₉ . y is set
c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
c₉ . c₁₂ is set
{ ((v . b₁) `1) where b<sub>1</sub> is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : b<sub>1</sub> in c<sub>12</sub> } is set
X \/ { ((v . b<sub>1</sub>) `1) where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : b₁ in c₁₂ } is set
f1 is set
k1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
v . k1 is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
(v . k1) `1 is set
[:NAT,(bool (CQC-WFF Al)):] is non empty Relation-like set
bool [:NAT,(bool (CQC-WFF Al)):] is non empty set
p is Relation-like NAT -defined bool (CQC-WFF Al) -valued Function-like V32( NAT , bool (CQC-WFF Al)) Element of bool [:NAT,(bool (CQC-WFF Al)):]
y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
y + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
p . (y + 1) is Element of bool (CQC-WFF Al)
p . y is Element of bool (CQC-WFF Al)
v . y is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
(v . y) `1 is set
{((v . y) `1)} is finite countable set
(p . y) \/ {((v . y) `1)} is set
c₁₂ is set
{ ((v . b₁) `1) where b<sub>1</sub> is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : b<sub>1</sub> in y + 1 } is set
f1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
v . f1 is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
(v . f1) `1 is set
f1 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
{ ((v . b₁) `1) where b<sub>1</sub> is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : b<sub>1</sub> in y } is set
{ ((v . b<sub>1</sub>) `1) where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : b₁ in y } \/ {((v . y) `1)} is set
c<sub>12</sub> is set
f1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
v . f1 is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
(v . f1) `1 is set
X \/ ( { ((v . b₁) `1) where b<sub>1</sub> is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : b<sub>1</sub> in y } \/ {((v . y) `1)}) is set
X \/ { ((v . b₁) `1) where b<sub>1</sub> is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : b<sub>1</sub> in y } is set
(X \/ { ((v . b<sub>1</sub>) `1) where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : b₁ in y } ) \/ {((v . y) `1)} is set
(v . 0) `2 is set
y is Element of CQC-WFF Al
still_not-bound_in y is Element of bool (bound_QC-variables Al)
{y} is finite countable Element of bool (CQC-WFF Al)
(Al,{y}) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {y} } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {y} } is set
(Al,{y}) \/ (Al,X) is Element of bool (bound_QC-variables Al)
y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
v . y is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
(v . y) `2 is set
y + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
v . (y + 1) is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
(v . (y + 1)) `2 is set
Y . (y + 1) is Element of CQC-WFF Al
{(Y . (y + 1))} is finite countable Element of bool (CQC-WFF Al)
(Al,{(Y . (y + 1))}) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {(Y . (y + 1))} } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {(Y . (y + 1))} } is set
'not' (Y . (y + 1)) is Element of CQC-WFF Al
(Al,Y,(y + 1)) is Element of CQC-WFF Al
(Al,Y,(y + 1)) is Element of bound_QC-variables Al
f1 is Element of bool (bound_QC-variables Al)
f1 \/ (Al,{(Y . (y + 1))}) is Element of bool (bound_QC-variables Al)
{ b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in f1 \/ (Al,{(Y . (y + 1))}) } is set
Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in f1 \/ (Al,{(Y . (y + 1))}) } is Element of QC-symbols Al
x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in f1 \/ (Al,{(Y . (y + 1))}) } ) is Element of bound_QC-variables Al
(Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in f1 \/ (Al,{(Y . (y + 1))}) } ))) is Element of CQC-WFF Al
('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in f1 \/ (Al,{(Y . (y + 1))}) } )))) is Element of CQC-WFF Al
still_not-bound_in (('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in f1 \/ (Al,{(Y . (y + 1))}) } ))))) is Element of bool (bound_QC-variables Al)
K is Element of bool (bound_QC-variables Al)
r1 is Element of bool (bound_QC-variables Al)
K \/ (Al,{(Y . (y + 1))}) is Element of bool (bound_QC-variables Al)
{ b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in r1 } is set
Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in r1 } is Element of QC-symbols Al
x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in r1 } ) is Element of bound_QC-variables Al
(Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in r1 } ))) is Element of CQC-WFF Al
('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in r1 } )))) is Element of CQC-WFF Al
still_not-bound_in (('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in r1 } ))))) is Element of bool (bound_QC-variables Al)
K \/ (still_not-bound_in (('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in r1 } )))))) is Element of bool (bound_QC-variables Al)
[(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in r1 } ))))),(K \/ (still_not-bound_in (('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in r1 } )))))))] is V7() Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
{(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in r1 } ))))),(K \/ (still_not-bound_in (('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in r1 } )))))))} is finite countable set
{(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in r1 } )))))} is finite countable set
{{(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in r1 } ))))),(K \/ (still_not-bound_in (('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in r1 } )))))))},{(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in r1 } )))))}} is finite V42() countable set
{ b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in (Al,{(Y . (a₁ + 1))}) \/ ((v . a₁) `2) } is set
Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,{(Y . (a<sub>1</sub> + 1))}) \/ ((v . a<sub>1</sub>) `2) } is Element of QC-symbols Al
x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in (Al,{(Y . (a₁ + 1))}) \/ ((v . a₁) `2) } ) is Element of bound_QC-variables Al
0 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
p . (0 + 1) is Element of bool (CQC-WFF Al)
(Al,(p . (0 + 1))) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in p . (0 + 1) } is set
union { (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in p . (0 + 1) } is set
Y . (0 + 1) is Element of CQC-WFF Al
{(Y . (0 + 1))} is finite countable Element of bool (CQC-WFF Al)
(Al,{(Y . (0 + 1))}) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in {(Y . (0 + 1))} } is set
union { (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in {(Y . (0 + 1))} } is set
(Al,{(Y . (0 + 1))}) \/ ((v . 0) `2) is set
{ b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in (Al,{(Y . (0 + 1))}) \/ ((v . 0) `2) } is set
Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,{(Y . (0 + 1))}) \/ ((v . 0) `2) } is Element of QC-symbols Al
x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in (Al,{(Y . (0 + 1))}) \/ ((v . 0) `2) } ) is Element of bound_QC-variables Al
(p . (0 + 1)) \/ {(Y . (0 + 1))} is Element of bool (CQC-WFF Al)
(Al,((p . (0 + 1)) \/ {(Y . (0 + 1))})) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in (p . (0 + 1)) \/ {(Y . (0 + 1))} } is set
union { (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in (p . (0 + 1)) \/ {(Y . (0 + 1))} } is set
Y . 1 is Element of CQC-WFF Al
f1 is Element of CQC-WFF Al
{f1} is finite countable Element of bool (CQC-WFF Al)
(Al,{f1}) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in {f1} } is set
union { (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in {f1} } is set
k1 is Element of bool (bound_QC-variables Al)
(Al,{f1}) \/ k1 is Element of bool (bound_QC-variables Al)
still_not-bound_in f1 is Element of bool (bound_QC-variables Al)
k1 is Element of bool (bound_QC-variables Al)
K is Element of bound_QC-variables Al
r1 is Element of QC-symbols Al
x. r1 is Element of bound_QC-variables Al
{ b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in k1 } is set
p1 is set
L is non empty set
s is Element of QC-symbols Al
x. s is Element of bound_QC-variables Al
bool (QC-symbols Al) is non empty set
p1 is non empty Element of bool (QC-symbols Al)
Al -one_in p1 is Element of QC-symbols Al
the Element of p1 is Element of p1
p . 0 is Element of bool (CQC-WFF Al)
{ ((v . b<sub>1</sub>) `1) where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : b₁ in 0 } is set
X \/ { ((v . b₁) `1) where b<sub>1</sub> is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : b<sub>1</sub> in 0 } is set
y is set
u is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
v . u is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
(v . u) `1 is set
(v . 0) `1 is set
y is Element of QC-symbols Al
x. y is Element of bound_QC-variables Al
y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
y + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
p . (y + 1) is Element of bool (CQC-WFF Al)
(Al,(p . (y + 1))) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in p . (y + 1) } is set
union { (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in p . (y + 1) } is set
v . y is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
(v . y) `2 is set
Y . (y + 1) is Element of CQC-WFF Al
{(Y . (y + 1))} is finite countable Element of bool (CQC-WFF Al)
(Al,{(Y . (y + 1))}) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {(Y . (y + 1))} } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {(Y . (y + 1))} } is set
(Al,{(Y . (y + 1))}) \/ ((v . y) `2) is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,{(Y . (y + 1))}) \/ ((v . y) `2) } is set
Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in (Al,{(Y . (y + 1))}) \/ ((v . y) `2) } is Element of QC-symbols Al
x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,{(Y . (y + 1))}) \/ ((v . y) `2) } ) is Element of bound_QC-variables Al
(p . (y + 1)) \/ {(Y . (y + 1))} is Element of bool (CQC-WFF Al)
(Al,((p . (y + 1)) \/ {(Y . (y + 1))})) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in (p . (y + 1)) \/ {(Y . (y + 1))} } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in (p . (y + 1)) \/ {(Y . (y + 1))} } is set
(y + 1) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
p . ((y + 1) + 1) is Element of bool (CQC-WFF Al)
(Al,(p . ((y + 1) + 1))) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in p . ((y + 1) + 1) } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in p . ((y + 1) + 1) } is set
v . (y + 1) is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
(v . (y + 1)) `2 is set
Y . ((y + 1) + 1) is Element of CQC-WFF Al
{(Y . ((y + 1) + 1))} is finite countable Element of bool (CQC-WFF Al)
(Al,{(Y . ((y + 1) + 1))}) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in {(Y . ((y + 1) + 1))} } is set
union { (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in {(Y . ((y + 1) + 1))} } is set
(Al,{(Y . ((y + 1) + 1))}) \/ ((v . (y + 1)) `2) is set
{ b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in (Al,{(Y . ((y + 1) + 1))}) \/ ((v . (y + 1)) `2) } is set
Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,{(Y . ((y + 1) + 1))}) \/ ((v . (y + 1)) `2) } is Element of QC-symbols Al
x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in (Al,{(Y . ((y + 1) + 1))}) \/ ((v . (y + 1)) `2) } ) is Element of bound_QC-variables Al
(p . ((y + 1) + 1)) \/ {(Y . ((y + 1) + 1))} is Element of bool (CQC-WFF Al)
(Al,((p . ((y + 1) + 1)) \/ {(Y . ((y + 1) + 1))})) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in (p . ((y + 1) + 1)) \/ {(Y . ((y + 1) + 1))} } is set
union { (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in (p . ((y + 1) + 1)) \/ {(Y . ((y + 1) + 1))} } is set
y + 2 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Y . (y + 2) is Element of CQC-WFF Al
'not' (Y . (y + 1)) is Element of CQC-WFF Al
(Al,Y,(y + 1)) is Element of CQC-WFF Al
(Al,Y,(y + 1)) is Element of bound_QC-variables Al
k1 is Element of bool (bound_QC-variables Al)
k1 \/ (Al,{(Y . (y + 1))}) is Element of bool (bound_QC-variables Al)
{ b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in k1 \/ (Al,{(Y . (y + 1))}) } is set
Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in k1 \/ (Al,{(Y . (y + 1))}) } is Element of QC-symbols Al
x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in k1 \/ (Al,{(Y . (y + 1))}) } ) is Element of bound_QC-variables Al
(Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in k1 \/ (Al,{(Y . (y + 1))}) } ))) is Element of CQC-WFF Al
('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in k1 \/ (Al,{(Y . (y + 1))}) } )))) is Element of CQC-WFF Al
(v . (y + 1)) `1 is set
r1 is Element of bool (bound_QC-variables Al)
L is Element of bool (bound_QC-variables Al)
r1 \/ (Al,{(Y . (y + 1))}) is Element of bool (bound_QC-variables Al)
{ b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } is set
Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } is Element of QC-symbols Al
x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } ) is Element of bound_QC-variables Al
(Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } ))) is Element of CQC-WFF Al
('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } )))) is Element of CQC-WFF Al
still_not-bound_in (('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } ))))) is Element of bool (bound_QC-variables Al)
r1 \/ (still_not-bound_in (('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } )))))) is Element of bool (bound_QC-variables Al)
[(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } ))))),(r1 \/ (still_not-bound_in (('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } )))))))] is V7() Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
{(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } ))))),(r1 \/ (still_not-bound_in (('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } )))))))} is finite countable set
{(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } )))))} is finite countable set
{{(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } ))))),(r1 \/ (still_not-bound_in (('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } )))))))},{(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } )))))}} is finite V42() countable set
still_not-bound_in (('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in k1 \/ (Al,{(Y . (y + 1))}) } ))))) is Element of bool (bound_QC-variables Al)
k1 \/ (still_not-bound_in (('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in k1 \/ (Al,{(Y . (y + 1))}) } )))))) is Element of bool (bound_QC-variables Al)
r1 is Element of bool (bound_QC-variables Al)
L is Element of bool (bound_QC-variables Al)
r1 \/ (Al,{(Y . (y + 1))}) is Element of bool (bound_QC-variables Al)
{ b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } is set
Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } is Element of QC-symbols Al
x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } ) is Element of bound_QC-variables Al
(Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } ))) is Element of CQC-WFF Al
('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } )))) is Element of CQC-WFF Al
still_not-bound_in (('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } ))))) is Element of bool (bound_QC-variables Al)
r1 \/ (still_not-bound_in (('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } )))))) is Element of bool (bound_QC-variables Al)
[(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } ))))),(r1 \/ (still_not-bound_in (('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } )))))))] is V7() Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
{(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } ))))),(r1 \/ (still_not-bound_in (('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } )))))))} is finite countable set
{(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } )))))} is finite countable set
{{(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } ))))),(r1 \/ (still_not-bound_in (('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } )))))))},{(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in L } )))))}} is finite V42() countable set
L is Element of bool (bound_QC-variables Al)
p1 is Element of bool (bound_QC-variables Al)
L \/ (Al,{(Y . (y + 1))}) is Element of bool (bound_QC-variables Al)
{ b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in p1 } is set
Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in p1 } is Element of QC-symbols Al
x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in p1 } ) is Element of bound_QC-variables Al
(Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in p1 } ))) is Element of CQC-WFF Al
('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in p1 } )))) is Element of CQC-WFF Al
still_not-bound_in (('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in p1 } ))))) is Element of bool (bound_QC-variables Al)
L \/ (still_not-bound_in (('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in p1 } )))))) is Element of bool (bound_QC-variables Al)
[(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in p1 } ))))),(L \/ (still_not-bound_in (('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in p1 } )))))))] is V7() Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
{(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in p1 } ))))),(L \/ (still_not-bound_in (('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in p1 } )))))))} is finite countable set
{(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in p1 } )))))} is finite countable set
{{(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in p1 } ))))),(L \/ (still_not-bound_in (('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in p1 } )))))))},{(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in p1 } )))))}} is finite V42() countable set
c₁₂ is Element of CQC-WFF Al
{c₁₂} is finite countable Element of bool (CQC-WFF Al)
(Al,{c₁₂}) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {c₁₂} } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {c₁₂} } is set
r1 is Element of bool (bound_QC-variables Al)
(Al,{c₁₂}) \/ r1 is Element of bool (bound_QC-variables Al)
still_not-bound_in c₁₂ is Element of bool (bound_QC-variables Al)
L is Element of bool (bound_QC-variables Al)
p1 is Element of bound_QC-variables Al
s is Element of QC-symbols Al
x. s is Element of bound_QC-variables Al
{ b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in (Al,{c₁₂}) \/ r1 } is set
u is set
y is non empty set
r2 is Element of QC-symbols Al
x. r2 is Element of bound_QC-variables Al
bool (QC-symbols Al) is non empty set
u is non empty Element of bool (QC-symbols Al)
Al -one_in u is Element of QC-symbols Al
the Element of u is Element of u
x. (Al -one_in u) is Element of bound_QC-variables Al
y2 is Element of QC-symbols Al
x. y2 is Element of bound_QC-variables Al
(Al,(p . (y + 1))) \/ (still_not-bound_in (('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in k1 \/ (Al,{(Y . (y + 1))}) } )))))) is Element of bool (bound_QC-variables Al)
{(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in k1 \/ (Al,{(Y . (y + 1))}) } )))))} is finite countable Element of bool (CQC-WFF Al)
(Al,{(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in k1 \/ (Al,{(Y . (y + 1))}) } )))))}) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₂ is Element of QC-symbols Al : not x. b₁ in k1 \/ (Al,{(Y . (y + 1))}) } )))))} } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₂ is Element of QC-symbols Al : not x. b₁ in k1 \/ (Al,{(Y . (y + 1))}) } )))))} } is set
(Al,(p . (y + 1))) \/ (Al,{(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in k1 \/ (Al,{(Y . (y + 1))}) } )))))}) is Element of bool (bound_QC-variables Al)
(p . (y + 1)) \/ {(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in k1 \/ (Al,{(Y . (y + 1))}) } )))))} is Element of bool (CQC-WFF Al)
(Al,((p . (y + 1)) \/ {(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in k1 \/ (Al,{(Y . (y + 1))}) } )))))})) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in (p . (y + 1)) \/ {(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₂ is Element of QC-symbols Al : not x. b₁ in k1 \/ (Al,{(Y . (y + 1))}) } )))))} } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in (p . (y + 1)) \/ {(('not' (Y . (y + 1))) 'or' ((Al,Y,(y + 1)) . ((Al,Y,(y + 1)),(x. (Al -one_in { b₁ where b₂ is Element of QC-symbols Al : not x. b₁ in k1 \/ (Al,{(Y . (y + 1))}) } )))))} } is set
y2 is Element of QC-symbols Al
x. y2 is Element of bound_QC-variables Al
(Al,(p . ((y + 1) + 1))) \/ (Al,{c₁₂}) is Element of bool (bound_QC-variables Al)
y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
y + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
p . (y + 1) is Element of bool (CQC-WFF Al)
(Al,(p . (y + 1))) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in p . (y + 1) } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in p . (y + 1) } is set
v . y is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
(v . y) `2 is set
c<sub>12</sub> is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
c<sub>12</sub> + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Y . (c<sub>12</sub> + 1) is Element of CQC-WFF Al
{(Y . (c<sub>12</sub> + 1))} is finite countable Element of bool (CQC-WFF Al)
(Al,{(Y . (c<sub>12</sub> + 1))}) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in {(Y . (c<sub>12</sub> + 1))} } is set
union { (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in {(Y . (c<sub>12</sub> + 1))} } is set
v . c<sub>12</sub> is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
(v . c<sub>12</sub>) `2 is set
(Al,{(Y . (c₁₂ + 1))}) \/ ((v . c₁₂) `2) is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,{(Y . (c<sub>12</sub> + 1))}) \/ ((v . c<sub>12</sub>) `2) } is set
Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in (Al,{(Y . (c₁₂ + 1))}) \/ ((v . c₁₂) `2) } is Element of QC-symbols Al
x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,{(Y . (c<sub>12</sub> + 1))}) \/ ((v . c<sub>12</sub>) `2) } ) is Element of bound_QC-variables Al
p . (c₁₂ + 1) is Element of bool (CQC-WFF Al)
(p . (c₁₂ + 1)) \/ {(Y . (c₁₂ + 1))} is Element of bool (CQC-WFF Al)
(Al,((p . (c₁₂ + 1)) \/ {(Y . (c₁₂ + 1))})) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in (p . (c₁₂ + 1)) \/ {(Y . (c₁₂ + 1))} } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in (p . (c₁₂ + 1)) \/ {(Y . (c₁₂ + 1))} } is set
y is set
{ ((v . b₁) `1) where b<sub>1</sub> is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : b<sub>1</sub> in 0 } is set
c<sub>12</sub> is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
v . c<sub>12</sub> is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
(v . c<sub>12</sub>) `1 is set
p . 0 is Element of bool (CQC-WFF Al)
X \/ {} is set
y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
p . y is Element of bool (CQC-WFF Al)
y + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
p . (y + 1) is Element of bool (CQC-WFF Al)
v . y is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
(v . y) `1 is set
f1 is set
k1 is set
[f1,k1] is V7() set
{f1,k1} is finite countable set
{f1} is finite countable set
{{f1,k1},{f1}} is finite V42() countable set
VERUM Al is Element of CQC-WFF Al
'not' (VERUM Al) is Element of CQC-WFF Al
c<sub>12</sub> is Element of CQC-WFF Al
{c<sub>12</sub>} is finite countable Element of bool (CQC-WFF Al)
(p . y) \/ {c<sub>12</sub>} is Element of bool (CQC-WFF Al)
<*c<sub>12</sub>*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*('not' (VERUM Al))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
f1 is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng f1 is finite countable Element of bool (CQC-WFF Al)
f1 ^ <*c<sub>12</sub>*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(f1 ^ <*c<sub>12</sub>*>) ^ <*('not' (VERUM Al))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Y . y is Element of CQC-WFF Al
'not' (Y . y) is Element of CQC-WFF Al
<*('not' (Y . y))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
f1 ^ <*('not' (Y . y))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(f1 ^ <*('not' (Y . y))*>) ^ <*('not' (Y . y))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
k1 is Element of CQC-WFF Al
('not' (Y . y)) 'or' k1 is Element of CQC-WFF Al
<*(('not' (Y . y)) 'or' k1)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(f1 ^ <*('not' (Y . y))*>) ^ <*(('not' (Y . y)) 'or' k1)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
0 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
len (f1 ^ <*c<sub>12</sub>*>) is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Ant (f1 ^ <*c<sub>12</sub>*>) is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(Ant (f1 ^ <*c<sub>12</sub>*>)) ^ <*('not' (Y . y))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Suc (f1 ^ <*c<sub>12</sub>*>) is Element of CQC-WFF Al
<*(Suc (f1 ^ <*c<sub>12</sub>*>))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
((Ant (f1 ^ <*c<sub>12</sub>*>)) ^ <*('not' (Y . y))*>) ^ <*(Suc (f1 ^ <*c<sub>12</sub>*>))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(((Ant (f1 ^ <*c<sub>12</sub>*>)) ^ <*('not' (Y . y))*>) ^ <*(Suc (f1 ^ <*c<sub>12</sub>*>))*>) ^ <*('not' (VERUM Al))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(f1 ^ <*('not' (Y . y))*>) ^ <*(Suc (f1 ^ <*c<sub>12</sub>*>))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
((f1 ^ <*('not' (Y . y))*>) ^ <*(Suc (f1 ^ <*c<sub>12</sub>*>))*>) ^ <*('not' (VERUM Al))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(f1 ^ <*('not' (Y . y))*>) ^ <*c<sub>12</sub>*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
((f1 ^ <*('not' (Y . y))*>) ^ <*c<sub>12</sub>*>) ^ <*('not' (VERUM Al))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(f1 ^ <*('not' (Y . y))*>) ^ <*('not' (VERUM Al))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*k1*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
f1 ^ <*k1*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(f1 ^ <*k1*>) ^ <*k1*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(f1 ^ <*k1*>) ^ <*(('not' (Y . y)) 'or' k1)*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(Ant (f1 ^ <*c<sub>12</sub>*>)) ^ <*k1*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
((Ant (f1 ^ <*c<sub>12</sub>*>)) ^ <*k1*>) ^ <*(Suc (f1 ^ <*c<sub>12</sub>*>))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(((Ant (f1 ^ <*c<sub>12</sub>*>)) ^ <*k1*>) ^ <*(Suc (f1 ^ <*c<sub>12</sub>*>))*>) ^ <*('not' (VERUM Al))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(f1 ^ <*k1*>) ^ <*(Suc (f1 ^ <*c<sub>12</sub>*>))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
((f1 ^ <*k1*>) ^ <*(Suc (f1 ^ <*c<sub>12</sub>*>))*>) ^ <*('not' (VERUM Al))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(f1 ^ <*k1*>) ^ <*c<sub>12</sub>*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
((f1 ^ <*k1*>) ^ <*c<sub>12</sub>*>) ^ <*('not' (VERUM Al))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(f1 ^ <*k1*>) ^ <*('not' (VERUM Al))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
k1 is Element of CQC-WFF Al
{k1} is finite countable Element of bool (CQC-WFF Al)
X \/ {k1} is Element of bool (CQC-WFF Al)
(Al,(X \/ {k1})) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in X \/ {k1} } is set
union { (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in X \/ {k1} } is set
still_not-bound_in k1 is Element of bool (bound_QC-variables Al)
(Al,{k1}) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in {k1} } is set
union { (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in {k1} } is set
(Al,{k1}) \/ (Al,X) is Element of bool (bound_QC-variables Al)
r1 is Element of bound_QC-variables Al
L is Element of QC-symbols Al
x. L is Element of bound_QC-variables Al
{ b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in (Al,(X \/ {k1})) } is set
s is set
p1 is non empty set
y is Element of QC-symbols Al
x. y is Element of bound_QC-variables Al
bool (QC-symbols Al) is non empty set
s is non empty Element of bool (QC-symbols Al)
Al -one_in s is Element of QC-symbols Al
the Element of s is Element of s
u is Element of QC-symbols Al
x. u is Element of bound_QC-variables Al
(Al,X) \/ (Al,{k1}) is Element of bool (bound_QC-variables Al)
X \/ { ((v . b<sub>1</sub>) `1) where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT : b₁ in 0 } is set
r2 is set
y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
v . y2 is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
(v . y2) `1 is set
(Al,(rng f1)) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in rng f1 } is set
union { (still_not-bound_in b<sub>1</sub>) where b<sub>1</sub> is Element of CQC-WFF Al : b<sub>1</sub> in rng f1 } is set
x. (Al -one_in s) is Element of bound_QC-variables Al
still_not-bound_in f1 is Element of bool (bound_QC-variables Al)
r1 is Element of bound_QC-variables Al
y1 is Element of CQC-WFF Al
Ex (r1,y1) is Element of CQC-WFF Al
(Al,k1) is Element of CQC-WFF Al
r2 is Element of CQC-WFF Al
(Al,k1) is Element of bound_QC-variables Al
y2 is Element of bound_QC-variables Al
<*k1*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
still_not-bound_in <*k1*> is Element of bool (bound_QC-variables Al)
(still_not-bound_in f1) \/ (still_not-bound_in <*k1*>) is Element of bool (bound_QC-variables Al)
f1 ^ <*k1*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
still_not-bound_in (f1 ^ <*k1*>) is Element of bool (bound_QC-variables Al)
still_not-bound_in (VERUM Al) is Element of bool (bound_QC-variables Al)
still_not-bound_in ('not' (VERUM Al)) is Element of bool (bound_QC-variables Al)
still_not-bound_in <*('not' (VERUM Al))*> is Element of bool (bound_QC-variables Al)
(still_not-bound_in (f1 ^ <*k1*>)) \/ (still_not-bound_in <*('not' (VERUM Al))*>) is Element of bool (bound_QC-variables Al)
(f1 ^ <*k1*>) ^ <*('not' (VERUM Al))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
still_not-bound_in ((f1 ^ <*k1*>) ^ <*('not' (VERUM Al))*>) is Element of bool (bound_QC-variables Al)
f1 ^ <*('not' (VERUM Al))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
k1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() set
k1 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
k1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
v . k1 is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
(v . k1) `2 is set
k1 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Y . (k1 + 1) is Element of CQC-WFF Al
{(Y . (k1 + 1))} is finite countable Element of bool (CQC-WFF Al)
(Al,{(Y . (k1 + 1))}) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {(Y . (k1 + 1))} } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {(Y . (k1 + 1))} } is set
v . (k1 + 1) is Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
'not' (Y . (k1 + 1)) is Element of CQC-WFF Al
(Al,Y,(k1 + 1)) is Element of CQC-WFF Al
(Al,Y,(k1 + 1)) is Element of bound_QC-variables Al
((v . k1) `2) \/ (Al,{(Y . (k1 + 1))}) is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in ((v . k1) `2) \/ (Al,{(Y . (k1 + 1))}) } is set
Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in ((v . k1) `2) \/ (Al,{(Y . (k1 + 1))}) } is Element of QC-symbols Al
x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in ((v . k1) `2) \/ (Al,{(Y . (k1 + 1))}) } ) is Element of bound_QC-variables Al
(Al,Y,(k1 + 1)) . ((Al,Y,(k1 + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in ((v . k1) `2) \/ (Al,{(Y . (k1 + 1))}) } ))) is Element of CQC-WFF Al
('not' (Y . (k1 + 1))) 'or' ((Al,Y,(k1 + 1)) . ((Al,Y,(k1 + 1)),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in ((v . k1) `2) \/ (Al,{(Y . (k1 + 1))}) } )))) is Element of CQC-WFF Al
s is Element of bool (bound_QC-variables Al)
y is Element of bool (bound_QC-variables Al)
s \/ (Al,{(Y . (k1 + 1))}) is Element of bool (bound_QC-variables Al)
{ b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in y } is set
Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in y } is Element of QC-symbols Al
x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in y } ) is Element of bound_QC-variables Al
(Al,Y,(k1 + 1)) . ((Al,Y,(k1 + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in y } ))) is Element of CQC-WFF Al
('not' (Y . (k1 + 1))) 'or' ((Al,Y,(k1 + 1)) . ((Al,Y,(k1 + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in y } )))) is Element of CQC-WFF Al
still_not-bound_in (('not' (Y . (k1 + 1))) 'or' ((Al,Y,(k1 + 1)) . ((Al,Y,(k1 + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in y } ))))) is Element of bool (bound_QC-variables Al)
s \/ (still_not-bound_in (('not' (Y . (k1 + 1))) 'or' ((Al,Y,(k1 + 1)) . ((Al,Y,(k1 + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in y } )))))) is Element of bool (bound_QC-variables Al)
[(('not' (Y . (k1 + 1))) 'or' ((Al,Y,(k1 + 1)) . ((Al,Y,(k1 + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in y } ))))),(s \/ (still_not-bound_in (('not' (Y . (k1 + 1))) 'or' ((Al,Y,(k1 + 1)) . ((Al,Y,(k1 + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in y } )))))))] is V7() Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]
{(('not' (Y . (k1 + 1))) 'or' ((Al,Y,(k1 + 1)) . ((Al,Y,(k1 + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in y } ))))),(s \/ (still_not-bound_in (('not' (Y . (k1 + 1))) 'or' ((Al,Y,(k1 + 1)) . ((Al,Y,(k1 + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in y } )))))))} is finite countable set
{(('not' (Y . (k1 + 1))) 'or' ((Al,Y,(k1 + 1)) . ((Al,Y,(k1 + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in y } )))))} is finite countable set
{{(('not' (Y . (k1 + 1))) 'or' ((Al,Y,(k1 + 1)) . ((Al,Y,(k1 + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in y } ))))),(s \/ (still_not-bound_in (('not' (Y . (k1 + 1))) 'or' ((Al,Y,(k1 + 1)) . ((Al,Y,(k1 + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in y } )))))))},{(('not' (Y . (k1 + 1))) 'or' ((Al,Y,(k1 + 1)) . ((Al,Y,(k1 + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in y } )))))}} is finite V42() countable set
<*('not' (Y . (k1 + 1)))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
f1 ^ <*('not' (Y . (k1 + 1)))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
<*(('not' (Y . (k1 + 1))) 'or' ((Al,Y,(k1 + 1)) . ((Al,Y,(k1 + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in ((v . k1) `2) \/ (Al,{(Y . (k1 + 1))}) } )))))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(f1 ^ <*('not' (Y . (k1 + 1)))*>) ^ <*(('not' (Y . (k1 + 1))) 'or' ((Al,Y,(k1 + 1)) . ((Al,Y,(k1 + 1)),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in ((v . k1) `2) \/ (Al,{(Y . (k1 + 1))}) } )))))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(Ant (f1 ^ <*c₁₂*>)) ^ <*('not' (Y . (k1 + 1)))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
((Ant (f1 ^ <*c₁₂*>)) ^ <*('not' (Y . (k1 + 1)))*>) ^ <*(Suc (f1 ^ <*c₁₂*>))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(((Ant (f1 ^ <*c₁₂*>)) ^ <*('not' (Y . (k1 + 1)))*>) ^ <*(Suc (f1 ^ <*c₁₂*>))*>) ^ <*('not' (VERUM Al))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(f1 ^ <*('not' (Y . (k1 + 1)))*>) ^ <*(Suc (f1 ^ <*c₁₂*>))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
((f1 ^ <*('not' (Y . (k1 + 1)))*>) ^ <*(Suc (f1 ^ <*c₁₂*>))*>) ^ <*('not' (VERUM Al))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(f1 ^ <*('not' (Y . (k1 + 1)))*>) ^ <*c₁₂*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
((f1 ^ <*('not' (Y . (k1 + 1)))*>) ^ <*c₁₂*>) ^ <*('not' (VERUM Al))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(f1 ^ <*('not' (Y . (k1 + 1)))*>) ^ <*('not' (VERUM Al))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
s is Element of CQC-WFF Al
<*s*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
f1 ^ <*s*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(f1 ^ <*s*>) ^ <*s*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(f1 ^ <*s*>) ^ <*(('not' (Y . (k1 + 1))) 'or' ((Al,Y,(k1 + 1)) . ((Al,Y,(k1 + 1)),(x. (Al -one_in { b₁ where b₁ is Element of QC-symbols Al : not x. b₁ in ((v . k1) `2) \/ (Al,{(Y . (k1 + 1))}) } )))))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(Ant (f1 ^ <*c<sub>12</sub>*>)) ^ <*s*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
((Ant (f1 ^ <*c<sub>12</sub>*>)) ^ <*s*>) ^ <*(Suc (f1 ^ <*c<sub>12</sub>*>))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(((Ant (f1 ^ <*c<sub>12</sub>*>)) ^ <*s*>) ^ <*(Suc (f1 ^ <*c<sub>12</sub>*>))*>) ^ <*('not' (VERUM Al))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(f1 ^ <*s*>) ^ <*(Suc (f1 ^ <*c<sub>12</sub>*>))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
((f1 ^ <*s*>) ^ <*(Suc (f1 ^ <*c<sub>12</sub>*>))*>) ^ <*('not' (VERUM Al))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
((f1 ^ <*s*>) ^ <*(('not' (Y . (k1 + 1))) 'or' ((Al,Y,(k1 + 1)) . ((Al,Y,(k1 + 1)),(x. (Al -one_in { b<sub>1</sub> where b<sub>1</sub> is Element of QC-symbols Al : not x. b<sub>1</sub> in ((v . k1) `2) \/ (Al,{(Y . (k1 + 1))}) } )))))*>) ^ <*('not' (VERUM Al))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
(f1 ^ <*s*>) ^ <*('not' (VERUM Al))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
r1 is Element of CQC-WFF Al
y1 is Element of bound_QC-variables Al
s1 is Element of CQC-WFF Al
Ex (y1,s1) is Element of CQC-WFF Al
(Al,r1) is Element of CQC-WFF Al
r2 is Element of CQC-WFF Al
(Al,r1) is Element of bound_QC-variables Al
y2 is Element of bound_QC-variables Al
Z is Element of bool (CQC-WFF Al)
{r1} is finite countable Element of bool (CQC-WFF Al)
Z \/ {r1} is Element of bool (CQC-WFF Al)
(Al,(Z \/ {r1})) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in Z \/ {r1} } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in Z \/ {r1} } is set
(Al,Z) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in Z } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in Z } is set
(Al,{r1}) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {r1} } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {r1} } is set
(Al,Z) \/ (Al,{r1}) is Element of bool (bound_QC-variables Al)
still_not-bound_in r1 is Element of bool (bound_QC-variables Al)
<*r1*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
still_not-bound_in <*r1*> is Element of bool (bound_QC-variables Al)
(still_not-bound_in f1) \/ (still_not-bound_in <*r1*>) is Element of bool (bound_QC-variables Al)
f1 ^ <*r1*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
still_not-bound_in (f1 ^ <*r1*>) is Element of bool (bound_QC-variables Al)
(still_not-bound_in (f1 ^ <*r1*>)) \/ (still_not-bound_in <*('not' (VERUM Al))*>) is Element of bool (bound_QC-variables Al)
(f1 ^ <*r1*>) ^ <*('not' (VERUM Al))*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
still_not-bound_in ((f1 ^ <*r1*>) ^ <*('not' (VERUM Al))*>) is Element of bool (bound_QC-variables Al)
dom p is countable Element of bool NAT
c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
p . y is Element of bool (CQC-WFF Al)
p . c₁₂ is Element of bool (CQC-WFF Al)
y is Consistent Element of bool (CQC-WFF Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
X is Element of bool (CQC-WFF Al)
p is Element of bool (CQC-WFF Al)
Y is Element of CQC-WFF Al
<*Y*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite V45(1) FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
J is Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
rng J is finite countable Element of bool (CQC-WFF Al)
J ^ <*Y*> is non empty Relation-like NAT -defined CQC-WFF Al -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of CQC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
X is Consistent Element of bool (CQC-WFF Al)
p is Relation-like Function-like set
dom p is set
rng p is set
[:NAT,(CQC-WFF Al):] is non empty Relation-like set
bool [:NAT,(CQC-WFF Al):] is non empty set
Y is Relation-like NAT -defined CQC-WFF Al -valued Function-like V32( NAT , CQC-WFF Al) Element of bool [:NAT,(CQC-WFF Al):]
J is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
Y . J is set
{(Y . J)} is finite countable set
Y . J is Element of CQC-WFF Al
CY is Element of bool (CQC-WFF Al)
CY \/ {(Y . J)} is set
v is Element of CQC-WFF Al
{v} is finite countable Element of bool (CQC-WFF Al)
CY \/ {v} is Element of bool (CQC-WFF Al)
c₉ is Element of bool (CQC-WFF Al)
p is Element of bool (CQC-WFF Al)
y is Element of bool (CQC-WFF Al)
[:NAT,(bool (CQC-WFF Al)):] is non empty Relation-like set
bool [:NAT,(bool (CQC-WFF Al)):] is non empty set
J is Relation-like NAT -defined bool (CQC-WFF Al) -valued Function-like V32( NAT , bool (CQC-WFF Al)) Element of bool [:NAT,(bool (CQC-WFF Al)):]
J . 0 is Element of bool (CQC-WFF Al)
rng J is Element of bool (bool (CQC-WFF Al))
bool (bool (CQC-WFF Al)) is non empty set
union (rng J) is set
CY is set
dom J is countable Element of bool NAT
CY is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
J . CY is Element of bool (CQC-WFF Al)
CY + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
J . (CY + 1) is Element of bool (CQC-WFF Al)
CY is set
Y . CY is Element of CQC-WFF Al
c₉ is Element of CQC-WFF Al
{c₉} is finite countable Element of bool (CQC-WFF Al)
(J . CY) \/ {c₉} is Element of bool (CQC-WFF Al)
y is Element of bool (CQC-WFF Al)
{(Y . CY)} is finite countable Element of bool (CQC-WFF Al)
(J . CY) \/ {(Y . CY)} is Element of bool (CQC-WFF Al)
c₁₂ is Element of bool (CQC-WFF Al)
CY is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
J . CY is Element of bool (CQC-WFF Al)
CY is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
J . CY is Element of bool (CQC-WFF Al)
c₉ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
J . c₉ is Element of bool (CQC-WFF Al)
c₉ + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
J . (c₉ + 1) is Element of bool (CQC-WFF Al)
CY is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
J . CY is Element of bool (CQC-WFF Al)
CY + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
J . (CY + 1) is Element of bool (CQC-WFF Al)
Y . CY is Element of CQC-WFF Al
{(Y . CY)} is finite countable Element of bool (CQC-WFF Al)
(J . CY) \/ {(Y . CY)} is Element of bool (CQC-WFF Al)
CY is Element of bool (CQC-WFF Al)
c₉ is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
CY is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
J . CY is Element of bool (CQC-WFF Al)
J . c₉ is Element of bool (CQC-WFF Al)
CY is Consistent Element of bool (CQC-WFF Al)
c₉ is Element of CQC-WFF Al
'not' c₉ is Element of CQC-WFF Al
dom Y is countable Element of bool NAT
p is set
Y . p is set
{c₉} is finite countable Element of bool (CQC-WFF Al)
CY \/ {c₉} is Element of bool (CQC-WFF Al)
y is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
J . y is Element of bool (CQC-WFF Al)
(J . y) \/ {c₉} is Element of bool (CQC-WFF Al)
VERUM Al is Element of CQC-WFF Al
'not' (VERUM Al) is Element of CQC-WFF Al
c₁₂ is set
Y . y is Element of CQC-WFF Al
{(Y . y)} is finite countable Element of bool (CQC-WFF Al)
(J . y) \/ {(Y . y)} is Element of bool (CQC-WFF Al)
y + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() Element of NAT
J . (y + 1) is Element of bool (CQC-WFF Al)
c₁₂ is set
c₁₂ is Element of bool (CQC-WFF Al)
QC-variables Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
bool (QC-variables Al) is non empty set
c₉ is Element of bound_QC-variables Al
p is Element of CQC-WFF Al
Ex (c₉,p) is Element of CQC-WFF Al
'not' (Ex (c₉,p)) is Element of CQC-WFF Al
y is Element of bound_QC-variables Al
p . (c₉,y) is Element of CQC-WFF Al
('not' (Ex (c₉,p))) 'or' (p . (c₉,y)) is Element of CQC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-pred_symbols Al is set
HCar Al is non empty set
K354((HCar Al)) is set
valH Al is Relation-like bound_QC-variables Al -defined HCar Al -valued Function-like V32( bound_QC-variables Al, HCar Al) Element of Valuations_in (Al,(HCar Al))
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
Valuations_in (Al,(HCar Al)) is non empty M5( bound_QC-variables Al, HCar Al)
X is Consistent Element of bool (CQC-WFF Al)
(Al,X) is Element of bool (bound_QC-variables Al)
bool (bound_QC-variables Al) is non empty set
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X } is set
p is Consistent Element of bool (CQC-WFF Al)
Y is Consistent Element of bool (CQC-WFF Al)
the Relation-like QC-pred_symbols Al -defined K354((HCar Al)) -valued Function-like V32( QC-pred_symbols Al,K354((HCar Al))) Henkin_interpretation of Y is Relation-like QC-pred_symbols Al -defined K354((HCar Al)) -valued Function-like V32( QC-pred_symbols Al,K354((HCar Al))) Henkin_interpretation of Y
v is Element of CQC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-pred_symbols Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
X is Element of bool (CQC-WFF Al)
p is Element of bool (CQC-WFF Al)
Y is non empty set
K354(Y) is set
Valuations_in (Al,Y) is non empty M5( bound_QC-variables Al,Y)
J is Relation-like QC-pred_symbols Al -defined K354(Y) -valued Function-like V32( QC-pred_symbols Al,K354(Y)) interpretation of Al,Y
v is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
CY is Element of CQC-WFF Al
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
X is Element of bool (CQC-WFF Al)
(Al,X) is Element of bool (bound_QC-variables Al)
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
bool (bound_QC-variables Al) is non empty set
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X } is set
p is Element of CQC-WFF Al
{p} is finite countable Element of bool (CQC-WFF Al)
X \/ {p} is Element of bool (CQC-WFF Al)
(Al,(X \/ {p})) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X \/ {p} } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X \/ {p} } is set
still_not-bound_in p is Element of bool (bound_QC-variables Al)
(Al,{p}) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {p} } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in {p} } is set
(Al,X) \/ (Al,{p}) is Element of bool (bound_QC-variables Al)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
QC-pred_symbols Al is set
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
X is Element of bool (CQC-WFF Al)
p is Element of CQC-WFF Al
'not' p is Element of CQC-WFF Al
{('not' p)} is finite countable Element of bool (CQC-WFF Al)
X \/ {('not' p)} is Element of bool (CQC-WFF Al)
Y is non empty set
K354(Y) is set
Valuations_in (Al,Y) is non empty M5( bound_QC-variables Al,Y)
J is Relation-like QC-pred_symbols Al -defined K354(Y) -valued Function-like V32( QC-pred_symbols Al,K354(Y)) interpretation of Al,Y
v is Relation-like bound_QC-variables Al -defined Y -valued Function-like V32( bound_QC-variables Al,Y) Element of Valuations_in (Al,Y)
Al is QC-alphabet
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
bool (CQC-WFF Al) is non empty set
X is Element of bool (CQC-WFF Al)
(Al,X) is Element of bool (bound_QC-variables Al)
bound_QC-variables Al is Element of bool (QC-variables Al)
QC-variables Al is set
bool (QC-variables Al) is non empty set
bool (bound_QC-variables Al) is non empty set
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in X } is set
p is Element of CQC-WFF Al
'not' p is Element of CQC-WFF Al
{('not' p)} is finite countable Element of bool (CQC-WFF Al)
X \/ {('not' p)} is Element of bool (CQC-WFF Al)
Y is Element of bool (CQC-WFF Al)
(Al,Y) is Element of bool (bound_QC-variables Al)
{ (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in Y } is set
union { (still_not-bound_in b₁) where b₁ is Element of CQC-WFF Al : b₁ in Y } is set
QC-pred_symbols Al is set
HCar Al is non empty set
K354((HCar Al)) is set
valH Al is Relation-like bound_QC-variables Al -defined HCar Al -valued Function-like V32( bound_QC-variables Al, HCar Al) Element of Valuations_in (Al,(HCar Al))
Valuations_in (Al,(HCar Al)) is non empty M5( bound_QC-variables Al, HCar Al)
J is Consistent Element of bool (CQC-WFF Al)
v is Relation-like QC-pred_symbols Al -defined K354((HCar Al)) -valued Function-like V32( QC-pred_symbols Al,K354((HCar Al))) Henkin_interpretation of J