Theorem ioopos

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

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

Proof

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