This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem leordtvallem2

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

Ref Expression
Hypotheses leordtval.1 
|- A = ran ( x e. RR* |-> ( x (,] +oo ) )
leordtval.2 
|- B = ran ( x e. RR* |-> ( -oo [,) x ) )
Assertion leordtvallem2 
|- B = ran ( x e. RR* |-> { y e. RR* | -. x <_ y } )

Proof

Step Hyp Ref Expression
1 leordtval.1 
 |-  A = ran ( x e. RR* |-> ( x (,] +oo ) )
2 leordtval.2 
 |-  B = ran ( x e. RR* |-> ( -oo [,) x ) )
3 icossxr 
 |-  ( -oo [,) x ) C_ RR*
4 sseqin2 
 |-  ( ( -oo [,) x ) C_ RR* <-> ( RR* i^i ( -oo [,) x ) ) = ( -oo [,) x ) )
5 3 4 mpbi 
 |-  ( RR* i^i ( -oo [,) x ) ) = ( -oo [,) x )
6 mnfxr 
 |-  -oo e. RR*
7 simpl 
 |-  ( ( x e. RR* /\ y e. RR* ) -> x e. RR* )
8 elico1 
 |-  ( ( -oo e. RR* /\ x e. RR* ) -> ( y e. ( -oo [,) x ) <-> ( y e. RR* /\ -oo <_ y /\ y < x ) ) )
9 6 7 8 sylancr 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( y e. ( -oo [,) x ) <-> ( y e. RR* /\ -oo <_ y /\ y < x ) ) )
10 simpr 
 |-  ( ( x e. RR* /\ y e. RR* ) -> y e. RR* )
11 mnfle 
 |-  ( y e. RR* -> -oo <_ y )
12 10 11 jccir 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( y e. RR* /\ -oo <_ y ) )
13 12 biantrurd 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( y < x <-> ( ( y e. RR* /\ -oo <_ y ) /\ y < x ) ) )
14 df-3an 
 |-  ( ( y e. RR* /\ -oo <_ y /\ y < x ) <-> ( ( y e. RR* /\ -oo <_ y ) /\ y < x ) )
15 13 14 bitr4di 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( y < x <-> ( y e. RR* /\ -oo <_ y /\ y < x ) ) )
16 xrltnle 
 |-  ( ( y e. RR* /\ x e. RR* ) -> ( y < x <-> -. x <_ y ) )
17 16 ancoms 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( y < x <-> -. x <_ y ) )
18 9 15 17 3bitr2d 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( y e. ( -oo [,) x ) <-> -. x <_ y ) )
19 18 rabbi2dva 
 |-  ( x e. RR* -> ( RR* i^i ( -oo [,) x ) ) = { y e. RR* | -. x <_ y } )
20 5 19 eqtr3id 
 |-  ( x e. RR* -> ( -oo [,) x ) = { y e. RR* | -. x <_ y } )
21 20 mpteq2ia 
 |-  ( x e. RR* |-> ( -oo [,) x ) ) = ( x e. RR* |-> { y e. RR* | -. x <_ y } )
22 21 rneqi 
 |-  ran ( x e. RR* |-> ( -oo [,) x ) ) = ran ( x e. RR* |-> { y e. RR* | -. x <_ y } )
23 2 22 eqtri 
 |-  B = ran ( x e. RR* |-> { y e. RR* | -. x <_ y } )