let E be non empty set ; :: thesis: for A being Ordinal
for d', d being Element of E st d' in d & d in Collapse E,A holds
( d' in Collapse E,A & ex B being Ordinal st
( B in A & d' in Collapse E,B ) )
let A be Ordinal; :: thesis: for d', d being Element of E st d' in d & d in Collapse E,A holds
( d' in Collapse E,A & ex B being Ordinal st
( B in A & d' in Collapse E,B ) )
let d', d be Element of E; :: thesis: ( d' in d & d in Collapse E,A implies ( d' in Collapse E,A & ex B being Ordinal st
( B in A & d' in Collapse E,B ) ) )
assume that
A1: d' in d and
A2: d in Collapse E,A ; :: thesis: ( d' in Collapse E,A & ex B being Ordinal st
( B in A & d' 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: d' 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 d' in Collapse E,A by A4; :: thesis: ex B being Ordinal st
( B in A & d' in Collapse E,B )
thus ex B being Ordinal st
( B in A & d' in Collapse E,B ) by A3, A4; :: thesis: verum