This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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. ‘ ℝ^*_𝑠 )