# Metamath Proof Explorer

## 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 {ℝ}^{*}|¬{y}\le {x}\right\}\right)$
8 1 2 leordtvallem2 ${⊢}{B}=\mathrm{ran}\left({x}\in {ℝ}^{*}⟼\left\{{y}\in {ℝ}^{*}|¬{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}↔¬{y}\le {a}\right)$
11 10 adantlr ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}\in {ℝ}^{*}\right)\wedge {y}\in {ℝ}^{*}\right)\to \left({a}<{y}↔¬{y}\le {a}\right)$
12 xrltnle ${⊢}\left({y}\in {ℝ}^{*}\wedge {b}\in {ℝ}^{*}\right)\to \left({y}<{b}↔¬{b}\le {y}\right)$
13 12 ancoms ${⊢}\left({b}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\to \left({y}<{b}↔¬{b}\le {y}\right)$
14 13 adantll ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}\in {ℝ}^{*}\right)\wedge {y}\in {ℝ}^{*}\right)\to \left({y}<{b}↔¬{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)↔\left(¬{y}\le {a}\wedge ¬{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(¬{y}\le {a}\wedge ¬{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(¬{y}\le {a}\wedge ¬{b}\le {y}\right)\right\}\right)$
18 9 17 eqtri ${⊢}\left(.\right)=\left({a}\in {ℝ}^{*},{b}\in {ℝ}^{*}⟼\left\{{y}\in {ℝ}^{*}|\left(¬{y}\le {a}\wedge ¬{b}\le {y}\right)\right\}\right)$
19 18 rneqi ${⊢}\mathrm{ran}\left(.\right)=\mathrm{ran}\left({a}\in {ℝ}^{*},{b}\in {ℝ}^{*}⟼\left\{{y}\in {ℝ}^{*}|\left(¬{y}\le {a}\wedge ¬{b}\le {y}\right)\right\}\right)$
20 3 19 eqtri ${⊢}{C}=\mathrm{ran}\left({a}\in {ℝ}^{*},{b}\in {ℝ}^{*}⟼\left\{{y}\in {ℝ}^{*}|\left(¬{y}\le {a}\wedge ¬{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)$