The abstract of the Mizar article:

The Contraction Lemma

by

Grzegorz Bancerek

Received April 14, 1989

MML identifier: ZF_COLLA

[ Mizar article, MML identifier index ]

environ

 vocabulary ORDINAL1, FUNCT_1, RELAT_1, TARSKI, BOOLE, ZF_LANG, ZF_MODEL,
      ZF_COLLA;
 notation TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, RELAT_1, FUNCT_1, ZF_LANG,
      FUNCT_2, ORDINAL1, ZF_MODEL;
 constructors NAT_1, ZF_MODEL, MEMBERED, XBOOLE_0;
 clusters FUNCT_1, ZF_LANG, ORDINAL1, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;


begin

 reserve X,Y,Z for set,
         v,x,y,z for set,
         E for non empty set,
         A,B,C for Ordinal,
         L,L1 for T-Sequence,
         f,f1,f2,h for Function,
         d,d1,d2,d' for Element of E;

 definition let E,A;
  func Collapse (E,A) -> set means
:: ZF_COLLA:def 1

   ex L st
    it = { d : for d1 st d1 in d ex B st B in dom L & d1 in union { L.B } } &
    dom L = A &
    for B st B in A holds
     L.B = { d1 : for d st d in d1 ex C st C in dom(L|B) & d in
 union { L|B.C } };
 end;

theorem :: ZF_COLLA:1
   Collapse (E,A) = { d : for d1 st d1 in d ex B st B in A & d1 in Collapse
 (E,B) };

theorem :: ZF_COLLA:2
   (not ex d1 st d1 in d) iff d in Collapse (E,{});

theorem :: ZF_COLLA:3
    d /\ E c= Collapse (E,A) iff d in Collapse (E,succ A);

theorem :: ZF_COLLA:4
  A c= B implies Collapse (E,A) c= Collapse (E,B);

theorem :: ZF_COLLA:5
  ex A st d in Collapse (E,A);

theorem :: ZF_COLLA:6
  d' in d & d in Collapse (E,A) implies d' in Collapse (E,A) &
   ex B st B in A & d' in Collapse (E,B);

theorem :: ZF_COLLA:7
  Collapse (E,A) c= E;

theorem :: ZF_COLLA:8
  ex A st E = Collapse (E,A);

theorem :: ZF_COLLA:9
  ex f st dom f = E & for d holds f.d = f.:d;

:::::::::::::::::::::::::::::::::::::::::::::::::
::   Definition of epsilon-isomorphism of two sets   ::
:::::::::::::::::::::::::::::::::::::::::::::::::

 definition let f,X,Y;
  pred f is_epsilon-isomorphism_of X,Y means
:: ZF_COLLA:def 2
    dom f = X & rng f = Y & f is one-to-one &
   for x,y st x in X & y in X holds
    (ex Z st Z = y & x in Z) iff (ex Z st f.y = Z & f.x in Z);
 end;

 definition let X,Y;
  pred X,Y are_epsilon-isomorphic means
:: ZF_COLLA:def 3
    ex f st f is_epsilon-isomorphism_of X,Y;
 end;

canceled 2;

theorem :: ZF_COLLA:12
  (dom f = E & for d holds f.d = f.:d) implies rng f is epsilon-transitive;

 reserve f,g,h for (Function of VAR,E),
         u,v,w for (Element of E),
         x for Variable,
         a,b,c for set;

theorem :: ZF_COLLA:13
  E |= the_axiom_of_extensionality implies
  for u,v st for w holds w in u iff w in v holds u = v;

:::::::::::::::::::::::::::::::
::   The contraction lemma   ::
:::::::::::::::::::::::::::::::

theorem :: ZF_COLLA:14
    E |= the_axiom_of_extensionality implies
    ex X st X is epsilon-transitive & E,X are_epsilon-isomorphic;