Metamath Proof Explorer

Theorem leordtvallem1

Description: Lemma for leordtval . (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypothesis leordtval.1 
|- A = ran ( x e. RR* |-> ( x (,] +oo ) )
Assertion leordtvallem1 
|- A = ran ( x e. RR* |-> { y e. RR* | -. y <_ x } )

Proof

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 } )