Metamath Proof Explorer

Theorem relowlssretop

Description: The lower limit topology on the reals is finer than the standard topology. (Contributed by ML, 1-Aug-2020)

Ref Expression
Hypothesis relowlssretop.1 ${⊢}{I}=\left[.\right)\left[{ℝ}^{2}\right]$
Assertion relowlssretop ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\subseteq \mathrm{topGen}\left({I}\right)$

Proof

Step Hyp Ref Expression
1 relowlssretop.1 ${⊢}{I}=\left[.\right)\left[{ℝ}^{2}\right]$
2 ioof ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ$
3 ffn ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ\to \left(.\right)Fn\left({ℝ}^{*}×{ℝ}^{*}\right)$
4 ovelrn ${⊢}\left(.\right)Fn\left({ℝ}^{*}×{ℝ}^{*}\right)\to \left({o}\in \mathrm{ran}\left(.\right)↔\exists {a}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\exists {b}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}{o}=\left({a},{b}\right)\right)$
5 2 3 4 mp2b ${⊢}{o}\in \mathrm{ran}\left(.\right)↔\exists {a}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\exists {b}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}{o}=\left({a},{b}\right)$
6 elxr ${⊢}{b}\in {ℝ}^{*}↔\left({b}\in ℝ\vee {b}=\mathrm{+\infty }\vee {b}=\mathrm{-\infty }\right)$
7 simpr ${⊢}\left({a}\in {ℝ}^{*}\wedge {b}\in ℝ\right)\to {b}\in ℝ$
8 elioore ${⊢}{x}\in \left({a},{b}\right)\to {x}\in ℝ$
9 7 8 anim12ci ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}\in ℝ\right)\wedge {x}\in \left({a},{b}\right)\right)\to \left({x}\in ℝ\wedge {b}\in ℝ\right)$
10 1 icoreelrn ${⊢}\left({x}\in ℝ\wedge {b}\in ℝ\right)\to \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}\in {I}$
11 9 10 syl ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}\in ℝ\right)\wedge {x}\in \left({a},{b}\right)\right)\to \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}\in {I}$
12 8 adantl ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}\in ℝ\right)\wedge {x}\in \left({a},{b}\right)\right)\to {x}\in ℝ$
13 8 leidd ${⊢}{x}\in \left({a},{b}\right)\to {x}\le {x}$
14 13 adantl ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}\in ℝ\right)\wedge {x}\in \left({a},{b}\right)\right)\to {x}\le {x}$
15 7 rexrd ${⊢}\left({a}\in {ℝ}^{*}\wedge {b}\in ℝ\right)\to {b}\in {ℝ}^{*}$
16 elioo1 ${⊢}\left({a}\in {ℝ}^{*}\wedge {b}\in {ℝ}^{*}\right)\to \left({x}\in \left({a},{b}\right)↔\left({x}\in {ℝ}^{*}\wedge {a}<{x}\wedge {x}<{b}\right)\right)$
17 15 16 syldan ${⊢}\left({a}\in {ℝ}^{*}\wedge {b}\in ℝ\right)\to \left({x}\in \left({a},{b}\right)↔\left({x}\in {ℝ}^{*}\wedge {a}<{x}\wedge {x}<{b}\right)\right)$
18 17 biimpa ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}\in ℝ\right)\wedge {x}\in \left({a},{b}\right)\right)\to \left({x}\in {ℝ}^{*}\wedge {a}<{x}\wedge {x}<{b}\right)$
19 18 simp3d ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}\in ℝ\right)\wedge {x}\in \left({a},{b}\right)\right)\to {x}<{b}$
20 rexr ${⊢}{x}\in ℝ\to {x}\in {ℝ}^{*}$
21 20 3anim1i ${⊢}\left({x}\in ℝ\wedge {x}\le {x}\wedge {x}<{b}\right)\to \left({x}\in {ℝ}^{*}\wedge {x}\le {x}\wedge {x}<{b}\right)$
22 rexr ${⊢}{b}\in ℝ\to {b}\in {ℝ}^{*}$
23 elico1 ${⊢}\left({x}\in {ℝ}^{*}\wedge {b}\in {ℝ}^{*}\right)\to \left({x}\in \left[{x},{b}\right)↔\left({x}\in {ℝ}^{*}\wedge {x}\le {x}\wedge {x}<{b}\right)\right)$
24 20 22 23 syl2an ${⊢}\left({x}\in ℝ\wedge {b}\in ℝ\right)\to \left({x}\in \left[{x},{b}\right)↔\left({x}\in {ℝ}^{*}\wedge {x}\le {x}\wedge {x}<{b}\right)\right)$
25 24 biimprd ${⊢}\left({x}\in ℝ\wedge {b}\in ℝ\right)\to \left(\left({x}\in {ℝ}^{*}\wedge {x}\le {x}\wedge {x}<{b}\right)\to {x}\in \left[{x},{b}\right)\right)$
26 9 21 25 syl2im ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}\in ℝ\right)\wedge {x}\in \left({a},{b}\right)\right)\to \left(\left({x}\in ℝ\wedge {x}\le {x}\wedge {x}<{b}\right)\to {x}\in \left[{x},{b}\right)\right)$
27 icoreval ${⊢}\left({x}\in ℝ\wedge {b}\in ℝ\right)\to \left[{x},{b}\right)=\left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}$
28 9 27 syl ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}\in ℝ\right)\wedge {x}\in \left({a},{b}\right)\right)\to \left[{x},{b}\right)=\left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}$
29 28 eleq2d ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}\in ℝ\right)\wedge {x}\in \left({a},{b}\right)\right)\to \left({x}\in \left[{x},{b}\right)↔{x}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}\right)$
30 26 29 sylibd ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}\in ℝ\right)\wedge {x}\in \left({a},{b}\right)\right)\to \left(\left({x}\in ℝ\wedge {x}\le {x}\wedge {x}<{b}\right)\to {x}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}\right)$
31 12 14 19 30 mp3and ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}\in ℝ\right)\wedge {x}\in \left({a},{b}\right)\right)\to {x}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}$
32 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left(\left({a}\in {ℝ}^{*}\wedge {b}\in {ℝ}^{*}\right)\wedge {x}\in \left({a},{b}\right)\right)$
33 nfrab1 ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}\left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}$
34 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}\left({a},{b}\right)$
35 iooval ${⊢}\left({a}\in {ℝ}^{*}\wedge {b}\in {ℝ}^{*}\right)\to \left({a},{b}\right)=\left\{{x}\in {ℝ}^{*}|\left({a}<{x}\wedge {x}<{b}\right)\right\}$
36 35 eleq2d ${⊢}\left({a}\in {ℝ}^{*}\wedge {b}\in {ℝ}^{*}\right)\to \left({x}\in \left({a},{b}\right)↔{x}\in \left\{{x}\in {ℝ}^{*}|\left({a}<{x}\wedge {x}<{b}\right)\right\}\right)$
37 36 anbi1d ${⊢}\left({a}\in {ℝ}^{*}\wedge {b}\in {ℝ}^{*}\right)\to \left(\left({x}\in \left({a},{b}\right)\wedge {z}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}\right)↔\left({x}\in \left\{{x}\in {ℝ}^{*}|\left({a}<{x}\wedge {x}<{b}\right)\right\}\wedge {z}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}\right)\right)$
38 37 pm5.32i ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}\in {ℝ}^{*}\right)\wedge \left({x}\in \left({a},{b}\right)\wedge {z}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}\right)\right)↔\left(\left({a}\in {ℝ}^{*}\wedge {b}\in {ℝ}^{*}\right)\wedge \left({x}\in \left\{{x}\in {ℝ}^{*}|\left({a}<{x}\wedge {x}<{b}\right)\right\}\wedge {z}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}\right)\right)$
39 rabid ${⊢}{x}\in \left\{{x}\in {ℝ}^{*}|\left({a}<{x}\wedge {x}<{b}\right)\right\}↔\left({x}\in {ℝ}^{*}\wedge \left({a}<{x}\wedge {x}<{b}\right)\right)$
40 rabid ${⊢}{z}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}↔\left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{b}\right)\right)$
41 39 40 anbi12i ${⊢}\left({x}\in \left\{{x}\in {ℝ}^{*}|\left({a}<{x}\wedge {x}<{b}\right)\right\}\wedge {z}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}\right)↔\left(\left({x}\in {ℝ}^{*}\wedge \left({a}<{x}\wedge {x}<{b}\right)\right)\wedge \left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{b}\right)\right)\right)$
42 simpl ${⊢}\left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{b}\right)\right)\to {z}\in ℝ$
43 42 rexrd ${⊢}\left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{b}\right)\right)\to {z}\in {ℝ}^{*}$
44 43 ad2antll ${⊢}\left({a}\in {ℝ}^{*}\wedge \left(\left({x}\in {ℝ}^{*}\wedge \left({a}<{x}\wedge {x}<{b}\right)\right)\wedge \left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{b}\right)\right)\right)\right)\to {z}\in {ℝ}^{*}$
45 simpl ${⊢}\left({x}\in {ℝ}^{*}\wedge \left({a}<{x}\wedge {x}<{b}\right)\right)\to {x}\in {ℝ}^{*}$
46 45 43 anim12i ${⊢}\left(\left({x}\in {ℝ}^{*}\wedge \left({a}<{x}\wedge {x}<{b}\right)\right)\wedge \left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{b}\right)\right)\right)\to \left({x}\in {ℝ}^{*}\wedge {z}\in {ℝ}^{*}\right)$
47 46 anim2i ${⊢}\left({a}\in {ℝ}^{*}\wedge \left(\left({x}\in {ℝ}^{*}\wedge \left({a}<{x}\wedge {x}<{b}\right)\right)\wedge \left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{b}\right)\right)\right)\right)\to \left({a}\in {ℝ}^{*}\wedge \left({x}\in {ℝ}^{*}\wedge {z}\in {ℝ}^{*}\right)\right)$
48 3anass ${⊢}\left({a}\in {ℝ}^{*}\wedge {x}\in {ℝ}^{*}\wedge {z}\in {ℝ}^{*}\right)↔\left({a}\in {ℝ}^{*}\wedge \left({x}\in {ℝ}^{*}\wedge {z}\in {ℝ}^{*}\right)\right)$
49 47 48 sylibr ${⊢}\left({a}\in {ℝ}^{*}\wedge \left(\left({x}\in {ℝ}^{*}\wedge \left({a}<{x}\wedge {x}<{b}\right)\right)\wedge \left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{b}\right)\right)\right)\right)\to \left({a}\in {ℝ}^{*}\wedge {x}\in {ℝ}^{*}\wedge {z}\in {ℝ}^{*}\right)$
50 simprl ${⊢}\left({x}\in {ℝ}^{*}\wedge \left({a}<{x}\wedge {x}<{b}\right)\right)\to {a}<{x}$
51 simprl ${⊢}\left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{b}\right)\right)\to {x}\le {z}$
52 50 51 anim12i ${⊢}\left(\left({x}\in {ℝ}^{*}\wedge \left({a}<{x}\wedge {x}<{b}\right)\right)\wedge \left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{b}\right)\right)\right)\to \left({a}<{x}\wedge {x}\le {z}\right)$
53 52 adantl ${⊢}\left({a}\in {ℝ}^{*}\wedge \left(\left({x}\in {ℝ}^{*}\wedge \left({a}<{x}\wedge {x}<{b}\right)\right)\wedge \left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{b}\right)\right)\right)\right)\to \left({a}<{x}\wedge {x}\le {z}\right)$
54 xrltletr ${⊢}\left({a}\in {ℝ}^{*}\wedge {x}\in {ℝ}^{*}\wedge {z}\in {ℝ}^{*}\right)\to \left(\left({a}<{x}\wedge {x}\le {z}\right)\to {a}<{z}\right)$
55 49 53 54 sylc ${⊢}\left({a}\in {ℝ}^{*}\wedge \left(\left({x}\in {ℝ}^{*}\wedge \left({a}<{x}\wedge {x}<{b}\right)\right)\wedge \left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{b}\right)\right)\right)\right)\to {a}<{z}$
56 simprr ${⊢}\left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{b}\right)\right)\to {z}<{b}$
57 56 ad2antll ${⊢}\left({a}\in {ℝ}^{*}\wedge \left(\left({x}\in {ℝ}^{*}\wedge \left({a}<{x}\wedge {x}<{b}\right)\right)\wedge \left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{b}\right)\right)\right)\right)\to {z}<{b}$
58 55 57 jca ${⊢}\left({a}\in {ℝ}^{*}\wedge \left(\left({x}\in {ℝ}^{*}\wedge \left({a}<{x}\wedge {x}<{b}\right)\right)\wedge \left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{b}\right)\right)\right)\right)\to \left({a}<{z}\wedge {z}<{b}\right)$
59 rabid ${⊢}{z}\in \left\{{z}\in {ℝ}^{*}|\left({a}<{z}\wedge {z}<{b}\right)\right\}↔\left({z}\in {ℝ}^{*}\wedge \left({a}<{z}\wedge {z}<{b}\right)\right)$
60 44 58 59 sylanbrc ${⊢}\left({a}\in {ℝ}^{*}\wedge \left(\left({x}\in {ℝ}^{*}\wedge \left({a}<{x}\wedge {x}<{b}\right)\right)\wedge \left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{b}\right)\right)\right)\right)\to {z}\in \left\{{z}\in {ℝ}^{*}|\left({a}<{z}\wedge {z}<{b}\right)\right\}$
61 60 adantlr ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}\in {ℝ}^{*}\right)\wedge \left(\left({x}\in {ℝ}^{*}\wedge \left({a}<{x}\wedge {x}<{b}\right)\right)\wedge \left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{b}\right)\right)\right)\right)\to {z}\in \left\{{z}\in {ℝ}^{*}|\left({a}<{z}\wedge {z}<{b}\right)\right\}$
62 iooval ${⊢}\left({a}\in {ℝ}^{*}\wedge {b}\in {ℝ}^{*}\right)\to \left({a},{b}\right)=\left\{{z}\in {ℝ}^{*}|\left({a}<{z}\wedge {z}<{b}\right)\right\}$
63 62 adantr ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}\in {ℝ}^{*}\right)\wedge \left(\left({x}\in {ℝ}^{*}\wedge \left({a}<{x}\wedge {x}<{b}\right)\right)\wedge \left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{b}\right)\right)\right)\right)\to \left({a},{b}\right)=\left\{{z}\in {ℝ}^{*}|\left({a}<{z}\wedge {z}<{b}\right)\right\}$
64 61 63 eleqtrrd ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}\in {ℝ}^{*}\right)\wedge \left(\left({x}\in {ℝ}^{*}\wedge \left({a}<{x}\wedge {x}<{b}\right)\right)\wedge \left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{b}\right)\right)\right)\right)\to {z}\in \left({a},{b}\right)$
65 41 64 sylan2b ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}\in {ℝ}^{*}\right)\wedge \left({x}\in \left\{{x}\in {ℝ}^{*}|\left({a}<{x}\wedge {x}<{b}\right)\right\}\wedge {z}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}\right)\right)\to {z}\in \left({a},{b}\right)$
66 38 65 sylbi ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}\in {ℝ}^{*}\right)\wedge \left({x}\in \left({a},{b}\right)\wedge {z}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}\right)\right)\to {z}\in \left({a},{b}\right)$
67 66 expr ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}\in {ℝ}^{*}\right)\wedge {x}\in \left({a},{b}\right)\right)\to \left({z}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}\to {z}\in \left({a},{b}\right)\right)$
68 32 33 34 67 ssrd ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}\in {ℝ}^{*}\right)\wedge {x}\in \left({a},{b}\right)\right)\to \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}\subseteq \left({a},{b}\right)$
69 22 68 sylanl2 ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}\in ℝ\right)\wedge {x}\in \left({a},{b}\right)\right)\to \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}\subseteq \left({a},{b}\right)$
70 eleq2 ${⊢}{i}=\left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}\to \left({x}\in {i}↔{x}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}\right)$
71 sseq1 ${⊢}{i}=\left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}\to \left({i}\subseteq \left({a},{b}\right)↔\left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}\subseteq \left({a},{b}\right)\right)$
72 70 71 anbi12d ${⊢}{i}=\left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}\to \left(\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)↔\left({x}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}\wedge \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}\subseteq \left({a},{b}\right)\right)\right)$
73 72 rspcev ${⊢}\left(\left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}\in {I}\wedge \left({x}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}\wedge \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{b}\right)\right\}\subseteq \left({a},{b}\right)\right)\right)\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)$
74 11 31 69 73 syl12anc ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}\in ℝ\right)\wedge {x}\in \left({a},{b}\right)\right)\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)$
75 74 ancom1s ${⊢}\left(\left({b}\in ℝ\wedge {a}\in {ℝ}^{*}\right)\wedge {x}\in \left({a},{b}\right)\right)\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)$
76 75 expl ${⊢}{b}\in ℝ\to \left(\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},{b}\right)\right)\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)\right)$
77 8 adantl ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}=\mathrm{+\infty }\right)\wedge {x}\in \left({a},{b}\right)\right)\to {x}\in ℝ$
78 peano2re ${⊢}{x}\in ℝ\to {x}+1\in ℝ$
79 1 icoreelrn ${⊢}\left({x}\in ℝ\wedge {x}+1\in ℝ\right)\to \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\in {I}$
80 77 78 79 syl2anc2 ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}=\mathrm{+\infty }\right)\wedge {x}\in \left({a},{b}\right)\right)\to \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\in {I}$
81 elioore ${⊢}{x}\in \left({a},\mathrm{+\infty }\right)\to {x}\in ℝ$
82 81 adantl ${⊢}\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},\mathrm{+\infty }\right)\right)\to {x}\in ℝ$
83 82 leidd ${⊢}\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},\mathrm{+\infty }\right)\right)\to {x}\le {x}$
84 82 ltp1d ${⊢}\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},\mathrm{+\infty }\right)\right)\to {x}<{x}+1$
85 82 83 84 jca32 ${⊢}\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},\mathrm{+\infty }\right)\right)\to \left({x}\in ℝ\wedge \left({x}\le {x}\wedge {x}<{x}+1\right)\right)$
86 breq2 ${⊢}{z}={x}\to \left({x}\le {z}↔{x}\le {x}\right)$
87 breq1 ${⊢}{z}={x}\to \left({z}<{x}+1↔{x}<{x}+1\right)$
88 86 87 anbi12d ${⊢}{z}={x}\to \left(\left({x}\le {z}\wedge {z}<{x}+1\right)↔\left({x}\le {x}\wedge {x}<{x}+1\right)\right)$
89 88 elrab ${⊢}{x}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}↔\left({x}\in ℝ\wedge \left({x}\le {x}\wedge {x}<{x}+1\right)\right)$
90 85 89 sylibr ${⊢}\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},\mathrm{+\infty }\right)\right)\to {x}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}$
91 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},\mathrm{+\infty }\right)\right)$
92 nfrab1 ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}\left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}$
93 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}\left({a},\mathrm{+\infty }\right)$
94 rabid ${⊢}{z}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}↔\left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{x}+1\right)\right)$
95 simprl ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},\mathrm{+\infty }\right)\right)\wedge \left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{x}+1\right)\right)\right)\to {z}\in ℝ$
96 simpll ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},\mathrm{+\infty }\right)\right)\wedge \left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{x}+1\right)\right)\right)\to {a}\in {ℝ}^{*}$
97 82 adantr ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},\mathrm{+\infty }\right)\right)\wedge \left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{x}+1\right)\right)\right)\to {x}\in ℝ$
98 97 rexrd ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},\mathrm{+\infty }\right)\right)\wedge \left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{x}+1\right)\right)\right)\to {x}\in {ℝ}^{*}$
99 95 rexrd ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},\mathrm{+\infty }\right)\right)\wedge \left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{x}+1\right)\right)\right)\to {z}\in {ℝ}^{*}$
100 elioopnf ${⊢}{a}\in {ℝ}^{*}\to \left({x}\in \left({a},\mathrm{+\infty }\right)↔\left({x}\in ℝ\wedge {a}<{x}\right)\right)$
101 100 simplbda ${⊢}\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},\mathrm{+\infty }\right)\right)\to {a}<{x}$
102 101 adantr ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},\mathrm{+\infty }\right)\right)\wedge \left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{x}+1\right)\right)\right)\to {a}<{x}$
103 simprl ${⊢}\left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{x}+1\right)\right)\to {x}\le {z}$
104 103 adantl ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},\mathrm{+\infty }\right)\right)\wedge \left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{x}+1\right)\right)\right)\to {x}\le {z}$
105 96 98 99 102 104 xrltletrd ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},\mathrm{+\infty }\right)\right)\wedge \left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{x}+1\right)\right)\right)\to {a}<{z}$
106 elioopnf ${⊢}{a}\in {ℝ}^{*}\to \left({z}\in \left({a},\mathrm{+\infty }\right)↔\left({z}\in ℝ\wedge {a}<{z}\right)\right)$
107 106 biimprd ${⊢}{a}\in {ℝ}^{*}\to \left(\left({z}\in ℝ\wedge {a}<{z}\right)\to {z}\in \left({a},\mathrm{+\infty }\right)\right)$
108 107 adantr ${⊢}\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},\mathrm{+\infty }\right)\right)\to \left(\left({z}\in ℝ\wedge {a}<{z}\right)\to {z}\in \left({a},\mathrm{+\infty }\right)\right)$
109 108 adantr ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},\mathrm{+\infty }\right)\right)\wedge \left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{x}+1\right)\right)\right)\to \left(\left({z}\in ℝ\wedge {a}<{z}\right)\to {z}\in \left({a},\mathrm{+\infty }\right)\right)$
110 95 105 109 mp2and ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},\mathrm{+\infty }\right)\right)\wedge \left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{x}+1\right)\right)\right)\to {z}\in \left({a},\mathrm{+\infty }\right)$
111 110 ex ${⊢}\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},\mathrm{+\infty }\right)\right)\to \left(\left({z}\in ℝ\wedge \left({x}\le {z}\wedge {z}<{x}+1\right)\right)\to {z}\in \left({a},\mathrm{+\infty }\right)\right)$
112 94 111 syl5bi ${⊢}\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},\mathrm{+\infty }\right)\right)\to \left({z}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\to {z}\in \left({a},\mathrm{+\infty }\right)\right)$
113 91 92 93 112 ssrd ${⊢}\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},\mathrm{+\infty }\right)\right)\to \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\subseteq \left({a},\mathrm{+\infty }\right)$
114 90 113 jca ${⊢}\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},\mathrm{+\infty }\right)\right)\to \left({x}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\wedge \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\subseteq \left({a},\mathrm{+\infty }\right)\right)$
115 oveq2 ${⊢}{b}=\mathrm{+\infty }\to \left({a},{b}\right)=\left({a},\mathrm{+\infty }\right)$
116 115 eleq2d ${⊢}{b}=\mathrm{+\infty }\to \left({x}\in \left({a},{b}\right)↔{x}\in \left({a},\mathrm{+\infty }\right)\right)$
117 116 anbi2d ${⊢}{b}=\mathrm{+\infty }\to \left(\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},{b}\right)\right)↔\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},\mathrm{+\infty }\right)\right)\right)$
118 115 sseq2d ${⊢}{b}=\mathrm{+\infty }\to \left(\left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\subseteq \left({a},{b}\right)↔\left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\subseteq \left({a},\mathrm{+\infty }\right)\right)$
119 118 anbi2d ${⊢}{b}=\mathrm{+\infty }\to \left(\left({x}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\wedge \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\subseteq \left({a},{b}\right)\right)↔\left({x}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\wedge \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\subseteq \left({a},\mathrm{+\infty }\right)\right)\right)$
120 117 119 imbi12d ${⊢}{b}=\mathrm{+\infty }\to \left(\left(\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},{b}\right)\right)\to \left({x}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\wedge \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\subseteq \left({a},{b}\right)\right)\right)↔\left(\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},\mathrm{+\infty }\right)\right)\to \left({x}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\wedge \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\subseteq \left({a},\mathrm{+\infty }\right)\right)\right)\right)$
121 114 120 mpbiri ${⊢}{b}=\mathrm{+\infty }\to \left(\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},{b}\right)\right)\to \left({x}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\wedge \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\subseteq \left({a},{b}\right)\right)\right)$
122 121 impl ${⊢}\left(\left({b}=\mathrm{+\infty }\wedge {a}\in {ℝ}^{*}\right)\wedge {x}\in \left({a},{b}\right)\right)\to \left({x}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\wedge \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\subseteq \left({a},{b}\right)\right)$
123 122 ancom1s ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}=\mathrm{+\infty }\right)\wedge {x}\in \left({a},{b}\right)\right)\to \left({x}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\wedge \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\subseteq \left({a},{b}\right)\right)$
124 eleq2 ${⊢}{i}=\left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\to \left({x}\in {i}↔{x}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\right)$
125 sseq1 ${⊢}{i}=\left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\to \left({i}\subseteq \left({a},{b}\right)↔\left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\subseteq \left({a},{b}\right)\right)$
126 124 125 anbi12d ${⊢}{i}=\left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\to \left(\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)↔\left({x}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\wedge \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\subseteq \left({a},{b}\right)\right)\right)$
127 126 rspcev ${⊢}\left(\left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\in {I}\wedge \left({x}\in \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\wedge \left\{{z}\in ℝ|\left({x}\le {z}\wedge {z}<{x}+1\right)\right\}\subseteq \left({a},{b}\right)\right)\right)\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)$
128 80 123 127 syl2anc ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}=\mathrm{+\infty }\right)\wedge {x}\in \left({a},{b}\right)\right)\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)$
129 128 ancom1s ${⊢}\left(\left({b}=\mathrm{+\infty }\wedge {a}\in {ℝ}^{*}\right)\wedge {x}\in \left({a},{b}\right)\right)\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)$
130 129 expl ${⊢}{b}=\mathrm{+\infty }\to \left(\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},{b}\right)\right)\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)\right)$
131 8 adantl ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}=\mathrm{-\infty }\right)\wedge {x}\in \left({a},{b}\right)\right)\to {x}\in ℝ$
132 oveq2 ${⊢}{b}=\mathrm{-\infty }\to \left({a},{b}\right)=\left({a},\mathrm{-\infty }\right)$
133 132 eleq2d ${⊢}{b}=\mathrm{-\infty }\to \left({x}\in \left({a},{b}\right)↔{x}\in \left({a},\mathrm{-\infty }\right)\right)$
134 133 adantl ${⊢}\left({a}\in {ℝ}^{*}\wedge {b}=\mathrm{-\infty }\right)\to \left({x}\in \left({a},{b}\right)↔{x}\in \left({a},\mathrm{-\infty }\right)\right)$
135 134 pm5.32i ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}=\mathrm{-\infty }\right)\wedge {x}\in \left({a},{b}\right)\right)↔\left(\left({a}\in {ℝ}^{*}\wedge {b}=\mathrm{-\infty }\right)\wedge {x}\in \left({a},\mathrm{-\infty }\right)\right)$
136 nltmnf ${⊢}{x}\in {ℝ}^{*}\to ¬{x}<\mathrm{-\infty }$
137 136 intnand ${⊢}{x}\in {ℝ}^{*}\to ¬\left({a}<{x}\wedge {x}<\mathrm{-\infty }\right)$
138 eliooord ${⊢}{x}\in \left({a},\mathrm{-\infty }\right)\to \left({a}<{x}\wedge {x}<\mathrm{-\infty }\right)$
139 137 138 nsyl ${⊢}{x}\in {ℝ}^{*}\to ¬{x}\in \left({a},\mathrm{-\infty }\right)$
140 139 pm2.21d ${⊢}{x}\in {ℝ}^{*}\to \left({x}\in \left({a},\mathrm{-\infty }\right)\to \left(\left({a}\in {ℝ}^{*}\wedge {b}=\mathrm{-\infty }\right)\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)\right)\right)$
141 140 impd ${⊢}{x}\in {ℝ}^{*}\to \left(\left({x}\in \left({a},\mathrm{-\infty }\right)\wedge \left({a}\in {ℝ}^{*}\wedge {b}=\mathrm{-\infty }\right)\right)\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)\right)$
142 141 ancomsd ${⊢}{x}\in {ℝ}^{*}\to \left(\left(\left({a}\in {ℝ}^{*}\wedge {b}=\mathrm{-\infty }\right)\wedge {x}\in \left({a},\mathrm{-\infty }\right)\right)\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)\right)$
143 135 142 syl5bi ${⊢}{x}\in {ℝ}^{*}\to \left(\left(\left({a}\in {ℝ}^{*}\wedge {b}=\mathrm{-\infty }\right)\wedge {x}\in \left({a},{b}\right)\right)\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)\right)$
144 20 143 syl ${⊢}{x}\in ℝ\to \left(\left(\left({a}\in {ℝ}^{*}\wedge {b}=\mathrm{-\infty }\right)\wedge {x}\in \left({a},{b}\right)\right)\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)\right)$
145 131 144 mpcom ${⊢}\left(\left({a}\in {ℝ}^{*}\wedge {b}=\mathrm{-\infty }\right)\wedge {x}\in \left({a},{b}\right)\right)\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)$
146 145 ancom1s ${⊢}\left(\left({b}=\mathrm{-\infty }\wedge {a}\in {ℝ}^{*}\right)\wedge {x}\in \left({a},{b}\right)\right)\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)$
147 146 expl ${⊢}{b}=\mathrm{-\infty }\to \left(\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},{b}\right)\right)\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)\right)$
148 76 130 147 3jaoi ${⊢}\left({b}\in ℝ\vee {b}=\mathrm{+\infty }\vee {b}=\mathrm{-\infty }\right)\to \left(\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},{b}\right)\right)\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)\right)$
149 6 148 sylbi ${⊢}{b}\in {ℝ}^{*}\to \left(\left({a}\in {ℝ}^{*}\wedge {x}\in \left({a},{b}\right)\right)\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)\right)$
150 149 expdimp ${⊢}\left({b}\in {ℝ}^{*}\wedge {a}\in {ℝ}^{*}\right)\to \left({x}\in \left({a},{b}\right)\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)\right)$
151 150 ancoms ${⊢}\left({a}\in {ℝ}^{*}\wedge {b}\in {ℝ}^{*}\right)\to \left({x}\in \left({a},{b}\right)\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)\right)$
152 eleq2 ${⊢}{o}=\left({a},{b}\right)\to \left({x}\in {o}↔{x}\in \left({a},{b}\right)\right)$
153 sseq2 ${⊢}{o}=\left({a},{b}\right)\to \left({i}\subseteq {o}↔{i}\subseteq \left({a},{b}\right)\right)$
154 153 anbi2d ${⊢}{o}=\left({a},{b}\right)\to \left(\left({x}\in {i}\wedge {i}\subseteq {o}\right)↔\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)\right)$
155 154 rexbidv ${⊢}{o}=\left({a},{b}\right)\to \left(\exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq {o}\right)↔\exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)\right)$
156 152 155 imbi12d ${⊢}{o}=\left({a},{b}\right)\to \left(\left({x}\in {o}\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq {o}\right)\right)↔\left({x}\in \left({a},{b}\right)\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq \left({a},{b}\right)\right)\right)\right)$
157 151 156 syl5ibrcom ${⊢}\left({a}\in {ℝ}^{*}\wedge {b}\in {ℝ}^{*}\right)\to \left({o}=\left({a},{b}\right)\to \left({x}\in {o}\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq {o}\right)\right)\right)$
158 157 rexlimivv ${⊢}\exists {a}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\exists {b}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}{o}=\left({a},{b}\right)\to \left({x}\in {o}\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq {o}\right)\right)$
159 5 158 sylbi ${⊢}{o}\in \mathrm{ran}\left(.\right)\to \left({x}\in {o}\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq {o}\right)\right)$
160 159 rgen ${⊢}\forall {o}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}\left({x}\in {o}\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq {o}\right)\right)$
161 160 rgenw ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {o}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}\left({x}\in {o}\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq {o}\right)\right)$
162 iooex ${⊢}\left(.\right)\in \mathrm{V}$
163 162 rnex ${⊢}\mathrm{ran}\left(.\right)\in \mathrm{V}$
164 unirnioo ${⊢}ℝ=\bigcup \mathrm{ran}\left(.\right)$
165 1 icoreunrn ${⊢}ℝ=\bigcup {I}$
166 164 165 eqtr3i ${⊢}\bigcup \mathrm{ran}\left(.\right)=\bigcup {I}$
167 tgss2 ${⊢}\left(\mathrm{ran}\left(.\right)\in \mathrm{V}\wedge \bigcup \mathrm{ran}\left(.\right)=\bigcup {I}\right)\to \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\subseteq \mathrm{topGen}\left({I}\right)↔\forall {x}\in \bigcup \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}\forall {o}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}\left({x}\in {o}\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq {o}\right)\right)\right)$
168 163 166 167 mp2an ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\subseteq \mathrm{topGen}\left({I}\right)↔\forall {x}\in \bigcup \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}\forall {o}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}\left({x}\in {o}\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq {o}\right)\right)$
169 164 raleqi ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {o}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}\left({x}\in {o}\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq {o}\right)\right)↔\forall {x}\in \bigcup \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}\forall {o}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}\left({x}\in {o}\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq {o}\right)\right)$
170 168 169 bitr4i ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\subseteq \mathrm{topGen}\left({I}\right)↔\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {o}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}\left({x}\in {o}\to \exists {i}\in {I}\phantom{\rule{.4em}{0ex}}\left({x}\in {i}\wedge {i}\subseteq {o}\right)\right)$
171 161 170 mpbir ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\subseteq \mathrm{topGen}\left({I}\right)$