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}$$