:: ZF_COLLA semantic presentation 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)} ) } ) ) proof consider L being T-Sequence such that A1: dom L = A and A2: for B being Ordinal for L1 being T-Sequence st B in A & L1 = L | B holds L . B = H1(L1) from ORDINAL1:sch_4(); take x = { 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)} ) } ; ::_thesis: ex L being T-Sequence st ( x = { 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)} ) } ) ) take L ; ::_thesis: ( x = { 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)} ) } ) ) thus x = { 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)} ) } ; ::_thesis: ( 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)} ) } ) ) thus dom L = A by A1; ::_thesis: 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)} ) } let B be Ordinal; ::_thesis: ( B in A implies 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)} ) } ) assume B in A ; ::_thesis: 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)} ) } hence 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)} ) } by A2; ::_thesis: verum end; 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 proof let X1, X2 be set ; ::_thesis: ( ex L being T-Sequence st ( X1 = { 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 ( X2 = { 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)} ) } ) ) implies X1 = X2 ) given L being T-Sequence such that A3: ( X1 = { 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)} ) } ) ) ; ::_thesis: ( for L being T-Sequence holds ( not X2 = { 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)} ) } or not dom L = A or ex B being Ordinal st ( B in A & not 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)} ) } ) ) or X1 = X2 ) A4: ( dom L = A & ( for B being Ordinal for L1 being T-Sequence st B in A & L1 = L | B holds L . B = H1(L1) ) ) by A3; given L1 being T-Sequence such that A5: ( X2 = { 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 L1 & d1 in union {(L1 . B)} ) } & dom L1 = A & ( for B being Ordinal st B in A holds L1 . 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 (L1 | B) & d in union {((L1 | B) . C)} ) } ) ) ; ::_thesis: X1 = X2 A6: ( dom L1 = A & ( for B being Ordinal for L being T-Sequence st B in A & L = L1 | B holds L1 . B = H1(L) ) ) by A5; L = L1 from ORDINAL1:sch_3(A4, A6); hence X1 = X2 by A3, A5; ::_thesis: verum end; 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) ) } proof let E be non empty set ; ::_thesis: 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) ) } let A be Ordinal; ::_thesis: 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) ) } defpred S1[ set , set ] means ex B being Ordinal st ( B = \$1 & \$2 = Collapse (E,B) ); 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)} ) } ; deffunc H2( Ordinal) -> set = Collapse (E,\$1); A1: for x being set st x in A holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in A implies ex y being set st S1[x,y] ) assume x in A ; ::_thesis: ex y being set st S1[x,y] then reconsider B = x as Ordinal ; take Collapse (E,B) ; ::_thesis: S1[x, Collapse (E,B)] take B ; ::_thesis: ( B = x & Collapse (E,B) = Collapse (E,B) ) thus ( B = x & Collapse (E,B) = Collapse (E,B) ) ; ::_thesis: verum end; consider f being Function such that A2: ( dom f = A & ( for x being set st x in A holds S1[x,f . x] ) ) from CLASSES1:sch_1(A1); reconsider L = f as T-Sequence by A2, ORDINAL1:def_7; A3: now__::_thesis:_for_A_being_Ordinal_st_A_in_dom_L_holds_ L_._A_=_H2(A) let A be Ordinal; ::_thesis: ( A in dom L implies L . A = H2(A) ) assume A in dom L ; ::_thesis: L . A = H2(A) then ex B being Ordinal st ( B = A & L . A = Collapse (E,B) ) by A2; hence L . A = H2(A) ; ::_thesis: verum end; A4: for A being Ordinal for x being set holds ( x = H2(A) iff ex L being T-Sequence st ( x = H1(L) & dom L = A & ( for B being Ordinal st B in A holds L . B = H1(L | B) ) ) ) by Def1; for B being Ordinal st B in dom L holds L . B = H1(L | B) from ORDINAL1:sch_5(A4, A3); then A5: 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 dom L & d1 in union {(L . B)} ) } by A2, Def1; now__::_thesis:_for_x_being_set_st_x_in__{__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)}_)__}__holds_ x_in__{__d1_where_d1_is_Element_of_E_:_for_d_being_Element_of_E_st_d_in_d1_holds_ ex_B_being_Ordinal_st_ (_B_in_A_&_d_in_Collapse_(E,B)_)__}_ let x be set ; ::_thesis: ( x in { 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)} ) } implies x in { d1 where d1 is Element of E : for d being Element of E st d in d1 holds ex B being Ordinal st ( B in A & d in Collapse (E,B) ) } ) assume x in { 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)} ) } ; ::_thesis: x in { d1 where d1 is Element of E : for d being Element of E st d in d1 holds ex B being Ordinal st ( B in A & d in Collapse (E,B) ) } then consider d being Element of E such that A6: x = d and A7: 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)} ) ; 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 let d1 be Element of E; ::_thesis: ( d1 in d implies ex B being Ordinal st ( B in A & d1 in Collapse (E,B) ) ) assume d1 in d ; ::_thesis: ex B being Ordinal st ( B in A & d1 in Collapse (E,B) ) then consider B being Ordinal such that A8: B in dom L and A9: d1 in union {(L . B)} by A7; take B ; ::_thesis: ( B in A & d1 in Collapse (E,B) ) thus B in A by A2, A8; ::_thesis: d1 in Collapse (E,B) L . B = Collapse (E,B) by A3, A8; hence d1 in Collapse (E,B) by A9, ZFMISC_1:25; ::_thesis: verum end; hence x in { d1 where d1 is Element of E : for d being Element of E st d in d1 holds ex B being Ordinal st ( B in A & d in Collapse (E,B) ) } by A6; ::_thesis: verum end; hence Collapse (E,A) c= { 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) ) } by A5, TARSKI:def_3; :: according to XBOOLE_0:def_10 ::_thesis: { 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) ) } c= Collapse (E,A) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { 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) ) } or x in Collapse (E,A) ) assume x in { d1 where d1 is Element of E : for d being Element of E st d in d1 holds ex B being Ordinal st ( B in A & d in Collapse (E,B) ) } ; ::_thesis: x in Collapse (E,A) then consider d1 being Element of E such that A10: x = d1 and A11: for d being Element of E st d in d1 holds ex B being Ordinal st ( B in A & d in Collapse (E,B) ) ; for d being Element of E st d in d1 holds ex B being Ordinal st ( B in dom L & d in union {(L . B)} ) proof let d be Element of E; ::_thesis: ( d in d1 implies ex B being Ordinal st ( B in dom L & d in union {(L . B)} ) ) assume d in d1 ; ::_thesis: ex B being Ordinal st ( B in dom L & d in union {(L . B)} ) then consider B being Ordinal such that A12: B in A and A13: d in Collapse (E,B) by A11; take B ; ::_thesis: ( B in dom L & d in union {(L . B)} ) thus B in dom L by A2, A12; ::_thesis: d in union {(L . B)} L . B = Collapse (E,B) by A2, A3, A12; hence d in union {(L . B)} by A13, ZFMISC_1:25; ::_thesis: verum end; hence x in Collapse (E,A) by A5, A10; ::_thesis: verum 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,{}) ) proof let E be non empty set ; ::_thesis: for d being Element of E holds ( ( for d1 being Element of E holds not d1 in d ) iff d in Collapse (E,{}) ) let d be Element of E; ::_thesis: ( ( for d1 being Element of E holds not d1 in d ) iff d in Collapse (E,{}) ) A1: Collapse (E,{}) = { d9 where d9 is Element of E : for d1 being Element of E st d1 in d9 holds ex B being Ordinal st ( B in {} & d1 in Collapse (E,B) ) } by Th1; thus ( ( for d1 being Element of E holds not d1 in d ) implies d in Collapse (E,{}) ) ::_thesis: ( d in Collapse (E,{}) implies for d1 being Element of E holds not d1 in d ) proof assume for d1 being Element of E holds not d1 in d ; ::_thesis: d in Collapse (E,{}) then for d1 being Element of E st d1 in d holds ex B being Ordinal st ( B in {} & d1 in Collapse (E,B) ) ; hence d in Collapse (E,{}) by A1; ::_thesis: verum end; assume d in Collapse (E,{}) ; ::_thesis: for d1 being Element of E holds not d1 in d then A2: ex d9 being Element of E st ( d9 = d & ( for d1 being Element of E st d1 in d9 holds ex B being Ordinal st ( B in {} & d1 in Collapse (E,B) ) ) ) by A1; given d1 being Element of E such that A3: d1 in d ; ::_thesis: contradiction ex B being Ordinal st ( B in {} & d1 in Collapse (E,B) ) by A3, A2; hence contradiction ; ::_thesis: verum 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)) ) proof let E be non empty set ; ::_thesis: for A being Ordinal for d being Element of E holds ( d /\ E c= Collapse (E,A) iff d in Collapse (E,(succ A)) ) let A be Ordinal; ::_thesis: for d being Element of E holds ( d /\ E c= Collapse (E,A) iff d in Collapse (E,(succ A)) ) let d be Element of E; ::_thesis: ( d /\ E c= Collapse (E,A) iff d in Collapse (E,(succ A)) ) A1: Collapse (E,(succ A)) = { d9 where d9 is Element of E : for d1 being Element of E st d1 in d9 holds ex B being Ordinal st ( B in succ A & d1 in Collapse (E,B) ) } by Th1; thus ( d /\ E c= Collapse (E,A) implies d in Collapse (E,(succ A)) ) ::_thesis: ( d in Collapse (E,(succ A)) implies d /\ E c= Collapse (E,A) ) proof assume A2: for a being set st a in d /\ E holds a in Collapse (E,A) ; :: according to TARSKI:def_3 ::_thesis: d in Collapse (E,(succ A)) now__::_thesis:_for_d1_being_Element_of_E_st_d1_in_d_holds_ ex_B_being_Ordinal_st_ (_B_in_succ_A_&_d1_in_Collapse_(E,B)_) let d1 be Element of E; ::_thesis: ( d1 in d implies ex B being Ordinal st ( B in succ A & d1 in Collapse (E,B) ) ) assume d1 in d ; ::_thesis: ex B being Ordinal st ( B in succ A & d1 in Collapse (E,B) ) then d1 in d /\ E by XBOOLE_0:def_4; then d1 in Collapse (E,A) by A2; hence ex B being Ordinal st ( B in succ A & d1 in Collapse (E,B) ) by ORDINAL1:6; ::_thesis: verum end; hence d in Collapse (E,(succ A)) by A1; ::_thesis: verum end; assume d in Collapse (E,(succ A)) ; ::_thesis: d /\ E c= Collapse (E,A) then A3: ex e1 being Element of E st ( e1 = d & ( for d1 being Element of E st d1 in e1 holds ex B being Ordinal st ( B in succ A & d1 in Collapse (E,B) ) ) ) by A1; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in d /\ E or a in Collapse (E,A) ) assume A4: a in d /\ E ; ::_thesis: a in Collapse (E,A) then reconsider e = a as Element of E by XBOOLE_0:def_4; a in d by A4, XBOOLE_0:def_4; then consider B being Ordinal such that A5: B in succ A and A6: e in Collapse (E,B) by A3; A7: now__::_thesis:_for_d1_being_Element_of_E_st_d1_in_e_holds_ ex_C_being_Ordinal_st_ (_C_in_A_&_d1_in_Collapse_(E,C)_) Collapse (E,B) = { d9 where d9 is Element of E : for d1 being Element of E st d1 in d9 holds ex C being Ordinal st ( C in B & d1 in Collapse (E,C) ) } by Th1; then A8: ex d9 being Element of E st ( d9 = e & ( for d1 being Element of E st d1 in d9 holds ex C being Ordinal st ( C in B & d1 in Collapse (E,C) ) ) ) by A6; let d1 be Element of E; ::_thesis: ( d1 in e implies ex C being Ordinal st ( C in A & d1 in Collapse (E,C) ) ) assume d1 in e ; ::_thesis: ex C being Ordinal st ( C in A & d1 in Collapse (E,C) ) then consider C being Ordinal such that A9: ( C in B & d1 in Collapse (E,C) ) by A8; take C = C; ::_thesis: ( C in A & d1 in Collapse (E,C) ) B c= A by A5, ORDINAL1:22; hence ( C in A & d1 in Collapse (E,C) ) by A9; ::_thesis: verum end; Collapse (E,A) = { d9 where d9 is Element of E : for d1 being Element of E st d1 in d9 holds ex B being Ordinal st ( B in A & d1 in Collapse (E,B) ) } by Th1; hence a in Collapse (E,A) by A7; ::_thesis: verum end; 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) proof let E be non empty set ; ::_thesis: for A, B being Ordinal st A c= B holds Collapse (E,A) c= Collapse (E,B) let A, B be Ordinal; ::_thesis: ( A c= B implies Collapse (E,A) c= Collapse (E,B) ) assume A1: A c= B ; ::_thesis: Collapse (E,A) c= Collapse (E,B) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Collapse (E,A) or x in Collapse (E,B) ) assume x in Collapse (E,A) ; ::_thesis: x in Collapse (E,B) then x in { 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) ) } by Th1; then consider d being Element of E such that A2: d = x and A3: 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 d1 being Element of E st d1 in d holds ex C being Ordinal st ( C in B & d1 in Collapse (E,C) ) proof let d1 be Element of E; ::_thesis: ( d1 in d implies ex C being Ordinal st ( C in B & d1 in Collapse (E,C) ) ) assume d1 in d ; ::_thesis: ex C being Ordinal st ( C in B & d1 in Collapse (E,C) ) then consider C being Ordinal such that A4: ( C in A & d1 in Collapse (E,C) ) by A3; take C ; ::_thesis: ( C in B & d1 in Collapse (E,C) ) thus ( C in B & d1 in Collapse (E,C) ) by A1, A4; ::_thesis: verum end; then x in { d9 where d9 is Element of E : for d1 being Element of E st d1 in d9 holds ex C being Ordinal st ( C in B & d1 in Collapse (E,C) ) } by A2; hence x in Collapse (E,B) by Th1; ::_thesis: verum end; 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) proof let E be non empty set ; ::_thesis: for d being Element of E ex A being Ordinal st d in Collapse (E,A) let d be Element of E; ::_thesis: ex A being Ordinal st d in Collapse (E,A) defpred S1[ set ] means for A being Ordinal holds not \$1 in Collapse (E,A); defpred S2[ set , set ] means ex A being Ordinal st ( \$2 = A & \$1 in Collapse (E,A) & ( for B being Ordinal st \$1 in Collapse (E,B) holds A c= B ) ); consider X being set such that A1: for x being set holds ( x in X iff ( x in E & S1[x] ) ) from XBOOLE_0:sch_1(); now__::_thesis:_for_x_being_set_holds_not_x_in_X given x being set such that A2: x in X ; ::_thesis: contradiction consider m being set such that A3: m in X and A4: X misses m by A2, XREGULAR:1; reconsider m = m as Element of E by A1, A3; A5: now__::_thesis:_for_x_being_set_st_x_in_m_/\_E_holds_ ex_y_being_set_st_S2[x,y] let x be set ; ::_thesis: ( x in m /\ E implies ex y being set st S2[x,y] ) defpred S3[ Ordinal] means x in Collapse (E,\$1); assume A6: x in m /\ E ; ::_thesis: ex y being set st S2[x,y] then x in m by XBOOLE_0:def_4; then A7: not x in X by A4, XBOOLE_0:3; x in E by A6, XBOOLE_0:def_4; then A8: ex A being Ordinal st S3[A] by A1, A7; ex A being Ordinal st ( S3[A] & ( for B being Ordinal st S3[B] holds A c= B ) ) from ORDINAL1:sch_1(A8); hence ex y being set st S2[x,y] ; ::_thesis: verum end; consider f being Function such that A9: ( dom f = m /\ E & ( for x being set st x in m /\ E holds S2[x,f . x] ) ) from CLASSES1:sch_1(A5); for y being set st y in rng f holds y is Ordinal proof let y be set ; ::_thesis: ( y in rng f implies y is Ordinal ) assume y in rng f ; ::_thesis: y is Ordinal then consider x being set such that A10: x in dom f and A11: y = f . x by FUNCT_1:def_3; ex A being Ordinal st ( f . x = A & x in Collapse (E,A) & ( for B being Ordinal st x in Collapse (E,B) holds A c= B ) ) by A9, A10; hence y is Ordinal by A11; ::_thesis: verum end; then consider A being Ordinal such that A12: rng f c= A by ORDINAL1:24; for d being Element of E st d in m holds ex B being Ordinal st ( B in A & d in Collapse (E,B) ) proof let d be Element of E; ::_thesis: ( d in m implies ex B being Ordinal st ( B in A & d in Collapse (E,B) ) ) assume d in m ; ::_thesis: ex B being Ordinal st ( B in A & d in Collapse (E,B) ) then A13: d in m /\ E by XBOOLE_0:def_4; then consider B being Ordinal such that A14: f . d = B and A15: d in Collapse (E,B) and for C being Ordinal st d in Collapse (E,C) holds B c= C by A9; take B ; ::_thesis: ( B in A & d in Collapse (E,B) ) B in rng f by A9, A13, A14, FUNCT_1:def_3; hence ( B in A & d in Collapse (E,B) ) by A12, A15; ::_thesis: verum end; then m in { d9 where d9 is Element of E : for d being Element of E st d in d9 holds ex B being Ordinal st ( B in A & d in Collapse (E,B) ) } ; then m in Collapse (E,A) by Th1; hence contradiction by A1, A3; ::_thesis: verum end; hence ex A being Ordinal st d in Collapse (E,A) by A1; ::_thesis: verum end; 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) ) ) proof let E be non empty set ; ::_thesis: 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) ) ) let A be Ordinal; ::_thesis: 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) ) ) let d9, d be Element of E; ::_thesis: ( d9 in d & d in Collapse (E,A) implies ( d9 in Collapse (E,A) & ex B being Ordinal st ( B in A & d9 in Collapse (E,B) ) ) ) assume that A1: d9 in d and A2: d in Collapse (E,A) ; ::_thesis: ( d9 in Collapse (E,A) & ex B being Ordinal st ( B in A & d9 in Collapse (E,B) ) ) d in { d1 where d1 is Element of E : for d being Element of E st d in d1 holds ex B being Ordinal st ( B in A & d in Collapse (E,B) ) } by A2, Th1; then ex d1 being Element of E st ( d = d1 & ( for d being Element of E st d in d1 holds ex B being Ordinal st ( B in A & d in Collapse (E,B) ) ) ) ; then consider B being Ordinal such that A3: B in A and A4: d9 in Collapse (E,B) by A1; Collapse (E,B) c= Collapse (E,A) by Th4, A3, ORDINAL1:def_2; hence d9 in Collapse (E,A) by A4; ::_thesis: ex B being Ordinal st ( B in A & d9 in Collapse (E,B) ) thus ex B being Ordinal st ( B in A & d9 in Collapse (E,B) ) by A3, A4; ::_thesis: verum end; theorem Th7: :: ZF_COLLA:7 for E being non empty set for A being Ordinal holds Collapse (E,A) c= E proof let E be non empty set ; ::_thesis: for A being Ordinal holds Collapse (E,A) c= E let A be Ordinal; ::_thesis: Collapse (E,A) c= E let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Collapse (E,A) or x in E ) assume x in Collapse (E,A) ; ::_thesis: x in E then x in { 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) ) } by Th1; then ex d being Element of E st ( x = d & ( for d1 being Element of E st d1 in d holds ex B being Ordinal st ( B in A & d1 in Collapse (E,B) ) ) ) ; hence x in E ; ::_thesis: verum end; theorem Th8: :: ZF_COLLA:8 for E being non empty set ex A being Ordinal st E = Collapse (E,A) proof let E be non empty set ; ::_thesis: ex A being Ordinal st E = Collapse (E,A) defpred S1[ set , set ] means ex A being Ordinal st ( \$2 = A & \$1 in Collapse (E,A) & ( for B being Ordinal st \$1 in Collapse (E,B) holds A c= B ) ); A1: now__::_thesis:_for_x_being_set_st_x_in_E_holds_ ex_y_being_set_st_S1[x,y] let x be set ; ::_thesis: ( x in E implies ex y being set st S1[x,y] ) assume x in E ; ::_thesis: ex y being set st S1[x,y] then reconsider d = x as Element of E ; defpred S2[ Ordinal] means d in Collapse (E,\$1); A2: ex A being Ordinal st S2[A] by Th5; ex A being Ordinal st ( S2[A] & ( for B being Ordinal st S2[B] holds A c= B ) ) from ORDINAL1:sch_1(A2); hence ex y being set st S1[x,y] ; ::_thesis: verum end; consider f being Function such that A3: ( dom f = E & ( for x being set st x in E holds S1[x,f . x] ) ) from CLASSES1:sch_1(A1); for x being set st x in rng f holds x is Ordinal proof let x be set ; ::_thesis: ( x in rng f implies x is Ordinal ) assume x in rng f ; ::_thesis: x is Ordinal then consider y being set such that A4: y in dom f and A5: x = f . y by FUNCT_1:def_3; ex A being Ordinal st ( f . y = A & y in Collapse (E,A) & ( for C being Ordinal st y in Collapse (E,C) holds A c= C ) ) by A3, A4; hence x is Ordinal by A5; ::_thesis: verum end; then consider A being Ordinal such that A6: rng f c= A by ORDINAL1:24; take A ; ::_thesis: E = Collapse (E,A) thus for x being set st x in E holds x in Collapse (E,A) :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: Collapse (E,A) c= E proof let x be set ; ::_thesis: ( x in E implies x in Collapse (E,A) ) assume A7: x in E ; ::_thesis: x in Collapse (E,A) then consider B being Ordinal such that A8: f . x = B and A9: x in Collapse (E,B) and for C being Ordinal st x in Collapse (E,C) holds B c= C by A3; B in rng f by A3, A7, A8, FUNCT_1:def_3; then Collapse (E,B) c= Collapse (E,A) by Th4, A6, ORDINAL1:def_2; hence x in Collapse (E,A) by A9; ::_thesis: verum end; thus Collapse (E,A) c= E by Th7; ::_thesis: verum 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 ) ) proof let E be non empty set ; ::_thesis: ex f being Function st ( dom f = E & ( for d being Element of E holds f . d = f .: d ) ) defpred S1[ Ordinal, Function, non empty set ] means ( dom \$2 = Collapse (\$3,\$1) & ( for d being Element of E st d in Collapse (\$3,\$1) holds \$2 . d = \$2 .: d ) ); defpred S2[ Ordinal] means for f1, f2 being Function st S1[\$1,f1,E] & S1[\$1,f2,E] holds f1 = f2; defpred S3[ Ordinal] means ex f being Function st S1[\$1,f,E]; A1: for A, B being Ordinal for f being Function st A c= B & S1[B,f,E] holds S1[A,f | (Collapse (E,A)),E] proof let A, B be Ordinal; ::_thesis: for f being Function st A c= B & S1[B,f,E] holds S1[A,f | (Collapse (E,A)),E] let f be Function; ::_thesis: ( A c= B & S1[B,f,E] implies S1[A,f | (Collapse (E,A)),E] ) assume that A2: A c= B and A3: dom f = Collapse (E,B) and A4: for d being Element of E st d in Collapse (E,B) holds f . d = f .: d ; ::_thesis: S1[A,f | (Collapse (E,A)),E] A5: Collapse (E,A) c= Collapse (E,B) by A2, Th4; thus dom (f | (Collapse (E,A))) = Collapse (E,A) by A2, A3, Th4, RELAT_1:62; ::_thesis: for d being Element of E st d in Collapse (E,A) holds (f | (Collapse (E,A))) . d = (f | (Collapse (E,A))) .: d let d be Element of E; ::_thesis: ( d in Collapse (E,A) implies (f | (Collapse (E,A))) . d = (f | (Collapse (E,A))) .: d ) assume A6: d in Collapse (E,A) ; ::_thesis: (f | (Collapse (E,A))) . d = (f | (Collapse (E,A))) .: d for x being set st x in f .: d holds x in (f | (Collapse (E,A))) .: d proof let x be set ; ::_thesis: ( x in f .: d implies x in (f | (Collapse (E,A))) .: d ) A7: dom (f | (Collapse (E,A))) = Collapse (E,A) by A2, A3, Th4, RELAT_1:62; assume x in f .: d ; ::_thesis: x in (f | (Collapse (E,A))) .: d then consider z being set such that A8: z in dom f and A9: z in d and A10: x = f . z by FUNCT_1:def_6; dom f c= E by A3, Th7; then reconsider d1 = z as Element of E by A8; A11: d1 in Collapse (E,A) by A6, A9, Th6; then (f | (Collapse (E,A))) . z = f . z by FUNCT_1:49; hence x in (f | (Collapse (E,A))) .: d by A9, A10, A11, A7, FUNCT_1:def_6; ::_thesis: verum end; then A12: f .: d c= (f | (Collapse (E,A))) .: d by TARSKI:def_3; (f | (Collapse (E,A))) .: d c= f .: d by RELAT_1:128; then A13: f .: d = (f | (Collapse (E,A))) .: d by A12, XBOOLE_0:def_10; thus (f | (Collapse (E,A))) . d = f . d by A6, FUNCT_1:49 .= (f | (Collapse (E,A))) .: d by A4, A5, A6, A13 ; ::_thesis: verum end; A14: now__::_thesis:_for_A_being_Ordinal_st_(_for_B_being_Ordinal_st_B_in_A_holds_ S2[B]_)_holds_ S2[A] let A be Ordinal; ::_thesis: ( ( for B being Ordinal st B in A holds S2[B] ) implies S2[A] ) assume A15: for B being Ordinal st B in A holds S2[B] ; ::_thesis: S2[A] thus S2[A] ::_thesis: verum proof let f1, f2 be Function; ::_thesis: ( S1[A,f1,E] & S1[A,f2,E] implies f1 = f2 ) assume that A16: S1[A,f1,E] and A17: S1[A,f2,E] ; ::_thesis: f1 = f2 now__::_thesis:_for_x_being_set_st_x_in_Collapse_(E,A)_holds_ f1_._x_=_f2_._x let x be set ; ::_thesis: ( x in Collapse (E,A) implies f1 . x = f2 . x ) assume A18: x in Collapse (E,A) ; ::_thesis: f1 . x = f2 . x Collapse (E,A) c= E by Th7; then reconsider d = x as Element of E by A18; A19: f1 .: d = f2 .: d proof thus for y being set st y in f1 .: d holds y in f2 .: d :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: f2 .: d c= f1 .: d proof let y be set ; ::_thesis: ( y in f1 .: d implies y in f2 .: d ) assume y in f1 .: d ; ::_thesis: y in f2 .: d then consider z being set such that A20: z in dom f1 and A21: z in d and A22: y = f1 . z by FUNCT_1:def_6; dom f1 c= E by A16, Th7; then reconsider d1 = z as Element of E by A20; consider B being Ordinal such that A23: B in A and A24: d1 in Collapse (E,B) by A18, A21, Th6; B c= A by A23, ORDINAL1:def_2; then ( S1[B,f1 | (Collapse (E,B)),E] & S1[B,f2 | (Collapse (E,B)),E] ) by A1, A16, A17; then A25: f1 | (Collapse (E,B)) = f2 | (Collapse (E,B)) by A15, A23; f1 . d1 = (f1 | (Collapse (E,B))) . d1 by A24, FUNCT_1:49 .= f2 . d1 by A24, A25, FUNCT_1:49 ; hence y in f2 .: d by A16, A17, A20, A21, A22, FUNCT_1:def_6; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f2 .: d or y in f1 .: d ) assume y in f2 .: d ; ::_thesis: y in f1 .: d then consider z being set such that A26: z in dom f2 and A27: z in d and A28: y = f2 . z by FUNCT_1:def_6; dom f2 c= E by A17, Th7; then reconsider d1 = z as Element of E by A26; consider B being Ordinal such that A29: B in A and A30: d1 in Collapse (E,B) by A18, A27, Th6; B c= A by A29, ORDINAL1:def_2; then ( S1[B,f1 | (Collapse (E,B)),E] & S1[B,f2 | (Collapse (E,B)),E] ) by A1, A16, A17; then A31: f1 | (Collapse (E,B)) = f2 | (Collapse (E,B)) by A15, A29; f1 . d1 = (f1 | (Collapse (E,B))) . d1 by A30, FUNCT_1:49 .= f2 . d1 by A30, A31, FUNCT_1:49 ; hence y in f1 .: d by A16, A17, A26, A27, A28, FUNCT_1:def_6; ::_thesis: verum end; f1 . d = f1 .: d by A16, A18; hence f1 . x = f2 . x by A17, A18, A19; ::_thesis: verum end; hence f1 = f2 by A16, A17, FUNCT_1:2; ::_thesis: verum end; end; A32: for A being Ordinal holds S2[A] from ORDINAL1:sch_2(A14); A33: for A being Ordinal st ( for B being Ordinal st B in A holds S3[B] ) holds S3[A] proof let A be Ordinal; ::_thesis: ( ( for B being Ordinal st B in A holds S3[B] ) implies S3[A] ) assume for B being Ordinal st B in A holds ex f being Function st S1[B,f,E] ; ::_thesis: S3[A] defpred S4[ set , set ] means ex d being Element of E st ( d = \$1 & ( for x being set holds ( x in \$2 iff ex d1 being Element of E ex B being Ordinal ex f being Function st ( d1 in d & B in A & d1 in Collapse (E,B) & S1[B,f,E] & x = f . d1 ) ) ) ); A34: for x being set st x in Collapse (E,A) holds ex y being set st S4[x,y] proof A35: Collapse (E,A) c= E by Th7; let x be set ; ::_thesis: ( x in Collapse (E,A) implies ex y being set st S4[x,y] ) assume x in Collapse (E,A) ; ::_thesis: ex y being set st S4[x,y] then reconsider d = x as Element of E by A35; defpred S5[ set , set ] means ex B being Ordinal ex f being Function st ( B in A & \$1 in Collapse (E,B) & S1[B,f,E] & \$2 = f . \$1 ); A36: for x, y, z being set st S5[x,y] & S5[x,z] holds y = z proof let x, y, z be set ; ::_thesis: ( S5[x,y] & S5[x,z] implies y = z ) given B1 being Ordinal, f1 being Function such that B1 in A and A37: x in Collapse (E,B1) and A38: S1[B1,f1,E] and A39: y = f1 . x ; ::_thesis: ( not S5[x,z] or y = z ) given B2 being Ordinal, f2 being Function such that B2 in A and A40: x in Collapse (E,B2) and A41: S1[B2,f2,E] and A42: z = f2 . x ; ::_thesis: y = z A43: now__::_thesis:_(_B2_c=_B1_implies_y_=_z_) assume B2 c= B1 ; ::_thesis: y = z then S1[B2,f1 | (Collapse (E,B2)),E] by A1, A38; then f1 | (Collapse (E,B2)) = f2 by A32, A41; hence y = z by A39, A40, A42, FUNCT_1:49; ::_thesis: verum end; now__::_thesis:_(_B1_c=_B2_implies_y_=_z_) assume B1 c= B2 ; ::_thesis: y = z then S1[B1,f2 | (Collapse (E,B1)),E] by A1, A41; then f2 | (Collapse (E,B1)) = f1 by A32, A38; hence y = z by A37, A39, A42, FUNCT_1:49; ::_thesis: verum end; hence y = z by A43; ::_thesis: verum end; consider X being set such that A44: for y being set holds ( y in X iff ex x being set st ( x in d & S5[x,y] ) ) from TARSKI:sch_1(A36); take y = X; ::_thesis: S4[x,y] take d ; ::_thesis: ( d = x & ( for x being set holds ( x in y iff ex d1 being Element of E ex B being Ordinal ex f being Function st ( d1 in d & B in A & d1 in Collapse (E,B) & S1[B,f,E] & x = f . d1 ) ) ) ) thus d = x ; ::_thesis: for x being set holds ( x in y iff ex d1 being Element of E ex B being Ordinal ex f being Function st ( d1 in d & B in A & d1 in Collapse (E,B) & S1[B,f,E] & x = f . d1 ) ) let x be set ; ::_thesis: ( x in y iff ex d1 being Element of E ex B being Ordinal ex f being Function st ( d1 in d & B in A & d1 in Collapse (E,B) & S1[B,f,E] & x = f . d1 ) ) thus ( x in y implies ex d1 being Element of E ex B being Ordinal ex f being Function st ( d1 in d & B in A & d1 in Collapse (E,B) & S1[B,f,E] & x = f . d1 ) ) ::_thesis: ( ex d1 being Element of E ex B being Ordinal ex f being Function st ( d1 in d & B in A & d1 in Collapse (E,B) & S1[B,f,E] & x = f . d1 ) implies x in y ) proof assume x in y ; ::_thesis: ex d1 being Element of E ex B being Ordinal ex f being Function st ( d1 in d & B in A & d1 in Collapse (E,B) & S1[B,f,E] & x = f . d1 ) then consider y being set such that A45: y in d and A46: ex B being Ordinal ex f being Function st ( B in A & y in Collapse (E,B) & S1[B,f,E] & x = f . y ) by A44; consider B being Ordinal, f being Function such that A47: B in A and A48: y in Collapse (E,B) and A49: ( S1[B,f,E] & x = f . y ) by A46; Collapse (E,B) c= E by Th7; then reconsider d1 = y as Element of E by A48; take d1 ; ::_thesis: ex B being Ordinal ex f being Function st ( d1 in d & B in A & d1 in Collapse (E,B) & S1[B,f,E] & x = f . d1 ) take B ; ::_thesis: ex f being Function st ( d1 in d & B in A & d1 in Collapse (E,B) & S1[B,f,E] & x = f . d1 ) take f ; ::_thesis: ( d1 in d & B in A & d1 in Collapse (E,B) & S1[B,f,E] & x = f . d1 ) thus ( d1 in d & B in A & d1 in Collapse (E,B) & S1[B,f,E] & x = f . d1 ) by A45, A47, A48, A49; ::_thesis: verum end; given d1 being Element of E, B being Ordinal, f being Function such that A50: ( d1 in d & B in A & d1 in Collapse (E,B) & S1[B,f,E] & x = f . d1 ) ; ::_thesis: x in y thus x in y by A44, A50; ::_thesis: verum end; consider f being Function such that A51: ( dom f = Collapse (E,A) & ( for x being set st x in Collapse (E,A) holds S4[x,f . x] ) ) from CLASSES1:sch_1(A34); defpred S5[ Ordinal] means ( \$1 c= A implies S1[\$1,f | (Collapse (E,\$1)),E] ); A52: for B being Ordinal st ( for C being Ordinal st C in B holds S5[C] ) holds S5[B] proof let B be Ordinal; ::_thesis: ( ( for C being Ordinal st C in B holds S5[C] ) implies S5[B] ) assume A53: for C being Ordinal st C in B holds S5[C] ; ::_thesis: S5[B] assume A54: B c= A ; ::_thesis: S1[B,f | (Collapse (E,B)),E] then A55: Collapse (E,B) c= Collapse (E,A) by Th4; thus A56: dom (f | (Collapse (E,B))) = Collapse (E,B) by A51, A54, Th4, RELAT_1:62; ::_thesis: for d being Element of E st d in Collapse (E,B) holds (f | (Collapse (E,B))) . d = (f | (Collapse (E,B))) .: d let d be Element of E; ::_thesis: ( d in Collapse (E,B) implies (f | (Collapse (E,B))) . d = (f | (Collapse (E,B))) .: d ) assume A57: d in Collapse (E,B) ; ::_thesis: (f | (Collapse (E,B))) . d = (f | (Collapse (E,B))) .: d then (f | (Collapse (E,B))) . d = f . d by FUNCT_1:49; then consider d9 being Element of E such that A58: d9 = d and A59: for x being set holds ( x in (f | (Collapse (E,B))) . d iff ex d1 being Element of E ex B being Ordinal ex f being Function st ( d1 in d9 & B in A & d1 in Collapse (E,B) & S1[B,f,E] & x = f . d1 ) ) by A51, A55, A57; set X = (f | (Collapse (E,B))) . d; A60: (f | (Collapse (E,B))) . d c= (f | (Collapse (E,B))) .: d proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (f | (Collapse (E,B))) . d or x in (f | (Collapse (E,B))) .: d ) assume x in (f | (Collapse (E,B))) . d ; ::_thesis: x in (f | (Collapse (E,B))) .: d then consider d1 being Element of E, C being Ordinal, h being Function such that A61: d1 in d9 and C in A and A62: d1 in Collapse (E,C) and A63: S1[C,h,E] and A64: x = h . d1 by A59; consider C9 being Ordinal such that A65: C9 in B and A66: d1 in Collapse (E,C9) by A57, A58, A61, Th6; A67: for C being Ordinal for h being Function st C c= C9 & S1[C,h,E] & d1 in Collapse (E,C) & x = h . d1 holds x in (f | (Collapse (E,B))) .: d proof let C be Ordinal; ::_thesis: for h being Function st C c= C9 & S1[C,h,E] & d1 in Collapse (E,C) & x = h . d1 holds x in (f | (Collapse (E,B))) .: d let h be Function; ::_thesis: ( C c= C9 & S1[C,h,E] & d1 in Collapse (E,C) & x = h . d1 implies x in (f | (Collapse (E,B))) .: d ) assume that A68: C c= C9 and A69: S1[C,h,E] and A70: d1 in Collapse (E,C) and A71: x = h . d1 ; ::_thesis: x in (f | (Collapse (E,B))) .: d A72: C in B by A65, A68, ORDINAL1:12; then C c= A by A54, ORDINAL1:def_2; then S1[C,f | (Collapse (E,C)),E] by A53, A72; then A73: f | (Collapse (E,C)) = h by A32, A69; A74: Collapse (E,C) c= Collapse (E,B) by Th4, A72, ORDINAL1:def_2; then f | (Collapse (E,C)) = (f | (Collapse (E,B))) | (Collapse (E,C)) by FUNCT_1:51; then h . d1 = (f | (Collapse (E,B))) . d1 by A70, A73, FUNCT_1:49; hence x in (f | (Collapse (E,B))) .: d by A56, A58, A61, A70, A71, A74, FUNCT_1:def_6; ::_thesis: verum end; ( C9 c= C implies x in (f | (Collapse (E,B))) .: d ) proof assume C9 c= C ; ::_thesis: x in (f | (Collapse (E,B))) .: d then A75: S1[C9,h | (Collapse (E,C9)),E] by A1, A63; h . d1 = (h | (Collapse (E,C9))) . d1 by A66, FUNCT_1:49; hence x in (f | (Collapse (E,B))) .: d by A64, A66, A67, A75; ::_thesis: verum end; hence x in (f | (Collapse (E,B))) .: d by A62, A63, A64, A67; ::_thesis: verum end; (f | (Collapse (E,B))) .: d c= (f | (Collapse (E,B))) . d proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (f | (Collapse (E,B))) .: d or x in (f | (Collapse (E,B))) . d ) assume x in (f | (Collapse (E,B))) .: d ; ::_thesis: x in (f | (Collapse (E,B))) . d then consider y being set such that A76: y in dom (f | (Collapse (E,B))) and A77: y in d and A78: x = (f | (Collapse (E,B))) . y by FUNCT_1:def_6; Collapse (E,B) c= E by Th7; then reconsider d1 = y as Element of E by A56, A76; consider C being Ordinal such that A79: C in B and A80: d1 in Collapse (E,C) by A57, A77, Th6; Collapse (E,C) c= Collapse (E,B) by Th4, A79, ORDINAL1:def_2; then (f | (Collapse (E,B))) | (Collapse (E,C)) = f | (Collapse (E,C)) by FUNCT_1:51; then A81: (f | (Collapse (E,C))) . y = (f | (Collapse (E,B))) . y by A80, FUNCT_1:49; C c= A by A54, A79, ORDINAL1:def_2; then S1[C,f | (Collapse (E,C)),E] by A53, A79; hence x in (f | (Collapse (E,B))) . d by A54, A58, A59, A77, A78, A79, A80, A81; ::_thesis: verum end; hence (f | (Collapse (E,B))) . d = (f | (Collapse (E,B))) .: d by A60, XBOOLE_0:def_10; ::_thesis: verum end; A82: for B being Ordinal holds S5[B] from ORDINAL1:sch_2(A52); take f ; ::_thesis: S1[A,f,E] f | (dom f) = f by RELAT_1:68; hence S1[A,f,E] by A51, A82; ::_thesis: verum end; A83: for A being Ordinal holds S3[A] from ORDINAL1:sch_2(A33); consider A being Ordinal such that A84: E = Collapse (E,A) by Th8; consider f being Function such that A85: S1[A,f,E] by A83; take f ; ::_thesis: ( dom f = E & ( for d being Element of E holds f . d = f .: d ) ) thus dom f = E by A84, A85; ::_thesis: for d being Element of E holds f . d = f .: d let d be Element of E; ::_thesis: f . d = f .: d thus f . d = f .: d by A84, A85; ::_thesis: verum end; 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 proof let E be non empty set ; ::_thesis: 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 let f be Function; ::_thesis: ( dom f = E & ( for d being Element of E holds f . d = f .: d ) implies rng f is epsilon-transitive ) assume that A1: dom f = E and A2: for d being Element of E holds f . d = f .: d ; ::_thesis: rng f is epsilon-transitive let Y be set ; :: according to ORDINAL1:def_2 ::_thesis: ( not Y in rng f or Y c= rng f ) assume Y in rng f ; ::_thesis: Y c= rng f then consider b being set such that A3: b in dom f and A4: Y = f . b by FUNCT_1:def_3; reconsider d = b as Element of E by A1, A3; A5: f . d = f .: d by A2; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Y or a in rng f ) assume a in Y ; ::_thesis: a in rng f then ex c being set st ( c in dom f & c in d & a = f . c ) by A4, A5, FUNCT_1:def_6; hence a in rng f by FUNCT_1:def_3; ::_thesis: verum 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 proof let E be non empty set ; ::_thesis: ( E |= the_axiom_of_extensionality implies 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 ) assume A1: E |= the_axiom_of_extensionality ; ::_thesis: 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 All ((x. 0),(All ((x. 1),((All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)))))) = All ((x. 0),(x. 1),((All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)))) by ZF_LANG:7; then B2: E |= All ((x. 1),((All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)))) by A1, ZF_MODEL:23, ZF_MODEL:def_6; A3: for f being Function of VAR,E st ( for g being Function of VAR,E st ( for x being Variable st g . x <> f . x holds x. 2 = x ) holds ( g . (x. 2) in g . (x. 0) iff g . (x. 2) in g . (x. 1) ) ) holds f . (x. 0) = f . (x. 1) proof let f be Function of VAR,E; ::_thesis: ( ( for g being Function of VAR,E st ( for x being Variable st g . x <> f . x holds x. 2 = x ) holds ( g . (x. 2) in g . (x. 0) iff g . (x. 2) in g . (x. 1) ) ) implies f . (x. 0) = f . (x. 1) ) assume A4: for g being Function of VAR,E st ( for x being Variable st g . x <> f . x holds x. 2 = x ) holds ( g . (x. 2) in g . (x. 0) iff g . (x. 2) in g . (x. 1) ) ; ::_thesis: f . (x. 0) = f . (x. 1) A5: now__::_thesis:_for_g_being_Function_of_VAR,E_st_(_for_x_being_Variable_st_g_._x_<>_f_._x_holds_ x._2_=_x_)_holds_ E,g_|=_((x._2)_'in'_(x._0))_<=>_((x._2)_'in'_(x._1)) let g be Function of VAR,E; ::_thesis: ( ( for x being Variable st g . x <> f . x holds x. 2 = x ) implies E,g |= ((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)) ) assume A6: for x being Variable st g . x <> f . x holds x. 2 = x ; ::_thesis: E,g |= ((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)) A7: ( g . (x. 2) in g . (x. 1) iff E,g |= (x. 2) 'in' (x. 1) ) by ZF_MODEL:13; ( g . (x. 2) in g . (x. 0) iff E,g |= (x. 2) 'in' (x. 0) ) by ZF_MODEL:13; hence E,g |= ((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)) by A4, A6, A7, ZF_MODEL:19; ::_thesis: verum end; E,f |= (All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)) by B2, ZF_MODEL:def_5, ZF_MODEL:23; then ( E,f |= All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)))) implies E,f |= (x. 0) '=' (x. 1) ) by ZF_MODEL:18; hence f . (x. 0) = f . (x. 1) by A5, ZF_MODEL:12, ZF_MODEL:16; ::_thesis: verum end; for X, Y being Element of E st ( for Z being Element of E holds ( Z in X iff Z in Y ) ) holds X = Y proof set g = the Function of VAR,E; let X, Y be Element of E; ::_thesis: ( ( for Z being Element of E holds ( Z in X iff Z in Y ) ) implies X = Y ) assume A8: for Z being Element of E holds ( Z in X iff Z in Y ) ; ::_thesis: X = Y set g0 = the Function of VAR,E +* ((x. 0),X); A9: ( the Function of VAR,E +* ((x. 0),X)) . (x. 0) = X by FUNCT_7:128; A10: ( x. 0 = 5 + 0 & x. 1 = 5 + 1 ) by ZF_LANG:def_2; set f = ( the Function of VAR,E +* ((x. 0),X)) +* ((x. 1),Y); A11: x. 2 = 5 + 2 by ZF_LANG:def_2; A12: for h being Function of VAR,E st ( for x being Variable st h . x <> (( the Function of VAR,E +* ((x. 0),X)) +* ((x. 1),Y)) . x holds x. 2 = x ) holds ( h . (x. 2) in h . (x. 0) iff h . (x. 2) in h . (x. 1) ) proof let h be Function of VAR,E; ::_thesis: ( ( for x being Variable st h . x <> (( the Function of VAR,E +* ((x. 0),X)) +* ((x. 1),Y)) . x holds x. 2 = x ) implies ( h . (x. 2) in h . (x. 0) iff h . (x. 2) in h . (x. 1) ) ) assume for x being Variable st h . x <> (( the Function of VAR,E +* ((x. 0),X)) +* ((x. 1),Y)) . x holds x. 2 = x ; ::_thesis: ( h . (x. 2) in h . (x. 0) iff h . (x. 2) in h . (x. 1) ) then A13: ( h . (x. 0) = (( the Function of VAR,E +* ((x. 0),X)) +* ((x. 1),Y)) . (x. 0) & h . (x. 1) = (( the Function of VAR,E +* ((x. 0),X)) +* ((x. 1),Y)) . (x. 1) ) by A10, A11; ( h . (x. 2) in X iff h . (x. 2) in Y ) by A8; hence ( h . (x. 2) in h . (x. 0) iff h . (x. 2) in h . (x. 1) ) by A9, A13, FUNCT_7:32, FUNCT_7:128; ::_thesis: verum end; ( (( the Function of VAR,E +* ((x. 0),X)) +* ((x. 1),Y)) . (x. 1) = Y & (( the Function of VAR,E +* ((x. 0),X)) +* ((x. 1),Y)) . (x. 0) = ( the Function of VAR,E +* ((x. 0),X)) . (x. 0) ) by A10, FUNCT_7:32, FUNCT_7:128; hence X = Y by A3, A9, A12; ::_thesis: verum end; hence 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 ; ::_thesis: verum 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 ) proof let E be non empty set ; ::_thesis: ( E |= the_axiom_of_extensionality implies ex X being set st ( X is epsilon-transitive & E,X are_epsilon-isomorphic ) ) consider f being Function such that A1: dom f = E and A2: for d being Element of E holds f . d = f .: d by Th9; assume A3: E |= the_axiom_of_extensionality ; ::_thesis: ex X being set st ( X is epsilon-transitive & E,X are_epsilon-isomorphic ) A4: now__::_thesis:_for_a,_b_being_set_holds_ (_not_a_in_dom_f_or_not_b_in_dom_f_or_not_f_._a_=_f_._b_or_not_a_<>_b_) defpred S1[ Ordinal] means ex d1, d2 being Element of E st ( d1 in Collapse (E,\$1) & d2 in Collapse (E,\$1) & f . d1 = f . d2 & d1 <> d2 ); given a, b being set such that A5: ( a in dom f & b in dom f ) and A6: ( f . a = f . b & a <> b ) ; ::_thesis: contradiction reconsider d1 = a, d2 = b as Element of E by A1, A5; consider A1 being Ordinal such that A7: d1 in Collapse (E,A1) by Th5; consider A2 being Ordinal such that A8: d2 in Collapse (E,A2) by Th5; ( A1 c= A2 or A2 c= A1 ) ; then ( Collapse (E,A1) c= Collapse (E,A2) or Collapse (E,A2) c= Collapse (E,A1) ) by Th4; then A9: ex A being Ordinal st S1[A] by A6, A7, A8; consider A being Ordinal such that A10: ( S1[A] & ( for B being Ordinal st S1[B] holds A c= B ) ) from ORDINAL1:sch_1(A9); consider d1, d2 being Element of E such that A11: d1 in Collapse (E,A) and A12: d2 in Collapse (E,A) and A13: f . d1 = f . d2 and A14: d1 <> d2 by A10; consider w being Element of E such that A15: ( ( w in d1 & not w in d2 ) or ( w in d2 & not w in d1 ) ) by A3, A14, Th11; A16: ( f . d1 = f .: d1 & f . d2 = f .: d2 ) by A2; A17: now__::_thesis:_(_w_in_d2_implies_w_in_d1_) assume that A18: w in d2 and A19: not w in d1 ; ::_thesis: contradiction consider A1 being Ordinal such that A20: ( A1 in A & w in Collapse (E,A1) ) by A12, A18, Th6; f . w in f .: d2 by A1, A18, FUNCT_1:def_6; then consider a being set such that A21: a in dom f and A22: a in d1 and A23: f . w = f . a by A13, A16, FUNCT_1:def_6; reconsider v = a as Element of E by A1, A21; consider A2 being Ordinal such that A24: ( A2 in A & v in Collapse (E,A2) ) by A11, A22, Th6; ( A1 c= A2 or A2 c= A1 ) ; then ( Collapse (E,A1) c= Collapse (E,A2) or Collapse (E,A2) c= Collapse (E,A1) ) by Th4; hence contradiction by A10, A19, A22, A23, A20, A24, ORDINAL1:5; ::_thesis: verum end; now__::_thesis:_(_w_in_d1_implies_w_in_d2_) assume that A25: w in d1 and A26: not w in d2 ; ::_thesis: contradiction consider A1 being Ordinal such that A27: ( A1 in A & w in Collapse (E,A1) ) by A11, A25, Th6; f . w in f .: d1 by A1, A25, FUNCT_1:def_6; then consider a being set such that A28: a in dom f and A29: a in d2 and A30: f . w = f . a by A13, A16, FUNCT_1:def_6; reconsider v = a as Element of E by A1, A28; consider A2 being Ordinal such that A31: ( A2 in A & v in Collapse (E,A2) ) by A12, A29, Th6; ( A1 c= A2 or A2 c= A1 ) ; then ( Collapse (E,A1) c= Collapse (E,A2) or Collapse (E,A2) c= Collapse (E,A1) ) by Th4; hence contradiction by A10, A26, A29, A30, A27, A31, ORDINAL1:5; ::_thesis: verum end; hence contradiction by A15, A17; ::_thesis: verum end; take X = rng f; ::_thesis: ( X is epsilon-transitive & E,X are_epsilon-isomorphic ) thus X is epsilon-transitive by A1, A2, Th10; ::_thesis: E,X are_epsilon-isomorphic take f ; :: according to ZF_COLLA:def_3 ::_thesis: f is_epsilon-isomorphism_of E,X thus ( dom f = E & rng f = X ) by A1; :: according to ZF_COLLA:def_2 ::_thesis: ( f is one-to-one & ( for x, y being set st x in E & y in E holds ( ex Z being set st ( Z = y & x in Z ) iff ex Z being set st ( f . y = Z & f . x in Z ) ) ) ) thus f is one-to-one by A4, FUNCT_1:def_4; ::_thesis: for x, y being set st x in E & y in E holds ( ex Z being set st ( Z = y & x in Z ) iff ex Z being set st ( f . y = Z & f . x in Z ) ) let a, b be set ; ::_thesis: ( a in E & b in E implies ( ex Z being set st ( Z = b & a in Z ) iff ex Z being set st ( f . b = Z & f . a in Z ) ) ) assume that A32: a in E and A33: b in E ; ::_thesis: ( ex Z being set st ( Z = b & a in Z ) iff ex Z being set st ( f . b = Z & f . a in Z ) ) reconsider d2 = b as Element of E by A33; thus ( ex Z being set st ( Z = b & a in Z ) implies ex Z being set st ( Z = f . b & f . a in Z ) ) ::_thesis: ( ex Z being set st ( f . b = Z & f . a in Z ) implies ex Z being set st ( Z = b & a in Z ) ) proof given Z being set such that A34: ( Z = b & a in Z ) ; ::_thesis: ex Z being set st ( Z = f . b & f . a in Z ) A35: f . d2 = f .: d2 by A2; f . a in f .: d2 by A1, A32, A34, FUNCT_1:def_6; hence ex Z being set st ( Z = f . b & f . a in Z ) by A35; ::_thesis: verum end; given Z being set such that A36: ( Z = f . b & f . a in Z ) ; ::_thesis: ex Z being set st ( Z = b & a in Z ) f . d2 = f .: d2 by A2; then consider c being set such that A37: c in dom f and A38: c in d2 and A39: f . a = f . c by A36, FUNCT_1:def_6; a = c by A1, A4, A32, A37, A39; hence ex Z being set st ( Z = b & a in Z ) by A38; ::_thesis: verum end;