Step | Hyp | Ref
| Expression |
1 | | reconnlem2.9 |
. . . . . . . . . . 11
⊢ 𝑆 = sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) |
2 | | inss2 3834 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∩ (𝐵[,]𝐶)) ⊆ (𝐵[,]𝐶) |
3 | | inss2 3834 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 ∩ 𝐴) ⊆ 𝐴 |
4 | | reconnlem2.5 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 ∈ (𝑈 ∩ 𝐴)) |
5 | 3, 4 | sseldi 3601 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈ 𝐴) |
6 | | inss2 3834 |
. . . . . . . . . . . . . . . 16
⊢ (𝑉 ∩ 𝐴) ⊆ 𝐴 |
7 | | reconnlem2.6 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 ∈ (𝑉 ∩ 𝐴)) |
8 | 6, 7 | sseldi 3601 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ∈ 𝐴) |
9 | | reconnlem2.4 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) |
10 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝐵 → (𝑥[,]𝑦) = (𝐵[,]𝑦)) |
11 | 10 | sseq1d 3632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝐵 → ((𝑥[,]𝑦) ⊆ 𝐴 ↔ (𝐵[,]𝑦) ⊆ 𝐴)) |
12 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝐶 → (𝐵[,]𝑦) = (𝐵[,]𝐶)) |
13 | 12 | sseq1d 3632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝐶 → ((𝐵[,]𝑦) ⊆ 𝐴 ↔ (𝐵[,]𝐶) ⊆ 𝐴)) |
14 | 11, 13 | rspc2va 3323 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) → (𝐵[,]𝐶) ⊆ 𝐴) |
15 | 5, 8, 9, 14 | syl21anc 1325 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵[,]𝐶) ⊆ 𝐴) |
16 | | reconnlem2.1 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
17 | 15, 16 | sstrd 3613 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵[,]𝐶) ⊆ ℝ) |
18 | 2, 17 | syl5ss 3614 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ) |
19 | | inss1 3833 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 ∩ 𝐴) ⊆ 𝑈 |
20 | 19, 4 | sseldi 3601 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ 𝑈) |
21 | 16, 5 | sseldd 3604 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 ∈ ℝ) |
22 | 21 | rexrd 10089 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
23 | 16, 8 | sseldd 3604 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 ∈ ℝ) |
24 | 23 | rexrd 10089 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
25 | | reconnlem2.8 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ≤ 𝐶) |
26 | | lbicc2 12288 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝐵
≤ 𝐶) → 𝐵 ∈ (𝐵[,]𝐶)) |
27 | 22, 24, 25, 26 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ (𝐵[,]𝐶)) |
28 | 20, 27 | elind 3798 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ (𝑈 ∩ (𝐵[,]𝐶))) |
29 | | ne0i 3921 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ (𝑈 ∩ (𝐵[,]𝐶)) → (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅) |
31 | 2 | sseli 3599 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) → 𝑤 ∈ (𝐵[,]𝐶)) |
32 | | elicc2 12238 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑤 ∈ (𝐵[,]𝐶) ↔ (𝑤 ∈ ℝ ∧ 𝐵 ≤ 𝑤 ∧ 𝑤 ≤ 𝐶))) |
33 | 21, 23, 32 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑤 ∈ (𝐵[,]𝐶) ↔ (𝑤 ∈ ℝ ∧ 𝐵 ≤ 𝑤 ∧ 𝑤 ≤ 𝐶))) |
34 | | simp3 1063 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ ℝ ∧ 𝐵 ≤ 𝑤 ∧ 𝑤 ≤ 𝐶) → 𝑤 ≤ 𝐶) |
35 | 33, 34 | syl6bi 243 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑤 ∈ (𝐵[,]𝐶) → 𝑤 ≤ 𝐶)) |
36 | 31, 35 | syl5 34 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) → 𝑤 ≤ 𝐶)) |
37 | 36 | ralrimiv 2965 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝐶) |
38 | | breq2 4657 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝐶 → (𝑤 ≤ 𝑧 ↔ 𝑤 ≤ 𝐶)) |
39 | 38 | ralbidv 2986 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝐶 → (∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝑧 ↔ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝐶)) |
40 | 39 | rspcev 3309 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ ℝ ∧
∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝐶) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝑧) |
41 | 23, 37, 40 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝑧) |
42 | | suprcl 10983 |
. . . . . . . . . . . 12
⊢ (((𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ ∧ (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝑧) → sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ∈
ℝ) |
43 | 18, 30, 41, 42 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (𝜑 → sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ∈
ℝ) |
44 | 1, 43 | syl5eqel 2705 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ ℝ) |
45 | | rphalfcl 11858 |
. . . . . . . . . 10
⊢ (𝑟 ∈ ℝ+
→ (𝑟 / 2) ∈
ℝ+) |
46 | | ltaddrp 11867 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ ℝ ∧ (𝑟 / 2) ∈
ℝ+) → 𝑆 < (𝑆 + (𝑟 / 2))) |
47 | 44, 45, 46 | syl2an 494 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑆 < (𝑆 + (𝑟 / 2))) |
48 | 44 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑆 ∈
ℝ) |
49 | 45 | rpred 11872 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ ℝ+
→ (𝑟 / 2) ∈
ℝ) |
50 | | readdcl 10019 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ ℝ ∧ (𝑟 / 2) ∈ ℝ) →
(𝑆 + (𝑟 / 2)) ∈ ℝ) |
51 | 44, 49, 50 | syl2an 494 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑆 + (𝑟 / 2)) ∈ ℝ) |
52 | 48, 51 | ltnled 10184 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑆 < (𝑆 + (𝑟 / 2)) ↔ ¬ (𝑆 + (𝑟 / 2)) ≤ 𝑆)) |
53 | 47, 52 | mpbid 222 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ¬
(𝑆 + (𝑟 / 2)) ≤ 𝑆) |
54 | 18 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ) |
55 | 30 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅) |
56 | 41 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝑧) |
57 | | inss1 3833 |
. . . . . . . . . . . 12
⊢ (𝑈 ∩ (-∞(,)𝐶)) ⊆ 𝑈 |
58 | | simpr 477 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) |
59 | 57, 58 | sseldi 3601 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ∈ 𝑈) |
60 | 51 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ∈ ℝ) |
61 | 21 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → 𝐵 ∈ ℝ) |
62 | 44 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → 𝑆 ∈ ℝ) |
63 | | suprub 10984 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ ∧ (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝑧) ∧ 𝐵 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → 𝐵 ≤ sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < )) |
64 | 18, 30, 41, 28, 63 | syl31anc 1329 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ≤ sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < )) |
65 | 64, 1 | syl6breqr 4695 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ≤ 𝑆) |
66 | 65 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → 𝐵 ≤ 𝑆) |
67 | 47 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → 𝑆 < (𝑆 + (𝑟 / 2))) |
68 | 62, 60, 67 | ltled 10185 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → 𝑆 ≤ (𝑆 + (𝑟 / 2))) |
69 | 61, 62, 60, 66, 68 | letrd 10194 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → 𝐵 ≤ (𝑆 + (𝑟 / 2))) |
70 | 23 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → 𝐶 ∈ ℝ) |
71 | | inss2 3834 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 ∩ (-∞(,)𝐶)) ⊆ (-∞(,)𝐶) |
72 | 71, 58 | sseldi 3601 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ∈ (-∞(,)𝐶)) |
73 | | eliooord 12233 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 + (𝑟 / 2)) ∈ (-∞(,)𝐶) → (-∞ < (𝑆 + (𝑟 / 2)) ∧ (𝑆 + (𝑟 / 2)) < 𝐶)) |
74 | 73 | simprd 479 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 + (𝑟 / 2)) ∈ (-∞(,)𝐶) → (𝑆 + (𝑟 / 2)) < 𝐶) |
75 | 72, 74 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) < 𝐶) |
76 | 60, 70, 75 | ltled 10185 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ≤ 𝐶) |
77 | | elicc2 12238 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝑆 + (𝑟 / 2)) ∈ (𝐵[,]𝐶) ↔ ((𝑆 + (𝑟 / 2)) ∈ ℝ ∧ 𝐵 ≤ (𝑆 + (𝑟 / 2)) ∧ (𝑆 + (𝑟 / 2)) ≤ 𝐶))) |
78 | 61, 70, 77 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → ((𝑆 + (𝑟 / 2)) ∈ (𝐵[,]𝐶) ↔ ((𝑆 + (𝑟 / 2)) ∈ ℝ ∧ 𝐵 ≤ (𝑆 + (𝑟 / 2)) ∧ (𝑆 + (𝑟 / 2)) ≤ 𝐶))) |
79 | 60, 69, 76, 78 | mpbir3and 1245 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ∈ (𝐵[,]𝐶)) |
80 | 59, 79 | elind 3798 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (𝐵[,]𝐶))) |
81 | | suprub 10984 |
. . . . . . . . . 10
⊢ ((((𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ ∧ (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝑧) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (𝐵[,]𝐶))) → (𝑆 + (𝑟 / 2)) ≤ sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < )) |
82 | 54, 55, 56, 80, 81 | syl31anc 1329 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ≤ sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < )) |
83 | 82, 1 | syl6breqr 4695 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) → (𝑆 + (𝑟 / 2)) ≤ 𝑆) |
84 | 53, 83 | mtand 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ¬
(𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶))) |
85 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − )
↾ (ℝ × ℝ)) |
86 | 85 | remetdval 22592 |
. . . . . . . . . . . 12
⊢ (((𝑆 + (𝑟 / 2)) ∈ ℝ ∧ 𝑆 ∈ ℝ) → ((𝑆 + (𝑟 / 2))((abs ∘ − ) ↾
(ℝ × ℝ))𝑆) = (abs‘((𝑆 + (𝑟 / 2)) − 𝑆))) |
87 | 51, 48, 86 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑆 + (𝑟 / 2))((abs ∘ − ) ↾
(ℝ × ℝ))𝑆) = (abs‘((𝑆 + (𝑟 / 2)) − 𝑆))) |
88 | 48 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑆 ∈
ℂ) |
89 | 49 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ∈
ℝ) |
90 | 89 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ∈
ℂ) |
91 | 88, 90 | pncan2d 10394 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑆 + (𝑟 / 2)) − 𝑆) = (𝑟 / 2)) |
92 | 91 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(abs‘((𝑆 + (𝑟 / 2)) − 𝑆)) = (abs‘(𝑟 / 2))) |
93 | 45 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ∈
ℝ+) |
94 | | rpre 11839 |
. . . . . . . . . . . . 13
⊢ ((𝑟 / 2) ∈ ℝ+
→ (𝑟 / 2) ∈
ℝ) |
95 | | rpge0 11845 |
. . . . . . . . . . . . 13
⊢ ((𝑟 / 2) ∈ ℝ+
→ 0 ≤ (𝑟 /
2)) |
96 | 94, 95 | absidd 14161 |
. . . . . . . . . . . 12
⊢ ((𝑟 / 2) ∈ ℝ+
→ (abs‘(𝑟 / 2))
= (𝑟 / 2)) |
97 | 93, 96 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(abs‘(𝑟 / 2)) =
(𝑟 / 2)) |
98 | 87, 92, 97 | 3eqtrd 2660 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑆 + (𝑟 / 2))((abs ∘ − ) ↾
(ℝ × ℝ))𝑆) = (𝑟 / 2)) |
99 | | rphalflt 11860 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ ℝ+
→ (𝑟 / 2) < 𝑟) |
100 | 99 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) < 𝑟) |
101 | 98, 100 | eqbrtrd 4675 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑆 + (𝑟 / 2))((abs ∘ − ) ↾
(ℝ × ℝ))𝑆) < 𝑟) |
102 | 85 | rexmet 22594 |
. . . . . . . . . . 11
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) |
103 | 102 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ)) |
104 | | rpxr 11840 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
105 | 104 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ*) |
106 | | elbl3 22197 |
. . . . . . . . . 10
⊢ (((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧ 𝑟 ∈ ℝ*) ∧ (𝑆 ∈ ℝ ∧ (𝑆 + (𝑟 / 2)) ∈ ℝ)) → ((𝑆 + (𝑟 / 2)) ∈ (𝑆(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ↔ ((𝑆 + (𝑟 / 2))((abs ∘ − ) ↾
(ℝ × ℝ))𝑆) < 𝑟)) |
107 | 103, 105,
48, 51, 106 | syl22anc 1327 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑆 + (𝑟 / 2)) ∈ (𝑆(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ↔ ((𝑆 + (𝑟 / 2))((abs ∘ − ) ↾
(ℝ × ℝ))𝑆) < 𝑟)) |
108 | 101, 107 | mpbird 247 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑆 + (𝑟 / 2)) ∈ (𝑆(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟)) |
109 | | ssel 3597 |
. . . . . . . 8
⊢ ((𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶)) → ((𝑆 + (𝑟 / 2)) ∈ (𝑆(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) → (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶)))) |
110 | 108, 109 | syl5com 31 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶)) → (𝑆 + (𝑟 / 2)) ∈ (𝑈 ∩ (-∞(,)𝐶)))) |
111 | 84, 110 | mtod 189 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ¬
(𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶))) |
112 | 111 | nrexdv 3001 |
. . . . 5
⊢ (𝜑 → ¬ ∃𝑟 ∈ ℝ+
(𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶))) |
113 | 44 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑈) → 𝑆 ∈ ℝ) |
114 | | mnflt 11957 |
. . . . . . . . . 10
⊢ (𝑆 ∈ ℝ → -∞
< 𝑆) |
115 | 113, 114 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑈) → -∞ < 𝑆) |
116 | | suprleub 10989 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ ∧ (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝑧) ∧ 𝐶 ∈ ℝ) → (sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ≤ 𝐶 ↔ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝐶)) |
117 | 18, 30, 41, 23, 116 | syl31anc 1329 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ≤ 𝐶 ↔ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝐶)) |
118 | 37, 117 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ≤ 𝐶) |
119 | 1, 118 | syl5eqbr 4688 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ≤ 𝐶) |
120 | 44, 23 | leloed 10180 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑆 ≤ 𝐶 ↔ (𝑆 < 𝐶 ∨ 𝑆 = 𝐶))) |
121 | 119, 120 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆 < 𝐶 ∨ 𝑆 = 𝐶)) |
122 | 121 | ord 392 |
. . . . . . . . . . . 12
⊢ (𝜑 → (¬ 𝑆 < 𝐶 → 𝑆 = 𝐶)) |
123 | | elndif 3734 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ∈ 𝐴 → ¬ 𝐶 ∈ (ℝ ∖ 𝐴)) |
124 | 8, 123 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ 𝐶 ∈ (ℝ ∖ 𝐴)) |
125 | | inss1 3833 |
. . . . . . . . . . . . . . . 16
⊢ (𝑉 ∩ 𝐴) ⊆ 𝑉 |
126 | 125, 7 | sseldi 3601 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
127 | | elin 3796 |
. . . . . . . . . . . . . . . 16
⊢ (𝐶 ∈ (𝑈 ∩ 𝑉) ↔ (𝐶 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉)) |
128 | | reconnlem2.7 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑈 ∩ 𝑉) ⊆ (ℝ ∖ 𝐴)) |
129 | 128 | sseld 3602 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐶 ∈ (𝑈 ∩ 𝑉) → 𝐶 ∈ (ℝ ∖ 𝐴))) |
130 | 127, 129 | syl5bir 233 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐶 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ (ℝ ∖ 𝐴))) |
131 | 126, 130 | mpan2d 710 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐶 ∈ 𝑈 → 𝐶 ∈ (ℝ ∖ 𝐴))) |
132 | 124, 131 | mtod 189 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 𝐶 ∈ 𝑈) |
133 | | eleq1 2689 |
. . . . . . . . . . . . . 14
⊢ (𝑆 = 𝐶 → (𝑆 ∈ 𝑈 ↔ 𝐶 ∈ 𝑈)) |
134 | 133 | notbid 308 |
. . . . . . . . . . . . 13
⊢ (𝑆 = 𝐶 → (¬ 𝑆 ∈ 𝑈 ↔ ¬ 𝐶 ∈ 𝑈)) |
135 | 132, 134 | syl5ibrcom 237 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 = 𝐶 → ¬ 𝑆 ∈ 𝑈)) |
136 | 122, 135 | syld 47 |
. . . . . . . . . . 11
⊢ (𝜑 → (¬ 𝑆 < 𝐶 → ¬ 𝑆 ∈ 𝑈)) |
137 | 136 | con4d 114 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 ∈ 𝑈 → 𝑆 < 𝐶)) |
138 | 137 | imp 445 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑈) → 𝑆 < 𝐶) |
139 | | mnfxr 10096 |
. . . . . . . . . . 11
⊢ -∞
∈ ℝ* |
140 | | elioo2 12216 |
. . . . . . . . . . 11
⊢
((-∞ ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝑆 ∈ (-∞(,)𝐶) ↔ (𝑆 ∈ ℝ ∧ -∞ < 𝑆 ∧ 𝑆 < 𝐶))) |
141 | 139, 24, 140 | sylancr 695 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 ∈ (-∞(,)𝐶) ↔ (𝑆 ∈ ℝ ∧ -∞ < 𝑆 ∧ 𝑆 < 𝐶))) |
142 | 141 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑈) → (𝑆 ∈ (-∞(,)𝐶) ↔ (𝑆 ∈ ℝ ∧ -∞ < 𝑆 ∧ 𝑆 < 𝐶))) |
143 | 113, 115,
138, 142 | mpbir3and 1245 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑈) → 𝑆 ∈ (-∞(,)𝐶)) |
144 | 143 | ex 450 |
. . . . . . 7
⊢ (𝜑 → (𝑆 ∈ 𝑈 → 𝑆 ∈ (-∞(,)𝐶))) |
145 | 144 | ancld 576 |
. . . . . 6
⊢ (𝜑 → (𝑆 ∈ 𝑈 → (𝑆 ∈ 𝑈 ∧ 𝑆 ∈ (-∞(,)𝐶)))) |
146 | | elin 3796 |
. . . . . . 7
⊢ (𝑆 ∈ (𝑈 ∩ (-∞(,)𝐶)) ↔ (𝑆 ∈ 𝑈 ∧ 𝑆 ∈ (-∞(,)𝐶))) |
147 | | reconnlem2.2 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ (topGen‘ran
(,))) |
148 | | retop 22565 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) ∈ Top |
149 | | iooretop 22569 |
. . . . . . . . 9
⊢
(-∞(,)𝐶)
∈ (topGen‘ran (,)) |
150 | | inopn 20704 |
. . . . . . . . 9
⊢
(((topGen‘ran (,)) ∈ Top ∧ 𝑈 ∈ (topGen‘ran (,)) ∧
(-∞(,)𝐶) ∈
(topGen‘ran (,))) → (𝑈 ∩ (-∞(,)𝐶)) ∈ (topGen‘ran
(,))) |
151 | 148, 149,
150 | mp3an13 1415 |
. . . . . . . 8
⊢ (𝑈 ∈ (topGen‘ran (,))
→ (𝑈 ∩
(-∞(,)𝐶)) ∈
(topGen‘ran (,))) |
152 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) |
153 | 85, 152 | tgioo 22599 |
. . . . . . . . . . 11
⊢
(topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾
(ℝ × ℝ))) |
154 | 153 | mopni2 22298 |
. . . . . . . . . 10
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧ (𝑈 ∩ (-∞(,)𝐶)) ∈ (topGen‘ran (,)) ∧ 𝑆 ∈ (𝑈 ∩ (-∞(,)𝐶))) → ∃𝑟 ∈ ℝ+ (𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶))) |
155 | 102, 154 | mp3an1 1411 |
. . . . . . . . 9
⊢ (((𝑈 ∩ (-∞(,)𝐶)) ∈ (topGen‘ran (,))
∧ 𝑆 ∈ (𝑈 ∩ (-∞(,)𝐶))) → ∃𝑟 ∈ ℝ+
(𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶))) |
156 | 155 | ex 450 |
. . . . . . . 8
⊢ ((𝑈 ∩ (-∞(,)𝐶)) ∈ (topGen‘ran (,))
→ (𝑆 ∈ (𝑈 ∩ (-∞(,)𝐶)) → ∃𝑟 ∈ ℝ+
(𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶)))) |
157 | 147, 151,
156 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (𝑆 ∈ (𝑈 ∩ (-∞(,)𝐶)) → ∃𝑟 ∈ ℝ+ (𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶)))) |
158 | 146, 157 | syl5bir 233 |
. . . . . 6
⊢ (𝜑 → ((𝑆 ∈ 𝑈 ∧ 𝑆 ∈ (-∞(,)𝐶)) → ∃𝑟 ∈ ℝ+ (𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶)))) |
159 | 145, 158 | syld 47 |
. . . . 5
⊢ (𝜑 → (𝑆 ∈ 𝑈 → ∃𝑟 ∈ ℝ+ (𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑈 ∩ (-∞(,)𝐶)))) |
160 | 112, 159 | mtod 189 |
. . . 4
⊢ (𝜑 → ¬ 𝑆 ∈ 𝑈) |
161 | | ltsubrp 11866 |
. . . . . . . . 9
⊢ ((𝑆 ∈ ℝ ∧ 𝑟 ∈ ℝ+)
→ (𝑆 − 𝑟) < 𝑆) |
162 | 44, 161 | sylan 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑆 − 𝑟) < 𝑆) |
163 | | rpre 11839 |
. . . . . . . . . 10
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) |
164 | | resubcl 10345 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝑆 − 𝑟) ∈ ℝ) |
165 | 44, 163, 164 | syl2an 494 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑆 − 𝑟) ∈ ℝ) |
166 | 165, 48 | ltnled 10184 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑆 − 𝑟) < 𝑆 ↔ ¬ 𝑆 ≤ (𝑆 − 𝑟))) |
167 | 162, 166 | mpbid 222 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ¬
𝑆 ≤ (𝑆 − 𝑟)) |
168 | 85 | bl2ioo 22595 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) = ((𝑆 − 𝑟)(,)(𝑆 + 𝑟))) |
169 | 44, 163, 168 | syl2an 494 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) = ((𝑆 − 𝑟)(,)(𝑆 + 𝑟))) |
170 | 169 | sseq1d 3632 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑉 ↔ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉)) |
171 | 15 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → (𝐵[,]𝐶) ⊆ 𝐴) |
172 | 2, 171 | syl5ss 3614 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → (𝑈 ∩ (𝐵[,]𝐶)) ⊆ 𝐴) |
173 | 172 | sselda 3603 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → 𝑤 ∈ 𝐴) |
174 | | elndif 3734 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ 𝐴 → ¬ 𝑤 ∈ (ℝ ∖ 𝐴)) |
175 | 173, 174 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → ¬ 𝑤 ∈ (ℝ ∖ 𝐴)) |
176 | 128 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → (𝑈 ∩ 𝑉) ⊆ (ℝ ∖ 𝐴)) |
177 | | inss1 3833 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈 ∩ (𝐵[,]𝐶)) ⊆ 𝑈 |
178 | | simprl 794 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) |
179 | 177, 178 | sseldi 3601 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑤 ∈ 𝑈) |
180 | | simplr 792 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) |
181 | 18 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → (𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ) |
182 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) |
183 | 181, 182 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → 𝑤 ∈ ℝ) |
184 | 183 | adantrr 753 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑤 ∈ ℝ) |
185 | | simprr 796 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → (𝑆 − 𝑟) < 𝑤) |
186 | 48 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑆 ∈ ℝ) |
187 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑟 ∈ ℝ+) |
188 | 187 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑟 ∈ ℝ) |
189 | 186, 188 | readdcld 10069 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → (𝑆 + 𝑟) ∈ ℝ) |
190 | 181 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → (𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ) |
191 | 30 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅) |
192 | 41 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝑧) |
193 | | suprub 10984 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ ∧ (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝑧) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → 𝑤 ≤ sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < )) |
194 | 190, 191,
192, 178, 193 | syl31anc 1329 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑤 ≤ sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < )) |
195 | 194, 1 | syl6breqr 4695 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑤 ≤ 𝑆) |
196 | 186, 187 | ltaddrpd 11905 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑆 < (𝑆 + 𝑟)) |
197 | 184, 186,
189, 195, 196 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑤 < (𝑆 + 𝑟)) |
198 | 165 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → (𝑆 − 𝑟) ∈ ℝ) |
199 | | rexr 10085 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑆 − 𝑟) ∈ ℝ → (𝑆 − 𝑟) ∈
ℝ*) |
200 | | rexr 10085 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑆 + 𝑟) ∈ ℝ → (𝑆 + 𝑟) ∈
ℝ*) |
201 | | elioo2 12216 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑆 − 𝑟) ∈ ℝ* ∧ (𝑆 + 𝑟) ∈ ℝ*) → (𝑤 ∈ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ↔ (𝑤 ∈ ℝ ∧ (𝑆 − 𝑟) < 𝑤 ∧ 𝑤 < (𝑆 + 𝑟)))) |
202 | 199, 200,
201 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑆 − 𝑟) ∈ ℝ ∧ (𝑆 + 𝑟) ∈ ℝ) → (𝑤 ∈ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ↔ (𝑤 ∈ ℝ ∧ (𝑆 − 𝑟) < 𝑤 ∧ 𝑤 < (𝑆 + 𝑟)))) |
203 | 198, 189,
202 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → (𝑤 ∈ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ↔ (𝑤 ∈ ℝ ∧ (𝑆 − 𝑟) < 𝑤 ∧ 𝑤 < (𝑆 + 𝑟)))) |
204 | 184, 185,
197, 203 | mpbir3and 1245 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑤 ∈ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟))) |
205 | 180, 204 | sseldd 3604 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑤 ∈ 𝑉) |
206 | 179, 205 | elind 3798 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑤 ∈ (𝑈 ∩ 𝑉)) |
207 | 176, 206 | sseldd 3604 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ (𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶)) ∧ (𝑆 − 𝑟) < 𝑤)) → 𝑤 ∈ (ℝ ∖ 𝐴)) |
208 | 207 | expr 643 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → ((𝑆 − 𝑟) < 𝑤 → 𝑤 ∈ (ℝ ∖ 𝐴))) |
209 | 175, 208 | mtod 189 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → ¬ (𝑆 − 𝑟) < 𝑤) |
210 | 165 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → (𝑆 − 𝑟) ∈ ℝ) |
211 | 183, 210 | lenltd 10183 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → (𝑤 ≤ (𝑆 − 𝑟) ↔ ¬ (𝑆 − 𝑟) < 𝑤)) |
212 | 209, 211 | mpbird 247 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) ∧ 𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))) → 𝑤 ≤ (𝑆 − 𝑟)) |
213 | 212 | ralrimiva 2966 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ (𝑆 − 𝑟)) |
214 | 18 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → (𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ) |
215 | 30 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅) |
216 | 41 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝑧) |
217 | 165 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → (𝑆 − 𝑟) ∈ ℝ) |
218 | | suprleub 10989 |
. . . . . . . . . . . 12
⊢ ((((𝑈 ∩ (𝐵[,]𝐶)) ⊆ ℝ ∧ (𝑈 ∩ (𝐵[,]𝐶)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ 𝑧) ∧ (𝑆 − 𝑟) ∈ ℝ) → (sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ≤ (𝑆 − 𝑟) ↔ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ (𝑆 − 𝑟))) |
219 | 214, 215,
216, 217, 218 | syl31anc 1329 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → (sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ≤ (𝑆 − 𝑟) ↔ ∀𝑤 ∈ (𝑈 ∩ (𝐵[,]𝐶))𝑤 ≤ (𝑆 − 𝑟))) |
220 | 213, 219 | mpbird 247 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ≤ (𝑆 − 𝑟)) |
221 | 1, 220 | syl5eqbr 4688 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ ((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉) → 𝑆 ≤ (𝑆 − 𝑟)) |
222 | 221 | ex 450 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (((𝑆 − 𝑟)(,)(𝑆 + 𝑟)) ⊆ 𝑉 → 𝑆 ≤ (𝑆 − 𝑟))) |
223 | 170, 222 | sylbid 230 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑉 → 𝑆 ≤ (𝑆 − 𝑟))) |
224 | 167, 223 | mtod 189 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ¬
(𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑉) |
225 | 224 | nrexdv 3001 |
. . . . 5
⊢ (𝜑 → ¬ ∃𝑟 ∈ ℝ+
(𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑉) |
226 | | reconnlem2.3 |
. . . . . 6
⊢ (𝜑 → 𝑉 ∈ (topGen‘ran
(,))) |
227 | 153 | mopni2 22298 |
. . . . . . . 8
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧ 𝑉 ∈ (topGen‘ran (,)) ∧ 𝑆 ∈ 𝑉) → ∃𝑟 ∈ ℝ+ (𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑉) |
228 | 102, 227 | mp3an1 1411 |
. . . . . . 7
⊢ ((𝑉 ∈ (topGen‘ran (,))
∧ 𝑆 ∈ 𝑉) → ∃𝑟 ∈ ℝ+
(𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑉) |
229 | 228 | ex 450 |
. . . . . 6
⊢ (𝑉 ∈ (topGen‘ran (,))
→ (𝑆 ∈ 𝑉 → ∃𝑟 ∈ ℝ+
(𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑉)) |
230 | 226, 229 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑆 ∈ 𝑉 → ∃𝑟 ∈ ℝ+ (𝑆(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝑉)) |
231 | 225, 230 | mtod 189 |
. . . 4
⊢ (𝜑 → ¬ 𝑆 ∈ 𝑉) |
232 | | ioran 511 |
. . . 4
⊢ (¬
(𝑆 ∈ 𝑈 ∨ 𝑆 ∈ 𝑉) ↔ (¬ 𝑆 ∈ 𝑈 ∧ ¬ 𝑆 ∈ 𝑉)) |
233 | 160, 231,
232 | sylanbrc 698 |
. . 3
⊢ (𝜑 → ¬ (𝑆 ∈ 𝑈 ∨ 𝑆 ∈ 𝑉)) |
234 | | elun 3753 |
. . 3
⊢ (𝑆 ∈ (𝑈 ∪ 𝑉) ↔ (𝑆 ∈ 𝑈 ∨ 𝑆 ∈ 𝑉)) |
235 | 233, 234 | sylnibr 319 |
. 2
⊢ (𝜑 → ¬ 𝑆 ∈ (𝑈 ∪ 𝑉)) |
236 | | elicc2 12238 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑆 ∈ (𝐵[,]𝐶) ↔ (𝑆 ∈ ℝ ∧ 𝐵 ≤ 𝑆 ∧ 𝑆 ≤ 𝐶))) |
237 | 21, 23, 236 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (𝑆 ∈ (𝐵[,]𝐶) ↔ (𝑆 ∈ ℝ ∧ 𝐵 ≤ 𝑆 ∧ 𝑆 ≤ 𝐶))) |
238 | 44, 65, 119, 237 | mpbir3and 1245 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ (𝐵[,]𝐶)) |
239 | 15, 238 | sseldd 3604 |
. . 3
⊢ (𝜑 → 𝑆 ∈ 𝐴) |
240 | | ssel 3597 |
. . 3
⊢ (𝐴 ⊆ (𝑈 ∪ 𝑉) → (𝑆 ∈ 𝐴 → 𝑆 ∈ (𝑈 ∪ 𝑉))) |
241 | 239, 240 | syl5com 31 |
. 2
⊢ (𝜑 → (𝐴 ⊆ (𝑈 ∪ 𝑉) → 𝑆 ∈ (𝑈 ∪ 𝑉))) |
242 | 235, 241 | mtod 189 |
1
⊢ (𝜑 → ¬ 𝐴 ⊆ (𝑈 ∪ 𝑉)) |