:: The Contraction Lemma
:: by Grzegorz Bancerek
::
:: Received April 14, 1989
:: Copyright (c) 1990-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, ORDINAL1, FUNCT_1, SUBSET_1, RELAT_1, TARSKI, ZF_LANG,
ZF_MODEL, BVFUNC_2, CARD_1, XBOOLEAN, FUNCT_4, ARYTM_3, ZF_COLLA;
notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, RELAT_1, FUNCT_1, ZF_LANG,
ORDINAL1, NUMBERS, FUNCT_2, FUNCT_7, ZF_MODEL;
constructors NAT_1, MEMBERED, ZF_MODEL, FUNCT_7, NUMBERS;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, MEMBERED, ZF_LANG, RELSET_1;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
begin
reserve X,Y,Z for set,
x,y,z for object,
E for non empty set,
A,B,C for Ordinal ,
L,L1 for Sequence,
f,f1,f2,h for Function,
d,d1,d2,d9 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
d9 in d & d in Collapse (E,A) implies d9 in Collapse (E,A) & ex B
st B in A & d9 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;
theorem :: ZF_COLLA:10
(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 object;
theorem :: ZF_COLLA:11
E |= the_axiom_of_extensionality implies for u,v st for w holds
w in u iff w in v holds u = v;
::$N Contraction Lemma
theorem :: ZF_COLLA:12
E |= the_axiom_of_extensionality implies ex X st X is
epsilon-transitive & E,X are_epsilon-isomorphic;