Step |
Hyp |
Ref |
Expression |
1 |
|
nconnsubb.2 |
⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
2 |
|
nconnsubb.3 |
⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 ) |
3 |
|
nconnsubb.4 |
⊢ ( 𝜑 → 𝑈 ∈ 𝐽 ) |
4 |
|
nconnsubb.5 |
⊢ ( 𝜑 → 𝑉 ∈ 𝐽 ) |
5 |
|
nconnsubb.6 |
⊢ ( 𝜑 → ( 𝑈 ∩ 𝐴 ) ≠ ∅ ) |
6 |
|
nconnsubb.7 |
⊢ ( 𝜑 → ( 𝑉 ∩ 𝐴 ) ≠ ∅ ) |
7 |
|
nconnsubb.8 |
⊢ ( 𝜑 → ( ( 𝑈 ∩ 𝑉 ) ∩ 𝐴 ) = ∅ ) |
8 |
|
nconnsubb.9 |
⊢ ( 𝜑 → 𝐴 ⊆ ( 𝑈 ∪ 𝑉 ) ) |
9 |
|
connsuba |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) → ( ( 𝑥 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) ) ) |
10 |
1 2 9
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) → ( ( 𝑥 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) ) ) |
11 |
5 6 7
|
3jca |
⊢ ( 𝜑 → ( ( 𝑈 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑉 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑈 ∩ 𝑉 ) ∩ 𝐴 ) = ∅ ) ) |
12 |
|
ineq1 |
⊢ ( 𝑥 = 𝑈 → ( 𝑥 ∩ 𝐴 ) = ( 𝑈 ∩ 𝐴 ) ) |
13 |
12
|
neeq1d |
⊢ ( 𝑥 = 𝑈 → ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ ↔ ( 𝑈 ∩ 𝐴 ) ≠ ∅ ) ) |
14 |
|
ineq1 |
⊢ ( 𝑥 = 𝑈 → ( 𝑥 ∩ 𝑦 ) = ( 𝑈 ∩ 𝑦 ) ) |
15 |
14
|
ineq1d |
⊢ ( 𝑥 = 𝑈 → ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ( ( 𝑈 ∩ 𝑦 ) ∩ 𝐴 ) ) |
16 |
15
|
eqeq1d |
⊢ ( 𝑥 = 𝑈 → ( ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ↔ ( ( 𝑈 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) ) |
17 |
13 16
|
3anbi13d |
⊢ ( 𝑥 = 𝑈 → ( ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) ↔ ( ( 𝑈 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑈 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) ) ) |
18 |
|
uneq1 |
⊢ ( 𝑥 = 𝑈 → ( 𝑥 ∪ 𝑦 ) = ( 𝑈 ∪ 𝑦 ) ) |
19 |
18
|
ineq1d |
⊢ ( 𝑥 = 𝑈 → ( ( 𝑥 ∪ 𝑦 ) ∩ 𝐴 ) = ( ( 𝑈 ∪ 𝑦 ) ∩ 𝐴 ) ) |
20 |
19
|
neeq1d |
⊢ ( 𝑥 = 𝑈 → ( ( ( 𝑥 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ↔ ( ( 𝑈 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) ) |
21 |
17 20
|
imbi12d |
⊢ ( 𝑥 = 𝑈 → ( ( ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) → ( ( 𝑥 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) ↔ ( ( ( 𝑈 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑈 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) → ( ( 𝑈 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) ) ) |
22 |
|
ineq1 |
⊢ ( 𝑦 = 𝑉 → ( 𝑦 ∩ 𝐴 ) = ( 𝑉 ∩ 𝐴 ) ) |
23 |
22
|
neeq1d |
⊢ ( 𝑦 = 𝑉 → ( ( 𝑦 ∩ 𝐴 ) ≠ ∅ ↔ ( 𝑉 ∩ 𝐴 ) ≠ ∅ ) ) |
24 |
|
ineq2 |
⊢ ( 𝑦 = 𝑉 → ( 𝑈 ∩ 𝑦 ) = ( 𝑈 ∩ 𝑉 ) ) |
25 |
24
|
ineq1d |
⊢ ( 𝑦 = 𝑉 → ( ( 𝑈 ∩ 𝑦 ) ∩ 𝐴 ) = ( ( 𝑈 ∩ 𝑉 ) ∩ 𝐴 ) ) |
26 |
25
|
eqeq1d |
⊢ ( 𝑦 = 𝑉 → ( ( ( 𝑈 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ↔ ( ( 𝑈 ∩ 𝑉 ) ∩ 𝐴 ) = ∅ ) ) |
27 |
23 26
|
3anbi23d |
⊢ ( 𝑦 = 𝑉 → ( ( ( 𝑈 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑈 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) ↔ ( ( 𝑈 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑉 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑈 ∩ 𝑉 ) ∩ 𝐴 ) = ∅ ) ) ) |
28 |
|
sseqin2 |
⊢ ( 𝐴 ⊆ ( 𝑈 ∪ 𝑦 ) ↔ ( ( 𝑈 ∪ 𝑦 ) ∩ 𝐴 ) = 𝐴 ) |
29 |
28
|
necon3bbii |
⊢ ( ¬ 𝐴 ⊆ ( 𝑈 ∪ 𝑦 ) ↔ ( ( 𝑈 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) |
30 |
|
uneq2 |
⊢ ( 𝑦 = 𝑉 → ( 𝑈 ∪ 𝑦 ) = ( 𝑈 ∪ 𝑉 ) ) |
31 |
30
|
sseq2d |
⊢ ( 𝑦 = 𝑉 → ( 𝐴 ⊆ ( 𝑈 ∪ 𝑦 ) ↔ 𝐴 ⊆ ( 𝑈 ∪ 𝑉 ) ) ) |
32 |
31
|
notbid |
⊢ ( 𝑦 = 𝑉 → ( ¬ 𝐴 ⊆ ( 𝑈 ∪ 𝑦 ) ↔ ¬ 𝐴 ⊆ ( 𝑈 ∪ 𝑉 ) ) ) |
33 |
29 32
|
bitr3id |
⊢ ( 𝑦 = 𝑉 → ( ( ( 𝑈 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ↔ ¬ 𝐴 ⊆ ( 𝑈 ∪ 𝑉 ) ) ) |
34 |
27 33
|
imbi12d |
⊢ ( 𝑦 = 𝑉 → ( ( ( ( 𝑈 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑈 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) → ( ( 𝑈 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) ↔ ( ( ( 𝑈 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑉 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑈 ∩ 𝑉 ) ∩ 𝐴 ) = ∅ ) → ¬ 𝐴 ⊆ ( 𝑈 ∪ 𝑉 ) ) ) ) |
35 |
21 34
|
rspc2v |
⊢ ( ( 𝑈 ∈ 𝐽 ∧ 𝑉 ∈ 𝐽 ) → ( ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) → ( ( 𝑥 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) → ( ( ( 𝑈 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑉 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑈 ∩ 𝑉 ) ∩ 𝐴 ) = ∅ ) → ¬ 𝐴 ⊆ ( 𝑈 ∪ 𝑉 ) ) ) ) |
36 |
3 4 35
|
syl2anc |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) → ( ( 𝑥 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) → ( ( ( 𝑈 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑉 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑈 ∩ 𝑉 ) ∩ 𝐴 ) = ∅ ) → ¬ 𝐴 ⊆ ( 𝑈 ∪ 𝑉 ) ) ) ) |
37 |
11 36
|
mpid |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ∧ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ) → ( ( 𝑥 ∪ 𝑦 ) ∩ 𝐴 ) ≠ 𝐴 ) → ¬ 𝐴 ⊆ ( 𝑈 ∪ 𝑉 ) ) ) |
38 |
10 37
|
sylbid |
⊢ ( 𝜑 → ( ( 𝐽 ↾t 𝐴 ) ∈ Conn → ¬ 𝐴 ⊆ ( 𝑈 ∪ 𝑉 ) ) ) |
39 |
8 38
|
mt2d |
⊢ ( 𝜑 → ¬ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) |