let E be non empty set ; :: thesis: 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]
A10:
for H being ZF-formula st H is negative & S2[ the_argument_of H] holds
S2[H]
proof
let H be
ZF-formula;
:: thesis: ( H is negative & S2[ the_argument_of H] implies S2[H] )
assume
H is
negative
;
:: thesis: ( not S2[ the_argument_of H] or S2[H] )
then A11:
(
H = 'not' (the_argument_of H) &
Free H = Free (the_argument_of H) )
by ZF_LANG:def 30, ZF_MODEL:1;
assume A12:
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
;
:: thesis: S2[H]
let f,
g be
Function of
VAR ,
E;
:: thesis: ( ( for x being Variable st f . x <> g . x holds
not x in Free H ) & E,f |= H implies E,g |= H )
assume that A13:
for
x being
Variable st
f . x <> g . x holds
not
x in Free H
and A14:
E,
f |= H
and A15:
not
E,
g |= H
;
:: thesis: contradiction
E,
g |= the_argument_of H
by A11, A15, ZF_MODEL:14;
then
(
E,
f |= the_argument_of H & not
E,
f |= the_argument_of H )
by A11, A12, A13, A14, ZF_MODEL:14;
hence
contradiction
;
:: thesis: verum
end;
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;
:: thesis: ( H is conjunctive & S2[ the_left_argument_of H] & S2[ the_right_argument_of H] implies S2[H] )
assume
H is
conjunctive
;
:: thesis: ( not S2[ the_left_argument_of H] or not S2[ the_right_argument_of H] or S2[H] )
then A17:
(
H = (the_left_argument_of H) '&' (the_right_argument_of H) &
Free H = (Free (the_left_argument_of H)) \/ (Free (the_right_argument_of H)) )
by ZF_LANG:58, ZF_MODEL:1;
assume that A18:
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 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_right_argument_of H) ) &
E,
f |= the_right_argument_of H holds
E,
g |= the_right_argument_of H
;
:: thesis: S2[H]
let f,
g be
Function of
VAR ,
E;
:: thesis: ( ( for x being Variable st f . x <> g . x holds
not x in Free H ) & E,f |= H implies E,g |= H )
assume that A20:
for
x being
Variable st
f . x <> g . x holds
not
x in Free H
and A21:
E,
f |= H
;
:: thesis: E,g |= H
A22:
(
E,
f |= the_left_argument_of H &
E,
f |= the_right_argument_of H )
by A17, A21, ZF_MODEL:15;
then A23:
E,
g |= the_left_argument_of H
by A18, A22;
then
E,
g |= the_right_argument_of H
by A19, A22;
hence
E,
g |= H
by A17, A23, ZF_MODEL:15;
:: thesis: verum
end;
A24:
for H being ZF-formula st H is universal & S2[ the_scope_of H] holds
S2[H]
proof
let H be
ZF-formula;
:: thesis: ( H is universal & S2[ the_scope_of H] implies S2[H] )
assume
H is
universal
;
:: thesis: ( not S2[ the_scope_of H] or S2[H] )
then A25:
(
H = All (bound_in H),
(the_scope_of H) &
Free H = (Free (the_scope_of H)) \ {(bound_in H)} )
by ZF_LANG:62, ZF_MODEL:1;
assume A26:
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
;
:: thesis: S2[H]
let f,
g be
Function of
VAR ,
E;
:: thesis: ( ( for x being Variable st f . x <> g . x holds
not x in Free H ) & E,f |= H implies E,g |= H )
assume that A27:
for
x being
Variable st
f . x <> g . x holds
not
x in Free H
and A28:
E,
f |= H
;
:: thesis: E,g |= H
now let j be
Function of
VAR ,
E;
:: thesis: ( ( for x being Variable st j . x <> g . x holds
bound_in H = x ) implies E,j |= the_scope_of H )assume A29:
for
x being
Variable st
j . x <> g . x holds
bound_in H = x
;
:: thesis: E,j |= the_scope_of Hset h =
f +* (bound_in H),
(j . (bound_in H));
A30:
(
(f +* (bound_in H),(j . (bound_in H))) . (bound_in H) = j . (bound_in H) & ( for
x being
Variable st
x <> bound_in H holds
(f +* (bound_in H),(j . (bound_in H))) . x = f . x ) )
by FUNCT_7:34, FUNCT_7:130;
for
x being
Variable st
(f +* (bound_in H),(j . (bound_in H))) . x <> f . x holds
bound_in H = x
by A30;
then A31:
E,
f +* (bound_in H),
(j . (bound_in H)) |= the_scope_of H
by A25, A28, ZF_MODEL:16;
hence
E,
j |= the_scope_of H
by A26, A31;
:: thesis: verum end;
hence
E,
g |= H
by A25, ZF_MODEL:16;
:: thesis: verum
end;
thus
for H being ZF-formula holds S2[H]
from ZF_LANG:sch 1(A1, A10, A16, A24); :: thesis: verum