let E be non empty set ; :: thesis: for A being Ordinal
for d, d9 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 d, d9 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 d, d9 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;
Collapse (E,B) c= Collapse (E,A) by Th4, A3, ORDINAL1:def 2;
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