:: by Grzegorz Bancerek

::

:: Received April 14, 1989

:: Copyright (c) 1990-2016 Association of Mizar Users

definition

let E be non empty set ;

let A be Ordinal;

deffunc H_{1}( 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)} ) } ;

ex b_{1} being set ex L being Sequence st

( b_{1} = { 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)} ) } ) )

for b_{1}, b_{2} being set st ex L being Sequence st

( b_{1} = { 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 Sequence st

( b_{2} = { 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

b_{1} = b_{2}

end;
let A be Ordinal;

deffunc H

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 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 L being 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)} ) } ) );

ex b

( b

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)} ) } ) )

proof end;

uniqueness for b

( b

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 Sequence st

( b

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

b

proof end;

:: deftheorem Def1 defines Collapse ZF_COLLA:def 1 :

for E being non empty set

for A being Ordinal

for b_{3} being set holds

( b_{3} = Collapse (E,A) iff ex L being Sequence st

( b_{3} = { 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)} ) } ) ) );

for E being non empty set

for A being Ordinal

for b

( b

( b

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) ) }

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) ) }

proof end;

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,{}) )

for d being Element of E holds

( ( for d1 being Element of E holds not d1 in d ) iff d in Collapse (E,{}) )

proof end;

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)) )

for A being Ordinal

for d being Element of E holds

( d /\ E c= Collapse (E,A) iff d in Collapse (E,(succ A)) )

proof end;

theorem Th6: :: ZF_COLLA:6

for E being non empty set

for A being Ordinal

for d, d9 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) ) )

for A being Ordinal

for d, d9 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) ) )

proof end;

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 ) )

( dom f = E & ( for d being Element of E holds f . d = f .: d ) )

proof end;

:: Definition of epsilon-isomorphism of two sets

:: 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 object 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 ) ) ) ) );

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

end;
pred X,Y are_epsilon-isomorphic means :: ZF_COLLA:def 3

ex f being Function st f is_epsilon-isomorphism_of X,Y;

ex f being Function st f is_epsilon-isomorphism_of X,Y;

:: 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 );

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

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

proof end;

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

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

proof end;

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 )

ex X being set st

( X is epsilon-transitive & E,X are_epsilon-isomorphic )

proof end;