let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for x, y being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds
( J,v |= p . (x,y) iff ex a being Element of A st
( v . y = a & J,v . (x | a) |= p ) )
let p be Element of CQC-WFF Al; :: thesis: for x, y being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds
( J,v |= p . (x,y) iff ex a being Element of A st
( v . y = a & J,v . (x | a) |= p ) )
let x, y be bound_QC-variable of Al; :: thesis: for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds
( J,v |= p . (x,y) iff ex a being Element of A st
( v . y = a & J,v . (x | a) |= p ) )
let A be non empty set ; :: thesis: for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds
( J,v |= p . (x,y) iff ex a being Element of A st
( v . y = a & J,v . (x | a) |= p ) )
let J be interpretation of Al,A; :: thesis: for v being Element of Valuations_in (Al,A) holds
( J,v |= p . (x,y) iff ex a being Element of A st
( v . y = a & J,v . (x | a) |= p ) )
let v be Element of Valuations_in (Al,A); :: thesis: ( J,v |= p . (x,y) iff ex a being Element of A st
( v . y = a & J,v . (x | a) |= p ) )
A1: ( J,v |= CQC_Sub [p,(Sbst (x,y))] iff J,v . (Val_S (v,[p,(Sbst (x,y))])) |= [p,(Sbst (x,y))] ) by SUBLEMMA:89;
A2: ( J,v . (Val_S (v,[p,(Sbst (x,y))])) |= [p,(Sbst (x,y))] iff J,v . (Val_S (v,[p,(Sbst (x,y))])) |= p ) by Th23;
Val_S (v,[p,(Sbst (x,y))]) = v * (@ ([p,(Sbst (x,y))] `2)) by SUBLEMMA:def 1;
then Val_S (v,[p,(Sbst (x,y))]) = v * (@ (Sbst (x,y))) ;
then A3: Val_S (v,[p,(Sbst (x,y))]) = v * (x .--> y) by SUBSTUT1:def 2;
y in bound_QC-variables Al ;
then y in dom v by SUBLEMMA:58;
then Val_S (v,[p,(Sbst (x,y))]) = x .--> (v . y) by A3, FUNCOP_1:17;
hence ( J,v |= p . (x,y) iff ex a being Element of A st
( v . y = a & J,v . (x | a) |= p ) ) by A1, A2, SUBSTUT2:def 1; :: thesis: verum