Step | Hyp | Ref
| Expression |
1 | | reconnlem1 22629 |
. . . 4
⊢ (((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥[,]𝑦) ⊆ 𝐴) |
2 | 1 | ralrimivva 2971 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧
((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) |
3 | 2 | ex 450 |
. 2
⊢ (𝐴 ⊆ ℝ →
(((topGen‘ran (,)) ↾t 𝐴) ∈ Conn → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴)) |
4 | | n0 3931 |
. . . . . . . . 9
⊢ ((𝑢 ∩ 𝐴) ≠ ∅ ↔ ∃𝑏 𝑏 ∈ (𝑢 ∩ 𝐴)) |
5 | | n0 3931 |
. . . . . . . . 9
⊢ ((𝑣 ∩ 𝐴) ≠ ∅ ↔ ∃𝑐 𝑐 ∈ (𝑣 ∩ 𝐴)) |
6 | 4, 5 | anbi12i 733 |
. . . . . . . 8
⊢ (((𝑢 ∩ 𝐴) ≠ ∅ ∧ (𝑣 ∩ 𝐴) ≠ ∅) ↔ (∃𝑏 𝑏 ∈ (𝑢 ∩ 𝐴) ∧ ∃𝑐 𝑐 ∈ (𝑣 ∩ 𝐴))) |
7 | | eeanv 2182 |
. . . . . . . . 9
⊢
(∃𝑏∃𝑐(𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ↔ (∃𝑏 𝑏 ∈ (𝑢 ∩ 𝐴) ∧ ∃𝑐 𝑐 ∈ (𝑣 ∩ 𝐴))) |
8 | | simplll 798 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ⊆ ℝ ∧ (𝑢 ∈ (topGen‘ran (,))
∧ 𝑣 ∈
(topGen‘ran (,)))) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) → 𝐴 ⊆ ℝ) |
9 | | inss2 3834 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∩ 𝐴) ⊆ 𝐴 |
10 | | simprll 802 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ⊆ ℝ ∧ (𝑢 ∈ (topGen‘ran (,))
∧ 𝑣 ∈
(topGen‘ran (,)))) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) → 𝑏 ∈ (𝑢 ∩ 𝐴)) |
11 | 9, 10 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ⊆ ℝ ∧ (𝑢 ∈ (topGen‘ran (,))
∧ 𝑣 ∈
(topGen‘ran (,)))) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) → 𝑏 ∈ 𝐴) |
12 | 8, 11 | sseldd 3604 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ⊆ ℝ ∧ (𝑢 ∈ (topGen‘ran (,))
∧ 𝑣 ∈
(topGen‘ran (,)))) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) → 𝑏 ∈ ℝ) |
13 | | inss2 3834 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∩ 𝐴) ⊆ 𝐴 |
14 | | simprlr 803 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ⊆ ℝ ∧ (𝑢 ∈ (topGen‘ran (,))
∧ 𝑣 ∈
(topGen‘ran (,)))) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) → 𝑐 ∈ (𝑣 ∩ 𝐴)) |
15 | 13, 14 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ⊆ ℝ ∧ (𝑢 ∈ (topGen‘ran (,))
∧ 𝑣 ∈
(topGen‘ran (,)))) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) → 𝑐 ∈ 𝐴) |
16 | 8, 15 | sseldd 3604 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ⊆ ℝ ∧ (𝑢 ∈ (topGen‘ran (,))
∧ 𝑣 ∈
(topGen‘ran (,)))) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) → 𝑐 ∈ ℝ) |
17 | 8 | adantr 481 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ⊆
ℝ ∧ (𝑢 ∈
(topGen‘ran (,)) ∧ 𝑣 ∈ (topGen‘ran (,)))) ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) ∧ 𝑏 ≤ 𝑐) → 𝐴 ⊆ ℝ) |
18 | | simplrl 800 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ⊆ ℝ ∧ (𝑢 ∈ (topGen‘ran (,))
∧ 𝑣 ∈
(topGen‘ran (,)))) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) → 𝑢 ∈ (topGen‘ran
(,))) |
19 | 18 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ⊆
ℝ ∧ (𝑢 ∈
(topGen‘ran (,)) ∧ 𝑣 ∈ (topGen‘ran (,)))) ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) ∧ 𝑏 ≤ 𝑐) → 𝑢 ∈ (topGen‘ran
(,))) |
20 | | simplrr 801 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ⊆ ℝ ∧ (𝑢 ∈ (topGen‘ran (,))
∧ 𝑣 ∈
(topGen‘ran (,)))) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) → 𝑣 ∈ (topGen‘ran
(,))) |
21 | 20 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ⊆
ℝ ∧ (𝑢 ∈
(topGen‘ran (,)) ∧ 𝑣 ∈ (topGen‘ran (,)))) ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) ∧ 𝑏 ≤ 𝑐) → 𝑣 ∈ (topGen‘ran
(,))) |
22 | | simpllr 799 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ⊆
ℝ ∧ (𝑢 ∈
(topGen‘ran (,)) ∧ 𝑣 ∈ (topGen‘ran (,)))) ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) ∧ 𝑏 ≤ 𝑐) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) |
23 | 10 | adantr 481 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ⊆
ℝ ∧ (𝑢 ∈
(topGen‘ran (,)) ∧ 𝑣 ∈ (topGen‘ran (,)))) ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) ∧ 𝑏 ≤ 𝑐) → 𝑏 ∈ (𝑢 ∩ 𝐴)) |
24 | 14 | adantr 481 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ⊆
ℝ ∧ (𝑢 ∈
(topGen‘ran (,)) ∧ 𝑣 ∈ (topGen‘ran (,)))) ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) ∧ 𝑏 ≤ 𝑐) → 𝑐 ∈ (𝑣 ∩ 𝐴)) |
25 | | simplrr 801 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ⊆
ℝ ∧ (𝑢 ∈
(topGen‘ran (,)) ∧ 𝑣 ∈ (topGen‘ran (,)))) ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) ∧ 𝑏 ≤ 𝑐) → (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴)) |
26 | | simpr 477 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ⊆
ℝ ∧ (𝑢 ∈
(topGen‘ran (,)) ∧ 𝑣 ∈ (topGen‘ran (,)))) ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) ∧ 𝑏 ≤ 𝑐) → 𝑏 ≤ 𝑐) |
27 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
sup((𝑢 ∩ (𝑏[,]𝑐)), ℝ, < ) = sup((𝑢 ∩ (𝑏[,]𝑐)), ℝ, < ) |
28 | 17, 19, 21, 22, 23, 24, 25, 26, 27 | reconnlem2 22630 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ⊆
ℝ ∧ (𝑢 ∈
(topGen‘ran (,)) ∧ 𝑣 ∈ (topGen‘ran (,)))) ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) ∧ 𝑏 ≤ 𝑐) → ¬ 𝐴 ⊆ (𝑢 ∪ 𝑣)) |
29 | 8 | adantr 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ⊆
ℝ ∧ (𝑢 ∈
(topGen‘ran (,)) ∧ 𝑣 ∈ (topGen‘ran (,)))) ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) ∧ 𝑐 ≤ 𝑏) → 𝐴 ⊆ ℝ) |
30 | 20 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ⊆
ℝ ∧ (𝑢 ∈
(topGen‘ran (,)) ∧ 𝑣 ∈ (topGen‘ran (,)))) ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) ∧ 𝑐 ≤ 𝑏) → 𝑣 ∈ (topGen‘ran
(,))) |
31 | 18 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ⊆
ℝ ∧ (𝑢 ∈
(topGen‘ran (,)) ∧ 𝑣 ∈ (topGen‘ran (,)))) ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) ∧ 𝑐 ≤ 𝑏) → 𝑢 ∈ (topGen‘ran
(,))) |
32 | | simpllr 799 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ⊆
ℝ ∧ (𝑢 ∈
(topGen‘ran (,)) ∧ 𝑣 ∈ (topGen‘ran (,)))) ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) ∧ 𝑐 ≤ 𝑏) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) |
33 | 14 | adantr 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ⊆
ℝ ∧ (𝑢 ∈
(topGen‘ran (,)) ∧ 𝑣 ∈ (topGen‘ran (,)))) ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) ∧ 𝑐 ≤ 𝑏) → 𝑐 ∈ (𝑣 ∩ 𝐴)) |
34 | 10 | adantr 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ⊆
ℝ ∧ (𝑢 ∈
(topGen‘ran (,)) ∧ 𝑣 ∈ (topGen‘ran (,)))) ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) ∧ 𝑐 ≤ 𝑏) → 𝑏 ∈ (𝑢 ∩ 𝐴)) |
35 | | incom 3805 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∩ 𝑢) = (𝑢 ∩ 𝑣) |
36 | | simplrr 801 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ⊆
ℝ ∧ (𝑢 ∈
(topGen‘ran (,)) ∧ 𝑣 ∈ (topGen‘ran (,)))) ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) ∧ 𝑐 ≤ 𝑏) → (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴)) |
37 | 35, 36 | syl5eqss 3649 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ⊆
ℝ ∧ (𝑢 ∈
(topGen‘ran (,)) ∧ 𝑣 ∈ (topGen‘ran (,)))) ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) ∧ 𝑐 ≤ 𝑏) → (𝑣 ∩ 𝑢) ⊆ (ℝ ∖ 𝐴)) |
38 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ⊆
ℝ ∧ (𝑢 ∈
(topGen‘ran (,)) ∧ 𝑣 ∈ (topGen‘ran (,)))) ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) ∧ 𝑐 ≤ 𝑏) → 𝑐 ≤ 𝑏) |
39 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
sup((𝑣 ∩ (𝑐[,]𝑏)), ℝ, < ) = sup((𝑣 ∩ (𝑐[,]𝑏)), ℝ, < ) |
40 | 29, 30, 31, 32, 33, 34, 37, 38, 39 | reconnlem2 22630 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ⊆
ℝ ∧ (𝑢 ∈
(topGen‘ran (,)) ∧ 𝑣 ∈ (topGen‘ran (,)))) ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) ∧ 𝑐 ≤ 𝑏) → ¬ 𝐴 ⊆ (𝑣 ∪ 𝑢)) |
41 | | uncom 3757 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∪ 𝑢) = (𝑢 ∪ 𝑣) |
42 | 41 | sseq2i 3630 |
. . . . . . . . . . . . 13
⊢ (𝐴 ⊆ (𝑣 ∪ 𝑢) ↔ 𝐴 ⊆ (𝑢 ∪ 𝑣)) |
43 | 40, 42 | sylnib 318 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ⊆
ℝ ∧ (𝑢 ∈
(topGen‘ran (,)) ∧ 𝑣 ∈ (topGen‘ran (,)))) ∧
∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) ∧ 𝑐 ≤ 𝑏) → ¬ 𝐴 ⊆ (𝑢 ∪ 𝑣)) |
44 | 12, 16, 28, 43 | lecasei 10143 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆ ℝ ∧ (𝑢 ∈ (topGen‘ran (,))
∧ 𝑣 ∈
(topGen‘ran (,)))) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) ∧ ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴))) → ¬ 𝐴 ⊆ (𝑢 ∪ 𝑣)) |
45 | 44 | exp32 631 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ ∧ (𝑢 ∈ (topGen‘ran (,))
∧ 𝑣 ∈
(topGen‘ran (,)))) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) → ((𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) → ((𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴) → ¬ 𝐴 ⊆ (𝑢 ∪ 𝑣)))) |
46 | 45 | exlimdvv 1862 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ ∧ (𝑢 ∈ (topGen‘ran (,))
∧ 𝑣 ∈
(topGen‘ran (,)))) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) → (∃𝑏∃𝑐(𝑏 ∈ (𝑢 ∩ 𝐴) ∧ 𝑐 ∈ (𝑣 ∩ 𝐴)) → ((𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴) → ¬ 𝐴 ⊆ (𝑢 ∪ 𝑣)))) |
47 | 7, 46 | syl5bir 233 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ (𝑢 ∈ (topGen‘ran (,))
∧ 𝑣 ∈
(topGen‘ran (,)))) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) → ((∃𝑏 𝑏 ∈ (𝑢 ∩ 𝐴) ∧ ∃𝑐 𝑐 ∈ (𝑣 ∩ 𝐴)) → ((𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴) → ¬ 𝐴 ⊆ (𝑢 ∪ 𝑣)))) |
48 | 6, 47 | syl5bi 232 |
. . . . . . 7
⊢ (((𝐴 ⊆ ℝ ∧ (𝑢 ∈ (topGen‘ran (,))
∧ 𝑣 ∈
(topGen‘ran (,)))) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) → (((𝑢 ∩ 𝐴) ≠ ∅ ∧ (𝑣 ∩ 𝐴) ≠ ∅) → ((𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴) → ¬ 𝐴 ⊆ (𝑢 ∪ 𝑣)))) |
49 | 48 | expd 452 |
. . . . . 6
⊢ (((𝐴 ⊆ ℝ ∧ (𝑢 ∈ (topGen‘ran (,))
∧ 𝑣 ∈
(topGen‘ran (,)))) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) → ((𝑢 ∩ 𝐴) ≠ ∅ → ((𝑣 ∩ 𝐴) ≠ ∅ → ((𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴) → ¬ 𝐴 ⊆ (𝑢 ∪ 𝑣))))) |
50 | 49 | 3impd 1281 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ (𝑢 ∈ (topGen‘ran (,))
∧ 𝑣 ∈
(topGen‘ran (,)))) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) → (((𝑢 ∩ 𝐴) ≠ ∅ ∧ (𝑣 ∩ 𝐴) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴)) → ¬ 𝐴 ⊆ (𝑢 ∪ 𝑣))) |
51 | 50 | ex 450 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ (𝑢 ∈ (topGen‘ran (,))
∧ 𝑣 ∈
(topGen‘ran (,)))) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴 → (((𝑢 ∩ 𝐴) ≠ ∅ ∧ (𝑣 ∩ 𝐴) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴)) → ¬ 𝐴 ⊆ (𝑢 ∪ 𝑣)))) |
52 | 51 | ralrimdvva 2974 |
. . 3
⊢ (𝐴 ⊆ ℝ →
(∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴 → ∀𝑢 ∈ (topGen‘ran (,))∀𝑣 ∈ (topGen‘ran
(,))(((𝑢 ∩ 𝐴) ≠ ∅ ∧ (𝑣 ∩ 𝐴) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴)) → ¬ 𝐴 ⊆ (𝑢 ∪ 𝑣)))) |
53 | | retopon 22567 |
. . . 4
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
54 | | connsub 21224 |
. . . 4
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ 𝐴 ⊆ ℝ) →
(((topGen‘ran (,)) ↾t 𝐴) ∈ Conn ↔ ∀𝑢 ∈ (topGen‘ran
(,))∀𝑣 ∈
(topGen‘ran (,))(((𝑢
∩ 𝐴) ≠ ∅ ∧
(𝑣 ∩ 𝐴) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴)) → ¬ 𝐴 ⊆ (𝑢 ∪ 𝑣)))) |
55 | 53, 54 | mpan 706 |
. . 3
⊢ (𝐴 ⊆ ℝ →
(((topGen‘ran (,)) ↾t 𝐴) ∈ Conn ↔ ∀𝑢 ∈ (topGen‘ran
(,))∀𝑣 ∈
(topGen‘ran (,))(((𝑢
∩ 𝐴) ≠ ∅ ∧
(𝑣 ∩ 𝐴) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (ℝ ∖ 𝐴)) → ¬ 𝐴 ⊆ (𝑢 ∪ 𝑣)))) |
56 | 52, 55 | sylibrd 249 |
. 2
⊢ (𝐴 ⊆ ℝ →
(∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴 → ((topGen‘ran (,))
↾t 𝐴)
∈ Conn)) |
57 | 3, 56 | impbid 202 |
1
⊢ (𝐴 ⊆ ℝ →
(((topGen‘ran (,)) ↾t 𝐴) ∈ Conn ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴)) |