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;
B c= A by A3, ORDINAL1:def 2;
then Collapse E,B c= Collapse E,A by Th4;
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