Step | Hyp | Ref
| Expression |
1 | | reconnlem2.9 |
. . . . . . . . . . 11
⊢ 𝑆 = sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) |
2 | | inss2 3982 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∩ (𝐵[,]𝐶)) ⊆ (𝐵[,]𝐶) |
3 | | inss2 3982 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 ∩ 𝐴) ⊆ 𝐴 |
4 | | reconnlem2.5 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 ∈ (𝑈 ∩ 𝐴)) |
5 | 3, 4 | sseldi 3750 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈ 𝐴) |
6 | | inss2 3982 |
. . . . . . . . . . . . . . . 16
⊢ (𝑉 ∩ 𝐴) ⊆ 𝐴 |
7 | | reconnlem2.6 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 ∈ (𝑉 ∩ 𝐴)) |
8 | 6, 7 | sseldi 3750 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ∈ 𝐴) |
9 | | reconnlem2.4 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) |
10 | | oveq1 6802 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝐵 → (𝑥[,]𝑦) = (𝐵[,]𝑦)) |
11 | 10 | sseq1d 3781 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝐵 → ((𝑥[,]𝑦) ⊆ 𝐴 ↔ (𝐵[,]𝑦) ⊆ 𝐴)) |
12 | | oveq2 6803 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝐶 → (𝐵[,]𝑦) = (𝐵[,]𝐶)) |
13 | 12 | sseq1d 3781 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝐶 → ((𝐵[,]𝑦) ⊆ 𝐴 ↔ (𝐵[,]𝐶) ⊆ 𝐴)) |
14 | 11, 13 | rspc2va 3473 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) → (𝐵[,]𝐶) ⊆ 𝐴) |
15 | 5, 8, 9, 14 | syl21anc 1475 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵[,]𝐶) ⊆ 𝐴) |
16 | | reconnlem2.1 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
17 | 15, 16 | sstrd 3762 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵[,]𝐶) ⊆ ℝ) |
18 | 2, 17 | syl5ss 3763 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ) |
19 | | inss1 3981 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 ∩ 𝐴) ⊆ 𝑈 |
20 | 19, 4 | sseldi 3750 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ 𝑈) |
21 | 16, 5 | sseldd 3753 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 ∈ ℝ) |
22 | 21 | rexrd 10294 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
23 | 16, 8 | sseldd 3753 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 ∈ ℝ) |
24 | 23 | rexrd 10294 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
25 | | reconnlem2.8 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ≤ 𝐶) |
26 | | lbicc2 12494 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝐵
≤ 𝐶) → 𝐵 ∈ (𝐵[,]𝐶)) |
27 | 22, 24, 25, 26 | syl3anc 1476 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ (𝐵[,]𝐶)) |
28 | 20, 27 | elind 3949 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ (𝑈 ∩ (𝐵[,]𝐶))) |
29 | 28 | ne0d 4070 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅) |
30 | 2 | sseli 3748 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) → 𝑤 ∈ (𝐵[,]𝐶)) |
31 | | elicc2 12442 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑤 ∈ (𝐵[,]𝐶) ↔ (𝑤 ∈ ℝ ∧ 𝐵 ≤ 𝑤 ∧ 𝑤 ≤ 𝐶))) |
32 | 21, 23, 31 | syl2anc 573 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑤 ∈ (𝐵[,]𝐶) ↔ (𝑤 ∈ ℝ ∧ 𝐵 ≤ 𝑤 ∧ 𝑤 ≤ 𝐶))) |
33 | | simp3 1132 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ ℝ ∧ 𝐵 ≤ 𝑤 ∧ 𝑤 ≤ 𝐶) → 𝑤 ≤ 𝐶) |
34 | 32, 33 | syl6bi 243 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑤 ∈ (𝐵[,]𝐶) → 𝑤 ≤ 𝐶)) |
35 | 30, 34 | syl5 34 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) → 𝑤 ≤ 𝐶)) |
36 | 35 | ralrimiv 3114 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝐶) |
37 | | breq2 4791 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝐶 → (𝑤 ≤ 𝑧 ↔ 𝑤 ≤ 𝐶)) |
38 | 37 | ralbidv 3135 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝐶 → (∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝑧 ↔ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝐶)) |
39 | 38 | rspcev 3460 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ ℝ ∧
∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝐶) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝑧) |
40 | 23, 36, 39 | syl2anc 573 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝑧) |
41 | | suprcl 11188 |
. . . . . . . . . . . 12
⊢ (((𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ ∧ (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝑧) → sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ∈
ℝ) |
42 | 18, 29, 40, 41 | syl3anc 1476 |
. . . . . . . . . . 11
⊢ (𝜑 → sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ∈
ℝ) |
43 | 1, 42 | syl5eqel 2854 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ ℝ) |
44 | | rphalfcl 12060 |
. . . . . . . . . 10
⊢ (𝑟 ∈ ℝ+
→ (𝑟 / 2) ∈
ℝ+) |
45 | | ltaddrp 12069 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ ℝ ∧ (𝑟 / 2) ∈
ℝ+) → 𝑆 < (𝑆 + (𝑟 / 2))) |
46 | 43, 44, 45 | syl2an 583 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑆 < (𝑆 + (𝑟 / 2))) |
47 | 43 | adantr 466 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑆 ∈
ℝ) |
48 | 44 | rpred 12074 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ ℝ+
→ (𝑟 / 2) ∈
ℝ) |
49 | | readdcl 10224 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ ℝ ∧ (𝑟 / 2) ∈ ℝ) →
(𝑆 + (𝑟 / 2)) ∈ ℝ) |
50 | 43, 48, 49 | syl2an 583 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑆 + (𝑟 / 2)) ∈ ℝ) |
51 | 47, 50 | ltnled 10389 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑆 < (𝑆 + (𝑟 / 2)) ↔ ¬ (𝑆 + (𝑟 / 2)) ≤ 𝑆)) |
52 | 46, 51 | mpbid 222 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ¬
(𝑆 + (𝑟 / 2)) ≤ 𝑆) |
53 | 18 | ad2antrr 705 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ) |
54 | 29 | ad2antrr 705 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅) |
55 | 40 | ad2antrr 705 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝑧) |
56 | | inss1 3981 |
. . . . . . . . . . . 12
⊢ (𝑈 ∩ (-∞(,)𝐶)) ⊆ 𝑈 |
57 | | simpr 471 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) |
58 | 56, 57 | sseldi 3750 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ∈ 𝑈) |
59 | 50 | adantr 466 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ∈ ℝ) |
60 | 21 | ad2antrr 705 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → 𝐵 ∈ ℝ) |
61 | 43 | ad2antrr 705 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → 𝑆 ∈ ℝ) |
62 | | suprub 11189 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ ∧ (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝑧) ∧ 𝐵 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → 𝐵 ≤ sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < )) |
63 | 18, 29, 40, 28, 62 | syl31anc 1479 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ≤ sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < )) |
64 | 63, 1 | syl6breqr 4829 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ≤ 𝑆) |
65 | 64 | ad2antrr 705 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → 𝐵 ≤ 𝑆) |
66 | 46 | adantr 466 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → 𝑆 < (𝑆 + (𝑟 / 2))) |
67 | 61, 59, 66 | ltled 10390 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → 𝑆 ≤ (𝑆 + (𝑟 / 2))) |
68 | 60, 61, 59, 65, 67 | letrd 10399 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → 𝐵 ≤ (𝑆 + (𝑟 / 2))) |
69 | 23 | ad2antrr 705 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → 𝐶 ∈ ℝ) |
70 | | inss2 3982 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 ∩ (-∞(,)𝐶)) ⊆ (-∞(,)𝐶) |
71 | 70, 57 | sseldi 3750 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ∈ (-∞(,)𝐶)) |
72 | | eliooord 12437 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 + (𝑟 / 2)) ∈ (-∞(,)𝐶) → (-∞ < (𝑆 + (𝑟 / 2)) ∧ (𝑆 + (𝑟 / 2)) < 𝐶)) |
73 | 72 | simprd 483 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 + (𝑟 / 2)) ∈ (-∞(,)𝐶) → (𝑆 + (𝑟 / 2)) < 𝐶) |
74 | 71, 73 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) < 𝐶) |
75 | 59, 69, 74 | ltled 10390 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ≤ 𝐶) |
76 | | elicc2 12442 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝑆 + (𝑟 / 2)) ∈ (𝐵[,]𝐶) ↔ ((𝑆 + (𝑟 / 2)) ∈ ℝ ∧ 𝐵 ≤ (𝑆 + (𝑟 / 2)) ∧ (𝑆 + (𝑟 / 2)) ≤ 𝐶))) |
77 | 60, 69, 76 | syl2anc 573 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → ((𝑆 + (𝑟 / 2)) ∈ (𝐵[,]𝐶) ↔ ((𝑆 + (𝑟 / 2)) ∈ ℝ ∧ 𝐵 ≤ (𝑆 + (𝑟 / 2)) ∧ (𝑆 + (𝑟 / 2)) ≤ 𝐶))) |
78 | 59, 68, 75, 77 | mpbir3and 1427 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ∈ (𝐵[,]𝐶)) |
79 | 58, 78 | elind 3949 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (𝐵[,]𝐶))) |
80 | | suprub 11189 |
. . . . . . . . . 10
⊢ ((((𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ ∧ (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝑧) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (𝐵[,]𝐶))) → (𝑆 + (𝑟 / 2)) ≤ sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < )) |
81 | 53, 54, 55, 79, 80 | syl31anc 1479 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ≤ sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < )) |
82 | 81, 1 | syl6breqr 4829 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ≤ 𝑆) |
83 | 52, 82 | mtand 817 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ¬
(𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) |
84 | | eqid 2771 |
. . . . . . . . . . . . 13
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − )
↾ (ℝ × ℝ)) |
85 | 84 | remetdval 22811 |
. . . . . . . . . . . 12
⊢ (((𝑆 + (𝑟 / 2)) ∈ ℝ ∧ 𝑆 ∈ ℝ) → ((𝑆 + (𝑟 / 2))((abs ∘ − ) ↾
(ℝ × ℝ))𝑆) = (abs‘((𝑆 + (𝑟 / 2)) − 𝑆))) |
86 | 50, 47, 85 | syl2anc 573 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑆 + (𝑟 / 2))((abs ∘ − ) ↾
(ℝ × ℝ))𝑆) = (abs‘((𝑆 + (𝑟 / 2)) − 𝑆))) |
87 | 47 | recnd 10273 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑆 ∈
ℂ) |
88 | 48 | adantl 467 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ∈
ℝ) |
89 | 88 | recnd 10273 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ∈
ℂ) |
90 | 87, 89 | pncan2d 10599 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑆 + (𝑟 / 2)) − 𝑆) = (𝑟 / 2)) |
91 | 90 | fveq2d 6337 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(abs‘((𝑆 + (𝑟 / 2)) − 𝑆)) = (abs‘(𝑟 / 2))) |
92 | 44 | adantl 467 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ∈
ℝ+) |
93 | | rpre 12041 |
. . . . . . . . . . . . 13
⊢ ((𝑟 / 2) ∈ ℝ+
→ (𝑟 / 2) ∈
ℝ) |
94 | | rpge0 12047 |
. . . . . . . . . . . . 13
⊢ ((𝑟 / 2) ∈ ℝ+
→ 0 ≤ (𝑟 /
2)) |
95 | 93, 94 | absidd 14368 |
. . . . . . . . . . . 12
⊢ ((𝑟 / 2) ∈ ℝ+
→ (abs‘(𝑟 / 2))
= (𝑟 / 2)) |
96 | 92, 95 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(abs‘(𝑟 / 2)) =
(𝑟 / 2)) |
97 | 86, 91, 96 | 3eqtrd 2809 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑆 + (𝑟 / 2))((abs ∘ − ) ↾
(ℝ × ℝ))𝑆) = (𝑟 / 2)) |
98 | | rphalflt 12062 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ ℝ+
→ (𝑟 / 2) < 𝑟) |
99 | 98 | adantl 467 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) < 𝑟) |
100 | 97, 99 | eqbrtrd 4809 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑆 + (𝑟 / 2))((abs ∘ − ) ↾
(ℝ × ℝ))𝑆) < 𝑟) |
101 | 84 | rexmet 22813 |
. . . . . . . . . . 11
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) |
102 | 101 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ)) |
103 | | rpxr 12042 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
104 | 103 | adantl 467 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ*) |
105 | | elbl3 22416 |
. . . . . . . . . 10
⊢ (((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧ 𝑟 ∈ ℝ*) ∧ (𝑆 ∈ ℝ ∧ (𝑆 + (𝑟 / 2)) ∈ ℝ)) → ((𝑆 + (𝑟 / 2)) ∈ (𝑆(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ↔ ((𝑆 + (𝑟 / 2))((abs ∘ − ) ↾
(ℝ × ℝ))𝑆) < 𝑟)) |
106 | 102, 104,
47, 50, 105 | syl22anc 1477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑆 + (𝑟 / 2)) ∈ (𝑆(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ↔ ((𝑆 + (𝑟 / 2))((abs ∘ − ) ↾
(ℝ × ℝ))𝑆) < 𝑟)) |
107 | 100, 106 | mpbird 247 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑆 + (𝑟 / 2)) ∈ (𝑆(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟)) |
108 | | ssel 3746 |
. . . . . . . 8
⊢ ((𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶)) → ((𝑆 + (𝑟 / 2)) ∈ (𝑆(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) → (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶)))) |
109 | 107, 108 | syl5com 31 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶)) → (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶)))) |
110 | 83, 109 | mtod 189 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ¬
(𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶))) |
111 | 110 | nrexdv 3149 |
. . . . 5
⊢ (𝜑 → ¬ ∃𝑟 ∈ ℝ+
(𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶))) |
112 | 43 | adantr 466 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑈) → 𝑆 ∈ ℝ) |
113 | | mnflt 12161 |
. . . . . . . . . 10
⊢ (𝑆 ∈ ℝ → -∞
< 𝑆) |
114 | 112, 113 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑈) → -∞ < 𝑆) |
115 | | suprleub 11194 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ ∧ (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝑧) ∧ 𝐶 ∈ ℝ) → (sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ≤ 𝐶 ↔ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝐶)) |
116 | 18, 29, 40, 23, 115 | syl31anc 1479 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ≤ 𝐶 ↔ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝐶)) |
117 | 36, 116 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ≤ 𝐶) |
118 | 1, 117 | syl5eqbr 4822 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ≤ 𝐶) |
119 | 43, 23 | leloed 10385 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑆 ≤ 𝐶 ↔ (𝑆 < 𝐶 ∨ 𝑆 = 𝐶))) |
120 | 118, 119 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆 < 𝐶 ∨ 𝑆 = 𝐶)) |
121 | 120 | ord 853 |
. . . . . . . . . . . 12
⊢ (𝜑 → (¬ 𝑆 < 𝐶 → 𝑆 = 𝐶)) |
122 | | elndif 3885 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ∈ 𝐴 → ¬ 𝐶 ∈ (ℝ ∖ 𝐴)) |
123 | 8, 122 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ 𝐶 ∈ (ℝ ∖ 𝐴)) |
124 | | inss1 3981 |
. . . . . . . . . . . . . . . 16
⊢ (𝑉 ∩ 𝐴) ⊆ 𝑉 |
125 | 124, 7 | sseldi 3750 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
126 | | elin 3947 |
. . . . . . . . . . . . . . . 16
⊢ (𝐶 ∈ (𝑈 ∩ 𝑉) ↔ (𝐶 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉)) |
127 | | reconnlem2.7 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑈 ∩ 𝑉) ⊆ (ℝ ∖ 𝐴)) |
128 | 127 | sseld 3751 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐶 ∈ (𝑈 ∩ 𝑉) → 𝐶 ∈ (ℝ ∖ 𝐴))) |
129 | 126, 128 | syl5bir 233 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐶 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ (ℝ ∖ 𝐴))) |
130 | 125, 129 | mpan2d 674 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐶 ∈ 𝑈 → 𝐶 ∈ (ℝ ∖ 𝐴))) |
131 | 123, 130 | mtod 189 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 𝐶 ∈ 𝑈) |
132 | | eleq1 2838 |
. . . . . . . . . . . . . 14
⊢ (𝑆 = 𝐶 → (𝑆 ∈ 𝑈 ↔ 𝐶 ∈ 𝑈)) |
133 | 132 | notbid 307 |
. . . . . . . . . . . . 13
⊢ (𝑆 = 𝐶 → (¬ 𝑆 ∈ 𝑈 ↔ ¬ 𝐶 ∈ 𝑈)) |
134 | 131, 133 | syl5ibrcom 237 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 = 𝐶 → ¬ 𝑆 ∈ 𝑈)) |
135 | 121, 134 | syld 47 |
. . . . . . . . . . 11
⊢ (𝜑 → (¬ 𝑆 < 𝐶 → ¬ 𝑆 ∈ 𝑈)) |
136 | 135 | con4d 115 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 ∈ 𝑈 → 𝑆 < 𝐶)) |
137 | 136 | imp 393 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑈) → 𝑆 < 𝐶) |
138 | | mnfxr 10301 |
. . . . . . . . . . 11
⊢ -∞
∈ ℝ* |
139 | | elioo2 12420 |
. . . . . . . . . . 11
⊢
((-∞ ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝑆 ∈ (-∞(,)𝐶) ↔ (𝑆 ∈ ℝ ∧ -∞ < 𝑆 ∧ 𝑆 < 𝐶))) |
140 | 138, 24, 139 | sylancr 575 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 ∈ (-∞(,)𝐶) ↔ (𝑆 ∈ ℝ ∧ -∞ < 𝑆 ∧ 𝑆 < 𝐶))) |
141 | 140 | adantr 466 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑈) → (𝑆 ∈ (-∞(,)𝐶) ↔ (𝑆 ∈ ℝ ∧ -∞ < 𝑆 ∧ 𝑆 < 𝐶))) |
142 | 112, 114,
137, 141 | mpbir3and 1427 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑈) → 𝑆 ∈ (-∞(,)𝐶)) |
143 | 142 | ex 397 |
. . . . . . 7
⊢ (𝜑 → (𝑆 ∈ 𝑈 → 𝑆 ∈ (-∞(,)𝐶))) |
144 | 143 | ancld 540 |
. . . . . 6
⊢ (𝜑 → (𝑆 ∈ 𝑈 → (𝑆 ∈ 𝑈 ∧ 𝑆 ∈ (-∞(,)𝐶)))) |
145 | | elin 3947 |
. . . . . . 7
⊢ (𝑆 ∈ (𝑈 ∩ (-∞(,)𝐶)) ↔ (𝑆 ∈ 𝑈 ∧ 𝑆 ∈ (-∞(,)𝐶))) |
146 | | reconnlem2.2 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ (topGen‘ran
(,))) |
147 | | retop 22784 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) ∈ Top |
148 | | iooretop 22788 |
. . . . . . . . 9
⊢
(-∞(,)𝐶)
∈ (topGen‘ran (,)) |
149 | | inopn 20923 |
. . . . . . . . 9
⊢
(((topGen‘ran (,)) ∈ Top ∧ 𝑈 ∈ (topGen‘ran (,)) ∧
(-∞(,)𝐶) ∈
(topGen‘ran (,))) → (𝑈 ∩ (-∞(,)𝐶)) ∈ (topGen‘ran
(,))) |
150 | 147, 148,
149 | mp3an13 1563 |
. . . . . . . 8
⊢ (𝑈 ∈ (topGen‘ran (,))
→ (𝑈 ∩
(-∞(,)𝐶)) ∈
(topGen‘ran (,))) |
151 | | eqid 2771 |
. . . . . . . . . . . 12
⊢
(MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) |
152 | 84, 151 | tgioo 22818 |
. . . . . . . . . . 11
⊢
(topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾
(ℝ × ℝ))) |
153 | 152 | mopni2 22517 |
. . . . . . . . . 10
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧ (𝑈 ∩ (-∞(,)𝐶)) ∈ (topGen‘ran (,)) ∧ 𝑆 ∈ (𝑈 ∩ (-∞(,)𝐶))) → ∃𝑟 ∈ ℝ+ (𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶))) |
154 | 101, 153 | mp3an1 1559 |
. . . . . . . . 9
⊢ (((𝑈 ∩ (-∞(,)𝐶)) ∈ (topGen‘ran (,))
∧ 𝑆 ∈ (𝑈 ∩ (-∞(,)𝐶))) → ∃𝑟 ∈ ℝ+
(𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶))) |
155 | 154 | ex 397 |
. . . . . . . 8
⊢ ((𝑈 ∩ (-∞(,)𝐶)) ∈ (topGen‘ran (,))
→ (𝑆 ∈ (𝑈 ∩ (-∞(,)𝐶)) → ∃𝑟 ∈ ℝ+
(𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶)))) |
156 | 146, 150,
155 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (𝑆 ∈ (𝑈 ∩ (-∞(,)𝐶)) → ∃𝑟 ∈ ℝ+ (𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶)))) |
157 | 145, 156 | syl5bir 233 |
. . . . . 6
⊢ (𝜑 → ((𝑆 ∈ 𝑈 ∧ 𝑆 ∈ (-∞(,)𝐶)) → ∃𝑟 ∈ ℝ+ (𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶)))) |
158 | 144, 157 | syld 47 |
. . . . 5
⊢ (𝜑 → (𝑆 ∈ 𝑈 → ∃𝑟 ∈ ℝ+ (𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶)))) |
159 | 111, 158 | mtod 189 |
. . . 4
⊢ (𝜑 → ¬ 𝑆 ∈ 𝑈) |
160 | | ltsubrp 12068 |
. . . . . . . . 9
⊢ ((𝑆 ∈ ℝ ∧ 𝑟 ∈ ℝ+)
→ (𝑆 − 𝑟) < 𝑆) |
161 | 43, 160 | sylan 569 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑆 − 𝑟) < 𝑆) |
162 | | rpre 12041 |
. . . . . . . . . 10
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) |
163 | | resubcl 10550 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝑆 − 𝑟) ∈ ℝ) |
164 | 43, 162, 163 | syl2an 583 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑆 − 𝑟) ∈ ℝ) |
165 | 164, 47 | ltnled 10389 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑆 − 𝑟) < 𝑆 ↔ ¬ 𝑆 ≤ (𝑆 − 𝑟))) |
166 | 161, 165 | mpbid 222 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ¬
𝑆 ≤ (𝑆 − 𝑟)) |
167 | 84 | bl2ioo 22814 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) = ((𝑆 − 𝑟)(,)(𝑆 + 𝑟))) |
168 | 43, 162, 167 | syl2an 583 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) = ((𝑆 − 𝑟)(,)(𝑆 + 𝑟))) |
169 | 168 | sseq1d 3781 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑉 ↔ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉)) |
170 | 15 | ad2antrr 705 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → (𝐵[,]𝐶) ⊆ 𝐴) |
171 | 2, 170 | syl5ss 3763 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → (𝑈 ∩ (𝐵[,]𝐶)) ⊆ 𝐴) |
172 | 171 | sselda 3752 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → 𝑤 ∈ 𝐴) |
173 | | elndif 3885 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ 𝐴 → ¬ 𝑤 ∈ (ℝ ∖ 𝐴)) |
174 | 172, 173 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → ¬ 𝑤 ∈ (ℝ ∖ 𝐴)) |
175 | 127 | ad3antrrr 709 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → (𝑈 ∩ 𝑉) ⊆ (ℝ ∖ 𝐴)) |
176 | | inss1 3981 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈 ∩ (𝐵[,]𝐶)) ⊆ 𝑈 |
177 | | simprl 754 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) |
178 | 176, 177 | sseldi 3750 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑤 ∈ 𝑈) |
179 | | simplr 752 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) |
180 | 18 | ad3antrrr 709 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → (𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ) |
181 | | simpr 471 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) |
182 | 180, 181 | sseldd 3753 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → 𝑤 ∈ ℝ) |
183 | 182 | adantrr 696 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑤 ∈ ℝ) |
184 | | simprr 756 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → (𝑆 − 𝑟) < 𝑤) |
185 | 47 | ad2antrr 705 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑆 ∈ ℝ) |
186 | | simpllr 760 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑟 ∈ ℝ+) |
187 | 186 | rpred 12074 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑟 ∈ ℝ) |
188 | 185, 187 | readdcld 10274 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → (𝑆 + 𝑟) ∈ ℝ) |
189 | 180 | adantrr 696 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → (𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ) |
190 | 29 | ad3antrrr 709 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅) |
191 | 40 | ad3antrrr 709 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝑧) |
192 | | suprub 11189 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ ∧ (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝑧) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → 𝑤 ≤ sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < )) |
193 | 189, 190,
191, 177, 192 | syl31anc 1479 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑤 ≤ sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < )) |
194 | 193, 1 | syl6breqr 4829 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑤 ≤ 𝑆) |
195 | 185, 186 | ltaddrpd 12107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑆 < (𝑆 + 𝑟)) |
196 | 183, 185,
188, 194, 195 | lelttrd 10400 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑤 < (𝑆 + 𝑟)) |
197 | 164 | ad2antrr 705 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → (𝑆 − 𝑟) ∈ ℝ) |
198 | | rexr 10290 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑆 − 𝑟) ∈ ℝ → (𝑆 − 𝑟) ∈
ℝ*) |
199 | | rexr 10290 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑆 + 𝑟) ∈ ℝ → (𝑆 + 𝑟) ∈
ℝ*) |
200 | | elioo2 12420 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑆 − 𝑟) ∈ ℝ* ∧ (𝑆 + 𝑟) ∈ ℝ*) → (𝑤 ∈ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ↔ (𝑤 ∈ ℝ ∧ (𝑆 − 𝑟) < 𝑤 ∧ 𝑤 < (𝑆 + 𝑟)))) |
201 | 198, 199,
200 | syl2an 583 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑆 − 𝑟) ∈ ℝ ∧ (𝑆 + 𝑟) ∈ ℝ) → (𝑤 ∈ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ↔ (𝑤 ∈ ℝ ∧ (𝑆 − 𝑟) < 𝑤 ∧ 𝑤 < (𝑆 + 𝑟)))) |
202 | 197, 188,
201 | syl2anc 573 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → (𝑤 ∈ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ↔ (𝑤 ∈ ℝ ∧ (𝑆 − 𝑟) < 𝑤 ∧ 𝑤 < (𝑆 + 𝑟)))) |
203 | 183, 184,
196, 202 | mpbir3and 1427 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑤 ∈ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟))) |
204 | 179, 203 | sseldd 3753 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑤 ∈ 𝑉) |
205 | 178, 204 | elind 3949 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑤 ∈ (𝑈 ∩ 𝑉)) |
206 | 175, 205 | sseldd 3753 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑤 ∈ (ℝ ∖ 𝐴)) |
207 | 206 | expr 444 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → ((𝑆 − 𝑟) < 𝑤 → 𝑤 ∈ (ℝ ∖ 𝐴))) |
208 | 174, 207 | mtod 189 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → ¬ (𝑆 − 𝑟) < 𝑤) |
209 | 164 | ad2antrr 705 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → (𝑆 − 𝑟) ∈ ℝ) |
210 | 182, 209 | lenltd 10388 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → (𝑤 ≤ (𝑆 − 𝑟) ↔ ¬ (𝑆 − 𝑟) < 𝑤)) |
211 | 208, 210 | mpbird 247 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → 𝑤 ≤ (𝑆 − 𝑟)) |
212 | 211 | ralrimiva 3115 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ (𝑆 − 𝑟)) |
213 | 18 | ad2antrr 705 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → (𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ) |
214 | 29 | ad2antrr 705 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅) |
215 | 40 | ad2antrr 705 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝑧) |
216 | 164 | adantr 466 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → (𝑆 − 𝑟) ∈ ℝ) |
217 | | suprleub 11194 |
. . . . . . . . . . . 12
⊢ ((((𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ ∧ (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝑧) ∧ (𝑆 − 𝑟) ∈ ℝ) → (sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ≤ (𝑆 − 𝑟) ↔ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ (𝑆 − 𝑟))) |
218 | 213, 214,
215, 216, 217 | syl31anc 1479 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → (sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ≤ (𝑆 − 𝑟) ↔ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ (𝑆 − 𝑟))) |
219 | 212, 218 | mpbird 247 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ≤ (𝑆 − 𝑟)) |
220 | 1, 219 | syl5eqbr 4822 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → 𝑆 ≤ (𝑆 − 𝑟)) |
221 | 220 | ex 397 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉 → 𝑆 ≤ (𝑆 − 𝑟))) |
222 | 169, 221 | sylbid 230 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑉 → 𝑆 ≤ (𝑆 − 𝑟))) |
223 | 166, 222 | mtod 189 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ¬
(𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑉) |
224 | 223 | nrexdv 3149 |
. . . . 5
⊢ (𝜑 → ¬ ∃𝑟 ∈ ℝ+
(𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑉) |
225 | | reconnlem2.3 |
. . . . . 6
⊢ (𝜑 → 𝑉 ∈ (topGen‘ran
(,))) |
226 | 152 | mopni2 22517 |
. . . . . . . 8
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧ 𝑉 ∈ (topGen‘ran (,)) ∧ 𝑆 ∈ 𝑉) → ∃𝑟 ∈ ℝ+ (𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑉) |
227 | 101, 226 | mp3an1 1559 |
. . . . . . 7
⊢ ((𝑉 ∈ (topGen‘ran (,))
∧ 𝑆 ∈ 𝑉) → ∃𝑟 ∈ ℝ+
(𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑉) |
228 | 227 | ex 397 |
. . . . . 6
⊢ (𝑉 ∈ (topGen‘ran (,))
→ (𝑆 ∈ 𝑉 → ∃𝑟 ∈ ℝ+
(𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑉)) |
229 | 225, 228 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑆 ∈ 𝑉 → ∃𝑟 ∈ ℝ+ (𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑉)) |
230 | 224, 229 | mtod 189 |
. . . 4
⊢ (𝜑 → ¬ 𝑆 ∈ 𝑉) |
231 | | ioran 968 |
. . . 4
⊢ (¬
(𝑆 ∈ 𝑈 ∨ 𝑆 ∈ 𝑉) ↔ (¬ 𝑆 ∈ 𝑈 ∧ ¬ 𝑆 ∈ 𝑉)) |
232 | 159, 230,
231 | sylanbrc 572 |
. . 3
⊢ (𝜑 → ¬ (𝑆 ∈ 𝑈 ∨ 𝑆 ∈ 𝑉)) |
233 | | elun 3904 |
. . 3
⊢ (𝑆 ∈ (𝑈 ∪ 𝑉) ↔ (𝑆 ∈ 𝑈 ∨ 𝑆 ∈ 𝑉)) |
234 | 232, 233 | sylnibr 318 |
. 2
⊢ (𝜑 → ¬ 𝑆 ∈ (𝑈 ∪ 𝑉)) |
235 | | elicc2 12442 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑆 ∈ (𝐵[,]𝐶) ↔ (𝑆 ∈ ℝ ∧ 𝐵 ≤ 𝑆 ∧ 𝑆 ≤ 𝐶))) |
236 | 21, 23, 235 | syl2anc 573 |
. . . . 5
⊢ (𝜑 → (𝑆 ∈ (𝐵[,]𝐶) ↔ (𝑆 ∈ ℝ ∧ 𝐵 ≤ 𝑆 ∧ 𝑆 ≤ 𝐶))) |
237 | 43, 64, 118, 236 | mpbir3and 1427 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ (𝐵[,]𝐶)) |
238 | 15, 237 | sseldd 3753 |
. . 3
⊢ (𝜑 → 𝑆 ∈ 𝐴) |
239 | | ssel 3746 |
. . 3
⊢ (𝐴 ⊆ (𝑈 ∪ 𝑉) → (𝑆 ∈ 𝐴 → 𝑆 ∈ (𝑈 ∪ 𝑉))) |
240 | 238, 239 | syl5com 31 |
. 2
⊢ (𝜑 → (𝐴 ⊆ (𝑈 ∪ 𝑉) → 𝑆 ∈ (𝑈 ∪ 𝑉))) |
241 | 234, 240 | mtod 189 |
1
⊢ (𝜑 → ¬ 𝐴 ⊆ (𝑈 ∪ 𝑉)) |