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 = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x R z \land z S y)\})$
	Assertion	ixxex	$⊢ O \in V$

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

Metamath Proof Explorer