Theorem xrge0le

Description: The "less than or equal to" relation in the extended real numbers. (Contributed by Thierry Arnoux, 14-Mar-2018)

	Ref	Expression
Assertion	xrge0le	⊢ ≤ = ( le ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )

Proof

Step	Hyp	Ref	Expression
1		ovex	⊢ ( 0 [,] +∞ ) ∈ V
2		eqid	⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
3		xrsle	⊢ ≤ = ( le ‘ ℝ*𝑠 )
4	2 3	ressle	⊢ ( ( 0 [,] +∞ ) ∈ V → ≤ = ( le ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) )
5	1 4	ax-mp	⊢ ≤ = ( le ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )