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 );
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;
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
A2: ( 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 A2, ORDINAL1:def 7;

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

end;

A4: 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(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

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:31; :: 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:31; :: thesis: verum

end;

hence x in Collapse E,A by A5, A10; :: thesis: verum