let E be non empty set ; :: thesis: ( E |= the_axiom_of_extensionality implies ex X being set st
( X is epsilon-transitive & E,X are_epsilon-isomorphic ) )
assume A1: E |= the_axiom_of_extensionality ; :: thesis: ex X being set st
( X is epsilon-transitive & E,X are_epsilon-isomorphic )
consider f being Function such that
A2: ( dom f = E & ( for d being Element of E holds f . d = f .: d ) ) by Th9;
take X = rng f; :: thesis: ( X is epsilon-transitive & E,X are_epsilon-isomorphic )
thus X is epsilon-transitive by A2, Th12; :: thesis: E,X are_epsilon-isomorphic
take f ; :: according to ZF_COLLA:def 3 :: thesis: f is_epsilon-isomorphism_of E,X
thus ( dom f = E & rng f = X ) by A2; :: according to ZF_COLLA:def 2 :: thesis: ( f is one-to-one & ( for x, y being set st x in E & y in E holds
( ex Z being set st
( Z = y & x in Z ) iff ex Z being set st
( f . y = Z & f . x in Z ) ) ) )

A3: now

given a, b being set such that A4: ( a in dom f & b in dom f & f . a = f . b ) and
A5: a <> b ; :: thesis: contradiction
reconsider d1 = a, d2 = b as Element of E by A2, A4;
defpred S₁[ Ordinal] means ex d1, d2 being Element of E st
( d1 in Collapse E,$1 & d2 in Collapse E,$1 & f . d1 = f . d2 & d1 <> d2 );
consider A1 being Ordinal such that
A6: d1 in Collapse E,A1 by Th5;
consider A2 being Ordinal such that
A7: d2 in Collapse E,A2 by Th5;
( A1 c= A2 or A2 c= A1 ) ;
then ( Collapse E,A1 c= Collapse E,A2 or Collapse E,A2 c= Collapse E,A1 ) by Th4;
then A8: ex A being Ordinal st S₁[A] by A4, A5, A6, A7;
consider A being Ordinal such that
A9: ( S₁[A] & ( for B being Ordinal st S₁[B] holds
A c= B ) ) from ORDINAL1:sch 1(A8);
consider d1, d2 being Element of E such that
A10: ( d1 in Collapse E,A & d2 in Collapse E,A & f . d1 = f . d2 & d1 <> d2 ) by A9;
A11: ( f . d1 = f .: d1 & f . d2 = f .: d2 ) by A2;
consider w being Element of E such that
A12: ( ( w in d1 & not w in d2 ) or ( w in d2 & not w in d1 ) ) by A1, A10, Th13;

A13: now

assume A14: ( w in d1 & not w in d2 ) ; :: thesis: contradiction
then f . w in f .: d1 by A2, FUNCT_1:def 12;
then consider a being set such that
A15: ( a in dom f & a in d2 & f . w = f . a ) by A10, A11, FUNCT_1:def 12;
reconsider v = a as Element of E by A2, A15;
consider A1 being Ordinal such that
A16: ( A1 in A & w in Collapse E,A1 ) by A10, A14, Th6;
consider A2 being Ordinal such that
A17: ( A2 in A & v in Collapse E,A2 ) by A10, A15, Th6;
( A1 c= A2 or A2 c= A1 ) ;
then ( Collapse E,A1 c= Collapse E,A2 or Collapse E,A2 c= Collapse E,A1 ) by Th4;
then consider B being Ordinal such that
A18: ( B in A & w in Collapse E,B & v in Collapse E,B ) by A16, A17;
thus contradiction by A9, A14, A15, A18, ORDINAL1:7; :: thesis: verum

end;

now

assume A19: ( w in d2 & not w in d1 ) ; :: thesis: contradiction
then f . w in f .: d2 by A2, FUNCT_1:def 12;
then consider a being set such that
A20: ( a in dom f & a in d1 & f . w = f . a ) by A10, A11, FUNCT_1:def 12;
reconsider v = a as Element of E by A2, A20;
consider A1 being Ordinal such that
A21: ( A1 in A & w in Collapse E,A1 ) by A10, A19, Th6;
consider A2 being Ordinal such that
A22: ( A2 in A & v in Collapse E,A2 ) by A10, A20, Th6;
( A1 c= A2 or A2 c= A1 ) ;
then ( Collapse E,A1 c= Collapse E,A2 or Collapse E,A2 c= Collapse E,A1 ) by Th4;
then consider B being Ordinal such that
A23: ( B in A & w in Collapse E,B & v in Collapse E,B ) by A21, A22;
thus contradiction by A9, A19, A20, A23, ORDINAL1:7; :: thesis: verum

end;

hence contradiction by A12, A13; :: thesis: verum

end;

hence f is one-to-one by FUNCT_1:def 8; :: thesis: for x, y being set st x in E & y in E holds
( ex Z being set st
( Z = y & x in Z ) iff ex Z being set st
( f . y = Z & f . x in Z ) )
let a, b be set ; :: thesis: ( a in E & b in E implies ( ex Z being set st
( Z = b & a in Z ) iff ex Z being set st
( f . b = Z & f . a in Z ) ) )
assume A24: ( a in E & b in E ) ; :: thesis: ( ex Z being set st
( Z = b & a in Z ) iff ex Z being set st
( f . b = Z & f . a in Z ) )
then reconsider d1 = a, d2 = b as Element of E ;
thus ( ex Z being set st
( Z = b & a in Z ) implies ex Z being set st
( Z = f . b & f . a in Z ) ) :: thesis: ( ex Z being set st
( f . b = Z & f . a in Z ) implies ex Z being set st
( Z = b & a in Z ) )

proof

given Z being set such that A25: ( Z = b & a in Z ) ; :: thesis: ex Z being set st
( Z = f . b & f . a in Z )
( f . a in f .: d2 & f . d1 = f .: d1 & f . d2 = f .: d2 ) by A2, A24, A25, FUNCT_1:def 12;
hence ex Z being set st
( Z = f . b & f . a in Z ) ; :: thesis: verum

end;

given Z being set such that A26: ( Z = f . b & f . a in Z ) ; :: thesis: ex Z being set st
( Z = b & a in Z )
f . d2 = f .: d2 by A2;
then consider c being set such that
A27: ( c in dom f & c in d2 & f . a = f . c ) by A26, FUNCT_1:def 12;
a = c by A2, A3, A24, A27;
hence ex Z being set st
( Z = b & a in Z ) by A27; :: thesis: verum