let A be non empty set ; :: thesis: for x being bound_QC-variable
for p being Element of CQC-WFF
for J being interpretation of A st not x in still_not-bound_in p holds
for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid p,J) . v = (Valid p,J) . w
let x be bound_QC-variable; :: thesis: for p being Element of CQC-WFF
for J being interpretation of A st not x in still_not-bound_in p holds
for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid p,J) . v = (Valid p,J) . w
let p be Element of CQC-WFF ; :: thesis: for J being interpretation of A st not x in still_not-bound_in p holds
for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid p,J) . v = (Valid p,J) . w
let J be interpretation of A; :: thesis: ( not x in still_not-bound_in p implies for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid p,J) . v = (Valid p,J) . w )
defpred S₁[ Element of CQC-WFF ] means ( not x in still_not-bound_in $1 implies for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid $1,J) . v = (Valid $1,J) . w );

A1: now

let s, t be Element of CQC-WFF ; :: thesis: for y being bound_QC-variable
for k being Element of NAT
for ll being CQC-variable_list of
for P being QC-pred_symbol of k holds
( S₁[ VERUM ] & S₁[P ! ll] & ( S₁[s] implies S₁[ 'not' s] ) & ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All y,s] ) )
let y be bound_QC-variable; :: thesis: for k being Element of NAT
for ll being CQC-variable_list of
for P being QC-pred_symbol of k holds
( S₁[ VERUM ] & S₁[P ! ll] & ( S₁[s] implies S₁[ 'not' s] ) & ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All y,s] ) )
let k be Element of NAT ; :: thesis: for ll being CQC-variable_list of
for P being QC-pred_symbol of k holds
( S₁[ VERUM ] & S₁[P ! ll] & ( S₁[s] implies S₁[ 'not' s] ) & ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All y,s] ) )
let ll be CQC-variable_list of ; :: thesis: for P being QC-pred_symbol of k holds
( S₁[ VERUM ] & S₁[P ! ll] & ( S₁[s] implies S₁[ 'not' s] ) & ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All y,s] ) )
let P be QC-pred_symbol of k; :: thesis: ( S₁[ VERUM ] & S₁[P ! ll] & ( S₁[s] implies S₁[ 'not' s] ) & ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All y,s] ) )
A2: rng ll c= bound_QC-variables by RELAT_1:def 19;
thus S₁[ VERUM ] :: thesis: ( S₁[P ! ll] & ( S₁[s] implies S₁[ 'not' s] ) & ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All y,s] ) )

proof

assume not x in still_not-bound_in VERUM ; :: thesis: for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid VERUM ,J) . v = (Valid VERUM ,J) . w
thus for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid VERUM ,J) . v = (Valid VERUM ,J) . w :: thesis: verum

proof

let v, w be Element of Valuations_in A; :: thesis: ( ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) implies (Valid VERUM ,J) . v = (Valid VERUM ,J) . w )
assume for y being bound_QC-variable st x <> y holds
w . y = v . y ; :: thesis: (Valid VERUM ,J) . v = (Valid VERUM ,J) . w
( (Valid VERUM ,J) . v = TRUE & (Valid VERUM ,J) . w = TRUE ) by Th14;
hence (Valid VERUM ,J) . v = (Valid VERUM ,J) . w ; :: thesis: verum

end;

end;

thus S₁[P ! ll] :: thesis: ( ( S₁[s] implies S₁[ 'not' s] ) & ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All y,s] ) )

proof

assume A3: not x in still_not-bound_in (P ! ll) ; :: thesis: for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid (P ! ll),J) . v = (Valid (P ! ll),J) . w
thus for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid (P ! ll),J) . v = (Valid (P ! ll),J) . w :: thesis: verum

proof

let v, w be Element of Valuations_in A; :: thesis: ( ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) implies (Valid (P ! ll),J) . v = (Valid (P ! ll),J) . w )
assume A4: for y being bound_QC-variable st x <> y holds
w . y = v . y ; :: thesis: (Valid (P ! ll),J) . v = (Valid (P ! ll),J) . w

A5: now

assume A6: (Valid (P ! ll),J) . v = TRUE ; :: thesis: (Valid (P ! ll),J) . v = (Valid (P ! ll),J) . w
then (ll 'in' (J . P)) . v = TRUE by Lm1;
then A7: v *' ll in J . P by Def9;
A8: ( len (v *' ll) = k & len (w *' ll) = k ) by Def8;

now

let i be Nat; :: thesis: ( 1 <= i & i <= len (v *' ll) implies (v *' ll) . i = (w *' ll) . i )
assume A9: ( 1 <= i & i <= len (v *' ll) ) ; :: thesis: (v *' ll) . i = (w *' ll) . i
then A10: (v *' ll) . i = v . (ll . i) by A8, Def8;
A11: i in NAT by ORDINAL1:def 13;
A12: len (v *' ll) = len ll by A8, FINSEQ_1:def 18;
A13: ll . i in bound_QC-variables

proof

i in dom ll by A9, A12, FINSEQ_3:27;
then ll . i in rng ll by FUNCT_1:def 5;
hence ll . i in bound_QC-variables by A2; :: thesis: verum

end;

A14: ll . i <> x

proof

reconsider M = still_not-bound_in ll as set ;
not x in M by A3, QC_LANG3:9;
then not x in variables_in ll,bound_QC-variables by QC_LANG3:6;
then not x in { (ll . i2) where i2 is Element of NAT : ( 1 <= i2 & i2 <= len ll & ll . i2 in bound_QC-variables ) } by QC_LANG3:def 2;
hence ll . i <> x by A9, A11, A12; :: thesis: verum

end;

reconsider z = ll . i as bound_QC-variable by A13;
w . z = v . z by A4, A14;
hence (v *' ll) . i = (w *' ll) . i by A8, A9, A10, Def8; :: thesis: verum

end;

then w *' ll in J . P by A7, A8, FINSEQ_1:18;
then (ll 'in' (J . P)) . w = TRUE by Def9;
hence (Valid (P ! ll),J) . v = (Valid (P ! ll),J) . w by A6, Lm1; :: thesis: verum

end;

now

assume A15: (Valid (P ! ll),J) . v = FALSE ; :: thesis: (Valid (P ! ll),J) . v = (Valid (P ! ll),J) . w
then (ll 'in' (J . P)) . v = FALSE by Lm1;
then A16: not v *' ll in J . P by Def9;
A17: ( len (v *' ll) = k & len (w *' ll) = k ) by Def8;

now

let i be Nat; :: thesis: ( 1 <= i & i <= len (v *' ll) implies (v *' ll) . i = (w *' ll) . i )
assume A18: ( 1 <= i & i <= len (v *' ll) ) ; :: thesis: (v *' ll) . i = (w *' ll) . i
then A19: (v *' ll) . i = v . (ll . i) by A17, Def8;
A20: len (v *' ll) = len ll by A17, FINSEQ_1:def 18;
A21: ll . i in bound_QC-variables

proof

i in dom ll by A18, A20, FINSEQ_3:27;
then ll . i in rng ll by FUNCT_1:def 5;
hence ll . i in bound_QC-variables by A2; :: thesis: verum

end;

A22: ll . i <> x

proof

A23: i in NAT by ORDINAL1:def 13;
reconsider M = still_not-bound_in ll as set ;
not x in M by A3, QC_LANG3:9;
then not x in variables_in ll,bound_QC-variables by QC_LANG3:6;
then not x in { (ll . i2) where i2 is Element of NAT : ( 1 <= i2 & i2 <= len ll & ll . i2 in bound_QC-variables ) } by QC_LANG3:def 2;
hence ll . i <> x by A18, A20, A23; :: thesis: verum

end;

reconsider z = ll . i as bound_QC-variable by A21;
w . z = v . z by A4, A22;
hence (v *' ll) . i = (w *' ll) . i by A17, A18, A19, Def8; :: thesis: verum

end;

then not w *' ll in J . P by A16, A17, FINSEQ_1:18;
then (ll 'in' (J . P)) . w = FALSE by Def9;
hence (Valid (P ! ll),J) . v = (Valid (P ! ll),J) . w by A15, Lm1; :: thesis: verum

end;

hence (Valid (P ! ll),J) . v = (Valid (P ! ll),J) . w by A5, XBOOLEAN:def 3; :: thesis: verum

end;

end;

thus ( S₁[s] implies S₁[ 'not' s] ) :: thesis: ( ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All y,s] ) )

proof

assume that
A24: ( not x in still_not-bound_in s implies for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid s,J) . v = (Valid s,J) . w ) and
A25: not x in still_not-bound_in ('not' s) ; :: thesis: for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid ('not' s),J) . v = (Valid ('not' s),J) . w
thus for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid ('not' s),J) . v = (Valid ('not' s),J) . w :: thesis: verum

proof

let v, w be Element of Valuations_in A; :: thesis: ( ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) implies (Valid ('not' s),J) . v = (Valid ('not' s),J) . w )
assume A26: for y being bound_QC-variable st x <> y holds
w . y = v . y ; :: thesis: (Valid ('not' s),J) . v = (Valid ('not' s),J) . w

A27: now

assume A28: (Valid ('not' s),J) . v = TRUE ; :: thesis: (Valid ('not' s),J) . v = (Valid ('not' s),J) . w
then 'not' ((Valid s,J) . v) = TRUE by Th20;
then (Valid s,J) . v = FALSE by MARGREL1:41;
then (Valid s,J) . w = FALSE by A24, A25, A26, QC_LANG3:11;
then 'not' ((Valid s,J) . w) = TRUE by MARGREL1:41;
hence (Valid ('not' s),J) . v = (Valid ('not' s),J) . w by A28, Th20; :: thesis: verum

end;

now

assume A29: (Valid ('not' s),J) . v = FALSE ; :: thesis: (Valid ('not' s),J) . v = (Valid ('not' s),J) . w
then 'not' ((Valid s,J) . v) = FALSE by Th20;
then (Valid s,J) . v = TRUE by MARGREL1:41;
then (Valid s,J) . w = TRUE by A24, A25, A26, QC_LANG3:11;
then 'not' ((Valid s,J) . w) = FALSE by MARGREL1:41;
hence (Valid ('not' s),J) . v = (Valid ('not' s),J) . w by A29, Th20; :: thesis: verum

end;

hence (Valid ('not' s),J) . v = (Valid ('not' s),J) . w by A27, XBOOLEAN:def 3; :: thesis: verum

end;

end;

thus ( S₁[s] & S₁[t] implies S₁[s '&' t] ) :: thesis: ( S₁[s] implies S₁[ All y,s] )

proof

assume that
A30: ( not x in still_not-bound_in s implies for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid s,J) . v = (Valid s,J) . w ) and
A31: ( not x in still_not-bound_in t implies for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid t,J) . v = (Valid t,J) . w ) and
A32: not x in still_not-bound_in (s '&' t) ; :: thesis: for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w
A33: not x in (still_not-bound_in s) \/ (still_not-bound_in t) by A32, QC_LANG3:14;
thus for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w :: thesis: verum

proof

let v, w be Element of Valuations_in A; :: thesis: ( ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) implies (Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w )
assume A34: for y being bound_QC-variable st x <> y holds
w . y = v . y ; :: thesis: (Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w

A35: now

assume A36: (Valid (s '&' t),J) . v = TRUE ; :: thesis: (Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w
then ((Valid s,J) . v) '&' ((Valid t,J) . v) = TRUE by Th22;
then ( (Valid s,J) . v = TRUE & (Valid t,J) . v = TRUE ) by MARGREL1:45;
then ( (Valid s,J) . w = TRUE & (Valid t,J) . w = TRUE ) by A30, A31, A33, A34, XBOOLE_0:def 3;
then ((Valid s,J) . w) '&' ((Valid t,J) . w) = TRUE ;
hence (Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w by A36, Th22; :: thesis: verum

end;

now

assume A37: (Valid (s '&' t),J) . v = FALSE ; :: thesis: (Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w
then A38: ((Valid s,J) . v) '&' ((Valid t,J) . v) = FALSE by Th22;

A39: now

assume (Valid s,J) . v = FALSE ; :: thesis: (Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w
then (Valid s,J) . w = FALSE by A30, A33, A34, XBOOLE_0:def 3;
then ((Valid s,J) . w) '&' ((Valid t,J) . w) = FALSE by MARGREL1:45;
hence (Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w by A37, Th22; :: thesis: verum

end;

now

assume (Valid t,J) . v = FALSE ; :: thesis: (Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w
then (Valid t,J) . w = FALSE by A31, A33, A34, XBOOLE_0:def 3;
then ((Valid s,J) . w) '&' ((Valid t,J) . w) = FALSE by MARGREL1:45;
hence (Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w by A37, Th22; :: thesis: verum

end;

hence (Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w by A38, A39, MARGREL1:45; :: thesis: verum

end;

hence (Valid (s '&' t),J) . v = (Valid (s '&' t),J) . w by A35, XBOOLEAN:def 3; :: thesis: verum

end;

end;

thus ( S₁[s] implies S₁[ All y,s] ) :: thesis: verum

proof

assume that
A40: ( not x in still_not-bound_in s implies for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid s,J) . v = (Valid s,J) . w ) and
A41: not x in still_not-bound_in (All y,s) ; :: thesis: for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid (All y,s),J) . v = (Valid (All y,s),J) . w
A42: not x in (still_not-bound_in s) \ {y} by A41, QC_LANG3:16;
thus for v, w being Element of Valuations_in A st ( for z being bound_QC-variable st x <> z holds
w . z = v . z ) holds
(Valid (All y,s),J) . v = (Valid (All y,s),J) . w :: thesis: verum

proof

let v, w be Element of Valuations_in A; :: thesis: ( ( for z being bound_QC-variable st x <> z holds
w . z = v . z ) implies (Valid (All y,s),J) . v = (Valid (All y,s),J) . w )
assume A43: for z being bound_QC-variable st x <> z holds
w . z = v . z ; :: thesis: (Valid (All y,s),J) . v = (Valid (All y,s),J) . w

A44: now

assume A45: (Valid (All y,s),J) . v = TRUE ; :: thesis: (Valid (All y,s),J) . v = (Valid (All y,s),J) . w
then A46: (FOR_ALL y,(Valid s,J)) . v = TRUE by Lm1;
for v1 being Element of Valuations_in A st ( for z being bound_QC-variable st y <> z holds
v1 . z = w . z ) holds
(Valid s,J) . v1 = TRUE

proof

let v1 be Element of Valuations_in A; :: thesis: ( ( for z being bound_QC-variable st y <> z holds
v1 . z = w . z ) implies (Valid s,J) . v1 = TRUE )
assume A47: for z being bound_QC-variable st y <> z holds
v1 . z = w . z ; :: thesis: (Valid s,J) . v1 = TRUE

A48: now

assume A49: not x in still_not-bound_in s ; :: thesis: (Valid s,J) . v1 = TRUE
consider v2 being Element of Valuations_in A such that
A50: ( ( for z being bound_QC-variable st z <> y holds
v2 . z = v . z ) & v2 . y = v1 . y ) from VALUAT_1:sch 1();
A51: for z being bound_QC-variable st x <> z holds
v2 . z = v1 . z

proof

let z be bound_QC-variable; :: thesis: ( x <> z implies v2 . z = v1 . z )
assume A52: x <> z ; :: thesis: v2 . z = v1 . z

now

assume A53: z <> y ; :: thesis: v2 . z = v1 . z
hence v2 . z = v . z by A50
.= w . z by A43, A52
.= v1 . z by A47, A53 ;
:: thesis: verum

end;

hence v2 . z = v1 . z by A50; :: thesis: verum

end;

(Valid s,J) . v2 = TRUE by A46, A50, Th8;
hence (Valid s,J) . v1 = TRUE by A40, A49, A51; :: thesis: verum

end;

now

assume x in {y} ; :: thesis: (Valid s,J) . v1 = TRUE
then A54: x = y by TARSKI:def 1;
for z being bound_QC-variable st y <> z holds
v1 . z = v . z

proof

let z be bound_QC-variable; :: thesis: ( y <> z implies v1 . z = v . z )
assume A55: y <> z ; :: thesis: v1 . z = v . z
hence v . z = w . z by A43, A54
.= v1 . z by A47, A55 ;
:: thesis: verum

end;

hence (Valid s,J) . v1 = TRUE by A46, Th8; :: thesis: verum

end;

hence (Valid s,J) . v1 = TRUE by A42, A48, XBOOLE_0:def 5; :: thesis: verum

end;

then (FOR_ALL y,(Valid s,J)) . w = TRUE by Th8;
hence (Valid (All y,s),J) . v = (Valid (All y,s),J) . w by A45, Lm1; :: thesis: verum

end;

now

assume A56: (Valid (All y,s),J) . v = FALSE ; :: thesis: (Valid (All y,s),J) . v = (Valid (All y,s),J) . w
then (FOR_ALL y,(Valid s,J)) . v = FALSE by Lm1;
then consider v1 being Element of Valuations_in A such that
A57: (Valid s,J) . v1 = FALSE and
A58: for z being bound_QC-variable st y <> z holds
v1 . z = v . z by Th7;
ex v2 being Element of Valuations_in A st
( (Valid s,J) . v2 = FALSE & ( for z being bound_QC-variable st y <> z holds
v2 . z = w . z ) )

proof

A59: now

assume A60: not x in still_not-bound_in s ; :: thesis: ex v2 being Element of Valuations_in A st
( (Valid s,J) . v2 = FALSE & ( for z being bound_QC-variable st y <> z holds
v2 . z = w . z ) )
consider v2 being Element of Valuations_in A such that
A61: ( ( for z being bound_QC-variable st z <> y holds
v2 . z = w . z ) & v2 . y = v1 . y ) from VALUAT_1:sch 1();
take v2 = v2; :: thesis: ( (Valid s,J) . v2 = FALSE & ( for z being bound_QC-variable st y <> z holds
v2 . z = w . z ) )
for z being bound_QC-variable st x <> z holds
v2 . z = v1 . z

proof

let z be bound_QC-variable; :: thesis: ( x <> z implies v2 . z = v1 . z )
assume A62: x <> z ; :: thesis: v2 . z = v1 . z

now

assume A63: z <> y ; :: thesis: v2 . z = v1 . z
hence v2 . z = w . z by A61
.= v . z by A43, A62
.= v1 . z by A58, A63 ;
:: thesis: verum

end;

hence v2 . z = v1 . z by A61; :: thesis: verum

end;

hence (Valid s,J) . v2 = FALSE by A40, A57, A60; :: thesis: for z being bound_QC-variable st y <> z holds
v2 . z = w . z
thus for z being bound_QC-variable st y <> z holds
v2 . z = w . z by A61; :: thesis: verum

end;

now

assume A64: x in {y} ; :: thesis: ex v2 being Element of Valuations_in A st
( (Valid s,J) . v2 = FALSE & ( for z being bound_QC-variable st y <> z holds
v2 . z = w . z ) )
take v2 = v1; :: thesis: ( (Valid s,J) . v2 = FALSE & ( for z being bound_QC-variable st y <> z holds
v2 . z = w . z ) )
thus (Valid s,J) . v2 = FALSE by A57; :: thesis: for z being bound_QC-variable st y <> z holds
v2 . z = w . z
for z being bound_QC-variable st y <> z holds
v1 . z = w . z

proof

let z be bound_QC-variable; :: thesis: ( y <> z implies v1 . z = w . z )
assume A65: y <> z ; :: thesis: v1 . z = w . z
then A66: x <> z by A64, TARSKI:def 1;
thus v1 . z = v . z by A58, A65
.= w . z by A43, A66 ; :: thesis: verum

end;

hence for z being bound_QC-variable st y <> z holds
v2 . z = w . z ; :: thesis: verum

end;

hence ex v2 being Element of Valuations_in A st
( (Valid s,J) . v2 = FALSE & ( for z being bound_QC-variable st y <> z holds
v2 . z = w . z ) ) by A42, A59, XBOOLE_0:def 5; :: thesis: verum

end;

then (FOR_ALL y,(Valid s,J)) . w = FALSE by Th7;
hence (Valid (All y,s),J) . v = (Valid (All y,s),J) . w by A56, Lm1; :: thesis: verum

end;

hence (Valid (All y,s),J) . v = (Valid (All y,s),J) . w by A44, XBOOLEAN:def 3; :: thesis: verum

end;

end;

end;

for s being Element of CQC-WFF holds S₁[s] from CQC_LANG:sch 1(A1);
hence ( not x in still_not-bound_in p implies for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid p,J) . v = (Valid p,J) . w ) ; :: thesis: verum