icoreresf

Description: Closed-below, open-above intervals of reals map to subsets of reals. (Contributed by ML, 25-Jul-2020)

		Ref	Expression
	Assertion	icoreresf	$⊢ ({[.) ↾}_{ℝ^{2}}) : ℝ^{2} ⟶ 𝒫 ℝ$

Proof

Step	Hyp	Ref	Expression
1		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
2		df-ico	$⊢ [.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
3	2	ixxf	$⊢ [.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
4		ffn	$⊢ [.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{} \to [.) Fn (ℝ^{} \times ℝ^{*})$
5		fnssresb	$⊢ [.) Fn (ℝ^{} \times ℝ^{}) \to (({[.) ↾}_{ℝ^{2}}) Fn ℝ^{2} \leftrightarrow ℝ^{2} \subseteq ℝ^{} \times ℝ^{})$
6	3 4 5	mp2b	$⊢ ({[.) ↾}_{ℝ^{2}}) Fn ℝ^{2} \leftrightarrow ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
7	1 6	mpbir	$⊢ ({[.) ↾}_{ℝ^{2}}) Fn ℝ^{2}$
8		eqid	$⊢ {[.) ↾}_{ℝ^{2}} = {[.) ↾}_{ℝ^{2}}$
9	8	icorempo	$⊢ {[.) ↾}_{ℝ^{2}} = (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ \| (x \leq z \land z < y)\})$
10	9	rneqi	$⊢ ran ({[.) ↾}_{ℝ^{2}}) = ran (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ \| (x \leq z \land z < y)\})$
11		ssrab2	$⊢ \{z \in ℝ \| (x \leq z \land z < y)\} \subseteq ℝ$
12		reex	$⊢ ℝ \in V$
13	12	elpw2	$⊢ \{z \in ℝ \| (x \leq z \land z < y)\} \in 𝒫 ℝ \leftrightarrow \{z \in ℝ \| (x \leq z \land z < y)\} \subseteq ℝ$
14	11 13	mpbir	$⊢ \{z \in ℝ \| (x \leq z \land z < y)\} \in 𝒫 ℝ$
15	14	rgen2w	$⊢ \forall x \in ℝ \forall y \in ℝ \{z \in ℝ \| (x \leq z \land z < y)\} \in 𝒫 ℝ$
16		eqid	$⊢ (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ \| (x \leq z \land z < y)\}) = (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ \| (x \leq z \land z < y)\})$
17	16	rnmpo	$⊢ ran (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ \| (x \leq z \land z < y)\}) = \{l \| \exists x \in ℝ \exists y \in ℝ l = \{z \in ℝ \| (x \leq z \land z < y)\}\}$
18	17	eqabri	$⊢ l \in ran (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ \| (x \leq z \land z < y)\}) \leftrightarrow \exists x \in ℝ \exists y \in ℝ l = \{z \in ℝ \| (x \leq z \land z < y)\}$
19		simpl	$⊢ (\forall x \in ℝ \forall y \in ℝ \{z \in ℝ \| (x \leq z \land z < y)\} \in 𝒫 ℝ \land \exists x \in ℝ \exists y \in ℝ l = \{z \in ℝ \| (x \leq z \land z < y)\}) \to \forall x \in ℝ \forall y \in ℝ \{z \in ℝ \| (x \leq z \land z < y)\} \in 𝒫 ℝ$
20		simpr	$⊢ (\forall x \in ℝ \forall y \in ℝ \{z \in ℝ \| (x \leq z \land z < y)\} \in 𝒫 ℝ \land \exists x \in ℝ \exists y \in ℝ l = \{z \in ℝ \| (x \leq z \land z < y)\}) \to \exists x \in ℝ \exists y \in ℝ l = \{z \in ℝ \| (x \leq z \land z < y)\}$
21	19 20	r19.29d2r	$⊢ (\forall x \in ℝ \forall y \in ℝ \{z \in ℝ \| (x \leq z \land z < y)\} \in 𝒫 ℝ \land \exists x \in ℝ \exists y \in ℝ l = \{z \in ℝ \| (x \leq z \land z < y)\}) \to \exists x \in ℝ \exists y \in ℝ (\{z \in ℝ \| (x \leq z \land z < y)\} \in 𝒫 ℝ \land l = \{z \in ℝ \| (x \leq z \land z < y)\})$
22		eleq1	$⊢ l = \{z \in ℝ \| (x \leq z \land z < y)\} \to (l \in 𝒫 ℝ \leftrightarrow \{z \in ℝ \| (x \leq z \land z < y)\} \in 𝒫 ℝ)$
23	22	biimparc	$⊢ (\{z \in ℝ \| (x \leq z \land z < y)\} \in 𝒫 ℝ \land l = \{z \in ℝ \| (x \leq z \land z < y)\}) \to l \in 𝒫 ℝ$
24	23	a1i	$⊢ (x \in ℝ \land y \in ℝ) \to ((\{z \in ℝ \| (x \leq z \land z < y)\} \in 𝒫 ℝ \land l = \{z \in ℝ \| (x \leq z \land z < y)\}) \to l \in 𝒫 ℝ)$
25	24	rexlimivv	$⊢ \exists x \in ℝ \exists y \in ℝ (\{z \in ℝ \| (x \leq z \land z < y)\} \in 𝒫 ℝ \land l = \{z \in ℝ \| (x \leq z \land z < y)\}) \to l \in 𝒫 ℝ$
26	21 25	syl	$⊢ (\forall x \in ℝ \forall y \in ℝ \{z \in ℝ \| (x \leq z \land z < y)\} \in 𝒫 ℝ \land \exists x \in ℝ \exists y \in ℝ l = \{z \in ℝ \| (x \leq z \land z < y)\}) \to l \in 𝒫 ℝ$
27	26	ex	$⊢ \forall x \in ℝ \forall y \in ℝ \{z \in ℝ \| (x \leq z \land z < y)\} \in 𝒫 ℝ \to (\exists x \in ℝ \exists y \in ℝ l = \{z \in ℝ \| (x \leq z \land z < y)\} \to l \in 𝒫 ℝ)$
28	18 27	biimtrid	$⊢ \forall x \in ℝ \forall y \in ℝ \{z \in ℝ \| (x \leq z \land z < y)\} \in 𝒫 ℝ \to (l \in ran (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ \| (x \leq z \land z < y)\}) \to l \in 𝒫 ℝ)$
29	28	ssrdv	$⊢ \forall x \in ℝ \forall y \in ℝ \{z \in ℝ \| (x \leq z \land z < y)\} \in 𝒫 ℝ \to ran (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ \| (x \leq z \land z < y)\}) \subseteq 𝒫 ℝ$
30	15 29	ax-mp	$⊢ ran (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ \| (x \leq z \land z < y)\}) \subseteq 𝒫 ℝ$
31	10 30	eqsstri	$⊢ ran ({[.) ↾}_{ℝ^{2}}) \subseteq 𝒫 ℝ$
32		df-f	$⊢ ({[.) ↾}_{ℝ^{2}}) : ℝ^{2} ⟶ 𝒫 ℝ \leftrightarrow (({[.) ↾}_{ℝ^{2}}) Fn ℝ^{2} \land ran ({[.) ↾}_{ℝ^{2}}) \subseteq 𝒫 ℝ)$
33	7 31 32	mpbir2an	$⊢ ({[.) ↾}_{ℝ^{2}}) : ℝ^{2} ⟶ 𝒫 ℝ$

Metamath Proof Explorer

Theorem icoreresf

Proof