Metamath Proof Explorer

Theorem reconnlem1

Description: Lemma for reconn . Connectedness in the reals-easy direction. (Contributed by Jeff Hankins, 13-Jul-2009) (Proof shortened by Mario Carneiro, 9-Sep-2015)

Ref Expression
Assertion reconnlem1 ${⊢}\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\to \left[{X},{Y}\right]\subseteq {A}$

Proof

Step Hyp Ref Expression
1 simplr ${⊢}\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\to \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}$
2 retopon ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{TopOn}\left(ℝ\right)$
3 2 a1i ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{TopOn}\left(ℝ\right)$
4 simplll ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to {A}\subseteq ℝ$
5 iooretop ${⊢}\left(\mathrm{-\infty },{z}\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
6 5 a1i ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \left(\mathrm{-\infty },{z}\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
7 iooretop ${⊢}\left({z},\mathrm{+\infty }\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
8 7 a1i ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \left({z},\mathrm{+\infty }\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
9 simplrl ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to {X}\in {A}$
10 4 9 sseldd ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to {X}\in ℝ$
11 10 mnfltd ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \mathrm{-\infty }<{X}$
12 eldifn ${⊢}{z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\to ¬{z}\in {A}$
13 12 adantl ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to ¬{z}\in {A}$
14 eleq1 ${⊢}{X}={z}\to \left({X}\in {A}↔{z}\in {A}\right)$
15 9 14 syl5ibcom ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \left({X}={z}\to {z}\in {A}\right)$
16 13 15 mtod ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to ¬{X}={z}$
17 eldifi ${⊢}{z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\to {z}\in \left[{X},{Y}\right]$
18 17 adantl ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to {z}\in \left[{X},{Y}\right]$
19 simplrr ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to {Y}\in {A}$
20 4 19 sseldd ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to {Y}\in ℝ$
21 elicc2 ${⊢}\left({X}\in ℝ\wedge {Y}\in ℝ\right)\to \left({z}\in \left[{X},{Y}\right]↔\left({z}\in ℝ\wedge {X}\le {z}\wedge {z}\le {Y}\right)\right)$
22 10 20 21 syl2anc ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \left({z}\in \left[{X},{Y}\right]↔\left({z}\in ℝ\wedge {X}\le {z}\wedge {z}\le {Y}\right)\right)$
23 18 22 mpbid ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \left({z}\in ℝ\wedge {X}\le {z}\wedge {z}\le {Y}\right)$
24 23 simp2d ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to {X}\le {z}$
25 23 simp1d ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to {z}\in ℝ$
26 10 25 leloed ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \left({X}\le {z}↔\left({X}<{z}\vee {X}={z}\right)\right)$
27 24 26 mpbid ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \left({X}<{z}\vee {X}={z}\right)$
28 27 ord ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \left(¬{X}<{z}\to {X}={z}\right)$
29 16 28 mt3d ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to {X}<{z}$
30 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
31 25 rexrd ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to {z}\in {ℝ}^{*}$
32 elioo2 ${⊢}\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge {z}\in {ℝ}^{*}\right)\to \left({X}\in \left(\mathrm{-\infty },{z}\right)↔\left({X}\in ℝ\wedge \mathrm{-\infty }<{X}\wedge {X}<{z}\right)\right)$
33 30 31 32 sylancr ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \left({X}\in \left(\mathrm{-\infty },{z}\right)↔\left({X}\in ℝ\wedge \mathrm{-\infty }<{X}\wedge {X}<{z}\right)\right)$
34 10 11 29 33 mpbir3and ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to {X}\in \left(\mathrm{-\infty },{z}\right)$
35 inelcm ${⊢}\left({X}\in \left(\mathrm{-\infty },{z}\right)\wedge {X}\in {A}\right)\to \left(\mathrm{-\infty },{z}\right)\cap {A}\ne \varnothing$
36 34 9 35 syl2anc ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \left(\mathrm{-\infty },{z}\right)\cap {A}\ne \varnothing$
37 eleq1 ${⊢}{z}={Y}\to \left({z}\in {A}↔{Y}\in {A}\right)$
38 19 37 syl5ibrcom ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \left({z}={Y}\to {z}\in {A}\right)$
39 13 38 mtod ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to ¬{z}={Y}$
40 23 simp3d ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to {z}\le {Y}$
41 25 20 leloed ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \left({z}\le {Y}↔\left({z}<{Y}\vee {z}={Y}\right)\right)$
42 40 41 mpbid ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \left({z}<{Y}\vee {z}={Y}\right)$
43 42 ord ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \left(¬{z}<{Y}\to {z}={Y}\right)$
44 39 43 mt3d ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to {z}<{Y}$
45 20 ltpnfd ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to {Y}<\mathrm{+\infty }$
46 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
47 elioo2 ${⊢}\left({z}\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left({Y}\in \left({z},\mathrm{+\infty }\right)↔\left({Y}\in ℝ\wedge {z}<{Y}\wedge {Y}<\mathrm{+\infty }\right)\right)$
48 31 46 47 sylancl ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \left({Y}\in \left({z},\mathrm{+\infty }\right)↔\left({Y}\in ℝ\wedge {z}<{Y}\wedge {Y}<\mathrm{+\infty }\right)\right)$
49 20 44 45 48 mpbir3and ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to {Y}\in \left({z},\mathrm{+\infty }\right)$
50 inelcm ${⊢}\left({Y}\in \left({z},\mathrm{+\infty }\right)\wedge {Y}\in {A}\right)\to \left({z},\mathrm{+\infty }\right)\cap {A}\ne \varnothing$
51 49 19 50 syl2anc ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \left({z},\mathrm{+\infty }\right)\cap {A}\ne \varnothing$
52 inss1 ${⊢}\left(\left(\mathrm{-\infty },{z}\right)\cap \left({z},\mathrm{+\infty }\right)\right)\cap {A}\subseteq \left(\mathrm{-\infty },{z}\right)\cap \left({z},\mathrm{+\infty }\right)$
53 31 30 jctil ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \left(\mathrm{-\infty }\in {ℝ}^{*}\wedge {z}\in {ℝ}^{*}\right)$
54 31 46 jctir ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \left({z}\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)$
55 25 leidd ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to {z}\le {z}$
56 ioodisj ${⊢}\left(\left(\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge {z}\in {ℝ}^{*}\right)\wedge \left({z}\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\right)\wedge {z}\le {z}\right)\to \left(\mathrm{-\infty },{z}\right)\cap \left({z},\mathrm{+\infty }\right)=\varnothing$
57 53 54 55 56 syl21anc ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \left(\mathrm{-\infty },{z}\right)\cap \left({z},\mathrm{+\infty }\right)=\varnothing$
58 sseq0 ${⊢}\left(\left(\left(\mathrm{-\infty },{z}\right)\cap \left({z},\mathrm{+\infty }\right)\right)\cap {A}\subseteq \left(\mathrm{-\infty },{z}\right)\cap \left({z},\mathrm{+\infty }\right)\wedge \left(\mathrm{-\infty },{z}\right)\cap \left({z},\mathrm{+\infty }\right)=\varnothing \right)\to \left(\left(\mathrm{-\infty },{z}\right)\cap \left({z},\mathrm{+\infty }\right)\right)\cap {A}=\varnothing$
59 52 57 58 sylancr ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \left(\left(\mathrm{-\infty },{z}\right)\cap \left({z},\mathrm{+\infty }\right)\right)\cap {A}=\varnothing$
60 30 a1i ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \mathrm{-\infty }\in {ℝ}^{*}$
61 46 a1i ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \mathrm{+\infty }\in {ℝ}^{*}$
62 25 mnfltd ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \mathrm{-\infty }<{z}$
63 25 ltpnfd ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to {z}<\mathrm{+\infty }$
64 ioojoin ${⊢}\left(\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge {z}\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\wedge \left(\mathrm{-\infty }<{z}\wedge {z}<\mathrm{+\infty }\right)\right)\to \left(\left(\mathrm{-\infty },{z}\right)\cup \left\{{z}\right\}\right)\cup \left({z},\mathrm{+\infty }\right)=\left(\mathrm{-\infty },\mathrm{+\infty }\right)$
65 60 31 61 62 63 64 syl32anc ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \left(\left(\mathrm{-\infty },{z}\right)\cup \left\{{z}\right\}\right)\cup \left({z},\mathrm{+\infty }\right)=\left(\mathrm{-\infty },\mathrm{+\infty }\right)$
66 unass ${⊢}\left(\left(\mathrm{-\infty },{z}\right)\cup \left\{{z}\right\}\right)\cup \left({z},\mathrm{+\infty }\right)=\left(\mathrm{-\infty },{z}\right)\cup \left(\left\{{z}\right\}\cup \left({z},\mathrm{+\infty }\right)\right)$
67 un12 ${⊢}\left(\mathrm{-\infty },{z}\right)\cup \left(\left\{{z}\right\}\cup \left({z},\mathrm{+\infty }\right)\right)=\left\{{z}\right\}\cup \left(\left(\mathrm{-\infty },{z}\right)\cup \left({z},\mathrm{+\infty }\right)\right)$
68 66 67 eqtri ${⊢}\left(\left(\mathrm{-\infty },{z}\right)\cup \left\{{z}\right\}\right)\cup \left({z},\mathrm{+\infty }\right)=\left\{{z}\right\}\cup \left(\left(\mathrm{-\infty },{z}\right)\cup \left({z},\mathrm{+\infty }\right)\right)$
69 ioomax ${⊢}\left(\mathrm{-\infty },\mathrm{+\infty }\right)=ℝ$
70 65 68 69 3eqtr3g ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \left\{{z}\right\}\cup \left(\left(\mathrm{-\infty },{z}\right)\cup \left({z},\mathrm{+\infty }\right)\right)=ℝ$
71 4 70 sseqtrrd ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to {A}\subseteq \left\{{z}\right\}\cup \left(\left(\mathrm{-\infty },{z}\right)\cup \left({z},\mathrm{+\infty }\right)\right)$
72 disjsn ${⊢}{A}\cap \left\{{z}\right\}=\varnothing ↔¬{z}\in {A}$
73 13 72 sylibr ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to {A}\cap \left\{{z}\right\}=\varnothing$
74 disjssun ${⊢}{A}\cap \left\{{z}\right\}=\varnothing \to \left({A}\subseteq \left\{{z}\right\}\cup \left(\left(\mathrm{-\infty },{z}\right)\cup \left({z},\mathrm{+\infty }\right)\right)↔{A}\subseteq \left(\mathrm{-\infty },{z}\right)\cup \left({z},\mathrm{+\infty }\right)\right)$
75 73 74 syl ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to \left({A}\subseteq \left\{{z}\right\}\cup \left(\left(\mathrm{-\infty },{z}\right)\cup \left({z},\mathrm{+\infty }\right)\right)↔{A}\subseteq \left(\mathrm{-\infty },{z}\right)\cup \left({z},\mathrm{+\infty }\right)\right)$
76 71 75 mpbid ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to {A}\subseteq \left(\mathrm{-\infty },{z}\right)\cup \left({z},\mathrm{+\infty }\right)$
77 3 4 6 8 36 51 59 76 nconnsubb ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\wedge {z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\right)\to ¬\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}$
78 77 ex ${⊢}\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\to \left({z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)\to ¬\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)$
79 1 78 mt2d ${⊢}\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\to ¬{z}\in \left(\left[{X},{Y}\right]\setminus {A}\right)$
80 79 eq0rdv ${⊢}\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\to \left[{X},{Y}\right]\setminus {A}=\varnothing$
81 ssdif0 ${⊢}\left[{X},{Y}\right]\subseteq {A}↔\left[{X},{Y}\right]\setminus {A}=\varnothing$
82 80 81 sylibr ${⊢}\left(\left({A}\subseteq ℝ\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){↾}_{𝑡}{A}\in \mathrm{Conn}\right)\wedge \left({X}\in {A}\wedge {Y}\in {A}\right)\right)\to \left[{X},{Y}\right]\subseteq {A}$