This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem icof

Description: The set of left-closed right-open intervals of extended reals maps to subsets of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

		Ref	Expression
	Assertion	icof	⊢ [,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ^*

Proof

Step	Hyp	Ref	Expression
1		eqidd	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) → { 𝑧 ∈ ℝ^* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } = { 𝑧 ∈ ℝ^* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
2		ssrab2	⊢ { 𝑧 ∈ ℝ^* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ⊆ ℝ^*
3		xrex	⊢ ℝ^* ∈ V
4	3	rabex	⊢ { 𝑧 ∈ ℝ^* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ V
5	4	elpw	⊢ ( { 𝑧 ∈ ℝ^* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ^* ↔ { 𝑧 ∈ ℝ^* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ⊆ ℝ^* )
6	2 5	mpbir	⊢ { 𝑧 ∈ ℝ^* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ^*
7	1 6	eqeltrrdi	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) → { 𝑧 ∈ ℝ^* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ^* )
8	7	rgen2	⊢ ∀ 𝑥 ∈ ℝ^* ∀ 𝑦 ∈ ℝ^* { 𝑧 ∈ ℝ^* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ^*
9		df-ico	⊢ [,) = ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ { 𝑧 ∈ ℝ^* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
10	9	fmpo	⊢ ( ∀ 𝑥 ∈ ℝ^* ∀ 𝑦 ∈ ℝ^* { 𝑧 ∈ ℝ^* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } ∈ 𝒫 ℝ^* ↔ [,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ^* )
11	8 10	mpbi	⊢ [,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ^*