let E be non empty set ; for H being ZF-formula
for f, g being Function of VAR,E st ( for x being Variable st f . x <> g . x holds
not x in Free H ) & E,f |= H holds
E,g |= H
defpred S2[ ZF-formula] means for f, g being Function of VAR,E st ( for x being Variable st f . x <> g . x holds
not x in Free $1 ) & E,f |= $1 holds
E,g |= $1;
A1:
for H being ZF-formula st H is atomic holds
S2[H]
A16:
for H being ZF-formula st H is conjunctive & S2[ the_left_argument_of H] & S2[ the_right_argument_of H] holds
S2[H]
proof
let H be
ZF-formula;
( H is conjunctive & S2[ the_left_argument_of H] & S2[ the_right_argument_of H] implies S2[H] )
assume A17:
H is
conjunctive
;
( not S2[ the_left_argument_of H] or not S2[ the_right_argument_of H] or S2[H] )
then A18:
H = (the_left_argument_of H) '&' (the_right_argument_of H)
by ZF_LANG:40;
assume that A19:
for
f,
g being
Function of
VAR,
E st ( for
x being
Variable st
f . x <> g . x holds
not
x in Free (the_left_argument_of H) ) &
E,
f |= the_left_argument_of H holds
E,
g |= the_left_argument_of H
and A20:
for
f,
g being
Function of
VAR,
E st ( for
x being
Variable st
f . x <> g . x holds
not
x in Free (the_right_argument_of H) ) &
E,
f |= the_right_argument_of H holds
E,
g |= the_right_argument_of H
;
S2[H]
let f,
g be
Function of
VAR,
E;
( ( for x being Variable st f . x <> g . x holds
not x in Free H ) & E,f |= H implies E,g |= H )
assume that A21:
for
x being
Variable st
f . x <> g . x holds
not
x in Free H
and A22:
E,
f |= H
;
E,g |= H
A23:
Free H = (Free (the_left_argument_of H)) \/ (Free (the_right_argument_of H))
by A17, ZF_MODEL:1;
E,
f |= the_right_argument_of H
by A18, A22, ZF_MODEL:15;
then A26:
E,
g |= the_right_argument_of H
by A20, A24;
E,
f |= the_left_argument_of H
by A18, A22, ZF_MODEL:15;
then
E,
g |= the_left_argument_of H
by A19, A25;
hence
E,
g |= H
by A18, A26, ZF_MODEL:15;
verum
end;
A27:
for H being ZF-formula st H is universal & S2[ the_scope_of H] holds
S2[H]
proof
let H be
ZF-formula;
( H is universal & S2[ the_scope_of H] implies S2[H] )
assume A28:
H is
universal
;
( not S2[ the_scope_of H] or S2[H] )
then A29:
H = All (
(bound_in H),
(the_scope_of H))
by ZF_LANG:44;
assume A30:
for
f,
g being
Function of
VAR,
E st ( for
x being
Variable st
f . x <> g . x holds
not
x in Free (the_scope_of H) ) &
E,
f |= the_scope_of H holds
E,
g |= the_scope_of H
;
S2[H]
let f,
g be
Function of
VAR,
E;
( ( for x being Variable st f . x <> g . x holds
not x in Free H ) & E,f |= H implies E,g |= H )
assume that A31:
for
x being
Variable st
f . x <> g . x holds
not
x in Free H
and A32:
E,
f |= H
;
E,g |= H
A33:
Free H = (Free (the_scope_of H)) \ {(bound_in H)}
by A28, ZF_MODEL:1;
now for j being Function of VAR,E st ( for x being Variable st j . x <> g . x holds
bound_in H = x ) holds
E,j |= the_scope_of Hlet j be
Function of
VAR,
E;
( ( for x being Variable st j . x <> g . x holds
bound_in H = x ) implies E,j |= the_scope_of H )assume A34:
for
x being
Variable st
j . x <> g . x holds
bound_in H = x
;
E,j |= the_scope_of Hset h =
f +* (
(bound_in H),
(j . (bound_in H)));
for
x being
Variable st
(f +* ((bound_in H),(j . (bound_in H)))) . x <> f . x holds
bound_in H = x
by FUNCT_7:32;
then
E,
f +* (
(bound_in H),
(j . (bound_in H)))
|= the_scope_of H
by A29, A32, ZF_MODEL:16;
hence
E,
j |= the_scope_of H
by A30, A35;
verum end;
hence
E,
g |= H
by A29, ZF_MODEL:16;
verum
end;
A39:
for H being ZF-formula st H is negative & S2[ the_argument_of H] holds
S2[H]
proof
let H be
ZF-formula;
( H is negative & S2[ the_argument_of H] implies S2[H] )
assume A40:
H is
negative
;
( not S2[ the_argument_of H] or S2[H] )
then A41:
Free H = Free (the_argument_of H)
by ZF_MODEL:1;
assume A42:
for
f,
g being
Function of
VAR,
E st ( for
x being
Variable st
f . x <> g . x holds
not
x in Free (the_argument_of H) ) &
E,
f |= the_argument_of H holds
E,
g |= the_argument_of H
;
S2[H]
let f,
g be
Function of
VAR,
E;
( ( for x being Variable st f . x <> g . x holds
not x in Free H ) & E,f |= H implies E,g |= H )
assume that A43:
for
x being
Variable st
f . x <> g . x holds
not
x in Free H
and A44:
E,
f |= H
and A45:
not
E,
g |= H
;
contradiction
A46:
H = 'not' (the_argument_of H)
by A40, ZF_LANG:def 30;
then
E,
g |= the_argument_of H
by A45, ZF_MODEL:14;
then
E,
f |= the_argument_of H
by A41, A42, A43;
hence
contradiction
by A46, A44, ZF_MODEL:14;
verum
end;
thus
for H being ZF-formula holds S2[H]
from ZF_LANG:sch 1(A1, A39, A16, A27); verum