# Metamath Proof Explorer

## Theorem leordtval2

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)$
Assertion leordtval2 ${⊢}\mathrm{ordTop}\left(\le \right)=\mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\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 letsr ${⊢}\le \in \mathrm{TosetRel}$
4 ledm ${⊢}{ℝ}^{*}=\mathrm{dom}\le$
5 1 leordtvallem1 ${⊢}{A}=\mathrm{ran}\left({x}\in {ℝ}^{*}⟼\left\{{y}\in {ℝ}^{*}|¬{y}\le {x}\right\}\right)$
6 1 2 leordtvallem2 ${⊢}{B}=\mathrm{ran}\left({x}\in {ℝ}^{*}⟼\left\{{y}\in {ℝ}^{*}|¬{x}\le {y}\right\}\right)$
7 4 5 6 ordtval ${⊢}\le \in \mathrm{TosetRel}\to \mathrm{ordTop}\left(\le \right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{{ℝ}^{*}\right\}\cup \left({A}\cup {B}\right)\right)\right)$
8 3 7 ax-mp ${⊢}\mathrm{ordTop}\left(\le \right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{{ℝ}^{*}\right\}\cup \left({A}\cup {B}\right)\right)\right)$
9 snex ${⊢}\left\{{ℝ}^{*}\right\}\in \mathrm{V}$
10 xrex ${⊢}{ℝ}^{*}\in \mathrm{V}$
11 10 pwex ${⊢}𝒫{ℝ}^{*}\in \mathrm{V}$
12 eqid ${⊢}\left({x}\in {ℝ}^{*}⟼\left({x},\mathrm{+\infty }\right]\right)=\left({x}\in {ℝ}^{*}⟼\left({x},\mathrm{+\infty }\right]\right)$
13 iocssxr ${⊢}\left({x},\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$
14 10 13 elpwi2 ${⊢}\left({x},\mathrm{+\infty }\right]\in 𝒫{ℝ}^{*}$
15 14 a1i ${⊢}{x}\in {ℝ}^{*}\to \left({x},\mathrm{+\infty }\right]\in 𝒫{ℝ}^{*}$
16 12 15 fmpti ${⊢}\left({x}\in {ℝ}^{*}⟼\left({x},\mathrm{+\infty }\right]\right):{ℝ}^{*}⟶𝒫{ℝ}^{*}$
17 frn ${⊢}\left({x}\in {ℝ}^{*}⟼\left({x},\mathrm{+\infty }\right]\right):{ℝ}^{*}⟶𝒫{ℝ}^{*}\to \mathrm{ran}\left({x}\in {ℝ}^{*}⟼\left({x},\mathrm{+\infty }\right]\right)\subseteq 𝒫{ℝ}^{*}$
18 16 17 ax-mp ${⊢}\mathrm{ran}\left({x}\in {ℝ}^{*}⟼\left({x},\mathrm{+\infty }\right]\right)\subseteq 𝒫{ℝ}^{*}$
19 1 18 eqsstri ${⊢}{A}\subseteq 𝒫{ℝ}^{*}$
20 eqid ${⊢}\left({x}\in {ℝ}^{*}⟼\left[\mathrm{-\infty },{x}\right)\right)=\left({x}\in {ℝ}^{*}⟼\left[\mathrm{-\infty },{x}\right)\right)$
21 icossxr ${⊢}\left[\mathrm{-\infty },{x}\right)\subseteq {ℝ}^{*}$
22 10 21 elpwi2 ${⊢}\left[\mathrm{-\infty },{x}\right)\in 𝒫{ℝ}^{*}$
23 22 a1i ${⊢}{x}\in {ℝ}^{*}\to \left[\mathrm{-\infty },{x}\right)\in 𝒫{ℝ}^{*}$
24 20 23 fmpti ${⊢}\left({x}\in {ℝ}^{*}⟼\left[\mathrm{-\infty },{x}\right)\right):{ℝ}^{*}⟶𝒫{ℝ}^{*}$
25 frn ${⊢}\left({x}\in {ℝ}^{*}⟼\left[\mathrm{-\infty },{x}\right)\right):{ℝ}^{*}⟶𝒫{ℝ}^{*}\to \mathrm{ran}\left({x}\in {ℝ}^{*}⟼\left[\mathrm{-\infty },{x}\right)\right)\subseteq 𝒫{ℝ}^{*}$
26 24 25 ax-mp ${⊢}\mathrm{ran}\left({x}\in {ℝ}^{*}⟼\left[\mathrm{-\infty },{x}\right)\right)\subseteq 𝒫{ℝ}^{*}$
27 2 26 eqsstri ${⊢}{B}\subseteq 𝒫{ℝ}^{*}$
28 19 27 unssi ${⊢}{A}\cup {B}\subseteq 𝒫{ℝ}^{*}$
29 11 28 ssexi ${⊢}{A}\cup {B}\in \mathrm{V}$
30 9 29 unex ${⊢}\left\{{ℝ}^{*}\right\}\cup \left({A}\cup {B}\right)\in \mathrm{V}$
31 ssun2 ${⊢}{A}\cup {B}\subseteq \left\{{ℝ}^{*}\right\}\cup \left({A}\cup {B}\right)$
32 fiss ${⊢}\left(\left\{{ℝ}^{*}\right\}\cup \left({A}\cup {B}\right)\in \mathrm{V}\wedge {A}\cup {B}\subseteq \left\{{ℝ}^{*}\right\}\cup \left({A}\cup {B}\right)\right)\to \mathrm{fi}\left({A}\cup {B}\right)\subseteq \mathrm{fi}\left(\left\{{ℝ}^{*}\right\}\cup \left({A}\cup {B}\right)\right)$
33 30 31 32 mp2an ${⊢}\mathrm{fi}\left({A}\cup {B}\right)\subseteq \mathrm{fi}\left(\left\{{ℝ}^{*}\right\}\cup \left({A}\cup {B}\right)\right)$
34 fvex ${⊢}\mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)\in \mathrm{V}$
35 ovex ${⊢}\left(0,\mathrm{+\infty }\right]\in \mathrm{V}$
36 ovex ${⊢}\left[\mathrm{-\infty },1\right)\in \mathrm{V}$
37 35 36 unipr ${⊢}\bigcup \left\{\left(0,\mathrm{+\infty }\right],\left[\mathrm{-\infty },1\right)\right\}=\left(0,\mathrm{+\infty }\right]\cup \left[\mathrm{-\infty },1\right)$
38 iocssxr ${⊢}\left(0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$
39 icossxr ${⊢}\left[\mathrm{-\infty },1\right)\subseteq {ℝ}^{*}$
40 38 39 unssi ${⊢}\left(0,\mathrm{+\infty }\right]\cup \left[\mathrm{-\infty },1\right)\subseteq {ℝ}^{*}$
41 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
42 0xr ${⊢}0\in {ℝ}^{*}$
43 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
44 mnflt0 ${⊢}\mathrm{-\infty }<0$
45 0lepnf ${⊢}0\le \mathrm{+\infty }$
46 df-icc ${⊢}\left[.\right]=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}\le {y}\right)\right\}\right)$
47 df-ioc ${⊢}\left(.\right]=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}<{z}\wedge {z}\le {y}\right)\right\}\right)$
48 xrltnle ${⊢}\left(0\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)\to \left(0<{w}↔¬{w}\le 0\right)$
49 xrletr ${⊢}\left({w}\in {ℝ}^{*}\wedge 0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left(\left({w}\le 0\wedge 0\le \mathrm{+\infty }\right)\to {w}\le \mathrm{+\infty }\right)$
50 xrlttr ${⊢}\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge 0\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)\to \left(\left(\mathrm{-\infty }<0\wedge 0<{w}\right)\to \mathrm{-\infty }<{w}\right)$
51 xrltle ${⊢}\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)\to \left(\mathrm{-\infty }<{w}\to \mathrm{-\infty }\le {w}\right)$
52 51 3adant2 ${⊢}\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge 0\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)\to \left(\mathrm{-\infty }<{w}\to \mathrm{-\infty }\le {w}\right)$
53 50 52 syld ${⊢}\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge 0\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)\to \left(\left(\mathrm{-\infty }<0\wedge 0<{w}\right)\to \mathrm{-\infty }\le {w}\right)$
54 46 47 48 46 49 53 ixxun ${⊢}\left(\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge 0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\wedge \left(\mathrm{-\infty }<0\wedge 0\le \mathrm{+\infty }\right)\right)\to \left[\mathrm{-\infty },0\right]\cup \left(0,\mathrm{+\infty }\right]=\left[\mathrm{-\infty },\mathrm{+\infty }\right]$
55 44 45 54 mpanr12 ${⊢}\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge 0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left[\mathrm{-\infty },0\right]\cup \left(0,\mathrm{+\infty }\right]=\left[\mathrm{-\infty },\mathrm{+\infty }\right]$
56 41 42 43 55 mp3an ${⊢}\left[\mathrm{-\infty },0\right]\cup \left(0,\mathrm{+\infty }\right]=\left[\mathrm{-\infty },\mathrm{+\infty }\right]$
57 1xr ${⊢}1\in {ℝ}^{*}$
58 0lt1 ${⊢}0<1$
59 df-ico ${⊢}\left[.\right)=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\right)$
60 xrlelttr ${⊢}\left({w}\in {ℝ}^{*}\wedge 0\in {ℝ}^{*}\wedge 1\in {ℝ}^{*}\right)\to \left(\left({w}\le 0\wedge 0<1\right)\to {w}<1\right)$
61 59 46 60 ixxss2 ${⊢}\left(1\in {ℝ}^{*}\wedge 0<1\right)\to \left[\mathrm{-\infty },0\right]\subseteq \left[\mathrm{-\infty },1\right)$
62 57 58 61 mp2an ${⊢}\left[\mathrm{-\infty },0\right]\subseteq \left[\mathrm{-\infty },1\right)$
63 unss1 ${⊢}\left[\mathrm{-\infty },0\right]\subseteq \left[\mathrm{-\infty },1\right)\to \left[\mathrm{-\infty },0\right]\cup \left(0,\mathrm{+\infty }\right]\subseteq \left[\mathrm{-\infty },1\right)\cup \left(0,\mathrm{+\infty }\right]$
64 62 63 ax-mp ${⊢}\left[\mathrm{-\infty },0\right]\cup \left(0,\mathrm{+\infty }\right]\subseteq \left[\mathrm{-\infty },1\right)\cup \left(0,\mathrm{+\infty }\right]$
65 56 64 eqsstrri ${⊢}\left[\mathrm{-\infty },\mathrm{+\infty }\right]\subseteq \left[\mathrm{-\infty },1\right)\cup \left(0,\mathrm{+\infty }\right]$
66 iccmax ${⊢}\left[\mathrm{-\infty },\mathrm{+\infty }\right]={ℝ}^{*}$
67 uncom ${⊢}\left[\mathrm{-\infty },1\right)\cup \left(0,\mathrm{+\infty }\right]=\left(0,\mathrm{+\infty }\right]\cup \left[\mathrm{-\infty },1\right)$
68 65 66 67 3sstr3i ${⊢}{ℝ}^{*}\subseteq \left(0,\mathrm{+\infty }\right]\cup \left[\mathrm{-\infty },1\right)$
69 40 68 eqssi ${⊢}\left(0,\mathrm{+\infty }\right]\cup \left[\mathrm{-\infty },1\right)={ℝ}^{*}$
70 37 69 eqtri ${⊢}\bigcup \left\{\left(0,\mathrm{+\infty }\right],\left[\mathrm{-\infty },1\right)\right\}={ℝ}^{*}$
71 fvex ${⊢}\mathrm{fi}\left({A}\cup {B}\right)\in \mathrm{V}$
72 ssun1 ${⊢}{A}\subseteq {A}\cup {B}$
73 eqid ${⊢}\left(0,\mathrm{+\infty }\right]=\left(0,\mathrm{+\infty }\right]$
74 oveq1 ${⊢}{x}=0\to \left({x},\mathrm{+\infty }\right]=\left(0,\mathrm{+\infty }\right]$
75 74 rspceeqv ${⊢}\left(0\in {ℝ}^{*}\wedge \left(0,\mathrm{+\infty }\right]=\left(0,\mathrm{+\infty }\right]\right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(0,\mathrm{+\infty }\right]=\left({x},\mathrm{+\infty }\right]$
76 42 73 75 mp2an ${⊢}\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(0,\mathrm{+\infty }\right]=\left({x},\mathrm{+\infty }\right]$
77 ovex ${⊢}\left({x},\mathrm{+\infty }\right]\in \mathrm{V}$
78 12 77 elrnmpti ${⊢}\left(0,\mathrm{+\infty }\right]\in \mathrm{ran}\left({x}\in {ℝ}^{*}⟼\left({x},\mathrm{+\infty }\right]\right)↔\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(0,\mathrm{+\infty }\right]=\left({x},\mathrm{+\infty }\right]$
79 76 78 mpbir ${⊢}\left(0,\mathrm{+\infty }\right]\in \mathrm{ran}\left({x}\in {ℝ}^{*}⟼\left({x},\mathrm{+\infty }\right]\right)$
80 79 1 eleqtrri ${⊢}\left(0,\mathrm{+\infty }\right]\in {A}$
81 72 80 sselii ${⊢}\left(0,\mathrm{+\infty }\right]\in \left({A}\cup {B}\right)$
82 ssun2 ${⊢}{B}\subseteq {A}\cup {B}$
83 eqid ${⊢}\left[\mathrm{-\infty },1\right)=\left[\mathrm{-\infty },1\right)$
84 oveq2 ${⊢}{x}=1\to \left[\mathrm{-\infty },{x}\right)=\left[\mathrm{-\infty },1\right)$
85 84 rspceeqv ${⊢}\left(1\in {ℝ}^{*}\wedge \left[\mathrm{-\infty },1\right)=\left[\mathrm{-\infty },1\right)\right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left[\mathrm{-\infty },1\right)=\left[\mathrm{-\infty },{x}\right)$
86 57 83 85 mp2an ${⊢}\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left[\mathrm{-\infty },1\right)=\left[\mathrm{-\infty },{x}\right)$
87 ovex ${⊢}\left[\mathrm{-\infty },{x}\right)\in \mathrm{V}$
88 20 87 elrnmpti ${⊢}\left[\mathrm{-\infty },1\right)\in \mathrm{ran}\left({x}\in {ℝ}^{*}⟼\left[\mathrm{-\infty },{x}\right)\right)↔\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left[\mathrm{-\infty },1\right)=\left[\mathrm{-\infty },{x}\right)$
89 86 88 mpbir ${⊢}\left[\mathrm{-\infty },1\right)\in \mathrm{ran}\left({x}\in {ℝ}^{*}⟼\left[\mathrm{-\infty },{x}\right)\right)$
90 89 2 eleqtrri ${⊢}\left[\mathrm{-\infty },1\right)\in {B}$
91 82 90 sselii ${⊢}\left[\mathrm{-\infty },1\right)\in \left({A}\cup {B}\right)$
92 prssi ${⊢}\left(\left(0,\mathrm{+\infty }\right]\in \left({A}\cup {B}\right)\wedge \left[\mathrm{-\infty },1\right)\in \left({A}\cup {B}\right)\right)\to \left\{\left(0,\mathrm{+\infty }\right],\left[\mathrm{-\infty },1\right)\right\}\subseteq {A}\cup {B}$
93 81 91 92 mp2an ${⊢}\left\{\left(0,\mathrm{+\infty }\right],\left[\mathrm{-\infty },1\right)\right\}\subseteq {A}\cup {B}$
94 ssfii ${⊢}{A}\cup {B}\in \mathrm{V}\to {A}\cup {B}\subseteq \mathrm{fi}\left({A}\cup {B}\right)$
95 29 94 ax-mp ${⊢}{A}\cup {B}\subseteq \mathrm{fi}\left({A}\cup {B}\right)$
96 93 95 sstri ${⊢}\left\{\left(0,\mathrm{+\infty }\right],\left[\mathrm{-\infty },1\right)\right\}\subseteq \mathrm{fi}\left({A}\cup {B}\right)$
97 eltg3i ${⊢}\left(\mathrm{fi}\left({A}\cup {B}\right)\in \mathrm{V}\wedge \left\{\left(0,\mathrm{+\infty }\right],\left[\mathrm{-\infty },1\right)\right\}\subseteq \mathrm{fi}\left({A}\cup {B}\right)\right)\to \bigcup \left\{\left(0,\mathrm{+\infty }\right],\left[\mathrm{-\infty },1\right)\right\}\in \mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)$
98 71 96 97 mp2an ${⊢}\bigcup \left\{\left(0,\mathrm{+\infty }\right],\left[\mathrm{-\infty },1\right)\right\}\in \mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)$
99 70 98 eqeltrri ${⊢}{ℝ}^{*}\in \mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)$
100 snssi ${⊢}{ℝ}^{*}\in \mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)\to \left\{{ℝ}^{*}\right\}\subseteq \mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)$
101 99 100 ax-mp ${⊢}\left\{{ℝ}^{*}\right\}\subseteq \mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)$
102 bastg ${⊢}\mathrm{fi}\left({A}\cup {B}\right)\in \mathrm{V}\to \mathrm{fi}\left({A}\cup {B}\right)\subseteq \mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)$
103 71 102 ax-mp ${⊢}\mathrm{fi}\left({A}\cup {B}\right)\subseteq \mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)$
104 95 103 sstri ${⊢}{A}\cup {B}\subseteq \mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)$
105 101 104 unssi ${⊢}\left\{{ℝ}^{*}\right\}\cup \left({A}\cup {B}\right)\subseteq \mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)$
106 fiss ${⊢}\left(\mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)\in \mathrm{V}\wedge \left\{{ℝ}^{*}\right\}\cup \left({A}\cup {B}\right)\subseteq \mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)\right)\to \mathrm{fi}\left(\left\{{ℝ}^{*}\right\}\cup \left({A}\cup {B}\right)\right)\subseteq \mathrm{fi}\left(\mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)\right)$
107 34 105 106 mp2an ${⊢}\mathrm{fi}\left(\left\{{ℝ}^{*}\right\}\cup \left({A}\cup {B}\right)\right)\subseteq \mathrm{fi}\left(\mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)\right)$
108 fibas ${⊢}\mathrm{fi}\left({A}\cup {B}\right)\in \mathrm{TopBases}$
109 tgcl ${⊢}\mathrm{fi}\left({A}\cup {B}\right)\in \mathrm{TopBases}\to \mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)\in \mathrm{Top}$
110 fitop ${⊢}\mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)\in \mathrm{Top}\to \mathrm{fi}\left(\mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)\right)=\mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)$
111 108 109 110 mp2b ${⊢}\mathrm{fi}\left(\mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)\right)=\mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)$
112 107 111 sseqtri ${⊢}\mathrm{fi}\left(\left\{{ℝ}^{*}\right\}\cup \left({A}\cup {B}\right)\right)\subseteq \mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)$
113 2basgen ${⊢}\left(\mathrm{fi}\left({A}\cup {B}\right)\subseteq \mathrm{fi}\left(\left\{{ℝ}^{*}\right\}\cup \left({A}\cup {B}\right)\right)\wedge \mathrm{fi}\left(\left\{{ℝ}^{*}\right\}\cup \left({A}\cup {B}\right)\right)\subseteq \mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)\right)\to \mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{{ℝ}^{*}\right\}\cup \left({A}\cup {B}\right)\right)\right)$
114 33 112 113 mp2an ${⊢}\mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{{ℝ}^{*}\right\}\cup \left({A}\cup {B}\right)\right)\right)$
115 8 114 eqtr4i ${⊢}\mathrm{ordTop}\left(\le \right)=\mathrm{topGen}\left(\mathrm{fi}\left({A}\cup {B}\right)\right)$