Metamath Proof Explorer

Theorem reltxrnmnf

Description: For all extended real numbers not being minus infinity there is a smaller real number. (Contributed by AV, 5-Sep-2020)

Ref Expression
Assertion reltxrnmnf 
|- A. x e. RR* ( -oo < x -> E. y e. RR y < x )

Proof

Step Hyp Ref Expression
1 elxr 
 |-  ( x e. RR* <-> ( x e. RR \/ x = +oo \/ x = -oo ) )
2 reltre 
 |-  A. x e. RR E. y e. RR y < x
3 2 rspec 
 |-  ( x e. RR -> E. y e. RR y < x )
4 3 a1d 
 |-  ( x e. RR -> ( -oo < x -> E. y e. RR y < x ) )
5 breq1 
 |-  ( y = 0 -> ( y < x <-> 0 < x ) )
6 0red 
 |-  ( x = +oo -> 0 e. RR )
7 0ltpnf 
 |-  0 < +oo
8 breq2 
 |-  ( x = +oo -> ( 0 < x <-> 0 < +oo ) )
9 7 8 mpbiri 
 |-  ( x = +oo -> 0 < x )
10 5 6 9 rspcedvdw 
 |-  ( x = +oo -> E. y e. RR y < x )
11 10 a1d 
 |-  ( x = +oo -> ( -oo < x -> E. y e. RR y < x ) )
12 breq2 
 |-  ( x = -oo -> ( -oo < x <-> -oo < -oo ) )
13 mnfxr 
 |-  -oo e. RR*
14 nltmnf 
 |-  ( -oo e. RR* -> -. -oo < -oo )
15 14 pm2.21d 
 |-  ( -oo e. RR* -> ( -oo < -oo -> E. y e. RR y < x ) )
16 13 15 ax-mp 
 |-  ( -oo < -oo -> E. y e. RR y < x )
17 12 16 biimtrdi 
 |-  ( x = -oo -> ( -oo < x -> E. y e. RR y < x ) )
18 4 11 17 3jaoi 
 |-  ( ( x e. RR \/ x = +oo \/ x = -oo ) -> ( -oo < x -> E. y e. RR y < x ) )
19 1 18 sylbi 
 |-  ( x e. RR* -> ( -oo < x -> E. y e. RR y < x ) )
20 19 rgen 
 |-  A. x e. RR* ( -oo < x -> E. y e. RR y < x )