Theorem xrsp0

Description: The poset 0 of the extended real numbers is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018) (Proof shortened by AV, 28-Sep-2020)

	Ref	Expression
Assertion	xrsp0	⊢ -∞ = ( 0. ‘ ℝ*𝑠 )

Proof

Step	Hyp	Ref	Expression
1		xrsex	⊢ ℝ*𝑠 ∈ V
2		xrsbas	⊢ ℝ* = ( Base ‘ ℝ*𝑠 )
3		eqid	⊢ ( glb ‘ ℝ*𝑠 ) = ( glb ‘ ℝ*𝑠 )
4		eqid	⊢ ( 0. ‘ ℝ*𝑠 ) = ( 0. ‘ ℝ*𝑠 )
5	2 3 4	p0val	⊢ ( ℝ*𝑠 ∈ V → ( 0. ‘ ℝ*𝑠 ) = ( ( glb ‘ ℝ*𝑠 ) ‘ ℝ* ) )
6	1 5	ax-mp	⊢ ( 0. ‘ ℝ*𝑠 ) = ( ( glb ‘ ℝ*𝑠 ) ‘ ℝ* )
7		ssid	⊢ ℝ* ⊆ ℝ*
8		xrslt	⊢ < = ( lt ‘ ℝ*𝑠 )
9		xrstos	⊢ ℝ*𝑠 ∈ Toset
10	9	a1i	⊢ ( ℝ* ⊆ ℝ* → ℝ*𝑠 ∈ Toset )
11		id	⊢ ( ℝ* ⊆ ℝ* → ℝ* ⊆ ℝ* )
12	2 8 10 11	tosglb	⊢ ( ℝ* ⊆ ℝ* → ( ( glb ‘ ℝ*𝑠 ) ‘ ℝ* ) = inf ( ℝ* , ℝ* , < ) )
13	7 12	ax-mp	⊢ ( ( glb ‘ ℝ*𝑠 ) ‘ ℝ* ) = inf ( ℝ* , ℝ* , < )
14		xrinfm	⊢ inf ( ℝ* , ℝ* , < ) = -∞
15	6 13 14	3eqtrri	⊢ -∞ = ( 0. ‘ ℝ*𝑠 )