Proof of Theorem fclsneii
Step | Hyp | Ref
| Expression |
1 | | simp1 1061 |
. . . . 5
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → 𝐴 ∈ (𝐽 fClus 𝐹)) |
2 | | fclstop 21815 |
. . . . 5
⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐽 ∈ Top) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → 𝐽 ∈ Top) |
4 | | simp2 1062 |
. . . . 5
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → 𝑁 ∈ ((nei‘𝐽)‘{𝐴})) |
5 | | eqid 2622 |
. . . . . 6
⊢ ∪ 𝐽 =
∪ 𝐽 |
6 | 5 | neii1 20910 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴})) → 𝑁 ⊆ ∪ 𝐽) |
7 | 3, 4, 6 | syl2anc 693 |
. . . 4
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → 𝑁 ⊆ ∪ 𝐽) |
8 | 5 | ntrss2 20861 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑁 ⊆ ∪ 𝐽)
→ ((int‘𝐽)‘𝑁) ⊆ 𝑁) |
9 | 3, 7, 8 | syl2anc 693 |
. . 3
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → ((int‘𝐽)‘𝑁) ⊆ 𝑁) |
10 | | ssrin 3838 |
. . 3
⊢
(((int‘𝐽)‘𝑁) ⊆ 𝑁 → (((int‘𝐽)‘𝑁) ∩ 𝑆) ⊆ (𝑁 ∩ 𝑆)) |
11 | 9, 10 | syl 17 |
. 2
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → (((int‘𝐽)‘𝑁) ∩ 𝑆) ⊆ (𝑁 ∩ 𝑆)) |
12 | 5 | ntropn 20853 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑁 ⊆ ∪ 𝐽)
→ ((int‘𝐽)‘𝑁) ∈ 𝐽) |
13 | 3, 7, 12 | syl2anc 693 |
. . 3
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → ((int‘𝐽)‘𝑁) ∈ 𝐽) |
14 | 5 | fclselbas 21820 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐴 ∈ ∪ 𝐽) |
15 | 1, 14 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → 𝐴 ∈ ∪ 𝐽) |
16 | 15 | snssd 4340 |
. . . . . 6
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → {𝐴} ⊆ ∪ 𝐽) |
17 | 5 | neiint 20908 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ {𝐴} ⊆ ∪ 𝐽
∧ 𝑁 ⊆ ∪ 𝐽)
→ (𝑁 ∈
((nei‘𝐽)‘{𝐴}) ↔ {𝐴} ⊆ ((int‘𝐽)‘𝑁))) |
18 | 3, 16, 7, 17 | syl3anc 1326 |
. . . . 5
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → (𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ↔ {𝐴} ⊆ ((int‘𝐽)‘𝑁))) |
19 | 4, 18 | mpbid 222 |
. . . 4
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → {𝐴} ⊆ ((int‘𝐽)‘𝑁)) |
20 | | snssg 4327 |
. . . . 5
⊢ (𝐴 ∈ ∪ 𝐽
→ (𝐴 ∈
((int‘𝐽)‘𝑁) ↔ {𝐴} ⊆ ((int‘𝐽)‘𝑁))) |
21 | 15, 20 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → (𝐴 ∈ ((int‘𝐽)‘𝑁) ↔ {𝐴} ⊆ ((int‘𝐽)‘𝑁))) |
22 | 19, 21 | mpbird 247 |
. . 3
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → 𝐴 ∈ ((int‘𝐽)‘𝑁)) |
23 | | simp3 1063 |
. . 3
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → 𝑆 ∈ 𝐹) |
24 | | fclsopni 21819 |
. . 3
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ (((int‘𝐽)‘𝑁) ∈ 𝐽 ∧ 𝐴 ∈ ((int‘𝐽)‘𝑁) ∧ 𝑆 ∈ 𝐹)) → (((int‘𝐽)‘𝑁) ∩ 𝑆) ≠ ∅) |
25 | 1, 13, 22, 23, 24 | syl13anc 1328 |
. 2
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → (((int‘𝐽)‘𝑁) ∩ 𝑆) ≠ ∅) |
26 | | ssn0 3976 |
. 2
⊢
(((((int‘𝐽)‘𝑁) ∩ 𝑆) ⊆ (𝑁 ∩ 𝑆) ∧ (((int‘𝐽)‘𝑁) ∩ 𝑆) ≠ ∅) → (𝑁 ∩ 𝑆) ≠ ∅) |
27 | 11, 25, 26 | syl2anc 693 |
1
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → (𝑁 ∩ 𝑆) ≠ ∅) |