Theorem icoreelrn

Description: A class abstraction which is an element of the set of closed-below, open-above intervals of reals. (Contributed by ML, 1-Aug-2020)

	Ref	Expression
Hypothesis	icoreelrn.1	⊢ 𝐼 = ( [,) “ ( ℝ × ℝ ) )
Assertion	icoreelrn	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → { 𝑧 ∈ ℝ ∣ ( 𝐴 ≤ 𝑧 ∧ 𝑧 < 𝐵 ) } ∈ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		icoreelrn.1	⊢ 𝐼 = ( [,) “ ( ℝ × ℝ ) )
2		icoreval	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,) 𝐵 ) = { 𝑧 ∈ ℝ ∣ ( 𝐴 ≤ 𝑧 ∧ 𝑧 < 𝐵 ) } )
3		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ )
4		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
5		df-ico	⊢ [,) = ( 𝑎 ∈ ℝ* , 𝑏 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } )
6	5	ixxf	⊢ [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*
7		ffun	⊢ ( [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* → Fun [,) )
8	6 7	mp1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → Fun [,) )
9		rexpssxrxp	⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
10	6	fdmi	⊢ dom [,) = ( ℝ* × ℝ* )
11	9 10	sseqtrri	⊢ ( ℝ × ℝ ) ⊆ dom [,)
12	11	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℝ × ℝ ) ⊆ dom [,) )
13	3 4 8 12	elovimad	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,) 𝐵 ) ∈ ( [,) “ ( ℝ × ℝ ) ) )
14	13 1	eleqtrrdi	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,) 𝐵 ) ∈ 𝐼 )
15	2 14	eqeltrrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → { 𝑧 ∈ ℝ ∣ ( 𝐴 ≤ 𝑧 ∧ 𝑧 < 𝐵 ) } ∈ 𝐼 )