Theorem ioopos

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

	Ref	Expression
Assertion	ioopos	|- ( 0 (,) +oo ) = { x e. RR | 0 < x }

Proof

Step	Hyp	Ref	Expression
1		0xr	|- 0 e. RR*
2		pnfxr	|- +oo e. RR*
3		iooval2	|- ( ( 0 e. RR* /\ +oo e. RR* ) -> ( 0 (,) +oo ) = { x e. RR | ( 0 < x /\ x < +oo ) } )
4	1 2 3	mp2an	|- ( 0 (,) +oo ) = { x e. RR | ( 0 < x /\ x < +oo ) }
5		ltpnf	|- ( x e. RR -> x < +oo )
6	5	biantrud	|- ( x e. RR -> ( 0 < x <-> ( 0 < x /\ x < +oo ) ) )
7	6	rabbiia	|- { x e. RR | 0 < x } = { x e. RR | ( 0 < x /\ x < +oo ) }
8	4 7	eqtr4i	|- ( 0 (,) +oo ) = { x e. RR | 0 < x }