let Al be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF Al
for A being non empty set
for J being interpretation of Al,A st ( for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in p ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= p iff J,v . ((vS +* vS1) +* vS2) |= p ) ) & ( for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in q ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= q iff J,v . ((vS +* vS1) +* vS2) |= q ) ) holds
for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (p '&' q) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= p '&' q iff J,v . ((vS +* vS1) +* vS2) |= p '&' q )
let p, q be Element of CQC-WFF Al; :: thesis: for A being non empty set
for J being interpretation of Al,A st ( for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in p ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= p iff J,v . ((vS +* vS1) +* vS2) |= p ) ) & ( for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in q ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= q iff J,v . ((vS +* vS1) +* vS2) |= q ) ) holds
for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (p '&' q) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= p '&' q iff J,v . ((vS +* vS1) +* vS2) |= p '&' q )
let A be non empty set ; :: thesis: for J being interpretation of Al,A st ( for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in p ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= p iff J,v . ((vS +* vS1) +* vS2) |= p ) ) & ( for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in q ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= q iff J,v . ((vS +* vS1) +* vS2) |= q ) ) holds
for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (p '&' q) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= p '&' q iff J,v . ((vS +* vS1) +* vS2) |= p '&' q )
let J be interpretation of Al,A; :: thesis: ( ( for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in p ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= p iff J,v . ((vS +* vS1) +* vS2) |= p ) ) & ( for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in q ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= q iff J,v . ((vS +* vS1) +* vS2) |= q ) ) implies for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (p '&' q) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= p '&' q iff J,v . ((vS +* vS1) +* vS2) |= p '&' q ) )
assume A1: ( ( for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in p ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= p iff J,v . ((vS +* vS1) +* vS2) |= p ) ) & ( for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in q ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= q iff J,v . ((vS +* vS1) +* vS2) |= q ) ) ) ; :: thesis: for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (p '&' q) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= p '&' q iff J,v . ((vS +* vS1) +* vS2) |= p '&' q )
let v be Element of Valuations_in (Al,A); :: thesis: for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (p '&' q) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 holds
( J,v . vS |= p '&' q iff J,v . ((vS +* vS1) +* vS2) |= p '&' q )
let vS, vS1, vS2 be Val_Sub of A,Al; :: thesis: ( ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (p '&' q) ) & ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 implies ( J,v . vS |= p '&' q iff J,v . ((vS +* vS1) +* vS2) |= p '&' q ) )
assume that
A2: for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (p '&' q) and
A3: ( ( for y being bound_QC-variable of Al st y in dom vS2 holds
vS2 . y = v . y ) & dom vS misses dom vS2 ) ; :: thesis: ( J,v . vS |= p '&' q iff J,v . ((vS +* vS1) +* vS2) |= p '&' q )
A4: for y being bound_QC-variable of Al st y in dom vS1 holds
( not y in still_not-bound_in p & not y in still_not-bound_in q )
proof
let y be bound_QC-variable of Al; :: thesis: ( y in dom vS1 implies ( not y in still_not-bound_in p & not y in still_not-bound_in q ) )
assume y in dom vS1 ; :: thesis: ( not y in still_not-bound_in p & not y in still_not-bound_in q )
then not y in still_not-bound_in (p '&' q) by A2;
then not y in (still_not-bound_in p) \/ (still_not-bound_in q) by QC_LANG3:10;
hence ( not y in still_not-bound_in p & not y in still_not-bound_in q ) by XBOOLE_0:def 3; :: thesis: verum
end;
A5: ( J,v . ((vS +* vS1) +* vS2) |= p & J,v . ((vS +* vS1) +* vS2) |= q implies ( J,v . vS |= p & J,v . vS |= q ) )
proof
assume A6: ( J,v . ((vS +* vS1) +* vS2) |= p & J,v . ((vS +* vS1) +* vS2) |= q ) ; :: thesis: ( J,v . vS |= p & J,v . vS |= q )
( ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in p ) & ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in q ) ) by A4;
hence ( J,v . vS |= p & J,v . vS |= q ) by A1, A3, A6; :: thesis: verum
end;
( J,v . vS |= p & J,v . vS |= q implies ( J,v . ((vS +* vS1) +* vS2) |= p & J,v . ((vS +* vS1) +* vS2) |= q ) )
proof
assume A7: ( J,v . vS |= p & J,v . vS |= q ) ; :: thesis: ( J,v . ((vS +* vS1) +* vS2) |= p & J,v . ((vS +* vS1) +* vS2) |= q )
( ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in p ) & ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in q ) ) by A4;
hence ( J,v . ((vS +* vS1) +* vS2) |= p & J,v . ((vS +* vS1) +* vS2) |= q ) by A1, A3, A7; :: thesis: verum
end;
hence ( J,v . vS |= p '&' q iff J,v . ((vS +* vS1) +* vS2) |= p '&' q ) by A5, VALUAT_1:18; :: thesis: verum