Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### The Contraction Lemma

by
Grzegorz Bancerek

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;
```