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