let Al be QC-alphabet ; 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 & ( for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S ) ) holds
for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub (CQCSub_All ([S,x],xSQ)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) )
let x be 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 & ( for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S ) ) holds
for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub (CQCSub_All ([S,x],xSQ)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) )
let A be 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 & ( for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S ) ) holds
for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub (CQCSub_All ([S,x],xSQ)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) )
let J be 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 & ( for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S ) ) holds
for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub (CQCSub_All ([S,x],xSQ)) 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; for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & ( for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S ) ) holds
for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub (CQCSub_All ([S,x],xSQ)) 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]; ( [S,x] is quantifiable & ( for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S ) ) implies for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub (CQCSub_All ([S,x],xSQ)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) ) )
assume that
A1:
[S,x] is quantifiable
and
A2:
for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S )
; for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub (CQCSub_All ([S,x],xSQ)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) )
let v be Element of Valuations_in (Al,A); ( J,v |= CQC_Sub (CQCSub_All ([S,x],xSQ)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) )
set S1 = CQCSub_All ([S,x],xSQ);
set z = S_Bound (@ (CQCSub_All ([S,x],xSQ)));
A3:
( ( for a being Element of A holds J,(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . (Val_S ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S)) |= S ) iff for a being Element of A holds J,(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ)) +* (x | a)) |= S )
by A1, Th54;
set q = CQC_Sub S;
A4:
( J,v |= All ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))),(CQC_Sub S)) iff for a being Element of A holds J,v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) |= CQC_Sub S )
by Th50;
A5:
( ( for a being Element of A holds J,v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) |= CQC_Sub S ) implies for a being Element of A holds J,(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . (Val_S ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S)) |= S )
by A2;
A6:
( ( for a being Element of A holds J,(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . (Val_S ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S)) |= S ) implies for a being Element of A holds J,v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) |= CQC_Sub S )
proof
assume A7:
for
a being
Element of
A holds
J,
(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . (Val_S ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S)) |= S
;
for a being Element of A holds J,v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) |= CQC_Sub S
let a be
Element of
A;
J,v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) |= CQC_Sub S
J,
(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . (Val_S ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S)) |= S
by A7;
hence
J,
v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) |= CQC_Sub S
by A2;
verum
end;
set p = CQC_Sub (CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ)));
A8:
( J,v |= CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub (CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ))))) iff J,v |= CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub S)) )
by A1, Th30;
A9:
( ( for a being Element of A holds J,(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a)) |= S ) iff for a being Element of A holds J,v . ((NEx_Val (v,S,x,xSQ)) +* (x | a)) |= S )
by A1, Th70;
A10:
( J,v . (NEx_Val (v,S,x,xSQ)) |= All (x,(S `1)) implies for a being Element of A holds J,(v . (NEx_Val (v,S,x,xSQ))) . (x | a) |= S )
by Th50;
A11:
( ( for a being Element of A holds J,(v . (NEx_Val (v,S,x,xSQ))) . (x | a) |= S ) implies J,v . (NEx_Val (v,S,x,xSQ)) |= All (x,(S `1)) )
proof
assume
for
a being
Element of
A holds
J,
(v . (NEx_Val (v,S,x,xSQ))) . (x | a) |= S
;
J,v . (NEx_Val (v,S,x,xSQ)) |= All (x,(S `1))
then
for
a being
Element of
A holds
J,
(v . (NEx_Val (v,S,x,xSQ))) . (x | a) |= S `1
by Th73;
hence
J,
v . (NEx_Val (v,S,x,xSQ)) |= All (
x,
(S `1))
by Th50;
verum
end;
CQCSub_All ([S,x],xSQ) is Sub_universal
by A1, Th27;
hence
( J,v |= CQC_Sub (CQCSub_All ([S,x],xSQ)) iff J,v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All ([S,x],xSQ) )
by A1, A8, A4, A5, A6, A3, A9, A11, A10, Th28, Th31, Th56, Th72, Th87; verum