let Al be QC-alphabet ; :: thesis: for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
for v being Element of Valuations_in (Al,A) holds
( J,v . (NEx_Val (v,S,x,xSQ)) |= All (x,(S `1)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) )
let x be bound_QC-variable of Al; :: thesis: for A being non empty set
for J being interpretation of Al,A
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
for v being Element of Valuations_in (Al,A) holds
( J,v . (NEx_Val (v,S,x,xSQ)) |= All (x,(S `1)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) )
let A be non empty set ; :: thesis: for J being interpretation of Al,A
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
for v being Element of Valuations_in (Al,A) holds
( J,v . (NEx_Val (v,S,x,xSQ)) |= All (x,(S `1)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) )
let J be interpretation of Al,A; :: thesis: for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
for v being Element of Valuations_in (Al,A) holds
( J,v . (NEx_Val (v,S,x,xSQ)) |= All (x,(S `1)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) )
let S be Element of CQC-Sub-WFF Al; :: thesis: for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
for v being Element of Valuations_in (Al,A) holds
( J,v . (NEx_Val (v,S,x,xSQ)) |= All (x,(S `1)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) )
let xSQ be second_Q_comp of [S,x]; :: thesis: ( [S,x] is quantifiable implies for v being Element of Valuations_in (Al,A) holds
( J,v . (NEx_Val (v,S,x,xSQ)) |= All (x,(S `1)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) ) )
set S1 = CQCSub_All ([S,x],xSQ);
assume A1: [S,x] is quantifiable ; :: thesis: for v being Element of Valuations_in (Al,A) holds
( J,v . (NEx_Val (v,S,x,xSQ)) |= All (x,(S `1)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) )
then CQCSub_All ([S,x],xSQ) = Sub_All ([S,x],xSQ) by Def5;
then (CQCSub_All ([S,x],xSQ)) `1 = All (([S,x] `2),(([S,x] `1) `1)) by A1, Th26;
then (CQCSub_All ([S,x],xSQ)) `1 = All (x,(([S,x] `1) `1)) ;
then A2: (CQCSub_All ([S,x],xSQ)) `1 = All (x,(S `1)) ;
let v be Element of Valuations_in (Al,A); :: thesis: ( J,v . (NEx_Val (v,S,x,xSQ)) |= All (x,(S `1)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) )
consider vS1, vS2 being Val_Sub of A,Al such that
A3: ( ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (All (x,(S `1))) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom (NEx_Val (v,S,x,xSQ)) misses dom vS2 ) and
A4: v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) = v . (((NEx_Val (v,S,x,xSQ)) +* vS1) +* vS2) by A1, Th86;
( J,v . (NEx_Val (v,S,x,xSQ)) |= All (x,(S `1)) iff J,v . (((NEx_Val (v,S,x,xSQ)) +* vS1) +* vS2) |= All (x,(S `1)) ) by A3, Th81;
hence ( J,v . (NEx_Val (v,S,x,xSQ)) |= All (x,(S `1)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) ) by A4, A2; :: thesis: verum