:: The Contraction Lemma
:: by Grzegorz Bancerek
::
:: Received April 14, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
let E be non empty set ;
let A be Ordinal;
deffunc H1( T-Sequence) ->  set =  {  d where d is Element of E : for d1 being Element of E st d1 in d holds
ex C being Ordinal st
( C in dom $1 & d1 in union {($1 . C)} )  }  ;
func Collapse (E,A) ->  set  means :Def1: :: ZF_COLLA:def 1
 ex L being T-Sequence st
( it =  {  d where d is Element of E : for d1 being Element of E st d1 in d holds
ex B being Ordinal st
( B in dom L & d1 in union {(L . B)} )  }  & dom L = A & ( for B being Ordinal st B in A holds
L . B =  {  d1 where d1 is Element of E : for d being Element of E st d in d1 holds
ex C being Ordinal st
( C in dom (L | B) & d in union {((L | B) . C)} )  }  ) );
existence
 ex b1 being set ex L being T-Sequence st
( b1 =  {  d where d is Element of E : for d1 being Element of E st d1 in d holds
ex B being Ordinal st
( B in dom L & d1 in union {(L . B)} )  }  & dom L = A & ( for B being Ordinal st B in A holds
L . B =  {  d1 where d1 is Element of E : for d being Element of E st d in d1 holds
ex C being Ordinal st
( C in dom (L | B) & d in union {((L | B) . C)} )  }  ) )
proofend;
uniqueness
 for b1, b2 being set st ex L being T-Sequence st
( b1 =  {  d where d is Element of E : for d1 being Element of E st d1 in d holds
ex B being Ordinal st
( B in dom L & d1 in union {(L . B)} )  }  & dom L = A & ( for B being Ordinal st B in A holds
L . B =  {  d1 where d1 is Element of E : for d being Element of E st d in d1 holds
ex C being Ordinal st
( C in dom (L | B) & d in union {((L | B) . C)} )  }  ) ) & ex L being T-Sequence st
( b2 =  {  d where d is Element of E : for d1 being Element of E st d1 in d holds
ex B being Ordinal st
( B in dom L & d1 in union {(L . B)} )  }  & dom L = A & ( for B being Ordinal st B in A holds
L . B =  {  d1 where d1 is Element of E : for d being Element of E st d in d1 holds
ex C being Ordinal st
( C in dom (L | B) & d in union {((L | B) . C)} )  }  ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines Collapse ZF_COLLA:def_1_:_
 for E being non empty set
for A being Ordinal
for b3 being set holds
( b3 = Collapse (E,A) iff ex L being T-Sequence st
( b3 =  {  d where d is Element of E : for d1 being Element of E st d1 in d holds
ex B being Ordinal st
( B in dom L & d1 in union {(L . B)} )  }  & dom L = A & ( for B being Ordinal st B in A holds
L . B =  {  d1 where d1 is Element of E : for d being Element of E st d in d1 holds
ex C being Ordinal st
( C in dom (L | B) & d in union {((L | B) . C)} )  }  ) ) );

theorem Th1: :: ZF_COLLA:1
for E being non empty set
for A being Ordinal holds Collapse (E,A) =  {  d where d is Element of E : for d1 being Element of E st d1 in d holds
ex B being Ordinal st
( B in A & d1 in Collapse (E,B) )  }
proofend;

theorem :: ZF_COLLA:2
for E being non empty set
for d being Element of E holds
( ( for d1 being Element of E holds not d1 in d ) iff d in Collapse (E,{}) )
proofend;

theorem :: ZF_COLLA:3
for E being non empty set
for A being Ordinal
for d being Element of E holds
( d /\ E c= Collapse (E,A) iff d in Collapse (E,(succ A)) )
proofend;

theorem Th4: :: ZF_COLLA:4
for E being non empty set
for A, B being Ordinal st A c= B holds
Collapse (E,A) c= Collapse (E,B)
proofend;

theorem Th5: :: ZF_COLLA:5
for E being non empty set
for d being Element of E ex A being Ordinal st d in Collapse (E,A)
proofend;

theorem Th6: :: ZF_COLLA:6
for E being non empty set
for A being Ordinal
for d9, d being Element of E st d9 in d & d in Collapse (E,A) holds
( d9 in Collapse (E,A) & ex B being Ordinal st
( B in A & d9 in Collapse (E,B) ) )
proofend;

theorem Th7: :: ZF_COLLA:7
for E being non empty set
for A being Ordinal holds Collapse (E,A) c= E
proofend;

theorem Th8: :: ZF_COLLA:8
for E being non empty set ex A being Ordinal st E = Collapse (E,A)
proofend;

theorem Th9: :: ZF_COLLA:9
for E being non empty set ex f being Function st
( dom f = E & ( for d being Element of E holds f . d = f .: d ) )
proofend;

:: Definition of epsilon-isomorphism of two sets
definition
let f be Function;
let X, Y be set ;
predf 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 being set st x in X & y in X holds
( ex Z being set st
( Z = y & x in Z ) iff ex Z being set st
( f . y = Z & f . x in Z ) ) ) );
end;

:: deftheorem  defines is_epsilon-isomorphism_of ZF_COLLA:def_2_:_
 for f being Function
for X, Y being set holds
( f is_epsilon-isomorphism_of X,Y iff ( dom f = X & rng f = Y & f is one-to-one & ( for x, y being set st x in X & y in X holds
( ex Z being set st
( Z = y & x in Z ) iff ex Z being set st
( f . y = Z & f . x in Z ) ) ) ) );

definition
let X, Y be set ;
predX,Y are_epsilon-isomorphic  means :: ZF_COLLA:def 3
 ex f being Function st f is_epsilon-isomorphism_of X,Y;
end;

:: deftheorem  defines are_epsilon-isomorphic ZF_COLLA:def_3_:_
 for X, Y being set holds
( X,Y are_epsilon-isomorphic iff ex f being Function st f is_epsilon-isomorphism_of X,Y );

theorem Th10: :: ZF_COLLA:10
for E being non empty set
for f being Function st dom f = E & ( for d being Element of E holds f . d = f .: d ) holds
rng f is epsilon-transitive
proofend;

theorem Th11: :: ZF_COLLA:11
for E being non empty set st E |= the_axiom_of_extensionality holds
for u, v being Element of E st ( for w being Element of E holds
( w in u iff w in v ) ) holds
u = v
proofend;

:: [WP: ] Contraction_Lemma
theorem :: ZF_COLLA:12
for E being non empty set st E |= the_axiom_of_extensionality holds
ex X being set st
( X is epsilon-transitive & E,X are_epsilon-isomorphic )
proofend;