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

Theorem reconnlem2 22438
 Description: Lemma for reconn 22439. (Contributed by Jeff Hankins, 17-Aug-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.)
Hypotheses
Ref Expression
reconnlem2.1 (𝜑𝐴 ⊆ ℝ)
reconnlem2.2 (𝜑𝑈 ∈ (topGen‘ran (,)))
reconnlem2.3 (𝜑𝑉 ∈ (topGen‘ran (,)))
reconnlem2.4 (𝜑 → ∀𝑥𝐴𝑦𝐴 (𝑥[,]𝑦) ⊆ 𝐴)
reconnlem2.5 (𝜑𝐵 ∈ (𝑈𝐴))
reconnlem2.6 (𝜑𝐶 ∈ (𝑉𝐴))
reconnlem2.7 (𝜑 → (𝑈𝑉) ⊆ (ℝ ∖ 𝐴))
reconnlem2.8 (𝜑𝐵𝐶)
reconnlem2.9 𝑆 = sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < )
Assertion
Ref Expression
reconnlem2 (𝜑 → ¬ 𝐴 ⊆ (𝑈𝑉))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑦,𝐶
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐶(𝑥)   𝑆(𝑥,𝑦)   𝑈(𝑥,𝑦)   𝑉(𝑥,𝑦)

Proof of Theorem reconnlem2
Dummy variables 𝑤 𝑧 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reconnlem2.9 . . . . . . . . . . 11 𝑆 = sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < )
2 inss2 3796 . . . . . . . . . . . . 13 (𝑈 ∩ (𝐵[,]𝐶)) ⊆ (𝐵[,]𝐶)
3 inss2 3796 . . . . . . . . . . . . . . . 16 (𝑈𝐴) ⊆ 𝐴
4 reconnlem2.5 . . . . . . . . . . . . . . . 16 (𝜑𝐵 ∈ (𝑈𝐴))
53, 4sseldi 3566 . . . . . . . . . . . . . . 15 (𝜑𝐵𝐴)
6 inss2 3796 . . . . . . . . . . . . . . . 16 (𝑉𝐴) ⊆ 𝐴
7 reconnlem2.6 . . . . . . . . . . . . . . . 16 (𝜑𝐶 ∈ (𝑉𝐴))
86, 7sseldi 3566 . . . . . . . . . . . . . . 15 (𝜑𝐶𝐴)
9 reconnlem2.4 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑥𝐴𝑦𝐴 (𝑥[,]𝑦) ⊆ 𝐴)
10 oveq1 6556 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐵 → (𝑥[,]𝑦) = (𝐵[,]𝑦))
1110sseq1d 3595 . . . . . . . . . . . . . . . 16 (𝑥 = 𝐵 → ((𝑥[,]𝑦) ⊆ 𝐴 ↔ (𝐵[,]𝑦) ⊆ 𝐴))
12 oveq2 6557 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝐶 → (𝐵[,]𝑦) = (𝐵[,]𝐶))
1312sseq1d 3595 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐶 → ((𝐵[,]𝑦) ⊆ 𝐴 ↔ (𝐵[,]𝐶) ⊆ 𝐴))
1411, 13rspc2va 3294 . . . . . . . . . . . . . . 15 (((𝐵𝐴𝐶𝐴) ∧ ∀𝑥𝐴𝑦𝐴 (𝑥[,]𝑦) ⊆ 𝐴) → (𝐵[,]𝐶) ⊆ 𝐴)
155, 8, 9, 14syl21anc 1317 . . . . . . . . . . . . . 14 (𝜑 → (𝐵[,]𝐶) ⊆ 𝐴)
16 reconnlem2.1 . . . . . . . . . . . . . 14 (𝜑𝐴 ⊆ ℝ)
1715, 16sstrd 3578 . . . . . . . . . . . . 13 (𝜑 → (𝐵[,]𝐶) ⊆ ℝ)
182, 17syl5ss 3579 . . . . . . . . . . . 12 (𝜑 → (𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ)
19 inss1 3795 . . . . . . . . . . . . . . 15 (𝑈𝐴) ⊆ 𝑈
2019, 4sseldi 3566 . . . . . . . . . . . . . 14 (𝜑𝐵𝑈)
2116, 5sseldd 3569 . . . . . . . . . . . . . . . 16 (𝜑𝐵 ∈ ℝ)
2221rexrd 9968 . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ ℝ*)
2316, 8sseldd 3569 . . . . . . . . . . . . . . . 16 (𝜑𝐶 ∈ ℝ)
2423rexrd 9968 . . . . . . . . . . . . . . 15 (𝜑𝐶 ∈ ℝ*)
25 reconnlem2.8 . . . . . . . . . . . . . . 15 (𝜑𝐵𝐶)
26 lbicc2 12159 . . . . . . . . . . . . . . 15 ((𝐵 ∈ ℝ*𝐶 ∈ ℝ*𝐵𝐶) → 𝐵 ∈ (𝐵[,]𝐶))
2722, 24, 25, 26syl3anc 1318 . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ (𝐵[,]𝐶))
2820, 27elind 3760 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ (𝑈 ∩ (𝐵[,]𝐶)))
29 ne0i 3880 . . . . . . . . . . . . 13 (𝐵 ∈ (𝑈 ∩ (𝐵[,]𝐶)) → (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅)
3028, 29syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅)
312sseli 3564 . . . . . . . . . . . . . . 15 (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) → 𝑤 ∈ (𝐵[,]𝐶))
32 elicc2 12109 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑤 ∈ (𝐵[,]𝐶) ↔ (𝑤 ∈ ℝ ∧ 𝐵𝑤𝑤𝐶)))
3321, 23, 32syl2anc 691 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑤 ∈ (𝐵[,]𝐶) ↔ (𝑤 ∈ ℝ ∧ 𝐵𝑤𝑤𝐶)))
34 simp3 1056 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ ℝ ∧ 𝐵𝑤𝑤𝐶) → 𝑤𝐶)
3533, 34syl6bi 242 . . . . . . . . . . . . . . 15 (𝜑 → (𝑤 ∈ (𝐵[,]𝐶) → 𝑤𝐶))
3631, 35syl5 33 . . . . . . . . . . . . . 14 (𝜑 → (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) → 𝑤𝐶))
3736ralrimiv 2948 . . . . . . . . . . . . 13 (𝜑 → ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤𝐶)
38 breq2 4587 . . . . . . . . . . . . . . 15 (𝑧 = 𝐶 → (𝑤𝑧𝑤𝐶))
3938ralbidv 2969 . . . . . . . . . . . . . 14 (𝑧 = 𝐶 → (∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤𝑧 ↔ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤𝐶))
4039rspcev 3282 . . . . . . . . . . . . 13 ((𝐶 ∈ ℝ ∧ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤𝐶) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤𝑧)
4123, 37, 40syl2anc 691 . . . . . . . . . . . 12 (𝜑 → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤𝑧)
42 suprcl 10862 . . . . . . . . . . . 12 (((𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ ∧ (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤𝑧) → sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ∈ ℝ)
4318, 30, 41, 42syl3anc 1318 . . . . . . . . . . 11 (𝜑 → sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ∈ ℝ)
441, 43syl5eqel 2692 . . . . . . . . . 10 (𝜑𝑆 ∈ ℝ)
45 rphalfcl 11734 . . . . . . . . . 10 (𝑟 ∈ ℝ+ → (𝑟 / 2) ∈ ℝ+)
46 ltaddrp 11743 . . . . . . . . . 10 ((𝑆 ∈ ℝ ∧ (𝑟 / 2) ∈ ℝ+) → 𝑆 < (𝑆 + (𝑟 / 2)))
4744, 45, 46syl2an 493 . . . . . . . . 9 ((𝜑𝑟 ∈ ℝ+) → 𝑆 < (𝑆 + (𝑟 / 2)))
4844adantr 480 . . . . . . . . . 10 ((𝜑𝑟 ∈ ℝ+) → 𝑆 ∈ ℝ)
4945rpred 11748 . . . . . . . . . . 11 (𝑟 ∈ ℝ+ → (𝑟 / 2) ∈ ℝ)
50 readdcl 9898 . . . . . . . . . . 11 ((𝑆 ∈ ℝ ∧ (𝑟 / 2) ∈ ℝ) → (𝑆 + (𝑟 / 2)) ∈ ℝ)
5144, 49, 50syl2an 493 . . . . . . . . . 10 ((𝜑𝑟 ∈ ℝ+) → (𝑆 + (𝑟 / 2)) ∈ ℝ)
5248, 51ltnled 10063 . . . . . . . . 9 ((𝜑𝑟 ∈ ℝ+) → (𝑆 < (𝑆 + (𝑟 / 2)) ↔ ¬ (𝑆 + (𝑟 / 2)) ≤ 𝑆))
5347, 52mpbid 221 . . . . . . . 8 ((𝜑𝑟 ∈ ℝ+) → ¬ (𝑆 + (𝑟 / 2)) ≤ 𝑆)
5418ad2antrr 758 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ)
5530ad2antrr 758 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅)
5641ad2antrr 758 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤𝑧)
57 inss1 3795 . . . . . . . . . . . 12 (𝑈 ∩ (-∞(,)𝐶)) ⊆ 𝑈
58 simpr 476 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶)))
5957, 58sseldi 3566 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ∈ 𝑈)
6051adantr 480 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ∈ ℝ)
6121ad2antrr 758 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → 𝐵 ∈ ℝ)
6244ad2antrr 758 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → 𝑆 ∈ ℝ)
63 suprub 10863 . . . . . . . . . . . . . . . 16 ((((𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ ∧ (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤𝑧) ∧ 𝐵 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → 𝐵 ≤ sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ))
6418, 30, 41, 28, 63syl31anc 1321 . . . . . . . . . . . . . . 15 (𝜑𝐵 ≤ sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ))
6564, 1syl6breqr 4625 . . . . . . . . . . . . . 14 (𝜑𝐵𝑆)
6665ad2antrr 758 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → 𝐵𝑆)
6747adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → 𝑆 < (𝑆 + (𝑟 / 2)))
6862, 60, 67ltled 10064 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → 𝑆 ≤ (𝑆 + (𝑟 / 2)))
6961, 62, 60, 66, 68letrd 10073 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → 𝐵 ≤ (𝑆 + (𝑟 / 2)))
7023ad2antrr 758 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → 𝐶 ∈ ℝ)
71 inss2 3796 . . . . . . . . . . . . . . 15 (𝑈 ∩ (-∞(,)𝐶)) ⊆ (-∞(,)𝐶)
7271, 58sseldi 3566 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ∈ (-∞(,)𝐶))
73 eliooord 12104 . . . . . . . . . . . . . . 15 ((𝑆 + (𝑟 / 2)) ∈ (-∞(,)𝐶) → (-∞ < (𝑆 + (𝑟 / 2)) ∧ (𝑆 + (𝑟 / 2)) < 𝐶))
7473simprd 478 . . . . . . . . . . . . . 14 ((𝑆 + (𝑟 / 2)) ∈ (-∞(,)𝐶) → (𝑆 + (𝑟 / 2)) < 𝐶)
7572, 74syl 17 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) < 𝐶)
7660, 70, 75ltled 10064 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ≤ 𝐶)
77 elicc2 12109 . . . . . . . . . . . . 13 ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝑆 + (𝑟 / 2)) ∈ (𝐵[,]𝐶) ↔ ((𝑆 + (𝑟 / 2)) ∈ ℝ ∧ 𝐵 ≤ (𝑆 + (𝑟 / 2)) ∧ (𝑆 + (𝑟 / 2)) ≤ 𝐶)))
7861, 70, 77syl2anc 691 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → ((𝑆 + (𝑟 / 2)) ∈ (𝐵[,]𝐶) ↔ ((𝑆 + (𝑟 / 2)) ∈ ℝ ∧ 𝐵 ≤ (𝑆 + (𝑟 / 2)) ∧ (𝑆 + (𝑟 / 2)) ≤ 𝐶)))
7960, 69, 76, 78mpbir3and 1238 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ∈ (𝐵[,]𝐶))
8059, 79elind 3760 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (𝐵[,]𝐶)))
81 suprub 10863 . . . . . . . . . 10 ((((𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ ∧ (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤𝑧) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (𝐵[,]𝐶))) → (𝑆 + (𝑟 / 2)) ≤ sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ))
8254, 55, 56, 80, 81syl31anc 1321 . . . . . . . . 9 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ≤ sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ))
8382, 1syl6breqr 4625 . . . . . . . 8 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ≤ 𝑆)
8453, 83mtand 689 . . . . . . 7 ((𝜑𝑟 ∈ ℝ+) → ¬ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶)))
85 eqid 2610 . . . . . . . . . . . . 13 ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
8685remetdval 22400 . . . . . . . . . . . 12 (((𝑆 + (𝑟 / 2)) ∈ ℝ ∧ 𝑆 ∈ ℝ) → ((𝑆 + (𝑟 / 2))((abs ∘ − ) ↾ (ℝ × ℝ))𝑆) = (abs‘((𝑆 + (𝑟 / 2)) − 𝑆)))
8751, 48, 86syl2anc 691 . . . . . . . . . . 11 ((𝜑𝑟 ∈ ℝ+) → ((𝑆 + (𝑟 / 2))((abs ∘ − ) ↾ (ℝ × ℝ))𝑆) = (abs‘((𝑆 + (𝑟 / 2)) − 𝑆)))
8848recnd 9947 . . . . . . . . . . . . 13 ((𝜑𝑟 ∈ ℝ+) → 𝑆 ∈ ℂ)
8949adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑟 ∈ ℝ+) → (𝑟 / 2) ∈ ℝ)
9089recnd 9947 . . . . . . . . . . . . 13 ((𝜑𝑟 ∈ ℝ+) → (𝑟 / 2) ∈ ℂ)
9188, 90pncan2d 10273 . . . . . . . . . . . 12 ((𝜑𝑟 ∈ ℝ+) → ((𝑆 + (𝑟 / 2)) − 𝑆) = (𝑟 / 2))
9291fveq2d 6107 . . . . . . . . . . 11 ((𝜑𝑟 ∈ ℝ+) → (abs‘((𝑆 + (𝑟 / 2)) − 𝑆)) = (abs‘(𝑟 / 2)))
9345adantl 481 . . . . . . . . . . . 12 ((𝜑𝑟 ∈ ℝ+) → (𝑟 / 2) ∈ ℝ+)
94 rpre 11715 . . . . . . . . . . . . 13 ((𝑟 / 2) ∈ ℝ+ → (𝑟 / 2) ∈ ℝ)
95 rpge0 11721 . . . . . . . . . . . . 13 ((𝑟 / 2) ∈ ℝ+ → 0 ≤ (𝑟 / 2))
9694, 95absidd 14009 . . . . . . . . . . . 12 ((𝑟 / 2) ∈ ℝ+ → (abs‘(𝑟 / 2)) = (𝑟 / 2))
9793, 96syl 17 . . . . . . . . . . 11 ((𝜑𝑟 ∈ ℝ+) → (abs‘(𝑟 / 2)) = (𝑟 / 2))
9887, 92, 973eqtrd 2648 . . . . . . . . . 10 ((𝜑𝑟 ∈ ℝ+) → ((𝑆 + (𝑟 / 2))((abs ∘ − ) ↾ (ℝ × ℝ))𝑆) = (𝑟 / 2))
99 rphalflt 11736 . . . . . . . . . . 11 (𝑟 ∈ ℝ+ → (𝑟 / 2) < 𝑟)
10099adantl 481 . . . . . . . . . 10 ((𝜑𝑟 ∈ ℝ+) → (𝑟 / 2) < 𝑟)
10198, 100eqbrtrd 4605 . . . . . . . . 9 ((𝜑𝑟 ∈ ℝ+) → ((𝑆 + (𝑟 / 2))((abs ∘ − ) ↾ (ℝ × ℝ))𝑆) < 𝑟)
10285rexmet 22402 . . . . . . . . . . 11 ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
103102a1i 11 . . . . . . . . . 10 ((𝜑𝑟 ∈ ℝ+) → ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ))
104 rpxr 11716 . . . . . . . . . . 11 (𝑟 ∈ ℝ+𝑟 ∈ ℝ*)
105104adantl 481 . . . . . . . . . 10 ((𝜑𝑟 ∈ ℝ+) → 𝑟 ∈ ℝ*)
106 elbl3 22007 . . . . . . . . . 10 (((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ 𝑟 ∈ ℝ*) ∧ (𝑆 ∈ ℝ ∧ (𝑆 + (𝑟 / 2)) ∈ ℝ)) → ((𝑆 + (𝑟 / 2)) ∈ (𝑆(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ↔ ((𝑆 + (𝑟 / 2))((abs ∘ − ) ↾ (ℝ × ℝ))𝑆) < 𝑟))
107103, 105, 48, 51, 106syl22anc 1319 . . . . . . . . 9 ((𝜑𝑟 ∈ ℝ+) → ((𝑆 + (𝑟 / 2)) ∈ (𝑆(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ↔ ((𝑆 + (𝑟 / 2))((abs ∘ − ) ↾ (ℝ × ℝ))𝑆) < 𝑟))
108101, 107mpbird 246 . . . . . . . 8 ((𝜑𝑟 ∈ ℝ+) → (𝑆 + (𝑟 / 2)) ∈ (𝑆(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟))
109 ssel 3562 . . . . . . . 8 ((𝑆(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶)) → ((𝑆 + (𝑟 / 2)) ∈ (𝑆(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) → (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))))
110108, 109syl5com 31 . . . . . . 7 ((𝜑𝑟 ∈ ℝ+) → ((𝑆(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶)) → (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))))
11184, 110mtod 188 . . . . . 6 ((𝜑𝑟 ∈ ℝ+) → ¬ (𝑆(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶)))
112111nrexdv 2984 . . . . 5 (𝜑 → ¬ ∃𝑟 ∈ ℝ+ (𝑆(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶)))
11344adantr 480 . . . . . . . . 9 ((𝜑𝑆𝑈) → 𝑆 ∈ ℝ)
114 mnflt 11833 . . . . . . . . . 10 (𝑆 ∈ ℝ → -∞ < 𝑆)
115113, 114syl 17 . . . . . . . . 9 ((𝜑𝑆𝑈) → -∞ < 𝑆)
116 suprleub 10866 . . . . . . . . . . . . . . . . 17 ((((𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ ∧ (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤𝑧) ∧ 𝐶 ∈ ℝ) → (sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ≤ 𝐶 ↔ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤𝐶))
11718, 30, 41, 23, 116syl31anc 1321 . . . . . . . . . . . . . . . 16 (𝜑 → (sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ≤ 𝐶 ↔ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤𝐶))
11837, 117mpbird 246 . . . . . . . . . . . . . . 15 (𝜑 → sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ≤ 𝐶)
1191, 118syl5eqbr 4618 . . . . . . . . . . . . . 14 (𝜑𝑆𝐶)
12044, 23leloed 10059 . . . . . . . . . . . . . 14 (𝜑 → (𝑆𝐶 ↔ (𝑆 < 𝐶𝑆 = 𝐶)))
121119, 120mpbid 221 . . . . . . . . . . . . 13 (𝜑 → (𝑆 < 𝐶𝑆 = 𝐶))
122121ord 391 . . . . . . . . . . . 12 (𝜑 → (¬ 𝑆 < 𝐶𝑆 = 𝐶))
123 elndif 3696 . . . . . . . . . . . . . . 15 (𝐶𝐴 → ¬ 𝐶 ∈ (ℝ ∖ 𝐴))
1248, 123syl 17 . . . . . . . . . . . . . 14 (𝜑 → ¬ 𝐶 ∈ (ℝ ∖ 𝐴))
125 inss1 3795 . . . . . . . . . . . . . . . 16 (𝑉𝐴) ⊆ 𝑉
126125, 7sseldi 3566 . . . . . . . . . . . . . . 15 (𝜑𝐶𝑉)
127 elin 3758 . . . . . . . . . . . . . . . 16 (𝐶 ∈ (𝑈𝑉) ↔ (𝐶𝑈𝐶𝑉))
128 reconnlem2.7 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑈𝑉) ⊆ (ℝ ∖ 𝐴))
129128sseld 3567 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶 ∈ (𝑈𝑉) → 𝐶 ∈ (ℝ ∖ 𝐴)))
130127, 129syl5bir 232 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶𝑈𝐶𝑉) → 𝐶 ∈ (ℝ ∖ 𝐴)))
131126, 130mpan2d 706 . . . . . . . . . . . . . 14 (𝜑 → (𝐶𝑈𝐶 ∈ (ℝ ∖ 𝐴)))
132124, 131mtod 188 . . . . . . . . . . . . 13 (𝜑 → ¬ 𝐶𝑈)
133 eleq1 2676 . . . . . . . . . . . . . 14 (𝑆 = 𝐶 → (𝑆𝑈𝐶𝑈))
134133notbid 307 . . . . . . . . . . . . 13 (𝑆 = 𝐶 → (¬ 𝑆𝑈 ↔ ¬ 𝐶𝑈))
135132, 134syl5ibrcom 236 . . . . . . . . . . . 12 (𝜑 → (𝑆 = 𝐶 → ¬ 𝑆𝑈))
136122, 135syld 46 . . . . . . . . . . 11 (𝜑 → (¬ 𝑆 < 𝐶 → ¬ 𝑆𝑈))
137136con4d 113 . . . . . . . . . 10 (𝜑 → (𝑆𝑈𝑆 < 𝐶))
138137imp 444 . . . . . . . . 9 ((𝜑𝑆𝑈) → 𝑆 < 𝐶)
139 mnfxr 9975 . . . . . . . . . . 11 -∞ ∈ ℝ*
140 elioo2 12087 . . . . . . . . . . 11 ((-∞ ∈ ℝ*𝐶 ∈ ℝ*) → (𝑆 ∈ (-∞(,)𝐶) ↔ (𝑆 ∈ ℝ ∧ -∞ < 𝑆𝑆 < 𝐶)))
141139, 24, 140sylancr 694 . . . . . . . . . 10 (𝜑 → (𝑆 ∈ (-∞(,)𝐶) ↔ (𝑆 ∈ ℝ ∧ -∞ < 𝑆𝑆 < 𝐶)))
142141adantr 480 . . . . . . . . 9 ((𝜑𝑆𝑈) → (𝑆 ∈ (-∞(,)𝐶) ↔ (𝑆 ∈ ℝ ∧ -∞ < 𝑆𝑆 < 𝐶)))
143113, 115, 138, 142mpbir3and 1238 . . . . . . . 8 ((𝜑𝑆𝑈) → 𝑆 ∈ (-∞(,)𝐶))
144143ex 449 . . . . . . 7 (𝜑 → (𝑆𝑈𝑆 ∈ (-∞(,)𝐶)))
145144ancld 574 . . . . . 6 (𝜑 → (𝑆𝑈 → (𝑆𝑈𝑆 ∈ (-∞(,)𝐶))))
146 elin 3758 . . . . . . 7 (𝑆 ∈ (𝑈 ∩ (-∞(,)𝐶)) ↔ (𝑆𝑈𝑆 ∈ (-∞(,)𝐶)))
147 reconnlem2.2 . . . . . . . 8 (𝜑𝑈 ∈ (topGen‘ran (,)))
148 retop 22375 . . . . . . . . 9 (topGen‘ran (,)) ∈ Top
149 iooretop 22379 . . . . . . . . 9 (-∞(,)𝐶) ∈ (topGen‘ran (,))
150 inopn 20529 . . . . . . . . 9 (((topGen‘ran (,)) ∈ Top ∧ 𝑈 ∈ (topGen‘ran (,)) ∧ (-∞(,)𝐶) ∈ (topGen‘ran (,))) → (𝑈 ∩ (-∞(,)𝐶)) ∈ (topGen‘ran (,)))
151148, 149, 150mp3an13 1407 . . . . . . . 8 (𝑈 ∈ (topGen‘ran (,)) → (𝑈 ∩ (-∞(,)𝐶)) ∈ (topGen‘ran (,)))
152 eqid 2610 . . . . . . . . . . . 12 (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
15385, 152tgioo 22407 . . . . . . . . . . 11 (topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
154153mopni2 22108 . . . . . . . . . 10 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ (𝑈 ∩ (-∞(,)𝐶)) ∈ (topGen‘ran (,)) ∧ 𝑆 ∈ (𝑈 ∩ (-∞(,)𝐶))) → ∃𝑟 ∈ ℝ+ (𝑆(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶)))
155102, 154mp3an1 1403 . . . . . . . . 9 (((𝑈 ∩ (-∞(,)𝐶)) ∈ (topGen‘ran (,)) ∧ 𝑆 ∈ (𝑈 ∩ (-∞(,)𝐶))) → ∃𝑟 ∈ ℝ+ (𝑆(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶)))
156155ex 449 . . . . . . . 8 ((𝑈 ∩ (-∞(,)𝐶)) ∈ (topGen‘ran (,)) → (𝑆 ∈ (𝑈 ∩ (-∞(,)𝐶)) → ∃𝑟 ∈ ℝ+ (𝑆(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶))))
157147, 151, 1563syl 18 . . . . . . 7 (𝜑 → (𝑆 ∈ (𝑈 ∩ (-∞(,)𝐶)) → ∃𝑟 ∈ ℝ+ (𝑆(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶))))
158146, 157syl5bir 232 . . . . . 6 (𝜑 → ((𝑆𝑈𝑆 ∈ (-∞(,)𝐶)) → ∃𝑟 ∈ ℝ+ (𝑆(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶))))
159145, 158syld 46 . . . . 5 (𝜑 → (𝑆𝑈 → ∃𝑟 ∈ ℝ+ (𝑆(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶))))
160112, 159mtod 188 . . . 4 (𝜑 → ¬ 𝑆𝑈)
161 ltsubrp 11742 . . . . . . . . 9 ((𝑆 ∈ ℝ ∧ 𝑟 ∈ ℝ+) → (𝑆𝑟) < 𝑆)
16244, 161sylan 487 . . . . . . . 8 ((𝜑𝑟 ∈ ℝ+) → (𝑆𝑟) < 𝑆)
163 rpre 11715 . . . . . . . . . 10 (𝑟 ∈ ℝ+𝑟 ∈ ℝ)
164 resubcl 10224 . . . . . . . . . 10 ((𝑆 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝑆𝑟) ∈ ℝ)
16544, 163, 164syl2an 493 . . . . . . . . 9 ((𝜑𝑟 ∈ ℝ+) → (𝑆𝑟) ∈ ℝ)
166165, 48ltnled 10063 . . . . . . . 8 ((𝜑𝑟 ∈ ℝ+) → ((𝑆𝑟) < 𝑆 ↔ ¬ 𝑆 ≤ (𝑆𝑟)))
167162, 166mpbid 221 . . . . . . 7 ((𝜑𝑟 ∈ ℝ+) → ¬ 𝑆 ≤ (𝑆𝑟))
16885bl2ioo 22403 . . . . . . . . . 10 ((𝑆 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝑆(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = ((𝑆𝑟)(,)(𝑆 + 𝑟)))
16944, 163, 168syl2an 493 . . . . . . . . 9 ((𝜑𝑟 ∈ ℝ+) → (𝑆(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = ((𝑆𝑟)(,)(𝑆 + 𝑟)))
170169sseq1d 3595 . . . . . . . 8 ((𝜑𝑟 ∈ ℝ+) → ((𝑆(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑉 ↔ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉))
17115ad2antrr 758 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → (𝐵[,]𝐶) ⊆ 𝐴)
1722, 171syl5ss 3579 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → (𝑈 ∩ (𝐵[,]𝐶)) ⊆ 𝐴)
173172sselda 3568 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → 𝑤𝐴)
174 elndif 3696 . . . . . . . . . . . . . . 15 (𝑤𝐴 → ¬ 𝑤 ∈ (ℝ ∖ 𝐴))
175173, 174syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → ¬ 𝑤 ∈ (ℝ ∖ 𝐴))
176128ad3antrrr 762 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆𝑟) < 𝑤)) → (𝑈𝑉) ⊆ (ℝ ∖ 𝐴))
177 inss1 3795 . . . . . . . . . . . . . . . . . 18 (𝑈 ∩ (𝐵[,]𝐶)) ⊆ 𝑈
178 simprl 790 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆𝑟) < 𝑤)) → 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)))
179177, 178sseldi 3566 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆𝑟) < 𝑤)) → 𝑤𝑈)
180 simplr 788 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆𝑟) < 𝑤)) → ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉)
18118ad3antrrr 762 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → (𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ)
182 simpr 476 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)))
183181, 182sseldd 3569 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → 𝑤 ∈ ℝ)
184183adantrr 749 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆𝑟) < 𝑤)) → 𝑤 ∈ ℝ)
185 simprr 792 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆𝑟) < 𝑤)) → (𝑆𝑟) < 𝑤)
18648ad2antrr 758 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆𝑟) < 𝑤)) → 𝑆 ∈ ℝ)
187 simpllr 795 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆𝑟) < 𝑤)) → 𝑟 ∈ ℝ+)
188187rpred 11748 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆𝑟) < 𝑤)) → 𝑟 ∈ ℝ)
189186, 188readdcld 9948 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆𝑟) < 𝑤)) → (𝑆 + 𝑟) ∈ ℝ)
190181adantrr 749 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆𝑟) < 𝑤)) → (𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ)
19130ad3antrrr 762 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆𝑟) < 𝑤)) → (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅)
19241ad3antrrr 762 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆𝑟) < 𝑤)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤𝑧)
193 suprub 10863 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ ∧ (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤𝑧) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → 𝑤 ≤ sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ))
194190, 191, 192, 178, 193syl31anc 1321 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆𝑟) < 𝑤)) → 𝑤 ≤ sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ))
195194, 1syl6breqr 4625 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆𝑟) < 𝑤)) → 𝑤𝑆)
196186, 187ltaddrpd 11781 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆𝑟) < 𝑤)) → 𝑆 < (𝑆 + 𝑟))
197184, 186, 189, 195, 196lelttrd 10074 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆𝑟) < 𝑤)) → 𝑤 < (𝑆 + 𝑟))
198165ad2antrr 758 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆𝑟) < 𝑤)) → (𝑆𝑟) ∈ ℝ)
199 rexr 9964 . . . . . . . . . . . . . . . . . . . . 21 ((𝑆𝑟) ∈ ℝ → (𝑆𝑟) ∈ ℝ*)
200 rexr 9964 . . . . . . . . . . . . . . . . . . . . 21 ((𝑆 + 𝑟) ∈ ℝ → (𝑆 + 𝑟) ∈ ℝ*)
201 elioo2 12087 . . . . . . . . . . . . . . . . . . . . 21 (((𝑆𝑟) ∈ ℝ* ∧ (𝑆 + 𝑟) ∈ ℝ*) → (𝑤 ∈ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ↔ (𝑤 ∈ ℝ ∧ (𝑆𝑟) < 𝑤𝑤 < (𝑆 + 𝑟))))
202199, 200, 201syl2an 493 . . . . . . . . . . . . . . . . . . . 20 (((𝑆𝑟) ∈ ℝ ∧ (𝑆 + 𝑟) ∈ ℝ) → (𝑤 ∈ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ↔ (𝑤 ∈ ℝ ∧ (𝑆𝑟) < 𝑤𝑤 < (𝑆 + 𝑟))))
203198, 189, 202syl2anc 691 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆𝑟) < 𝑤)) → (𝑤 ∈ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ↔ (𝑤 ∈ ℝ ∧ (𝑆𝑟) < 𝑤𝑤 < (𝑆 + 𝑟))))
204184, 185, 197, 203mpbir3and 1238 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆𝑟) < 𝑤)) → 𝑤 ∈ ((𝑆𝑟)(,)(𝑆 + 𝑟)))
205180, 204sseldd 3569 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆𝑟) < 𝑤)) → 𝑤𝑉)
206179, 205elind 3760 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆𝑟) < 𝑤)) → 𝑤 ∈ (𝑈𝑉))
207176, 206sseldd 3569 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆𝑟) < 𝑤)) → 𝑤 ∈ (ℝ ∖ 𝐴))
208207expr 641 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → ((𝑆𝑟) < 𝑤𝑤 ∈ (ℝ ∖ 𝐴)))
209175, 208mtod 188 . . . . . . . . . . . . 13 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → ¬ (𝑆𝑟) < 𝑤)
210165ad2antrr 758 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → (𝑆𝑟) ∈ ℝ)
211183, 210lenltd 10062 . . . . . . . . . . . . 13 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → (𝑤 ≤ (𝑆𝑟) ↔ ¬ (𝑆𝑟) < 𝑤))
212209, 211mpbird 246 . . . . . . . . . . . 12 ((((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → 𝑤 ≤ (𝑆𝑟))
213212ralrimiva 2949 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ (𝑆𝑟))
21418ad2antrr 758 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → (𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ)
21530ad2antrr 758 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅)
21641ad2antrr 758 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤𝑧)
217165adantr 480 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → (𝑆𝑟) ∈ ℝ)
218 suprleub 10866 . . . . . . . . . . . 12 ((((𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ ∧ (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤𝑧) ∧ (𝑆𝑟) ∈ ℝ) → (sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ≤ (𝑆𝑟) ↔ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ (𝑆𝑟)))
219214, 215, 216, 217, 218syl31anc 1321 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → (sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ≤ (𝑆𝑟) ↔ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ (𝑆𝑟)))
220213, 219mpbird 246 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ≤ (𝑆𝑟))
2211, 220syl5eqbr 4618 . . . . . . . . 9 (((𝜑𝑟 ∈ ℝ+) ∧ ((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → 𝑆 ≤ (𝑆𝑟))
222221ex 449 . . . . . . . 8 ((𝜑𝑟 ∈ ℝ+) → (((𝑆𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉𝑆 ≤ (𝑆𝑟)))
223170, 222sylbid 229 . . . . . . 7 ((𝜑𝑟 ∈ ℝ+) → ((𝑆(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑉𝑆 ≤ (𝑆𝑟)))
224167, 223mtod 188 . . . . . 6 ((𝜑𝑟 ∈ ℝ+) → ¬ (𝑆(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑉)
225224nrexdv 2984 . . . . 5 (𝜑 → ¬ ∃𝑟 ∈ ℝ+ (𝑆(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑉)
226 reconnlem2.3 . . . . . 6 (𝜑𝑉 ∈ (topGen‘ran (,)))
227153mopni2 22108 . . . . . . . 8 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ 𝑉 ∈ (topGen‘ran (,)) ∧ 𝑆𝑉) → ∃𝑟 ∈ ℝ+ (𝑆(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑉)
228102, 227mp3an1 1403 . . . . . . 7 ((𝑉 ∈ (topGen‘ran (,)) ∧ 𝑆𝑉) → ∃𝑟 ∈ ℝ+ (𝑆(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑉)
229228ex 449 . . . . . 6 (𝑉 ∈ (topGen‘ran (,)) → (𝑆𝑉 → ∃𝑟 ∈ ℝ+ (𝑆(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑉))
230226, 229syl 17 . . . . 5 (𝜑 → (𝑆𝑉 → ∃𝑟 ∈ ℝ+ (𝑆(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑉))
231225, 230mtod 188 . . . 4 (𝜑 → ¬ 𝑆𝑉)
232 ioran 510 . . . 4 (¬ (𝑆𝑈𝑆𝑉) ↔ (¬ 𝑆𝑈 ∧ ¬ 𝑆𝑉))
233160, 231, 232sylanbrc 695 . . 3 (𝜑 → ¬ (𝑆𝑈𝑆𝑉))
234 elun 3715 . . 3 (𝑆 ∈ (𝑈𝑉) ↔ (𝑆𝑈𝑆𝑉))
235233, 234sylnibr 318 . 2 (𝜑 → ¬ 𝑆 ∈ (𝑈𝑉))
236 elicc2 12109 . . . . . 6 ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑆 ∈ (𝐵[,]𝐶) ↔ (𝑆 ∈ ℝ ∧ 𝐵𝑆𝑆𝐶)))
23721, 23, 236syl2anc 691 . . . . 5 (𝜑 → (𝑆 ∈ (𝐵[,]𝐶) ↔ (𝑆 ∈ ℝ ∧ 𝐵𝑆𝑆𝐶)))
23844, 65, 119, 237mpbir3and 1238 . . . 4 (𝜑𝑆 ∈ (𝐵[,]𝐶))
23915, 238sseldd 3569 . . 3 (𝜑𝑆𝐴)
240 ssel 3562 . . 3 (𝐴 ⊆ (𝑈𝑉) → (𝑆𝐴𝑆 ∈ (𝑈𝑉)))
241239, 240syl5com 31 . 2 (𝜑 → (𝐴 ⊆ (𝑈𝑉) → 𝑆 ∈ (𝑈𝑉)))
242235, 241mtod 188 1 (𝜑 → ¬ 𝐴 ⊆ (𝑈𝑉))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874   class class class wbr 4583   × cxp 5036  ran crn 5039   ↾ cres 5040   ∘ ccom 5042  ‘cfv 5804  (class class class)co 6549  supcsup 8229  ℝcr 9814   + caddc 9818  -∞cmnf 9951  ℝ*cxr 9952   < clt 9953   ≤ cle 9954   − cmin 10145   / cdiv 10563  2c2 10947  ℝ+crp 11708  (,)cioo 12046  [,]cicc 12049  abscabs 13822  topGenctg 15921  ∞Metcxmt 19552  ballcbl 19554  MetOpencmopn 19557  Topctop 20517 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-icc 12053  df-seq 12664  df-exp 12723  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-topgen 15927  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-top 20521  df-bases 20522  df-topon 20523 This theorem is referenced by:  reconn  22439
 Copyright terms: Public domain W3C validator