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