Theorem iooordt

Description: An open interval is open in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Assertion	iooordt	$$⊢\left(A,B\right)\in \mathrm{ordTop}\left(\le \right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{ran}\left(x\in {ℝ}^{*}⟼\left(x,\mathrm{+\infty }\right]\right)=\mathrm{ran}\left(x\in {ℝ}^{*}⟼\left(x,\mathrm{+\infty }\right]\right)$$
2		eqid	$$⊢\mathrm{ran}\left(x\in {ℝ}^{*}⟼\left[\mathrm{-\infty },x\right)\right)=\mathrm{ran}\left(x\in {ℝ}^{*}⟼\left[\mathrm{-\infty },x\right)\right)$$
3		eqid	$$⊢\mathrm{ran}\left(.\right)=\mathrm{ran}\left(.\right)$$
4	1 2 3	leordtval	$$⊢\mathrm{ordTop}\left(\le \right)=\mathrm{topGen}\left(\left(\mathrm{ran}\left(x\in {ℝ}^{*}⟼\left(x,\mathrm{+\infty }\right]\right)\cup \mathrm{ran}\left(x\in {ℝ}^{*}⟼\left[\mathrm{-\infty },x\right)\right)\right)\cup \mathrm{ran}\left(.\right)\right)$$
5		letop	$$⊢\mathrm{ordTop}\left(\le \right)\in \mathrm{Top}$$
6	4 5	eqeltrri	$$⊢\mathrm{topGen}\left(\left(\mathrm{ran}\left(x\in {ℝ}^{*}⟼\left(x,\mathrm{+\infty }\right]\right)\cup \mathrm{ran}\left(x\in {ℝ}^{*}⟼\left[\mathrm{-\infty },x\right)\right)\right)\cup \mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$$
7		tgclb	$$⊢\left(\mathrm{ran}\left(x\in {ℝ}^{*}⟼\left(x,\mathrm{+\infty }\right]\right)\cup \mathrm{ran}\left(x\in {ℝ}^{*}⟼\left[\mathrm{-\infty },x\right)\right)\right)\cup \mathrm{ran}\left(.\right)\in \mathrm{TopBases}\leftrightarrow \mathrm{topGen}\left(\left(\mathrm{ran}\left(x\in {ℝ}^{*}⟼\left(x,\mathrm{+\infty }\right]\right)\cup \mathrm{ran}\left(x\in {ℝ}^{*}⟼\left[\mathrm{-\infty },x\right)\right)\right)\cup \mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$$
8	6 7	mpbir	$$⊢\left(\mathrm{ran}\left(x\in {ℝ}^{*}⟼\left(x,\mathrm{+\infty }\right]\right)\cup \mathrm{ran}\left(x\in {ℝ}^{*}⟼\left[\mathrm{-\infty },x\right)\right)\right)\cup \mathrm{ran}\left(.\right)\in \mathrm{TopBases}$$
9		bastg	$$⊢\left(\mathrm{ran}\left(x\in {ℝ}^{*}⟼\left(x,\mathrm{+\infty }\right]\right)\cup \mathrm{ran}\left(x\in {ℝ}^{*}⟼\left[\mathrm{-\infty },x\right)\right)\right)\cup \mathrm{ran}\left(.\right)\in \mathrm{TopBases}\to \left(\mathrm{ran}\left(x\in {ℝ}^{*}⟼\left(x,\mathrm{+\infty }\right]\right)\cup \mathrm{ran}\left(x\in {ℝ}^{*}⟼\left[\mathrm{-\infty },x\right)\right)\right)\cup \mathrm{ran}\left(.\right)\subseteq \mathrm{topGen}\left(\left(\mathrm{ran}\left(x\in {ℝ}^{*}⟼\left(x,\mathrm{+\infty }\right]\right)\cup \mathrm{ran}\left(x\in {ℝ}^{*}⟼\left[\mathrm{-\infty },x\right)\right)\right)\cup \mathrm{ran}\left(.\right)\right)$$
10	8 9	ax-mp	$$⊢\left(\mathrm{ran}\left(x\in {ℝ}^{*}⟼\left(x,\mathrm{+\infty }\right]\right)\cup \mathrm{ran}\left(x\in {ℝ}^{*}⟼\left[\mathrm{-\infty },x\right)\right)\right)\cup \mathrm{ran}\left(.\right)\subseteq \mathrm{topGen}\left(\left(\mathrm{ran}\left(x\in {ℝ}^{*}⟼\left(x,\mathrm{+\infty }\right]\right)\cup \mathrm{ran}\left(x\in {ℝ}^{*}⟼\left[\mathrm{-\infty },x\right)\right)\right)\cup \mathrm{ran}\left(.\right)\right)$$
11	10 4	sseqtrri	$$⊢\left(\mathrm{ran}\left(x\in {ℝ}^{*}⟼\left(x,\mathrm{+\infty }\right]\right)\cup \mathrm{ran}\left(x\in {ℝ}^{*}⟼\left[\mathrm{-\infty },x\right)\right)\right)\cup \mathrm{ran}\left(.\right)\subseteq \mathrm{ordTop}\left(\le \right)$$
12		ssun2	$$⊢\mathrm{ran}\left(.\right)\subseteq \left(\mathrm{ran}\left(x\in {ℝ}^{*}⟼\left(x,\mathrm{+\infty }\right]\right)\cup \mathrm{ran}\left(x\in {ℝ}^{*}⟼\left[\mathrm{-\infty },x\right)\right)\right)\cup \mathrm{ran}\left(.\right)$$
13		ioorebas	$$⊢\left(A,B\right)\in \mathrm{ran}\left(.\right)$$
14	12 13	sselii	$$⊢\left(A,B\right)\in \left(\left(\mathrm{ran}\left(x\in {ℝ}^{*}⟼\left(x,\mathrm{+\infty }\right]\right)\cup \mathrm{ran}\left(x\in {ℝ}^{*}⟼\left[\mathrm{-\infty },x\right)\right)\right)\cup \mathrm{ran}\left(.\right)\right)$$
15	11 14	sselii	$$⊢\left(A,B\right)\in \mathrm{ordTop}\left(\le \right)$$