let x, y be Variable; :: thesis: for M being non empty set holds
( M |= x '=' y iff ( x = y or ex a being set st {a} = M ) )
let M be non empty set ; :: thesis: ( M |= x '=' y iff ( x = y or ex a being set st {a} = M ) )
thus
( not M |= x '=' y or x = y or ex a being set st {a} = M )
:: thesis: ( ( x = y or ex a being set st {a} = M ) implies M |= x '=' y )proof
assume A1:
( ( for
v being
Function of
VAR ,
M holds
M,
v |= x '=' y ) &
x <> y )
;
:: according to ZF_MODEL:def 5 :: thesis: ex a being set st {a} = M
consider m being
Element of
M;
reconsider a =
m as
set ;
take
a
;
:: thesis: {a} = M
thus
{a} c= M
by ZFMISC_1:37;
:: according to XBOOLE_0:def 10 :: thesis: M c= {a}
let b be
set ;
:: according to TARSKI:def 3 :: thesis: ( not b in M or b in {a} )
assume A2:
(
b in M & not
b in {a} )
;
:: thesis: contradiction
then reconsider b =
b as
Element of
M ;
consider v being
Function of
VAR ,
M;
M,
(v / x,m) / y,
b |= x '=' y
by A1;
then
(
((v / x,m) / y,b) . x = ((v / x,m) / y,b) . y &
(v / x,m) . x = m &
((v / x,m) / y,b) . y = b &
((v / x,m) / y,b) . x = (v / x,m) . x )
by A1, FUNCT_7:34, FUNCT_7:130, ZF_MODEL:12;
hence
contradiction
by A2, TARSKI:def 1;
:: thesis: verum
end;
hence
( ( x = y or ex a being set st {a} = M ) implies M |= x '=' y )
by Th90, ZF_MODEL:def 5; :: thesis: verum