defpred S1[ Element of QC-Sub-WFF F1()] means F3() . $1 = F4() . $1;
A3:
for k being Nat
for P being QC-pred_symbol of k,F1()
for l being QC-variable_list of k,F1()
for e being Element of vSUB F1() holds S1[ Sub_P (P,l,e)]
proof
let k be
Nat;
for P being QC-pred_symbol of k,F1()
for l being QC-variable_list of k,F1()
for e being Element of vSUB F1() holds S1[ Sub_P (P,l,e)]let P be
QC-pred_symbol of
k,
F1();
for l being QC-variable_list of k,F1()
for e being Element of vSUB F1() holds S1[ Sub_P (P,l,e)]let l be
QC-variable_list of
k,
F1();
for e being Element of vSUB F1() holds S1[ Sub_P (P,l,e)]let e be
Element of
vSUB F1();
S1[ Sub_P (P,l,e)]
thus F3()
. (Sub_P (P,l,e)) =
F6(
(Sub_P (P,l,e)))
by A1
.=
F4()
. (Sub_P (P,l,e))
by A2
;
verum
end;
A4:
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 A5:
[S,x] is
quantifiable
and A6:
F3()
. S = F4()
. S
;
S1[ Sub_All ([S,x],SQ)]
A7:
Sub_All (
[S,x],
SQ) is
Sub_universal
by A5;
Sub_the_scope_of (Sub_All ([S,x],SQ)) = [S,x] `1
by A5, Th21;
then
Sub_the_scope_of (Sub_All ([S,x],SQ)) = S
;
hence F3()
. (Sub_All ([S,x],SQ)) =
F9(
F1(),
(Sub_All ([S,x],SQ)),
(F4() . (Sub_the_scope_of (Sub_All ([S,x],SQ)))))
by A1, A6, A7
.=
F4()
. (Sub_All ([S,x],SQ))
by A2, A7
;
verum
end;
A8:
for S being Element of QC-Sub-WFF F1() st S is F1() -Sub_VERUM holds
S1[S]
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:
(
F3()
. S1 = F4()
. S1 &
F3()
. S2 = F4()
. S2 )
;
S1[ Sub_& (S1,S2)]
A13:
Sub_the_right_argument_of (Sub_& (S1,S2)) = S2
by A11, Th19;
A14:
(
Sub_& (
S1,
S2) is
Sub_conjunctive &
Sub_the_left_argument_of (Sub_& (S1,S2)) = S1 )
by A11, Th18;
hence F3()
. (Sub_& (S1,S2)) =
F8(
(F4() . S1),
(F4() . S2))
by A1, A12, A13
.=
F4()
. (Sub_& (S1,S2))
by A2, A14, A13
;
verum
end;
A15:
for S being Element of QC-Sub-WFF F1() st S1[S] holds
S1[ Sub_not S]
for S being Element of QC-Sub-WFF F1() holds S1[S]
from SUBSTUT1:sch 1(A3, A8, A15, A10, A4);
hence
F3() = F4()
by FUNCT_2:63; verum