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