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 ℝ 𝑠 * ↾ 𝑠 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 ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ = ℝ 𝑠 * ↾ 𝑠 0 +∞
6 xrsbas ⊢ ℝ * = Base ℝ 𝑠 *
7 5 6 ressbas ⊢ 0 +∞ ∈ V → 0 +∞ ∩ ℝ * = Base ℝ 𝑠 * ↾ 𝑠 0 +∞
8 4 7 ax-mp ⊢ 0 +∞ ∩ ℝ * = Base ℝ 𝑠 * ↾ 𝑠 0 +∞
9 3 8 eqtr3i ⊢ 0 +∞ = Base ℝ 𝑠 * ↾ 𝑠 0 +∞