let E be non empty set ; for A being Ordinal holds Collapse (E,A) = { d where d is Element of E : for d1 being Element of E st d1 in d holds
ex B being Ordinal st
( B in A & d1 in Collapse (E,B) ) }
let A be Ordinal; Collapse (E,A) = { d where d is Element of E : for d1 being Element of E st d1 in d holds
ex B being Ordinal st
( B in A & d1 in Collapse (E,B) ) }
defpred S1[ object , object ] means ex B being Ordinal st
( B = $1 & $2 = Collapse (E,B) );
deffunc H1( Sequence) -> set = { d where d is Element of E : for d1 being Element of E st d1 in d holds
ex C being Ordinal st
( C in dom $1 & d1 in union {($1 . C)} ) } ;
deffunc H2( Ordinal) -> set = Collapse (E,$1);
A1:
for x being object st x in A holds
ex y being object st S1[x,y]
consider f being Function such that
A2:
( dom f = A & ( for x being object st x in A holds
S1[x,f . x] ) )
from CLASSES1:sch 1(A1);
reconsider L = f as Sequence by A2, ORDINAL1:def 7;
A4:
for A being Ordinal
for x being object holds
( x = H2(A) iff ex L being Sequence st
( x = H1(L) & dom L = A & ( for B being Ordinal st B in A holds
L . B = H1(L | B) ) ) )
by Def1;
for B being Ordinal st B in dom L holds
L . B = H1(L | B)
from ORDINAL1:sch 5(A4, A3);
then A5:
Collapse (E,A) = { d where d is Element of E : for d1 being Element of E st d1 in d holds
ex B being Ordinal st
( B in dom L & d1 in union {(L . B)} ) }
by A2, Def1;
hence
Collapse (E,A) c= { d where d is Element of E : for d1 being Element of E st d1 in d holds
ex B being Ordinal st
( B in A & d1 in Collapse (E,B) ) }
by A5; XBOOLE_0:def 10 { d where d is Element of E : for d1 being Element of E st d1 in d holds
ex B being Ordinal st
( B in A & d1 in Collapse (E,B) ) } c= Collapse (E,A)
let x be object ; TARSKI:def 3 ( not x in { d where d is Element of E : for d1 being Element of E st d1 in d holds
ex B being Ordinal st
( B in A & d1 in Collapse (E,B) ) } or x in Collapse (E,A) )
assume
x 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) ) }
; x in Collapse (E,A)
then consider d1 being Element of E such that
A10:
x = d1
and
A11:
for d being Element of E st d in d1 holds
ex B being Ordinal st
( B in A & d in Collapse (E,B) )
;
for d being Element of E st d in d1 holds
ex B being Ordinal st
( B in dom L & d in union {(L . B)} )
hence
x in Collapse (E,A)
by A5, A10; verum