This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem icof

Description: The set of left-closed right-open intervals of extended reals maps to subsets of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

		Ref	Expression
	Assertion	icof	$⊢ [.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$

Proof

Step	Hyp	Ref	Expression
1		eqidd	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to \{z \in ℝ^{} \| (x \leq z \land z < y)\} = \{z \in ℝ^{} \| (x \leq z \land z < y)\}$
2		ssrab2	$⊢ \{z \in ℝ^{} \| (x \leq z \land z < y)\} \subseteq ℝ^{}$
3		xrex	$⊢ ℝ^{*} \in V$
4	3	rabex	$⊢ \{z \in ℝ^{*} \| (x \leq z \land z < y)\} \in V$
5	4	elpw	$⊢ \{z \in ℝ^{} \| (x \leq z \land z < y)\} \in 𝒫 ℝ^{} \leftrightarrow \{z \in ℝ^{} \| (x \leq z \land z < y)\} \subseteq ℝ^{}$
6	2 5	mpbir	$⊢ \{z \in ℝ^{} \| (x \leq z \land z < y)\} \in 𝒫 ℝ^{}$
7	1 6	eqeltrrdi	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to \{z \in ℝ^{} \| (x \leq z \land z < y)\} \in 𝒫 ℝ^{}$
8	7	rgen2	$⊢ \forall x \in ℝ^{} \forall y \in ℝ^{} \{z \in ℝ^{} \| (x \leq z \land z < y)\} \in 𝒫 ℝ^{}$
9		df-ico	$⊢ [.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
10	9	fmpo	$⊢ \forall x \in ℝ^{} \forall y \in ℝ^{} \{z \in ℝ^{} \| (x \leq z \land z < y)\} \in 𝒫 ℝ^{} \leftrightarrow [.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
11	8 10	mpbi	$⊢ [.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$