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

proof

let x be set ; :: thesis: ( x in A implies ex y being set st S₁[x,y] )
assume x in A ; :: thesis: ex y being set st S₁[x,y]
then reconsider B = x as Ordinal ;
take y = Collapse E,B; :: thesis: S₁[x,y]
take B ; :: thesis: ( B = x & y = Collapse E,B )
thus ( B = x & y = Collapse E,B ) ; :: thesis: verum

end;

consider f being Function such that
A3: ( dom f = A & ( for x being set st x in A holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A1);
reconsider L = f as T-Sequence by A3, ORDINAL1:def 7;
deffunc H₁( 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 H₂( Ordinal) -> set = Collapse E,$1;

A4: now

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 A3;
hence L . A = H₂(A) ; :: thesis: verum

end;

A5: for A being Ordinal
for x being set holds
( x = H₂(A) iff ex L being T-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(A5, A4);
then A6: 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 A3, Def1;

now

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
A7: ( x = d & ( 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 & d1 in union {(L . B)} ) by A7;
take B ; :: thesis: ( B in A & d1 in Collapse E,B )
thus B in A by A3, A8; :: thesis: d1 in Collapse E,B
( L . B = Collapse E,B & union {(L . B)} = L . B ) by A4, A8, ZFMISC_1:31;
hence d1 in Collapse E,B by A8; :: 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 A7; :: 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 A6, 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
A9: ( x = 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 ) ) ) ;
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
A10: ( B in A & d in Collapse E,B ) by A9;
take B ; :: thesis: ( B in dom L & d in union {(L . B)} )
thus B in dom L by A3, A10; :: thesis: d in union {(L . B)}
( L . B = Collapse E,B & union {(L . B)} = L . B ) by A3, A4, A10, ZFMISC_1:31;
hence d in union {(L . B)} by A10; :: thesis: verum

end;

hence x in Collapse E,A by A6, A9; :: thesis: verum