Theorem ixxex

Description: The set of intervals of extended reals exists. (Contributed by Mario Carneiro, 3-Nov-2013) (Revised by Mario Carneiro, 17-Nov-2014)

	Ref	Expression
Hypothesis	ixx.1	$$⊢O=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{z\in {ℝ}^{*}|\left(xRz\wedge zSy\right)\right\}\right)$$
Assertion	ixxex	$$⊢O\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ixx.1	$$⊢O=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{z\in {ℝ}^{*}|\left(xRz\wedge zSy\right)\right\}\right)$$
2		xrex	$$⊢{ℝ}^{*}\in \mathrm{V}$$
3	2 2	xpex	$$⊢{ℝ}^{*}\times {ℝ}^{*}\in \mathrm{V}$$
4	2	pwex	$$⊢𝒫{ℝ}^{*}\in \mathrm{V}$$
5	3 4	xpex	$$⊢\left({ℝ}^{*}\times {ℝ}^{*}\right)\times 𝒫{ℝ}^{*}\in \mathrm{V}$$
6	1	ixxf	$$⊢O:{ℝ}^{*}\times {ℝ}^{*}⟶𝒫{ℝ}^{*}$$
7		fssxp	$$⊢O:{ℝ}^{*}\times {ℝ}^{*}⟶𝒫{ℝ}^{*}\to O\subseteq \left({ℝ}^{*}\times {ℝ}^{*}\right)\times 𝒫{ℝ}^{*}$$
8	6 7	ax-mp	$$⊢O\subseteq \left({ℝ}^{*}\times {ℝ}^{*}\right)\times 𝒫{ℝ}^{*}$$
9	5 8	ssexi	$$⊢O\in \mathrm{V}$$