set X = { S where S is Element of QC-Sub-WFF F1() : P1[S] } ;
not { S where S is Element of QC-Sub-WFF F1() : P1[S] } is empty
then reconsider X = { S where S is Element of QC-Sub-WFF F1() : P1[S] } as non empty set ;
for e being Element of vSUB F1() holds [(VERUM F1()),e] in X
then A6:
for e being Element of vSUB F1() holds [<*[0,0]*>,e] in X
;
A7:
for p being FinSequence of [:NAT,(QC-symbols F1()):]
for e being Element of vSUB F1() st [p,e] in X holds
[(<*[1,0]*> ^ p),e] in X
proof
let p be
FinSequence of
[:NAT,(QC-symbols F1()):];
for e being Element of vSUB F1() st [p,e] in X holds
[(<*[1,0]*> ^ p),e] in Xlet e be
Element of
vSUB F1();
( [p,e] in X implies [(<*[1,0]*> ^ p),e] in X )
assume
[p,e] in X
;
[(<*[1,0]*> ^ p),e] in X
then consider S being
Element of
QC-Sub-WFF F1()
such that A8:
S = [p,e]
and A9:
P1[
S]
;
P1[
Sub_not S]
by A3, A9;
then
Sub_not S in X
;
hence
[(<*[1,0]*> ^ p),e] in X
by A8;
verum
end;
A10:
for x being bound_QC-variable of F1()
for p being FinSequence of [:NAT,(QC-symbols F1()):]
for e being Element of vSUB F1() st [p,((QSub F1()) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in X holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in X
proof
let x be
bound_QC-variable of
F1();
for p being FinSequence of [:NAT,(QC-symbols F1()):]
for e being Element of vSUB F1() st [p,((QSub F1()) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in X holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in Xlet p be
FinSequence of
[:NAT,(QC-symbols F1()):];
for e being Element of vSUB F1() st [p,((QSub F1()) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in X holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in Xlet e be
Element of
vSUB F1();
( [p,((QSub F1()) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in X implies [((<*[3,0]*> ^ <*x*>) ^ p),e] in X )
assume
[p,((QSub F1()) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in X
;
[((<*[3,0]*> ^ <*x*>) ^ p),e] in X
then consider S being
Element of
QC-Sub-WFF F1()
such that A11:
S = [p,((QSub F1()) . [((<*[3,0]*> ^ <*x*>) ^ p),e])]
and A12:
P1[
S]
;
consider B being
set such that A13:
B = [S,x]
;
reconsider B =
B as
Element of
[:(QC-Sub-WFF F1()),(bound_QC-variables F1()):] by A13;
A14:
(
B `1 = S &
B `2 = x )
by A13;
A15:
S `2 = (QSub F1()) . [(All (x,(S `1))),e]
by A11;
then A16:
B is
quantifiable
by A14;
then reconsider e =
e as
second_Q_comp of
B by A15, A14, Def23;
P1[
Sub_All (
B,
e)]
by A5, A12, A13, A16;
then
Sub_All (
B,
e)
in X
;
then
[(All ((B `2),((B `1) `1))),e] in X
by A16, Def24;
hence
[((<*[3,0]*> ^ <*x*>) ^ p),e] in X
by A11, A14;
verum
end;
let F be Element of QC-Sub-WFF F1(); P1[F]
A17:
X c= [:([:NAT,(QC-symbols F1()):] *),(vSUB F1()):]
proof
let x be
object ;
TARSKI:def 3 ( not x in X or x in [:([:NAT,(QC-symbols F1()):] *),(vSUB F1()):] )
assume
x in X
;
x in [:([:NAT,(QC-symbols F1()):] *),(vSUB F1()):]
then
ex
S being
Element of
QC-Sub-WFF F1() st
(
x = S &
P1[
S] )
;
then consider p being
Element of
QC-WFF F1(),
e being
Element of
vSUB F1()
such that A18:
x = [p,e]
by Th8;
p = @ p
;
then
p in [:NAT,(QC-symbols F1()):] *
by FINSEQ_1:def 11;
hence
x in [:([:NAT,(QC-symbols F1()):] *),(vSUB F1()):]
by A18, ZFMISC_1:def 2;
verum
end;
A19:
for p, q being FinSequence of [:NAT,(QC-symbols F1()):]
for e being Element of vSUB F1() st [p,e] in X & [q,e] in X holds
[((<*[2,0]*> ^ p) ^ q),e] in X
proof
let p,
q be
FinSequence of
[:NAT,(QC-symbols F1()):];
for e being Element of vSUB F1() st [p,e] in X & [q,e] in X holds
[((<*[2,0]*> ^ p) ^ q),e] in Xlet e be
Element of
vSUB F1();
( [p,e] in X & [q,e] in X implies [((<*[2,0]*> ^ p) ^ q),e] in X )
assume
[p,e] in X
;
( not [q,e] in X or [((<*[2,0]*> ^ p) ^ q),e] in X )
then consider S1 being
Element of
QC-Sub-WFF F1()
such that A20:
S1 = [p,e]
and A21:
P1[
S1]
;
assume
[q,e] in X
;
[((<*[2,0]*> ^ p) ^ q),e] in X
then consider S2 being
Element of
QC-Sub-WFF F1()
such that A22:
S2 = [q,e]
and A23:
P1[
S2]
;
consider p9 being
Element of
QC-WFF F1(),
e1 being
Element of
vSUB F1()
such that A24:
[p,e] = [p9,e1]
by A20, Th8;
A25:
e = e1
by A24, XTUPLE_0:1;
then A26:
S1 `2 = e1
by A20;
then A27:
S1 `2 = S2 `2
by A22, A25;
then
P1[
Sub_& (
S1,
S2)]
by A4, A21, A23;
then
Sub_& (
S1,
S2)
in X
;
then A28:
[((S1 `1) '&' (S2 `1)),(S1 `2)] in X
by A27, Def21;
A29:
p = p9
by A24, XTUPLE_0:1;
then
S1 `1 = p9
by A20;
hence
[((<*[2,0]*> ^ p) ^ q),e] in X
by A22, A29, A25, A26, A28;
verum
end;
for k being Nat
for P being QC-pred_symbol of k,F1()
for ll being QC-variable_list of k,F1()
for e being Element of vSUB F1() holds [(<*P*> ^ ll),e] in X
proof
let k be
Nat;
for P being QC-pred_symbol of k,F1()
for ll being QC-variable_list of k,F1()
for e being Element of vSUB F1() holds [(<*P*> ^ ll),e] in Xlet P be
QC-pred_symbol of
k,
F1();
for ll being QC-variable_list of k,F1()
for e being Element of vSUB F1() holds [(<*P*> ^ ll),e] in Xlet ll be
QC-variable_list of
k,
F1();
for e being Element of vSUB F1() holds [(<*P*> ^ ll),e] in Xlet e be
Element of
vSUB F1();
[(<*P*> ^ ll),e] in X
(
P1[
Sub_P (
P,
ll,
e)] &
[(P ! ll),e] = Sub_P (
P,
ll,
e) )
by A1, Th9;
then
[(P ! ll),e] in X
;
hence
[(<*P*> ^ ll),e] in X
by QC_LANG1:8;
verum
end;
then
X is F1() -Sub-closed
by A17, A6, A7, A19, A10;
then
QC-Sub-WFF F1() c= X
by Def17;
then
F in X
;
then
ex S being Element of QC-Sub-WFF F1() st
( S = F & P1[S] )
;
hence
P1[F]
; verum