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