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	⊢ [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*