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 ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( 𝑋 [,] 𝑌 ) ⊆ 𝐴 )

Proof

Step Hyp Ref Expression
1 simplr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn )
2 retopon ⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
3 2 a1i ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) )
4 simplll ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → 𝐴 ⊆ ℝ )
5 iooretop ⊢ ( -∞ (,) 𝑧 ) ∈ ( topGen ‘ ran (,) )
6 5 a1i ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( -∞ (,) 𝑧 ) ∈ ( topGen ‘ ran (,) ) )
7 iooretop ⊢ ( 𝑧 (,) +∞ ) ∈ ( topGen ‘ ran (,) )
8 7 a1i ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( 𝑧 (,) +∞ ) ∈ ( topGen ‘ ran (,) ) )
9 simplrl ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → 𝑋 ∈ 𝐴 )
10 4 9 sseldd ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → 𝑋 ∈ ℝ )
11 10 mnfltd ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → -∞ < 𝑋 )
12 eldifn ⊢ ( 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) → ¬ 𝑧 ∈ 𝐴 )
13 12 adantl ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ¬ 𝑧 ∈ 𝐴 )
14 eleq1 ⊢ ( 𝑋 = 𝑧 → ( 𝑋 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
15 9 14 syl5ibcom ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( 𝑋 = 𝑧 → 𝑧 ∈ 𝐴 ) )
16 13 15 mtod ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ¬ 𝑋 = 𝑧 )
17 eldifi ⊢ ( 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) → 𝑧 ∈ ( 𝑋 [,] 𝑌 ) )
18 17 adantl ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → 𝑧 ∈ ( 𝑋 [,] 𝑌 ) )
19 simplrr ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → 𝑌 ∈ 𝐴 )
20 4 19 sseldd ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → 𝑌 ∈ ℝ )
21 elicc2 ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ↔ ( 𝑧 ∈ ℝ ∧ 𝑋 ≤ 𝑧 ∧ 𝑧 ≤ 𝑌 ) ) )
22 10 20 21 syl2anc ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( 𝑧 ∈ ( 𝑋 [,] 𝑌 ) ↔ ( 𝑧 ∈ ℝ ∧ 𝑋 ≤ 𝑧 ∧ 𝑧 ≤ 𝑌 ) ) )
23 18 22 mpbid ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( 𝑧 ∈ ℝ ∧ 𝑋 ≤ 𝑧 ∧ 𝑧 ≤ 𝑌 ) )
24 23 simp2d ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → 𝑋 ≤ 𝑧 )
25 23 simp1d ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → 𝑧 ∈ ℝ )
26 10 25 leloed ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( 𝑋 ≤ 𝑧 ↔ ( 𝑋 < 𝑧 ∨ 𝑋 = 𝑧 ) ) )
27 24 26 mpbid ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( 𝑋 < 𝑧 ∨ 𝑋 = 𝑧 ) )
28 27 ord ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( ¬ 𝑋 < 𝑧 → 𝑋 = 𝑧 ) )
29 16 28 mt3d ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → 𝑋 < 𝑧 )
30 mnfxr ⊢ -∞ ∈ ℝ*
31 25 rexrd ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → 𝑧 ∈ ℝ* )
32 elioo2 ⊢ ( ( -∞ ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) → ( 𝑋 ∈ ( -∞ (,) 𝑧 ) ↔ ( 𝑋 ∈ ℝ ∧ -∞ < 𝑋 ∧ 𝑋 < 𝑧 ) ) )
33 30 31 32 sylancr ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( 𝑋 ∈ ( -∞ (,) 𝑧 ) ↔ ( 𝑋 ∈ ℝ ∧ -∞ < 𝑋 ∧ 𝑋 < 𝑧 ) ) )
34 10 11 29 33 mpbir3and ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → 𝑋 ∈ ( -∞ (,) 𝑧 ) )
35 inelcm ⊢ ( ( 𝑋 ∈ ( -∞ (,) 𝑧 ) ∧ 𝑋 ∈ 𝐴 ) → ( ( -∞ (,) 𝑧 ) ∩ 𝐴 ) ≠ ∅ )
36 34 9 35 syl2anc ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( ( -∞ (,) 𝑧 ) ∩ 𝐴 ) ≠ ∅ )
37 eleq1 ⊢ ( 𝑧 = 𝑌 → ( 𝑧 ∈ 𝐴 ↔ 𝑌 ∈ 𝐴 ) )
38 19 37 syl5ibrcom ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( 𝑧 = 𝑌 → 𝑧 ∈ 𝐴 ) )
39 13 38 mtod ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ¬ 𝑧 = 𝑌 )
40 23 simp3d ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → 𝑧 ≤ 𝑌 )
41 25 20 leloed ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( 𝑧 ≤ 𝑌 ↔ ( 𝑧 < 𝑌 ∨ 𝑧 = 𝑌 ) ) )
42 40 41 mpbid ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( 𝑧 < 𝑌 ∨ 𝑧 = 𝑌 ) )
43 42 ord ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( ¬ 𝑧 < 𝑌 → 𝑧 = 𝑌 ) )
44 39 43 mt3d ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → 𝑧 < 𝑌 )
45 20 ltpnfd ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → 𝑌 < +∞ )
46 pnfxr ⊢ +∞ ∈ ℝ*
47 elioo2 ⊢ ( ( 𝑧 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝑌 ∈ ( 𝑧 (,) +∞ ) ↔ ( 𝑌 ∈ ℝ ∧ 𝑧 < 𝑌 ∧ 𝑌 < +∞ ) ) )
48 31 46 47 sylancl ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( 𝑌 ∈ ( 𝑧 (,) +∞ ) ↔ ( 𝑌 ∈ ℝ ∧ 𝑧 < 𝑌 ∧ 𝑌 < +∞ ) ) )
49 20 44 45 48 mpbir3and ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → 𝑌 ∈ ( 𝑧 (,) +∞ ) )
50 inelcm ⊢ ( ( 𝑌 ∈ ( 𝑧 (,) +∞ ) ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝑧 (,) +∞ ) ∩ 𝐴 ) ≠ ∅ )
51 49 19 50 syl2anc ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( ( 𝑧 (,) +∞ ) ∩ 𝐴 ) ≠ ∅ )
52 inss1 ⊢ ( ( ( -∞ (,) 𝑧 ) ∩ ( 𝑧 (,) +∞ ) ) ∩ 𝐴 ) ⊆ ( ( -∞ (,) 𝑧 ) ∩ ( 𝑧 (,) +∞ ) )
53 31 30 jctil ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( -∞ ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) )
54 31 46 jctir ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( 𝑧 ∈ ℝ* ∧ +∞ ∈ ℝ* ) )
55 25 leidd ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → 𝑧 ≤ 𝑧 )
56 ioodisj ⊢ ( ( ( ( -∞ ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( 𝑧 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ) ∧ 𝑧 ≤ 𝑧 ) → ( ( -∞ (,) 𝑧 ) ∩ ( 𝑧 (,) +∞ ) ) = ∅ )
57 53 54 55 56 syl21anc ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( ( -∞ (,) 𝑧 ) ∩ ( 𝑧 (,) +∞ ) ) = ∅ )
58 sseq0 ⊢ ( ( ( ( ( -∞ (,) 𝑧 ) ∩ ( 𝑧 (,) +∞ ) ) ∩ 𝐴 ) ⊆ ( ( -∞ (,) 𝑧 ) ∩ ( 𝑧 (,) +∞ ) ) ∧ ( ( -∞ (,) 𝑧 ) ∩ ( 𝑧 (,) +∞ ) ) = ∅ ) → ( ( ( -∞ (,) 𝑧 ) ∩ ( 𝑧 (,) +∞ ) ) ∩ 𝐴 ) = ∅ )
59 52 57 58 sylancr ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( ( ( -∞ (,) 𝑧 ) ∩ ( 𝑧 (,) +∞ ) ) ∩ 𝐴 ) = ∅ )
60 30 a1i ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → -∞ ∈ ℝ* )
61 46 a1i ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → +∞ ∈ ℝ* )
62 25 mnfltd ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → -∞ < 𝑧 )
63 25 ltpnfd ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → 𝑧 < +∞ )
64 ioojoin ⊢ ( ( ( -∞ ∈ ℝ* ∧ 𝑧 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( -∞ < 𝑧 ∧ 𝑧 < +∞ ) ) → ( ( ( -∞ (,) 𝑧 ) ∪ { 𝑧 } ) ∪ ( 𝑧 (,) +∞ ) ) = ( -∞ (,) +∞ ) )
65 60 31 61 62 63 64 syl32anc ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( ( ( -∞ (,) 𝑧 ) ∪ { 𝑧 } ) ∪ ( 𝑧 (,) +∞ ) ) = ( -∞ (,) +∞ ) )
66 unass ⊢ ( ( ( -∞ (,) 𝑧 ) ∪ { 𝑧 } ) ∪ ( 𝑧 (,) +∞ ) ) = ( ( -∞ (,) 𝑧 ) ∪ ( { 𝑧 } ∪ ( 𝑧 (,) +∞ ) ) )
67 un12 ⊢ ( ( -∞ (,) 𝑧 ) ∪ ( { 𝑧 } ∪ ( 𝑧 (,) +∞ ) ) ) = ( { 𝑧 } ∪ ( ( -∞ (,) 𝑧 ) ∪ ( 𝑧 (,) +∞ ) ) )
68 66 67 eqtri ⊢ ( ( ( -∞ (,) 𝑧 ) ∪ { 𝑧 } ) ∪ ( 𝑧 (,) +∞ ) ) = ( { 𝑧 } ∪ ( ( -∞ (,) 𝑧 ) ∪ ( 𝑧 (,) +∞ ) ) )
69 ioomax ⊢ ( -∞ (,) +∞ ) = ℝ
70 65 68 69 3eqtr3g ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( { 𝑧 } ∪ ( ( -∞ (,) 𝑧 ) ∪ ( 𝑧 (,) +∞ ) ) ) = ℝ )
71 4 70 sseqtrrd ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → 𝐴 ⊆ ( { 𝑧 } ∪ ( ( -∞ (,) 𝑧 ) ∪ ( 𝑧 (,) +∞ ) ) ) )
72 disjsn ⊢ ( ( 𝐴 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ 𝐴 )
73 13 72 sylibr ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( 𝐴 ∩ { 𝑧 } ) = ∅ )
74 disjssun ⊢ ( ( 𝐴 ∩ { 𝑧 } ) = ∅ → ( 𝐴 ⊆ ( { 𝑧 } ∪ ( ( -∞ (,) 𝑧 ) ∪ ( 𝑧 (,) +∞ ) ) ) ↔ 𝐴 ⊆ ( ( -∞ (,) 𝑧 ) ∪ ( 𝑧 (,) +∞ ) ) ) )
75 73 74 syl ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ( 𝐴 ⊆ ( { 𝑧 } ∪ ( ( -∞ (,) 𝑧 ) ∪ ( 𝑧 (,) +∞ ) ) ) ↔ 𝐴 ⊆ ( ( -∞ (,) 𝑧 ) ∪ ( 𝑧 (,) +∞ ) ) ) )
76 71 75 mpbid ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → 𝐴 ⊆ ( ( -∞ (,) 𝑧 ) ∪ ( 𝑧 (,) +∞ ) ) )
77 3 4 6 8 36 51 59 76 nconnsubb ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) ∧ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) ) → ¬ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn )
78 77 ex ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) → ¬ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) )
79 1 78 mt2d ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ¬ 𝑧 ∈ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) )
80 79 eq0rdv ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) = ∅ )
81 ssdif0 ⊢ ( ( 𝑋 [,] 𝑌 ) ⊆ 𝐴 ↔ ( ( 𝑋 [,] 𝑌 ) ∖ 𝐴 ) = ∅ )
82 80 81 sylibr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( 𝑋 [,] 𝑌 ) ⊆ 𝐴 )