let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for A being non empty set
for J being interpretation of Al,A holds
( Valid ((VERUM Al),J) = (Valuations_in (Al,A)) --> TRUE & ( for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds Valid ((P ! ll),J) = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF Al holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF Al holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) )
let p be Element of CQC-WFF Al; :: thesis: for A being non empty set
for J being interpretation of Al,A holds
( Valid ((VERUM Al),J) = (Valuations_in (Al,A)) --> TRUE & ( for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds Valid ((P ! ll),J) = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF Al holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF Al holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) )
let A be non empty set ; :: thesis: for J being interpretation of Al,A holds
( Valid ((VERUM Al),J) = (Valuations_in (Al,A)) --> TRUE & ( for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds Valid ((P ! ll),J) = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF Al holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF Al holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) )
let J be interpretation of Al,A; :: thesis: ( Valid ((VERUM Al),J) = (Valuations_in (Al,A)) --> TRUE & ( for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds Valid ((P ! ll),J) = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF Al holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF Al holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) )
set D = Funcs ((Valuations_in (Al,A)),BOOLEAN);
set V = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN)));
deffunc H1( Nat, QC-pred_symbol of $1,Al, CQC-variable_list of $1,Al) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = $3 'in' (J . $2);
deffunc H2( Element of Funcs ((Valuations_in (Al,A)),BOOLEAN)) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = In (('not' $1),(Funcs ((Valuations_in (Al,A)),BOOLEAN)));
deffunc H3( Element of Funcs ((Valuations_in (Al,A)),BOOLEAN), Element of Funcs ((Valuations_in (Al,A)),BOOLEAN)) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = In (($1 '&' $2),(Funcs ((Valuations_in (Al,A)),BOOLEAN)));
deffunc H4( bound_QC-variable of Al, Element of Funcs ((Valuations_in (Al,A)),BOOLEAN)) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = In ((FOR_ALL ($1,$2)),(Funcs ((Valuations_in (Al,A)),BOOLEAN)));
deffunc H5( Element of CQC-WFF Al) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = Valid ($1,J);
A1: for p being Element of CQC-WFF Al
for d being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( d = H5(p) iff ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( d = F . p & F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ) ) )
proof
let p be Element of CQC-WFF Al; :: thesis: for d being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( d = H5(p) iff ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( d = F . p & F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ) ) )
let d be Element of Funcs ((Valuations_in (Al,A)),BOOLEAN); :: thesis: ( d = H5(p) iff ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( d = F . p & F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ) ) )
thus ( d = H5(p) implies ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( d = F . p & F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ) ) ) :: thesis: ( ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( d = F . p & F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ) ) implies d = H5(p) )
proof
assume d = H5(p) ; :: thesis: ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( d = F . p & F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ) )
then consider F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) such that
A2: d = F . p and
A3: F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE and
A4: for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) by Def6;
take F ; :: thesis: ( d = F . p & F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ) )
thus d = F . p by A2; :: thesis: ( F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ) )
thus F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) by A3, SUBSET_1:def 8; :: thesis: for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) )
let p, q be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) )
let x be bound_QC-variable of Al; :: thesis: for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) )
let k be Nat; :: thesis: for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) )
let ll be CQC-variable_list of k,Al; :: thesis: for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) )
let P be QC-pred_symbol of k,Al; :: thesis: ( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) )
thus F . (P ! ll) = H1(k,P,ll) by A4; :: thesis: ( F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) )
A5: 'not' (F . p) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
thus F . ('not' p) = 'not' (F . p) by A4
.= H2(F . p) by A5, SUBSET_1:def 8 ; :: thesis: ( F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) )
A6: (F . p) '&' (F . q) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
thus F . (p '&' q) = (F . p) '&' (F . q) by A4
.= H3(F . p,F . q) by A6, SUBSET_1:def 8 ; :: thesis: F . (All (x,p)) = H4(x,F . p)
thus F . (All (x,p)) = FOR_ALL (x,(F . p)) by A4
.= H4(x,F . p) by SUBSET_1:def 8 ; :: thesis: verum
end;
given F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) such that A7: d = F . p and
A8: F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) and
A9: for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ; :: thesis: d = H5(p)
(Valuations_in (Al,A)) --> TRUE in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
then A10: F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE by A8, SUBSET_1:def 8;
for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) )
proof
let p, q be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) )
let x be bound_QC-variable of Al; :: thesis: for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) )
let k be Nat; :: thesis: for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) )
let ll be CQC-variable_list of k,Al; :: thesis: for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) )
let P be QC-pred_symbol of k,Al; :: thesis: ( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) )
thus F . (P ! ll) = H1(k,P,ll) by A9; :: thesis: ( F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) )
A11: 'not' (F . p) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
thus F . ('not' p) = H2(F . p) by A9
.= 'not' (F . p) by A11, SUBSET_1:def 8 ; :: thesis: ( F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) )
A12: (F . p) '&' (F . q) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
thus F . (p '&' q) = H3(F . p,F . q) by A9
.= (F . p) '&' (F . q) by A12, SUBSET_1:def 8 ; :: thesis: F . (All (x,p)) = FOR_ALL (x,(F . p))
thus F . (All (x,p)) = H4(x,F . p) by A9
.= FOR_ALL (x,(F . p)) by SUBSET_1:def 8 ; :: thesis: verum
end;
hence d = H5(p) by A7, A10, Def6; :: thesis: verum
end;
A13: (Valuations_in (Al,A)) --> TRUE in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
H5( VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) from CQC_LANG:sch 5(A1);
 hence H5( VERUM Al) = (Valuations_in (Al,A)) --> TRUE by A13, SUBSET_1:def 8; :: thesis: ( ( for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds Valid ((P ! ll),J) = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF Al holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF Al holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) )
hereby :: thesis: ( ( for p being Element of CQC-WFF Al holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF Al holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) )
let k be Nat; :: thesis: for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds H5(P ! ll) = H1(k,P,ll)
let ll be CQC-variable_list of k,Al; :: thesis: for P being QC-pred_symbol of k,Al holds H5(P ! ll) = H1(k,P,ll)
let P be QC-pred_symbol of k,Al; :: thesis: H5(P ! ll) = H1(k,P,ll)
thus H5(P ! ll) = H1(k,P,ll) from CQC_LANG:sch 6(A1); :: thesis: verum
end;
hereby :: thesis: ( ( for q being Element of CQC-WFF Al holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) )
let p be Element of CQC-WFF Al; :: thesis: H5( 'not' p) = 'not' H5(p)
A14: 'not' H5(p) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
H5( 'not' p) = H2(H5(p)) from CQC_LANG:sch 7(A1);
hence H5( 'not' p) = 'not' H5(p) by A14, SUBSET_1:def 8; :: thesis: verum
end;
hereby :: thesis: for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J)))
let q be Element of CQC-WFF Al; :: thesis: H5(p '&' q) = H5(p) '&' H5(q)
A15: H5(p) '&' H5(q) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
H5(p '&' q) = H3(H5(p),H5(q)) from CQC_LANG:sch 8(A1);
hence H5(p '&' q) = H5(p) '&' H5(q) by A15, SUBSET_1:def 8; :: thesis: verum
end;
let x be bound_QC-variable of Al; :: thesis: Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J)))
H5( All (x,p)) = H4(x,H5(p)) from CQC_LANG:sch 9(A1);
 hence H5( All (x,p)) = FOR_ALL (x,H5(p)) by SUBSET_1:def 8; :: thesis: verum