MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reconnlem1 Structured version   Visualization version   GIF version

Theorem reconnlem1 22623
Description: Lemma for reconn 22625. Connectedness in the reals-easy direction. (Contributed by Jeff Hankins, 13-Jul-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.)
Assertion
Ref Expression
reconnlem1 (((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) → (𝑋[,]𝑌) ⊆ 𝐴)

Proof of Theorem reconnlem1
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 simplr 792 . . . 4 (((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) → ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn)
2 retopon 22561 . . . . . . 7 (topGen‘ran (,)) ∈ (TopOn‘ℝ)
32a1i 11 . . . . . 6 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (topGen‘ran (,)) ∈ (TopOn‘ℝ))
4 simplll 798 . . . . . 6 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝐴 ⊆ ℝ)
5 iooretop 22563 . . . . . . 7 (-∞(,)𝑧) ∈ (topGen‘ran (,))
65a1i 11 . . . . . 6 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (-∞(,)𝑧) ∈ (topGen‘ran (,)))
7 iooretop 22563 . . . . . . 7 (𝑧(,)+∞) ∈ (topGen‘ran (,))
87a1i 11 . . . . . 6 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝑧(,)+∞) ∈ (topGen‘ran (,)))
9 simplrl 800 . . . . . . . . 9 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑋𝐴)
104, 9sseldd 3602 . . . . . . . 8 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑋 ∈ ℝ)
11 mnflt 11954 . . . . . . . . 9 (𝑋 ∈ ℝ → -∞ < 𝑋)
1210, 11syl 17 . . . . . . . 8 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → -∞ < 𝑋)
13 eldifn 3731 . . . . . . . . . . 11 (𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴) → ¬ 𝑧𝐴)
1413adantl 482 . . . . . . . . . 10 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → ¬ 𝑧𝐴)
15 eleq1 2688 . . . . . . . . . . 11 (𝑋 = 𝑧 → (𝑋𝐴𝑧𝐴))
169, 15syl5ibcom 235 . . . . . . . . . 10 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝑋 = 𝑧𝑧𝐴))
1714, 16mtod 189 . . . . . . . . 9 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → ¬ 𝑋 = 𝑧)
18 eldifi 3730 . . . . . . . . . . . . . 14 (𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴) → 𝑧 ∈ (𝑋[,]𝑌))
1918adantl 482 . . . . . . . . . . . . 13 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑧 ∈ (𝑋[,]𝑌))
20 simplrr 801 . . . . . . . . . . . . . . 15 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑌𝐴)
214, 20sseldd 3602 . . . . . . . . . . . . . 14 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑌 ∈ ℝ)
22 elicc2 12235 . . . . . . . . . . . . . 14 ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑧 ∈ (𝑋[,]𝑌) ↔ (𝑧 ∈ ℝ ∧ 𝑋𝑧𝑧𝑌)))
2310, 21, 22syl2anc 693 . . . . . . . . . . . . 13 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝑧 ∈ (𝑋[,]𝑌) ↔ (𝑧 ∈ ℝ ∧ 𝑋𝑧𝑧𝑌)))
2419, 23mpbid 222 . . . . . . . . . . . 12 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝑧 ∈ ℝ ∧ 𝑋𝑧𝑧𝑌))
2524simp2d 1073 . . . . . . . . . . 11 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑋𝑧)
2624simp1d 1072 . . . . . . . . . . . 12 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑧 ∈ ℝ)
2710, 26leloed 10177 . . . . . . . . . . 11 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝑋𝑧 ↔ (𝑋 < 𝑧𝑋 = 𝑧)))
2825, 27mpbid 222 . . . . . . . . . 10 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝑋 < 𝑧𝑋 = 𝑧))
2928ord 392 . . . . . . . . 9 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (¬ 𝑋 < 𝑧𝑋 = 𝑧))
3017, 29mt3d 140 . . . . . . . 8 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑋 < 𝑧)
31 mnfxr 10093 . . . . . . . . 9 -∞ ∈ ℝ*
3226rexrd 10086 . . . . . . . . 9 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑧 ∈ ℝ*)
33 elioo2 12213 . . . . . . . . 9 ((-∞ ∈ ℝ*𝑧 ∈ ℝ*) → (𝑋 ∈ (-∞(,)𝑧) ↔ (𝑋 ∈ ℝ ∧ -∞ < 𝑋𝑋 < 𝑧)))
3431, 32, 33sylancr 695 . . . . . . . 8 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝑋 ∈ (-∞(,)𝑧) ↔ (𝑋 ∈ ℝ ∧ -∞ < 𝑋𝑋 < 𝑧)))
3510, 12, 30, 34mpbir3and 1244 . . . . . . 7 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑋 ∈ (-∞(,)𝑧))
36 inelcm 4030 . . . . . . 7 ((𝑋 ∈ (-∞(,)𝑧) ∧ 𝑋𝐴) → ((-∞(,)𝑧) ∩ 𝐴) ≠ ∅)
3735, 9, 36syl2anc 693 . . . . . 6 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → ((-∞(,)𝑧) ∩ 𝐴) ≠ ∅)
38 eleq1 2688 . . . . . . . . . . 11 (𝑧 = 𝑌 → (𝑧𝐴𝑌𝐴))
3920, 38syl5ibrcom 237 . . . . . . . . . 10 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝑧 = 𝑌𝑧𝐴))
4014, 39mtod 189 . . . . . . . . 9 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → ¬ 𝑧 = 𝑌)
4124simp3d 1074 . . . . . . . . . . 11 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑧𝑌)
4226, 21leloed 10177 . . . . . . . . . . 11 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝑧𝑌 ↔ (𝑧 < 𝑌𝑧 = 𝑌)))
4341, 42mpbid 222 . . . . . . . . . 10 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝑧 < 𝑌𝑧 = 𝑌))
4443ord 392 . . . . . . . . 9 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (¬ 𝑧 < 𝑌𝑧 = 𝑌))
4540, 44mt3d 140 . . . . . . . 8 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑧 < 𝑌)
46 ltpnf 11951 . . . . . . . . 9 (𝑌 ∈ ℝ → 𝑌 < +∞)
4721, 46syl 17 . . . . . . . 8 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑌 < +∞)
48 pnfxr 10089 . . . . . . . . 9 +∞ ∈ ℝ*
49 elioo2 12213 . . . . . . . . 9 ((𝑧 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝑌 ∈ (𝑧(,)+∞) ↔ (𝑌 ∈ ℝ ∧ 𝑧 < 𝑌𝑌 < +∞)))
5032, 48, 49sylancl 694 . . . . . . . 8 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝑌 ∈ (𝑧(,)+∞) ↔ (𝑌 ∈ ℝ ∧ 𝑧 < 𝑌𝑌 < +∞)))
5121, 45, 47, 50mpbir3and 1244 . . . . . . 7 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑌 ∈ (𝑧(,)+∞))
52 inelcm 4030 . . . . . . 7 ((𝑌 ∈ (𝑧(,)+∞) ∧ 𝑌𝐴) → ((𝑧(,)+∞) ∩ 𝐴) ≠ ∅)
5351, 20, 52syl2anc 693 . . . . . 6 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → ((𝑧(,)+∞) ∩ 𝐴) ≠ ∅)
54 inss1 3831 . . . . . . 7 (((-∞(,)𝑧) ∩ (𝑧(,)+∞)) ∩ 𝐴) ⊆ ((-∞(,)𝑧) ∩ (𝑧(,)+∞))
5532, 31jctil 560 . . . . . . . 8 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (-∞ ∈ ℝ*𝑧 ∈ ℝ*))
5632, 48jctir 561 . . . . . . . 8 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝑧 ∈ ℝ* ∧ +∞ ∈ ℝ*))
5726leidd 10591 . . . . . . . 8 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑧𝑧)
58 ioodisj 12299 . . . . . . . 8 ((((-∞ ∈ ℝ*𝑧 ∈ ℝ*) ∧ (𝑧 ∈ ℝ* ∧ +∞ ∈ ℝ*)) ∧ 𝑧𝑧) → ((-∞(,)𝑧) ∩ (𝑧(,)+∞)) = ∅)
5955, 56, 57, 58syl21anc 1324 . . . . . . 7 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → ((-∞(,)𝑧) ∩ (𝑧(,)+∞)) = ∅)
60 sseq0 3973 . . . . . . 7 (((((-∞(,)𝑧) ∩ (𝑧(,)+∞)) ∩ 𝐴) ⊆ ((-∞(,)𝑧) ∩ (𝑧(,)+∞)) ∧ ((-∞(,)𝑧) ∩ (𝑧(,)+∞)) = ∅) → (((-∞(,)𝑧) ∩ (𝑧(,)+∞)) ∩ 𝐴) = ∅)
6154, 59, 60sylancr 695 . . . . . 6 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (((-∞(,)𝑧) ∩ (𝑧(,)+∞)) ∩ 𝐴) = ∅)
6231a1i 11 . . . . . . . . . 10 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → -∞ ∈ ℝ*)
6348a1i 11 . . . . . . . . . 10 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → +∞ ∈ ℝ*)
64 mnflt 11954 . . . . . . . . . . 11 (𝑧 ∈ ℝ → -∞ < 𝑧)
6526, 64syl 17 . . . . . . . . . 10 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → -∞ < 𝑧)
66 ltpnf 11951 . . . . . . . . . . 11 (𝑧 ∈ ℝ → 𝑧 < +∞)
6726, 66syl 17 . . . . . . . . . 10 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝑧 < +∞)
68 ioojoin 12300 . . . . . . . . . 10 (((-∞ ∈ ℝ*𝑧 ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (-∞ < 𝑧𝑧 < +∞)) → (((-∞(,)𝑧) ∪ {𝑧}) ∪ (𝑧(,)+∞)) = (-∞(,)+∞))
6962, 32, 63, 65, 67, 68syl32anc 1333 . . . . . . . . 9 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (((-∞(,)𝑧) ∪ {𝑧}) ∪ (𝑧(,)+∞)) = (-∞(,)+∞))
70 unass 3768 . . . . . . . . . 10 (((-∞(,)𝑧) ∪ {𝑧}) ∪ (𝑧(,)+∞)) = ((-∞(,)𝑧) ∪ ({𝑧} ∪ (𝑧(,)+∞)))
71 un12 3769 . . . . . . . . . 10 ((-∞(,)𝑧) ∪ ({𝑧} ∪ (𝑧(,)+∞))) = ({𝑧} ∪ ((-∞(,)𝑧) ∪ (𝑧(,)+∞)))
7270, 71eqtri 2643 . . . . . . . . 9 (((-∞(,)𝑧) ∪ {𝑧}) ∪ (𝑧(,)+∞)) = ({𝑧} ∪ ((-∞(,)𝑧) ∪ (𝑧(,)+∞)))
73 ioomax 12245 . . . . . . . . 9 (-∞(,)+∞) = ℝ
7469, 72, 733eqtr3g 2678 . . . . . . . 8 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → ({𝑧} ∪ ((-∞(,)𝑧) ∪ (𝑧(,)+∞))) = ℝ)
754, 74sseqtr4d 3640 . . . . . . 7 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝐴 ⊆ ({𝑧} ∪ ((-∞(,)𝑧) ∪ (𝑧(,)+∞))))
76 disjsn 4244 . . . . . . . . 9 ((𝐴 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝐴)
7714, 76sylibr 224 . . . . . . . 8 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝐴 ∩ {𝑧}) = ∅)
78 disjssun 4034 . . . . . . . 8 ((𝐴 ∩ {𝑧}) = ∅ → (𝐴 ⊆ ({𝑧} ∪ ((-∞(,)𝑧) ∪ (𝑧(,)+∞))) ↔ 𝐴 ⊆ ((-∞(,)𝑧) ∪ (𝑧(,)+∞))))
7977, 78syl 17 . . . . . . 7 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → (𝐴 ⊆ ({𝑧} ∪ ((-∞(,)𝑧) ∪ (𝑧(,)+∞))) ↔ 𝐴 ⊆ ((-∞(,)𝑧) ∪ (𝑧(,)+∞))))
8075, 79mpbid 222 . . . . . 6 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → 𝐴 ⊆ ((-∞(,)𝑧) ∪ (𝑧(,)+∞)))
813, 4, 6, 8, 37, 53, 61, 80nconnsubb 21220 . . . . 5 ((((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) ∧ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴)) → ¬ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn)
8281ex 450 . . . 4 (((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) → (𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴) → ¬ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn))
831, 82mt2d 131 . . 3 (((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) → ¬ 𝑧 ∈ ((𝑋[,]𝑌) ∖ 𝐴))
8483eq0rdv 3977 . 2 (((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) → ((𝑋[,]𝑌) ∖ 𝐴) = ∅)
85 ssdif0 3940 . 2 ((𝑋[,]𝑌) ⊆ 𝐴 ↔ ((𝑋[,]𝑌) ∖ 𝐴) = ∅)
8684, 85sylibr 224 1 (((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋𝐴𝑌𝐴)) → (𝑋[,]𝑌) ⊆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3a 1037   = wceq 1482  wcel 1989  wne 2793  cdif 3569  cun 3570  cin 3571  wss 3572  c0 3913  {csn 4175   class class class wbr 4651  ran crn 5113  cfv 5886  (class class class)co 6647  cr 9932  +∞cpnf 10068  -∞cmnf 10069  *cxr 10070   < clt 10071  cle 10072  (,)cioo 12172  [,]cicc 12175  t crest 16075  topGenctg 16092  TopOnctopon 20709  Conncconn 21208
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-rep 4769  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946  ax-cnex 9989  ax-resscn 9990  ax-1cn 9991  ax-icn 9992  ax-addcl 9993  ax-addrcl 9994  ax-mulcl 9995  ax-mulrcl 9996  ax-mulcom 9997  ax-addass 9998  ax-mulass 9999  ax-distr 10000  ax-i2m1 10001  ax-1ne0 10002  ax-1rid 10003  ax-rnegex 10004  ax-rrecex 10005  ax-cnre 10006  ax-pre-lttri 10007  ax-pre-lttrn 10008  ax-pre-ltadd 10009  ax-pre-mulgt0 10010  ax-pre-sup 10011
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-nel 2897  df-ral 2916  df-rex 2917  df-reu 2918  df-rmo 2919  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-int 4474  df-iun 4520  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-riota 6608  df-ov 6650  df-oprab 6651  df-mpt2 6652  df-om 7063  df-1st 7165  df-2nd 7166  df-wrecs 7404  df-recs 7465  df-rdg 7503  df-oadd 7561  df-er 7739  df-en 7953  df-dom 7954  df-sdom 7955  df-fin 7956  df-fi 8314  df-sup 8345  df-inf 8346  df-pnf 10073  df-mnf 10074  df-xr 10075  df-ltxr 10076  df-le 10077  df-sub 10265  df-neg 10266  df-div 10682  df-nn 11018  df-n0 11290  df-z 11375  df-uz 11685  df-q 11786  df-ioo 12176  df-ico 12178  df-icc 12179  df-rest 16077  df-topgen 16098  df-top 20693  df-topon 20710  df-bases 20744  df-cld 20817  df-conn 21209
This theorem is referenced by:  reconn  22625
  Copyright terms: Public domain W3C validator