let E be non empty set ; ex A being Ordinal st E = Collapse (E,A)
defpred S1[ object , object ] means ex A being Ordinal st
( $2 = A & $1 in Collapse (E,A) & ( for B being Ordinal st $1 in Collapse (E,B) holds
A c= B ) );
consider f being Function such that
A3:
( dom f = E & ( for x being object st x in E holds
S1[x,f . x] ) )
from CLASSES1:sch 1(A1);
for x being object st x in rng f holds
x is Ordinal
then consider A being Ordinal such that
A6:
rng f c= A
by ORDINAL1:24;
take
A
; E = Collapse (E,A)
thus
for x being object st x in E holds
x in Collapse (E,A)
TARSKI:def 3,XBOOLE_0:def 10 Collapse (E,A) c= Eproof
let x be
object ;
( x in E implies x in Collapse (E,A) )
assume A7:
x in E
;
x in Collapse (E,A)
then consider B being
Ordinal such that A8:
f . x = B
and A9:
x in Collapse (
E,
B)
and
for
C being
Ordinal st
x in Collapse (
E,
C) holds
B c= C
by A3;
B in rng f
by A3, A7, A8, FUNCT_1:def 3;
then
Collapse (
E,
B)
c= Collapse (
E,
A)
by Th4, A6, ORDINAL1:def 2;
hence
x in Collapse (
E,
A)
by A9;
verum
end;
thus
Collapse (E,A) c= E
by Th7; verum