Theorem dfioo2

Description: Alternate definition of the set of open intervals of extended reals. (Contributed by NM, 1-Mar-2007) (Revised by Mario Carneiro, 1-Sep-2015)

	Ref	Expression
Assertion	dfioo2	$$⊢\left(.\right)=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{w\in ℝ|\left(x<w\wedge w<y\right)\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ioof	$$⊢\left(.\right):{ℝ}^{*}\times {ℝ}^{*}⟶𝒫ℝ$$
2		ffn	$$⊢\left(.\right):{ℝ}^{*}\times {ℝ}^{*}⟶𝒫ℝ\to \left(.\right)Fn\left({ℝ}^{*}\times {ℝ}^{*}\right)$$
3	1 2	ax-mp	$$⊢\left(.\right)Fn\left({ℝ}^{*}\times {ℝ}^{*}\right)$$
4		fnov	$$⊢\left(.\right)Fn\left({ℝ}^{*}\times {ℝ}^{*}\right)\leftrightarrow \left(.\right)=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left(x,y\right)\right)$$
5	3 4	mpbi	$$⊢\left(.\right)=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left(x,y\right)\right)$$
6		iooval2	$$⊢\left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to \left(x,y\right)=\left\{w\in ℝ|\left(x<w\wedge w<y\right)\right\}$$
7	6	mpoeq3ia	$$⊢\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left(x,y\right)\right)=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{w\in ℝ|\left(x<w\wedge w<y\right)\right\}\right)$$
8	5 7	eqtri	$$⊢\left(.\right)=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{w\in ℝ|\left(x<w\wedge w<y\right)\right\}\right)$$