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