let E be non empty set ; :: thesis: ( E is epsilon-transitive implies E |= the_axiom_of_extensionality )
assume A1:
for X being set st X in E holds
X c= E
; :: according to ORDINAL1:def 2 :: thesis: E |= the_axiom_of_extensionality
E |= (All (x. 2),(((x. 2) 'in' (x. 0 )) <=> ((x. 2) 'in' (x. 1)))) => ((x. 0 ) '=' (x. 1))
proof
let f be
Function of
VAR ,
E;
:: according to ZF_MODEL:def 5 :: thesis: E,f |= (All (x. 2),(((x. 2) 'in' (x. 0 )) <=> ((x. 2) 'in' (x. 1)))) => ((x. 0 ) '=' (x. 1))
now assume A2:
E,
f |= All (x. 2),
(((x. 2) 'in' (x. 0 )) <=> ((x. 2) 'in' (x. 1)))
;
:: thesis: E,f |= (x. 0 ) '=' (x. 1)
f . (x. 0 ) = f . (x. 1)
proof
thus
for
a being
set st
a in f . (x. 0 ) holds
a in f . (x. 1)
:: according to TARSKI:def 3,
XBOOLE_0:def 10 :: thesis: f . (x. 1) c= f . (x. 0 )proof
let a be
set ;
:: thesis: ( a in f . (x. 0 ) implies a in f . (x. 1) )
assume A3:
a in f . (x. 0 )
;
:: thesis: a in f . (x. 1)
f . (x. 0 ) c= E
by A1;
then reconsider a' =
a as
Element of
E by A3;
set g =
f +* (x. 2),
a';
A4:
(
(f +* (x. 2),a') . (x. 2) = a' & ( for
x being
Variable st
x <> x. 2 holds
(f +* (x. 2),a') . x = f . x ) )
by FUNCT_7:34, FUNCT_7:130;
for
x being
Variable st
(f +* (x. 2),a') . x <> f . x holds
x. 2
= x
by A4;
then
E,
f +* (x. 2),
a' |= ((x. 2) 'in' (x. 0 )) <=> ((x. 2) 'in' (x. 1))
by A2, ZF_MODEL:16;
then A5:
(
E,
f +* (x. 2),
a' |= (x. 2) 'in' (x. 0 ) iff
E,
f +* (x. 2),
a' |= (x. 2) 'in' (x. 1) )
by ZF_MODEL:19;
(
(f +* (x. 2),a') . (x. 0 ) = f . (x. 0 ) &
(f +* (x. 2),a') . (x. 1) = f . (x. 1) )
by A4;
hence
a in f . (x. 1)
by A3, A4, A5, ZF_MODEL:13;
:: thesis: verum
end;
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in f . (x. 1) or a in f . (x. 0 ) )
assume A6:
a in f . (x. 1)
;
:: thesis: a in f . (x. 0 )
f . (x. 1) c= E
by A1;
then reconsider a' =
a as
Element of
E by A6;
set g =
f +* (x. 2),
a';
A7:
(
(f +* (x. 2),a') . (x. 2) = a' & ( for
x being
Variable st
x <> x. 2 holds
(f +* (x. 2),a') . x = f . x ) )
by FUNCT_7:34, FUNCT_7:130;
for
x being
Variable st
(f +* (x. 2),a') . x <> f . x holds
x. 2
= x
by A7;
then
E,
f +* (x. 2),
a' |= ((x. 2) 'in' (x. 0 )) <=> ((x. 2) 'in' (x. 1))
by A2, ZF_MODEL:16;
then A8:
(
E,
f +* (x. 2),
a' |= (x. 2) 'in' (x. 0 ) iff
E,
f +* (x. 2),
a' |= (x. 2) 'in' (x. 1) )
by ZF_MODEL:19;
(
(f +* (x. 2),a') . (x. 0 ) = f . (x. 0 ) &
(f +* (x. 2),a') . (x. 1) = f . (x. 1) )
by A7;
hence
a in f . (x. 0 )
by A6, A7, A8, ZF_MODEL:13;
:: thesis: verum
end; hence
E,
f |= (x. 0 ) '=' (x. 1)
by ZF_MODEL:12;
:: thesis: verum end;
hence
E,
f |= (All (x. 2),(((x. 2) 'in' (x. 0 )) <=> ((x. 2) 'in' (x. 1)))) => ((x. 0 ) '=' (x. 1))
by ZF_MODEL:18;
:: thesis: verum
end;
then
E |= All (x. 1),((All (x. 2),(((x. 2) 'in' (x. 0 )) <=> ((x. 2) 'in' (x. 1)))) => ((x. 0 ) '=' (x. 1)))
by ZF_MODEL:25;
hence
E |= the_axiom_of_extensionality
by ZF_MODEL:25; :: thesis: verum