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 H₁( 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 H₂( 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 H₃( 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 H₄( 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 H₅( 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 = H₅(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) = H₁(k,P,ll) & F . ('not' p) = H₂(F . p) & F . (p '&' q) = H₃(F . p,F . q) & F . (All (x,p)) = H₄(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 = H₅(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) = H₁(k,P,ll) & F . ('not' p) = H₂(F . p) & F . (p '&' q) = H₃(F . p,F . q) & F . (All (x,p)) = H₄(x,F . p) ) ) ) )
let d be Element of Funcs ((Valuations_in (Al,A)),BOOLEAN); :: thesis: ( d = H₅(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) = H₁(k,P,ll) & F . ('not' p) = H₂(F . p) & F . (p '&' q) = H₃(F . p,F . q) & F . (All (x,p)) = H₄(x,F . p) ) ) ) )
thus ( d = H₅(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) = H₁(k,P,ll) & F . ('not' p) = H₂(F . p) & F . (p '&' q) = H₃(F . p,F . q) & F . (All (x,p)) = H₄(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) = H₁(k,P,ll) & F . ('not' p) = H₂(F . p) & F . (p '&' q) = H₃(F . p,F . q) & F . (All (x,p)) = H₄(x,F . p) ) ) ) implies d = H₅(p) )

proof

assume d = H₅(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) = H₁(k,P,ll) & F . ('not' p) = H₂(F . p) & F . (p '&' q) = H₃(F . p,F . q) & F . (All (x,p)) = H₄(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) = H₁(k,P,ll) & F . ('not' p) = H₂(F . p) & F . (p '&' q) = H₃(F . p,F . q) & F . (All (x,p)) = H₄(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) = H₁(k,P,ll) & F . ('not' p) = H₂(F . p) & F . (p '&' q) = H₃(F . p,F . q) & F . (All (x,p)) = H₄(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) = H₁(k,P,ll) & F . ('not' p) = H₂(F . p) & F . (p '&' q) = H₃(F . p,F . q) & F . (All (x,p)) = H₄(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) = H₁(k,P,ll) & F . ('not' p) = H₂(F . p) & F . (p '&' q) = H₃(F . p,F . q) & F . (All (x,p)) = H₄(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) = H₁(k,P,ll) & F . ('not' p) = H₂(F . p) & F . (p '&' q) = H₃(F . p,F . q) & F . (All (x,p)) = H₄(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) = H₁(k,P,ll) & F . ('not' p) = H₂(F . p) & F . (p '&' q) = H₃(F . p,F . q) & F . (All (x,p)) = H₄(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) = H₁(k,P,ll) & F . ('not' p) = H₂(F . p) & F . (p '&' q) = H₃(F . p,F . q) & F . (All (x,p)) = H₄(x,F . p) )
let P be QC-pred_symbol of k,Al; :: thesis: ( F . (P ! ll) = H₁(k,P,ll) & F . ('not' p) = H₂(F . p) & F . (p '&' q) = H₃(F . p,F . q) & F . (All (x,p)) = H₄(x,F . p) )
thus F . (P ! ll) = H₁(k,P,ll) by A4; :: thesis: ( F . ('not' p) = H₂(F . p) & F . (p '&' q) = H₃(F . p,F . q) & F . (All (x,p)) = H₄(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
.= H₂(F . p) by A5, SUBSET_1:def 8 ; :: thesis: ( F . (p '&' q) = H₃(F . p,F . q) & F . (All (x,p)) = H₄(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
.= H₃(F . p,F . q) by A6, SUBSET_1:def 8 ; :: thesis: F . (All (x,p)) = H₄(x,F . p)
thus F . (All (x,p)) = FOR_ALL (x,(F . p)) by A4
.= H₄(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) = H₁(k,P,ll) & F . ('not' p) = H₂(F . p) & F . (p '&' q) = H₃(F . p,F . q) & F . (All (x,p)) = H₄(x,F . p) ) ; :: thesis: d = H₅(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) = H₁(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) = H₁(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) = H₁(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) = H₁(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) = H₁(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) = H₁(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) = H₁(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) = H₂(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) = H₃(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)) = H₄(x,F . p) by A9
.= FOR_ALL (x,(F . p)) by SUBSET_1:def 8 ; :: thesis: verum

end;

hence d = H₅(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;
H₅( VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) from CQC_LANG:sch 5(A1);
hence H₅( 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 H₅(P ! ll) = H₁(k,P,ll)
let ll be CQC-variable_list of k,Al; :: thesis: for P being QC-pred_symbol of k,Al holds H₅(P ! ll) = H₁(k,P,ll)
let P be QC-pred_symbol of k,Al; :: thesis: H₅(P ! ll) = H₁(k,P,ll)
thus H₅(P ! ll) = H₁(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: H₅( 'not' p) = 'not' H₅(p)
A14: 'not' H₅(p) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
H₅( 'not' p) = H₂(H₅(p)) from CQC_LANG:sch 7(A1);
hence H₅( 'not' p) = 'not' H₅(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: H₅(p '&' q) = H₅(p) '&' H₅(q)
A15: H₅(p) '&' H₅(q) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
H₅(p '&' q) = H₃(H₅(p),H₅(q)) from CQC_LANG:sch 8(A1);
hence H₅(p '&' q) = H₅(p) '&' H₅(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)))
H₅( All (x,p)) = H₄(x,H₅(p)) from CQC_LANG:sch 9(A1);
hence H₅( All (x,p)) = FOR_ALL (x,H₅(p)) by SUBSET_1:def 8; :: thesis: verum