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 \in I \leftrightarrow \exists a \in ℝ \exists b \in ℝ X = \{z \in ℝ \| (a \leq z \land 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 \in I \leftrightarrow X \in ran ({[.) ↾}_{ℝ^{2}})$
5		icoreresf	$⊢ ({[.) ↾}_{ℝ^{2}}) : ℝ^{2} ⟶ 𝒫 ℝ$
6		ffn	$⊢ ({[.) ↾}_{ℝ^{2}}) : ℝ^{2} ⟶ 𝒫 ℝ \to ({[.) ↾}_{ℝ^{2}}) Fn ℝ^{2}$
7		ovelrn	$⊢ ({[.) ↾}_{ℝ^{2}}) Fn ℝ^{2} \to (X \in ran ({[.) ↾}_{ℝ^{2}}) \leftrightarrow \exists a \in ℝ \exists b \in ℝ X = a ({[.) ↾}_{ℝ^{2}}) b)$
8	5 6 7	mp2b	$⊢ X \in ran ({[.) ↾}_{ℝ^{2}}) \leftrightarrow \exists a \in ℝ \exists b \in ℝ X = a ({[.) ↾}_{ℝ^{2}}) b$
9	4 8	bitri	$⊢ X \in I \leftrightarrow \exists a \in ℝ \exists b \in ℝ X = a ({[.) ↾}_{ℝ^{2}}) b$
10		ovres	$⊢ (a \in ℝ \land b \in ℝ) \to a ({[.) ↾}_{ℝ^{2}}) b = [a, b)$
11	10	eqeq2d	$⊢ (a \in ℝ \land b \in ℝ) \to (X = a ({[.) ↾}_{ℝ^{2}}) b \leftrightarrow X = [a, b))$
12	11	2rexbiia	$⊢ \exists a \in ℝ \exists b \in ℝ X = a ({[.) ↾}_{ℝ^{2}}) b \leftrightarrow \exists a \in ℝ \exists b \in ℝ X = [a, b)$
13	9 12	bitri	$⊢ X \in I \leftrightarrow \exists a \in ℝ \exists b \in ℝ X = [a, b)$
14		icoreval	$⊢ (a \in ℝ \land b \in ℝ) \to [a, b) = \{z \in ℝ \| (a \leq z \land z < b)\}$
15	14	eqeq2d	$⊢ (a \in ℝ \land b \in ℝ) \to (X = [a, b) \leftrightarrow X = \{z \in ℝ \| (a \leq z \land z < b)\})$
16	15	2rexbiia	$⊢ \exists a \in ℝ \exists b \in ℝ X = [a, b) \leftrightarrow \exists a \in ℝ \exists b \in ℝ X = \{z \in ℝ \| (a \leq z \land z < b)\}$
17	13 16	bitri	$⊢ X \in I \leftrightarrow \exists a \in ℝ \exists b \in ℝ X = \{z \in ℝ \| (a \leq z \land z < b)\}$