:: The Contraction Lemma :: by Grzegorz Bancerek :: :: Received April 14, 1989 :: Copyright (c) 1990-2021 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;