Theorem xrge0base

Description: The base of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 30-Jan-2017)

	Ref	Expression
Assertion	xrge0base	⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )

Proof

Step	Hyp	Ref	Expression
1		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
2		dfss2	⊢ ( ( 0 [,] +∞ ) ⊆ ℝ* ↔ ( ( 0 [,] +∞ ) ∩ ℝ* ) = ( 0 [,] +∞ ) )
3	1 2	mpbi	⊢ ( ( 0 [,] +∞ ) ∩ ℝ* ) = ( 0 [,] +∞ )
4		ovex	⊢ ( 0 [,] +∞ ) ∈ V
5		eqid	⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
6		xrsbas	⊢ ℝ* = ( Base ‘ ℝ*𝑠 )
7	5 6	ressbas	⊢ ( ( 0 [,] +∞ ) ∈ V → ( ( 0 [,] +∞ ) ∩ ℝ* ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) )
8	4 7	ax-mp	⊢ ( ( 0 [,] +∞ ) ∩ ℝ* ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
9	3 8	eqtr3i	⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )