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 ) )
consider f being Function such that
A1: dom f = E and
A2: for d being Element of E holds f . d = f .: d by Th9;
assume A3: E |= the_axiom_of_extensionality ; :: thesis: ex X being set st
( X is epsilon-transitive & E,X are_epsilon-isomorphic )

A4: now :: thesis: for a, b being object holds
( not a in dom f or not b in dom f or not f . a = f . b or not a <> b )

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 );
given a, b being object such that A5: ( a in dom f & b in dom f ) and
A6: ( f . a = f . b & a <> b ) ; :: thesis: contradiction
reconsider d1 = a, d2 = b as Element of E by A1, A5;
consider A1 being Ordinal such that
A7: d1 in Collapse (E,A1) by Th5;
consider A2 being Ordinal such that
A8: 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 A9: ex A being Ordinal st S₁[A] by A6, A7, A8;
consider A being Ordinal such that
A10: ( S₁[A] & ( for B being Ordinal st S₁[B] holds
A c= B ) ) from ORDINAL1:sch 1(A9);
consider d1, d2 being Element of E such that
A11: d1 in Collapse (E,A) and
A12: d2 in Collapse (E,A) and
A13: f . d1 = f . d2 and
A14: d1 <> d2 by A10;
consider w being Element of E such that
A15: ( ( w in d1 & not w in d2 ) or ( w in d2 & not w in d1 ) ) by A3, A14, Th11;
A16: ( f . d1 = f .: d1 & f . d2 = f .: d2 ) by A2;

A17: now :: thesis: ( w in d2 implies w in d1 )

assume that
A18: w in d2 and
A19: not w in d1 ; :: thesis: contradiction
consider A1 being Ordinal such that
A20: ( A1 in A & w in Collapse (E,A1) ) by A12, A18, Th6;
f . w in f .: d2 by A1, A18, FUNCT_1:def 6;
then consider a being object such that
A21: a in dom f and
A22: a in d1 and
A23: f . w = f . a by A13, A16, FUNCT_1:def 6;
reconsider v = a as Element of E by A1, A21;
consider A2 being Ordinal such that
A24: ( A2 in A & v in Collapse (E,A2) ) by A11, A22, 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;
hence contradiction by A10, A19, A22, A23, A20, A24, ORDINAL1:5; :: thesis: verum

end;

now :: thesis: ( w in d1 implies w in d2 )

assume that
A25: w in d1 and
A26: not w in d2 ; :: thesis: contradiction
consider A1 being Ordinal such that
A27: ( A1 in A & w in Collapse (E,A1) ) by A11, A25, Th6;
f . w in f .: d1 by A1, A25, FUNCT_1:def 6;
then consider a being object such that
A28: a in dom f and
A29: a in d2 and
A30: f . w = f . a by A13, A16, FUNCT_1:def 6;
reconsider v = a as Element of E by A1, A28;
consider A2 being Ordinal such that
A31: ( A2 in A & v in Collapse (E,A2) ) by A12, A29, 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;
hence contradiction by A10, A26, A29, A30, A27, A31, ORDINAL1:5; :: thesis: verum

end;

hence contradiction by A15, A17; :: thesis: verum

end;

take X = rng f; :: thesis: ( X is epsilon-transitive & E,X are_epsilon-isomorphic )
thus X is epsilon-transitive by A1, A2, Th10; :: 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 A1; :: according to ZF_COLLA:def 2 :: thesis: ( f is one-to-one & ( for x, y being object 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 ) ) ) )
thus f is one-to-one by A4, FUNCT_1:def 4; :: thesis: for x, y being object 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 object ; :: 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 that
A32: a in E and
A33: 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 ) )
reconsider d2 = b as Element of E by A33;
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 A34: ( Z = b & a in Z ) ; :: thesis: ex Z being set st
( Z = f . b & f . a in Z )
A35: f . d2 = f .: d2 by A2;
f . a in f .: d2 by A1, A32, A34, FUNCT_1:def 6;
hence ex Z being set st
( Z = f . b & f . a in Z ) by A35; :: thesis: verum

end;

given Z being set such that A36: ( 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 object such that
A37: c in dom f and
A38: c in d2 and
A39: f . a = f . c by A36, FUNCT_1:def 6;
a = c by A1, A4, A32, A37, A39;
hence ex Z being set st
( Z = b & a in Z ) by A38; :: thesis: verum