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

Metamath Proof Explorer

Theorem xrsex

Description: The extended real structure is a set. (Contributed by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion xrsex ℝ*𝑠 ∈ V

Proof

Step Hyp Ref Expression
1 df-xrs ⊢ ℝ*𝑠 = ( { ⟨ ( Base ‘ ndx ) , ℝ* ⟩ , ⟨ ( +g ‘ ndx ) , +𝑒 ⟩ , ⟨ ( .r ‘ ndx ) , ·e ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) ) ⟩ } )
2 tpex ⊢ { ⟨ ( Base ‘ ndx ) , ℝ* ⟩ , ⟨ ( +g ‘ ndx ) , +𝑒 ⟩ , ⟨ ( .r ‘ ndx ) , ·e ⟩ } ∈ V
3 tpex ⊢ { ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) ) ⟩ } ∈ V
4 2 3 unex ⊢ ( { ⟨ ( Base ‘ ndx ) , ℝ* ⟩ , ⟨ ( +g ‘ ndx ) , +𝑒 ⟩ , ⟨ ( .r ‘ ndx ) , ·e ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) ) ⟩ } ) ∈ V
5 1 4 eqeltri ⊢ ℝ*𝑠 ∈ V