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))

hence E |= the_axiom_of_extensionality by ZF_MODEL:23; :: thesis: verum

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

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:23;
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))

end;now :: thesis: ( E,f |= All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)))) implies E,f |= (x. 0) '=' (x. 1) )

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: verumassume 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)

end;f . (x. 0) = f . (x. 1)

proof

hence
E,f |= (x. 0) '=' (x. 1)
by ZF_MODEL:12; :: thesis: verum
thus
for a being object 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)

assume A6: a in f . (x. 1) ; :: thesis: a in f . (x. 0)

f . (x. 1) c= E by A1;

then reconsider a9 = a as Element of E by A6;

set g = f +* ((x. 2),a9);

A7: (f +* ((x. 2),a9)) . (x. 1) = f . (x. 1) by FUNCT_7:32;

for x being Variable st (f +* ((x. 2),a9)) . x <> f . x holds

x. 2 = x by FUNCT_7:32;

then E,f +* ((x. 2),a9) |= ((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)) by A2, ZF_MODEL:16;

then A8: ( E,f +* ((x. 2),a9) |= (x. 2) 'in' (x. 0) iff E,f +* ((x. 2),a9) |= (x. 2) 'in' (x. 1) ) by ZF_MODEL:19;

( (f +* ((x. 2),a9)) . (x. 2) = a9 & (f +* ((x. 2),a9)) . (x. 0) = f . (x. 0) ) by FUNCT_7:32, FUNCT_7:128;

hence a in f . (x. 0) by A6, A8, A7, ZF_MODEL:13; :: thesis: verum

end;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 object ; :: according to TARSKI:def 3 :: thesis: ( not a in f . (x. 1) or a in f . (x. 0) )
let a be object ; :: 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 a9 = a as Element of E by A3;

set g = f +* ((x. 2),a9);

A4: (f +* ((x. 2),a9)) . (x. 1) = f . (x. 1) by FUNCT_7:32;

for x being Variable st (f +* ((x. 2),a9)) . x <> f . x holds

x. 2 = x by FUNCT_7:32;

then E,f +* ((x. 2),a9) |= ((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)) by A2, ZF_MODEL:16;

then A5: ( E,f +* ((x. 2),a9) |= (x. 2) 'in' (x. 0) iff E,f +* ((x. 2),a9) |= (x. 2) 'in' (x. 1) ) by ZF_MODEL:19;

( (f +* ((x. 2),a9)) . (x. 2) = a9 & (f +* ((x. 2),a9)) . (x. 0) = f . (x. 0) ) by FUNCT_7:32, FUNCT_7:128;

hence a in f . (x. 1) by A3, A5, A4, ZF_MODEL:13; :: thesis: verum

end;assume A3: a in f . (x. 0) ; :: thesis: a in f . (x. 1)

f . (x. 0) c= E by A1;

then reconsider a9 = a as Element of E by A3;

set g = f +* ((x. 2),a9);

A4: (f +* ((x. 2),a9)) . (x. 1) = f . (x. 1) by FUNCT_7:32;

for x being Variable st (f +* ((x. 2),a9)) . x <> f . x holds

x. 2 = x by FUNCT_7:32;

then E,f +* ((x. 2),a9) |= ((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)) by A2, ZF_MODEL:16;

then A5: ( E,f +* ((x. 2),a9) |= (x. 2) 'in' (x. 0) iff E,f +* ((x. 2),a9) |= (x. 2) 'in' (x. 1) ) by ZF_MODEL:19;

( (f +* ((x. 2),a9)) . (x. 2) = a9 & (f +* ((x. 2),a9)) . (x. 0) = f . (x. 0) ) by FUNCT_7:32, FUNCT_7:128;

hence a in f . (x. 1) by A3, A5, A4, ZF_MODEL:13; :: thesis: verum

assume A6: a in f . (x. 1) ; :: thesis: a in f . (x. 0)

f . (x. 1) c= E by A1;

then reconsider a9 = a as Element of E by A6;

set g = f +* ((x. 2),a9);

A7: (f +* ((x. 2),a9)) . (x. 1) = f . (x. 1) by FUNCT_7:32;

for x being Variable st (f +* ((x. 2),a9)) . x <> f . x holds

x. 2 = x by FUNCT_7:32;

then E,f +* ((x. 2),a9) |= ((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)) by A2, ZF_MODEL:16;

then A8: ( E,f +* ((x. 2),a9) |= (x. 2) 'in' (x. 0) iff E,f +* ((x. 2),a9) |= (x. 2) 'in' (x. 1) ) by ZF_MODEL:19;

( (f +* ((x. 2),a9)) . (x. 2) = a9 & (f +* ((x. 2),a9)) . (x. 0) = f . (x. 0) ) by FUNCT_7:32, FUNCT_7:128;

hence a in f . (x. 0) by A6, A8, A7, ZF_MODEL:13; :: thesis: verum

hence E |= the_axiom_of_extensionality by ZF_MODEL:23; :: thesis: verum