Metamath Proof Explorer

Theorem ixxf

Description: The set of intervals of extended reals maps to subsets of extended reals. (Contributed by FL, 14-Jun-2007) (Revised by Mario Carneiro, 16-Nov-2013)

		Ref	Expression
	Hypothesis	ixx.1	⊢ 𝑂 = ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ { 𝑧 ∈ ℝ^* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
	Assertion	ixxf	⊢ 𝑂 : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ^*

Proof

Step	Hyp	Ref	Expression
1		ixx.1	⊢ 𝑂 = ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ { 𝑧 ∈ ℝ^* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
2		xrex	⊢ ℝ^* ∈ V
3		ssrab2	⊢ { 𝑧 ∈ ℝ^* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } ⊆ ℝ^*
4	2 3	elpwi2	⊢ { 𝑧 ∈ ℝ^* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } ∈ 𝒫 ℝ^*
5	4	rgen2w	⊢ ∀ 𝑥 ∈ ℝ^* ∀ 𝑦 ∈ ℝ^* { 𝑧 ∈ ℝ^* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } ∈ 𝒫 ℝ^*
6	1	fmpo	⊢ ( ∀ 𝑥 ∈ ℝ^* ∀ 𝑦 ∈ ℝ^* { 𝑧 ∈ ℝ^* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } ∈ 𝒫 ℝ^* ↔ 𝑂 : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ^* )
7	5 6	mpbi	⊢ 𝑂 : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ^*