Theorem xrsp1

Description: The poset 1 of the extended real numbers is plus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018)

	Ref	Expression
Assertion	xrsp1	⊢ +∞ = ( 1. ‘ ℝ*𝑠 )

Proof

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