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	⊢ 𝑂 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
Assertion	ixxex	⊢ 𝑂 ∈ V

Proof

Step	Hyp	Ref	Expression
1		ixx.1	⊢ 𝑂 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
2		xrex	⊢ ℝ* ∈ V
3	2 2	xpex	⊢ ( ℝ* × ℝ* ) ∈ V
4	2	pwex	⊢ 𝒫 ℝ* ∈ V
5	3 4	xpex	⊢ ( ( ℝ* × ℝ* ) × 𝒫 ℝ* ) ∈ V
6	1	ixxf	⊢ 𝑂 : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*
7		fssxp	⊢ ( 𝑂 : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* → 𝑂 ⊆ ( ( ℝ* × ℝ* ) × 𝒫 ℝ* ) )
8	6 7	ax-mp	⊢ 𝑂 ⊆ ( ( ℝ* × ℝ* ) × 𝒫 ℝ* )
9	5 8	ssexi	⊢ 𝑂 ∈ V