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

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

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