Theorem leordtval

Description: The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Hypotheses	leordtval.1	$$⊢A=\mathrm{ran}\left(x\in {ℝ}^{*}⟼\left(x,\mathrm{+\infty }\right]\right)$$
	leordtval.2	$$⊢B=\mathrm{ran}\left(x\in {ℝ}^{*}⟼\left[\mathrm{-\infty },x\right)\right)$$
	leordtval.3	$$⊢C=\mathrm{ran}\left(.\right)$$
Assertion	leordtval	$$⊢\mathrm{ordTop}\left(\le \right)=\mathrm{topGen}\left(\left(A\cup B\right)\cup C\right)$$

Proof

Step	Hyp	Ref	Expression
1		leordtval.1	$$⊢A=\mathrm{ran}\left(x\in {ℝ}^{*}⟼\left(x,\mathrm{+\infty }\right]\right)$$
2		leordtval.2	$$⊢B=\mathrm{ran}\left(x\in {ℝ}^{*}⟼\left[\mathrm{-\infty },x\right)\right)$$
3		leordtval.3	$$⊢C=\mathrm{ran}\left(.\right)$$
4	1 2	leordtval2	$$⊢\mathrm{ordTop}\left(\le \right)=\mathrm{topGen}\left(\mathrm{fi}\left(A\cup B\right)\right)$$
5		letsr	$$⊢\le \in \mathrm{TosetRel}$$
6		ledm	$$⊢{ℝ}^{*}=\mathrm{dom}\le$$
7	1	leordtvallem1	$$⊢A=\mathrm{ran}\left(x\in {ℝ}^{*}⟼\left\{y\in {ℝ}^{*}|\neg y\le x\right\}\right)$$
8	1 2	leordtvallem2	$$⊢B=\mathrm{ran}\left(x\in {ℝ}^{*}⟼\left\{y\in {ℝ}^{*}|\neg x\le y\right\}\right)$$
9		df-ioo	$$⊢\left(.\right)=\left(a\in {ℝ}^{*},b\in {ℝ}^{*}⟼\left\{y\in {ℝ}^{*}|\left(a<y\wedge y<b\right)\right\}\right)$$
10		xrltnle	$$⊢\left(a\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to \left(a<y\leftrightarrow \neg y\le a\right)$$
11	10	adantlr	$$⊢\left(\left(a\in {ℝ}^{*}\wedge b\in {ℝ}^{*}\right)\wedge y\in {ℝ}^{*}\right)\to \left(a<y\leftrightarrow \neg y\le a\right)$$
12		xrltnle	$$⊢\left(y\in {ℝ}^{*}\wedge b\in {ℝ}^{*}\right)\to \left(y<b\leftrightarrow \neg b\le y\right)$$
13	12	ancoms	$$⊢\left(b\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to \left(y<b\leftrightarrow \neg b\le y\right)$$
14	13	adantll	$$⊢\left(\left(a\in {ℝ}^{*}\wedge b\in {ℝ}^{*}\right)\wedge y\in {ℝ}^{*}\right)\to \left(y<b\leftrightarrow \neg b\le y\right)$$
15	11 14	anbi12d	$$⊢\left(\left(a\in {ℝ}^{*}\wedge b\in {ℝ}^{*}\right)\wedge y\in {ℝ}^{*}\right)\to \left(\left(a<y\wedge y<b\right)\leftrightarrow \left(\neg y\le a\wedge \neg b\le y\right)\right)$$
16	15	rabbidva	$$⊢\left(a\in {ℝ}^{*}\wedge b\in {ℝ}^{*}\right)\to \left\{y\in {ℝ}^{*}|\left(a<y\wedge y<b\right)\right\}=\left\{y\in {ℝ}^{*}|\left(\neg y\le a\wedge \neg b\le y\right)\right\}$$
17	16	mpoeq3ia	$$⊢\left(a\in {ℝ}^{*},b\in {ℝ}^{*}⟼\left\{y\in {ℝ}^{*}|\left(a<y\wedge y<b\right)\right\}\right)=\left(a\in {ℝ}^{*},b\in {ℝ}^{*}⟼\left\{y\in {ℝ}^{*}|\left(\neg y\le a\wedge \neg b\le y\right)\right\}\right)$$
18	9 17	eqtri	$$⊢\left(.\right)=\left(a\in {ℝ}^{*},b\in {ℝ}^{*}⟼\left\{y\in {ℝ}^{*}|\left(\neg y\le a\wedge \neg b\le y\right)\right\}\right)$$
19	18	rneqi	$$⊢\mathrm{ran}\left(.\right)=\mathrm{ran}\left(a\in {ℝ}^{*},b\in {ℝ}^{*}⟼\left\{y\in {ℝ}^{*}|\left(\neg y\le a\wedge \neg b\le y\right)\right\}\right)$$
20	3 19	eqtri	$$⊢C=\mathrm{ran}\left(a\in {ℝ}^{*},b\in {ℝ}^{*}⟼\left\{y\in {ℝ}^{*}|\left(\neg y\le a\wedge \neg b\le y\right)\right\}\right)$$
21	6 7 8 20	ordtbas2	$$⊢\le \in \mathrm{TosetRel}\to \mathrm{fi}\left(A\cup B\right)=\left(A\cup B\right)\cup C$$
22	5 21	ax-mp	$$⊢\mathrm{fi}\left(A\cup B\right)=\left(A\cup B\right)\cup C$$
23	22	fveq2i	$$⊢\mathrm{topGen}\left(\mathrm{fi}\left(A\cup B\right)\right)=\mathrm{topGen}\left(\left(A\cup B\right)\cup C\right)$$
24	4 23	eqtri	$$⊢\mathrm{ordTop}\left(\le \right)=\mathrm{topGen}\left(\left(A\cup B\right)\cup C\right)$$