ioopos

Description: The set of positive reals expressed as an open interval. (Contributed by NM, 7-May-2007)

		Ref	Expression
	Assertion	ioopos	$⊢ (0, +∞) = \{x \in ℝ \| 0 < x\}$

Step	Hyp	Ref	Expression
1		0xr	$⊢ 0 \in ℝ^{*}$
2		pnfxr	$⊢ +∞ \in ℝ^{*}$
3		iooval2	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{}) \to (0, +∞) = \{x \in ℝ \| (0 < x \land x < +∞)\}$
4	1 2 3	mp2an	$⊢ (0, +∞) = \{x \in ℝ \| (0 < x \land x < +∞)\}$
5		ltpnf	$⊢ x \in ℝ \to x < +∞$
6	5	biantrud	$⊢ x \in ℝ \to (0 < x \leftrightarrow (0 < x \land x < +∞))$
7	6	rabbiia	$⊢ \{x \in ℝ \| 0 < x\} = \{x \in ℝ \| (0 < x \land x < +∞)\}$
8	4 7	eqtr4i	$⊢ (0, +∞) = \{x \in ℝ \| 0 < x\}$

Metamath Proof Explorer