# Metamath Proof Explorer

## Theorem xrsex

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

Ref Expression
Assertion xrsex ${⊢}{ℝ}_{𝑠}^{*}\in \mathrm{V}$

### Proof

Step Hyp Ref Expression
1 df-xrs ${⊢}{ℝ}_{𝑠}^{*}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{ℝ}^{*}⟩,⟨{+}_{\mathrm{ndx}},{+}_{𝑒}⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_{𝑒}⟩\right\}\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(\le \right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼if\left({x}\le {y},{y}{+}_{𝑒}\left(-{x}\right),{x}{+}_{𝑒}\left(-{y}\right)\right)\right)⟩\right\}$
2 tpex ${⊢}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{ℝ}^{*}⟩,⟨{+}_{\mathrm{ndx}},{+}_{𝑒}⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_{𝑒}⟩\right\}\in \mathrm{V}$
3 tpex ${⊢}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(\le \right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼if\left({x}\le {y},{y}{+}_{𝑒}\left(-{x}\right),{x}{+}_{𝑒}\left(-{y}\right)\right)\right)⟩\right\}\in \mathrm{V}$
4 2 3 unex ${⊢}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{ℝ}^{*}⟩,⟨{+}_{\mathrm{ndx}},{+}_{𝑒}⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_{𝑒}⟩\right\}\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(\le \right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼if\left({x}\le {y},{y}{+}_{𝑒}\left(-{x}\right),{x}{+}_{𝑒}\left(-{y}\right)\right)\right)⟩\right\}\in \mathrm{V}$
5 1 4 eqeltri ${⊢}{ℝ}_{𝑠}^{*}\in \mathrm{V}$