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 S₁[ object , object ] means ex B being Ordinal st
( B = $1 & $2 = Collapse (E,B) );
deffunc H₁( 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 H₂( Ordinal) -> set = Collapse (E,$1);
A1: for x being object st x in A holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in A implies ex y being object st S₁[x,y] )
assume x in A ; :: thesis: ex y being object st S₁[x,y]
then reconsider B = x as Ordinal ;
take Collapse (E,B) ; :: thesis: S₁[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 object st x in A holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A1);
reconsider L = f as Sequence by A2, ORDINAL1:def 7;

A3: now :: thesis: for A being Ordinal st A in dom L holds
L . A = H₂(A)

let A be Ordinal; :: thesis: ( A in dom L implies L . A = H₂(A) )
assume A in dom L ; :: thesis: L . A = H₂(A)
then ex B being Ordinal st
( B = A & L . A = Collapse (E,B) ) by A2;
hence L . A = H₂(A) ; :: thesis: verum

end;

A4: for A being Ordinal
for x being object holds
( x = H₂(A) iff ex L being Sequence st
( x = H₁(L) & dom L = A & ( for B being Ordinal st B in A holds
L . B = H₁(L | B) ) ) ) by Def1;
for B being Ordinal st B in dom L holds
L . B = H₁(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 object 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 object ; :: 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; :: 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 object ; :: 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