Theorem icoreelrnab

Description: Elementhood in the set of closed-below, open-above intervals of reals. (Contributed by ML, 27-Jul-2020)

	Ref	Expression
Hypothesis	icoreelrnab.1	⊢ 𝐼 = ( [,) “ ( ℝ × ℝ ) )
Assertion	icoreelrnab	⊢ ( 𝑋 ∈ 𝐼 ↔ ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ 𝑋 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } )

Proof

Step	Hyp	Ref	Expression
1		icoreelrnab.1	⊢ 𝐼 = ( [,) “ ( ℝ × ℝ ) )
2		df-ima	⊢ ( [,) “ ( ℝ × ℝ ) ) = ran ( [,) ↾ ( ℝ × ℝ ) )
3	1 2	eqtri	⊢ 𝐼 = ran ( [,) ↾ ( ℝ × ℝ ) )
4	3	eleq2i	⊢ ( 𝑋 ∈ 𝐼 ↔ 𝑋 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) )
5		icoreresf	⊢ ( [,) ↾ ( ℝ × ℝ ) ) : ( ℝ × ℝ ) ⟶ 𝒫 ℝ
6		ffn	⊢ ( ( [,) ↾ ( ℝ × ℝ ) ) : ( ℝ × ℝ ) ⟶ 𝒫 ℝ → ( [,) ↾ ( ℝ × ℝ ) ) Fn ( ℝ × ℝ ) )
7		ovelrn	⊢ ( ( [,) ↾ ( ℝ × ℝ ) ) Fn ( ℝ × ℝ ) → ( 𝑋 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) ↔ ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ 𝑋 = ( 𝑎 ( [,) ↾ ( ℝ × ℝ ) ) 𝑏 ) ) )
8	5 6 7	mp2b	⊢ ( 𝑋 ∈ ran ( [,) ↾ ( ℝ × ℝ ) ) ↔ ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ 𝑋 = ( 𝑎 ( [,) ↾ ( ℝ × ℝ ) ) 𝑏 ) )
9	4 8	bitri	⊢ ( 𝑋 ∈ 𝐼 ↔ ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ 𝑋 = ( 𝑎 ( [,) ↾ ( ℝ × ℝ ) ) 𝑏 ) )
10		ovres	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( 𝑎 ( [,) ↾ ( ℝ × ℝ ) ) 𝑏 ) = ( 𝑎 [,) 𝑏 ) )
11	10	eqeq2d	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( 𝑋 = ( 𝑎 ( [,) ↾ ( ℝ × ℝ ) ) 𝑏 ) ↔ 𝑋 = ( 𝑎 [,) 𝑏 ) ) )
12	11	2rexbiia	⊢ ( ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ 𝑋 = ( 𝑎 ( [,) ↾ ( ℝ × ℝ ) ) 𝑏 ) ↔ ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ 𝑋 = ( 𝑎 [,) 𝑏 ) )
13	9 12	bitri	⊢ ( 𝑋 ∈ 𝐼 ↔ ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ 𝑋 = ( 𝑎 [,) 𝑏 ) )
14		icoreval	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( 𝑎 [,) 𝑏 ) = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } )
15	14	eqeq2d	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( 𝑋 = ( 𝑎 [,) 𝑏 ) ↔ 𝑋 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) )
16	15	2rexbiia	⊢ ( ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ 𝑋 = ( 𝑎 [,) 𝑏 ) ↔ ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ 𝑋 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } )
17	13 16	bitri	⊢ ( 𝑋 ∈ 𝐼 ↔ ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ 𝑋 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } )