defpred S1[ Element of QC-Sub-WFF ] means ( $1 is Element of CQC-Sub-WFF implies P1[$1] );
A2:
for S being Element of QC-Sub-WFF st S1[S] holds
S1[ Sub_not S]
A6:
for k being Element of NAT
for P being QC-pred_symbol of k
for ll being QC-variable_list of k
for e being Element of vSUB holds S1[ Sub_P P,ll,e]
proof
let k be
Element of
NAT ;
for P being QC-pred_symbol of k
for ll being QC-variable_list of k
for e being Element of vSUB holds S1[ Sub_P P,ll,e]let P be
QC-pred_symbol of
k;
for ll being QC-variable_list of k
for e being Element of vSUB holds S1[ Sub_P P,ll,e]let ll be
QC-variable_list of
k;
for e being Element of vSUB holds S1[ Sub_P P,ll,e]let e be
Element of
vSUB ;
S1[ Sub_P P,ll,e]
assume
Sub_P P,
ll,
e is
Element of
CQC-Sub-WFF
;
P1[ Sub_P P,ll,e]
then
Sub_P P,
ll,
e in CQC-Sub-WFF
;
then A7:
ex
S1 being
Element of
QC-Sub-WFF st
(
Sub_P P,
ll,
e = S1 &
S1 `1 is
Element of
CQC-WFF )
;
Sub_P P,
ll,
e = [(P ! ll),e]
by Th9;
then A8:
P ! ll is
Element of
CQC-WFF
by A7, MCART_1:7;
then A9:
{ (ll . j) where j is Element of NAT : ( 1 <= j & j <= len ll & ll . j in fixed_QC-variables ) } = {}
by CQC_LANG:17;
{ (ll . i) where i is Element of NAT : ( 1 <= i & i <= len ll & ll . i in free_QC-variables ) } = {}
by A8, CQC_LANG:17;
then
ll is
CQC-variable_list of
k
by A9, CQC_LANG:15;
hence
P1[
Sub_P P,
ll,
e]
by A1;
verum
end;
A10:
for S1, S2 being Element of QC-Sub-WFF st S1 `2 = S2 `2 & S1[S1] & S1[S2] holds
S1[ Sub_& S1,S2]
proof
let S1,
S2 be
Element of
QC-Sub-WFF ;
( S1 `2 = S2 `2 & S1[S1] & S1[S2] implies S1[ Sub_& S1,S2] )
assume that A11:
S1 `2 = S2 `2
and A12:
(
S1[
S1] &
S1[
S2] )
;
S1[ Sub_& S1,S2]
assume
Sub_& S1,
S2 is
Element of
CQC-Sub-WFF
;
P1[ Sub_& S1,S2]
then
Sub_& S1,
S2 in CQC-Sub-WFF
;
then consider S9 being
Element of
QC-Sub-WFF such that A13:
Sub_& S1,
S2 = S9
and A14:
S9 `1 is
Element of
CQC-WFF
;
Sub_& S1,
S2 = [((S1 `1 ) '&' (S2 `1 )),(S1 `2 )]
by A11, Def21;
then A15:
S9 `1 = (S1 `1 ) '&' (S2 `1 )
by A13, MCART_1:7;
then
S2 `1 is
Element of
CQC-WFF
by A14, CQC_LANG:19;
then A16:
S2 in CQC-Sub-WFF
;
S1 `1 is
Element of
CQC-WFF
by A14, A15, CQC_LANG:19;
then
S1 in CQC-Sub-WFF
;
hence
P1[
Sub_& S1,
S2]
by A1, A11, A12, A16;
verum
end;
A17:
for x being bound_QC-variable
for S being Element of QC-Sub-WFF
for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & S1[S] holds
S1[ Sub_All [S,x],SQ]
proof
let x be
bound_QC-variable;
for S being Element of QC-Sub-WFF
for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & S1[S] holds
S1[ Sub_All [S,x],SQ]let S be
Element of
QC-Sub-WFF ;
for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & S1[S] holds
S1[ Sub_All [S,x],SQ]let SQ be
second_Q_comp of
[S,x];
( [S,x] is quantifiable & S1[S] implies S1[ Sub_All [S,x],SQ] )
assume that A18:
[S,x] is
quantifiable
and A19:
S1[
S]
;
S1[ Sub_All [S,x],SQ]
assume
Sub_All [S,x],
SQ is
Element of
CQC-Sub-WFF
;
P1[ Sub_All [S,x],SQ]
then
Sub_All [S,x],
SQ in CQC-Sub-WFF
;
then consider S9 being
Element of
QC-Sub-WFF such that A20:
Sub_All [S,x],
SQ = S9
and A21:
S9 `1 is
Element of
CQC-WFF
;
A22:
[S,x] `1 = S
by MCART_1:7;
Sub_All [S,x],
SQ = [(All ([S,x] `2 ),(([S,x] `1 ) `1 )),SQ]
by A18, Def24;
then
S9 `1 = All ([S,x] `2 ),
(([S,x] `1 ) `1 )
by A20, MCART_1:7;
then
([S,x] `1 ) `1 is
Element of
CQC-WFF
by A21, CQC_LANG:23;
then
S in CQC-Sub-WFF
by A22;
hence
P1[
Sub_All [S,x],
SQ]
by A1, A18, A19;
verum
end;
A23:
for S being Element of QC-Sub-WFF st S is Sub_VERUM holds
S1[S]
by A1;
for S being Element of QC-Sub-WFF holds S1[S]
from SUBSTUT1:sch 1(A6, A23, A2, A10, A17);
hence
for S being Element of CQC-Sub-WFF holds P1[S]
; verum