Step |
Hyp |
Ref |
Expression |
1 |
|
ioomax |
|- ( -oo (,) +oo ) = RR |
2 |
|
ioof |
|- (,) : ( RR* X. RR* ) --> ~P RR |
3 |
|
ffn |
|- ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) ) |
4 |
2 3
|
ax-mp |
|- (,) Fn ( RR* X. RR* ) |
5 |
|
mnfxr |
|- -oo e. RR* |
6 |
|
pnfxr |
|- +oo e. RR* |
7 |
|
fnovrn |
|- ( ( (,) Fn ( RR* X. RR* ) /\ -oo e. RR* /\ +oo e. RR* ) -> ( -oo (,) +oo ) e. ran (,) ) |
8 |
4 5 6 7
|
mp3an |
|- ( -oo (,) +oo ) e. ran (,) |
9 |
1 8
|
eqeltrri |
|- RR e. ran (,) |
10 |
|
elssuni |
|- ( RR e. ran (,) -> RR C_ U. ran (,) ) |
11 |
9 10
|
ax-mp |
|- RR C_ U. ran (,) |
12 |
|
frn |
|- ( (,) : ( RR* X. RR* ) --> ~P RR -> ran (,) C_ ~P RR ) |
13 |
2 12
|
ax-mp |
|- ran (,) C_ ~P RR |
14 |
|
sspwuni |
|- ( ran (,) C_ ~P RR <-> U. ran (,) C_ RR ) |
15 |
13 14
|
mpbi |
|- U. ran (,) C_ RR |
16 |
11 15
|
eqssi |
|- RR = U. ran (,) |