| Step |
Hyp |
Ref |
Expression |
| 1 |
|
leordtval.1 |
|- A = ran ( x e. RR* |-> ( x (,] +oo ) ) |
| 2 |
|
iocssxr |
|- ( x (,] +oo ) C_ RR* |
| 3 |
|
sseqin2 |
|- ( ( x (,] +oo ) C_ RR* <-> ( RR* i^i ( x (,] +oo ) ) = ( x (,] +oo ) ) |
| 4 |
2 3
|
mpbi |
|- ( RR* i^i ( x (,] +oo ) ) = ( x (,] +oo ) |
| 5 |
|
simpl |
|- ( ( x e. RR* /\ y e. RR* ) -> x e. RR* ) |
| 6 |
|
pnfxr |
|- +oo e. RR* |
| 7 |
|
elioc1 |
|- ( ( x e. RR* /\ +oo e. RR* ) -> ( y e. ( x (,] +oo ) <-> ( y e. RR* /\ x < y /\ y <_ +oo ) ) ) |
| 8 |
5 6 7
|
sylancl |
|- ( ( x e. RR* /\ y e. RR* ) -> ( y e. ( x (,] +oo ) <-> ( y e. RR* /\ x < y /\ y <_ +oo ) ) ) |
| 9 |
|
simpr |
|- ( ( x e. RR* /\ y e. RR* ) -> y e. RR* ) |
| 10 |
|
pnfge |
|- ( y e. RR* -> y <_ +oo ) |
| 11 |
9 10
|
jccir |
|- ( ( x e. RR* /\ y e. RR* ) -> ( y e. RR* /\ y <_ +oo ) ) |
| 12 |
11
|
biantrurd |
|- ( ( x e. RR* /\ y e. RR* ) -> ( x < y <-> ( ( y e. RR* /\ y <_ +oo ) /\ x < y ) ) ) |
| 13 |
|
3anan32 |
|- ( ( y e. RR* /\ x < y /\ y <_ +oo ) <-> ( ( y e. RR* /\ y <_ +oo ) /\ x < y ) ) |
| 14 |
12 13
|
bitr4di |
|- ( ( x e. RR* /\ y e. RR* ) -> ( x < y <-> ( y e. RR* /\ x < y /\ y <_ +oo ) ) ) |
| 15 |
|
xrltnle |
|- ( ( x e. RR* /\ y e. RR* ) -> ( x < y <-> -. y <_ x ) ) |
| 16 |
8 14 15
|
3bitr2d |
|- ( ( x e. RR* /\ y e. RR* ) -> ( y e. ( x (,] +oo ) <-> -. y <_ x ) ) |
| 17 |
16
|
rabbi2dva |
|- ( x e. RR* -> ( RR* i^i ( x (,] +oo ) ) = { y e. RR* | -. y <_ x } ) |
| 18 |
4 17
|
eqtr3id |
|- ( x e. RR* -> ( x (,] +oo ) = { y e. RR* | -. y <_ x } ) |
| 19 |
18
|
mpteq2ia |
|- ( x e. RR* |-> ( x (,] +oo ) ) = ( x e. RR* |-> { y e. RR* | -. y <_ x } ) |
| 20 |
19
|
rneqi |
|- ran ( x e. RR* |-> ( x (,] +oo ) ) = ran ( x e. RR* |-> { y e. RR* | -. y <_ x } ) |
| 21 |
1 20
|
eqtri |
|- A = ran ( x e. RR* |-> { y e. RR* | -. y <_ x } ) |