begin
:: 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:
theorem
theorem
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
:: 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 ) ) ) ) );
:: 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
canceled;
theorem
canceled;
theorem Th12:
theorem Th13:
theorem