let A be QC-alphabet ; ( [:(QC-WFF A),(vSUB A):] is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for k being Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):] ) & ( for e being Element of vSUB A holds [<*[0,0]*>,e] in [:(QC-WFF A),(vSUB A):] ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] holds
[(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):] ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] holds
[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] ) )
QC-WFF A is A -closed
by QC_LANG1:7;
then
QC-WFF A is Subset of ([:NAT,(QC-symbols A):] *)
;
hence
[:(QC-WFF A),(vSUB A):] is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):]
by ZFMISC_1:95; ( ( for k being Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):] ) & ( for e being Element of vSUB A holds [<*[0,0]*>,e] in [:(QC-WFF A),(vSUB A):] ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] holds
[(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):] ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] holds
[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] ) )
thus
for k being Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):]
( ( for e being Element of vSUB A holds [<*[0,0]*>,e] in [:(QC-WFF A),(vSUB A):] ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] holds
[(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):] ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] holds
[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] ) )proof
let k be
Nat;
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):]let p be
QC-pred_symbol of
k,
A;
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):]let ll be
QC-variable_list of
k,
A;
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):]let e be
Element of
vSUB A;
[(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):]
p ! ll = <*p*> ^ ll
by QC_LANG1:8;
hence
[(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):]
by ZFMISC_1:def 2;
verum
end;
VERUM A in QC-WFF A
;
hence
for e being Element of vSUB A holds [<*[0,0]*>,e] in [:(QC-WFF A),(vSUB A):]
by ZFMISC_1:def 2; ( ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] holds
[(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):] ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] holds
[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] ) )
thus
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] holds
[(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):]
( ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] holds
[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] ) )proof
let p be
FinSequence of
[:NAT,(QC-symbols A):];
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] holds
[(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):]let e be
Element of
vSUB A;
( [p,e] in [:(QC-WFF A),(vSUB A):] implies [(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):] )
assume
[p,e] in [:(QC-WFF A),(vSUB A):]
;
[(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):]
then
ex
a,
b being
object st
(
a in QC-WFF A &
b in vSUB A &
[p,e] = [a,b] )
by ZFMISC_1:def 2;
then reconsider p9 =
p as
Element of
QC-WFF A by XTUPLE_0:1;
'not' p9 = <*[1,0]*> ^ (@ p9)
;
hence
[(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):]
by ZFMISC_1:def 2;
verum
end;
thus
for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] holds
[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):]
for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):]proof
let p,
q be
FinSequence of
[:NAT,(QC-symbols A):];
for e being Element of vSUB A st [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] holds
[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):]let e be
Element of
vSUB A;
( [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] implies [((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] )
assume that A1:
[p,e] in [:(QC-WFF A),(vSUB A):]
and A2:
[q,e] in [:(QC-WFF A),(vSUB A):]
;
[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):]
ex
c,
d being
object st
(
c in QC-WFF A &
d in vSUB A &
[q,e] = [c,d] )
by A2, ZFMISC_1:def 2;
then reconsider q9 =
q as
Element of
QC-WFF A by XTUPLE_0:1;
ex
a,
b being
object st
(
a in QC-WFF A &
b in vSUB A &
[p,e] = [a,b] )
by A1, ZFMISC_1:def 2;
then reconsider p9 =
p as
Element of
QC-WFF A by XTUPLE_0:1;
p9 '&' q9 = (<*[2,0]*> ^ (@ p9)) ^ (@ q9)
;
hence
[((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):]
by ZFMISC_1:def 2;
verum
end;
thus
for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):]
verumproof
let x be
bound_QC-variable of
A;
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):]let p be
FinSequence of
[:NAT,(QC-symbols A):];
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):]let e be
Element of
vSUB A;
( [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] implies [((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] )
assume
[p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):]
;
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):]
then
ex
a,
b being
object st
(
a in QC-WFF A &
b in vSUB A &
[p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] = [a,b] )
by ZFMISC_1:def 2;
then reconsider p9 =
p as
Element of
QC-WFF A by XTUPLE_0:1;
All (
x,
p9)
= (<*[3,0]*> ^ <*x*>) ^ (@ p9)
;
hence
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):]
by ZFMISC_1:def 2;
verum
end;