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		0red	|- ( x = +oo -> 0 e. RR )
6		breq1	|- ( y = 0 -> ( y < x <-> 0 < x ) )
7	6	adantl	|- ( ( x = +oo /\ y = 0 ) -> ( y < x <-> 0 < x ) )
8		0ltpnf	|- 0 < +oo
9		breq2	|- ( x = +oo -> ( 0 < x <-> 0 < +oo ) )
10	8 9	mpbiri	|- ( x = +oo -> 0 < x )
11	5 7 10	rspcedvd	|- ( x = +oo -> E. y e. RR y < x )
12	11	a1d	|- ( x = +oo -> ( -oo < x -> E. y e. RR y < x ) )
13		breq2	|- ( x = -oo -> ( -oo < x <-> -oo < -oo ) )
14		mnfxr	|- -oo e. RR*
15		nltmnf	|- ( -oo e. RR* -> -. -oo < -oo )
16	15	pm2.21d	|- ( -oo e. RR* -> ( -oo < -oo -> E. y e. RR y < x ) )
17	14 16	ax-mp	|- ( -oo < -oo -> E. y e. RR y < x )
18	13 17	syl6bi	|- ( x = -oo -> ( -oo < x -> E. y e. RR y < x ) )
19	4 12 18	3jaoi	|- ( ( x e. RR \/ x = +oo \/ x = -oo ) -> ( -oo < x -> E. y e. RR y < x ) )
20	1 19	sylbi	|- ( x e. RR* -> ( -oo < x -> E. y e. RR y < x ) )
21	20	rgen	|- A. x e. RR* ( -oo < x -> E. y e. RR y < x )