Metamath Proof Explorer

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 ⊢ I = . ℝ 2
Assertion icoreelrnab ⊢ X ∈ I ↔ ∃ a ∈ ℝ ∃ b ∈ ℝ X = z ∈ ℝ | a ≤ z ∧ z < b

Proof

Step Hyp Ref Expression
1 icoreelrnab.1 ⊢ I = . ℝ 2
2 df-ima ⊢ . ℝ 2 = ran ⁡ . ↾ ℝ 2
3 1 2 eqtri ⊢ I = ran ⁡ . ↾ ℝ 2
4 3 eleq2i ⊢ X ∈ I ↔ X ∈ ran ⁡ . ↾ ℝ 2
5 icoreresf ⊢ . ↾ ℝ 2 : ℝ 2 ⟶ 𝒫 ℝ
6 ffn ⊢ . ↾ ℝ 2 : ℝ 2 ⟶ 𝒫 ℝ → . ↾ ℝ 2 Fn ℝ 2
7 ovelrn ⊢ . ↾ ℝ 2 Fn ℝ 2 → X ∈ ran ⁡ . ↾ ℝ 2 ↔ ∃ a ∈ ℝ ∃ b ∈ ℝ X = a . ↾ ℝ 2 b
8 5 6 7 mp2b ⊢ X ∈ ran ⁡ . ↾ ℝ 2 ↔ ∃ a ∈ ℝ ∃ b ∈ ℝ X = a . ↾ ℝ 2 b
9 4 8 bitri ⊢ X ∈ I ↔ ∃ a ∈ ℝ ∃ b ∈ ℝ X = a . ↾ ℝ 2 b
10 ovres ⊢ a ∈ ℝ ∧ b ∈ ℝ → a . ↾ ℝ 2 b = a b
11 10 eqeq2d ⊢ a ∈ ℝ ∧ b ∈ ℝ → X = a . ↾ ℝ 2 b ↔ X = a b
12 11 2rexbiia ⊢ ∃ a ∈ ℝ ∃ b ∈ ℝ X = a . ↾ ℝ 2 b ↔ ∃ a ∈ ℝ ∃ b ∈ ℝ X = a b
13 9 12 bitri ⊢ X ∈ I ↔ ∃ a ∈ ℝ ∃ b ∈ ℝ X = a b
14 icoreval ⊢ a ∈ ℝ ∧ b ∈ ℝ → a b = z ∈ ℝ | a ≤ z ∧ z < b
15 14 eqeq2d ⊢ a ∈ ℝ ∧ b ∈ ℝ → X = a b ↔ X = z ∈ ℝ | a ≤ z ∧ z < b
16 15 2rexbiia ⊢ ∃ a ∈ ℝ ∃ b ∈ ℝ X = a b ↔ ∃ a ∈ ℝ ∃ b ∈ ℝ X = z ∈ ℝ | a ≤ z ∧ z < b
17 13 16 bitri ⊢ X ∈ I ↔ ∃ a ∈ ℝ ∃ b ∈ ℝ X = z ∈ ℝ | a ≤ z ∧ z < b