Metamath Proof Explorer

Theorem reltre

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

Ref Expression
Assertion reltre 
|- A. x e. RR E. y e. RR y < x

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( y = ( x - 1 ) -> ( y < x <-> ( x - 1 ) < x ) )
2 peano2rem 
 |-  ( x e. RR -> ( x - 1 ) e. RR )
3 ltm1 
 |-  ( x e. RR -> ( x - 1 ) < x )
4 1 2 3 rspcedvdw 
 |-  ( x e. RR -> E. y e. RR y < x )
5 4 rgen 
 |-  A. x e. RR E. y e. RR y < x