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

Metamath Proof Explorer

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 [,] +∞ ) ) )