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 A1: ( d' in d & d in Collapse E,A ) ; :: thesis: ( d' in Collapse E,A & ex B being Ordinal st
( B in A & d' in Collapse E,B ) )
then 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 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
A2: ( B in A & d' in Collapse E,B ) by A1;
B c= A by A2, ORDINAL1:def 2;
then Collapse E,B c= Collapse E,A by Th4;
hence d' in Collapse E,A by A2; :: 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 A2; :: thesis: verum