Proof of Theorem fclsneii
Step | Hyp | Ref
| Expression |
1 | | simp1 1138 |
. . . . 5
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → 𝐴 ∈ (𝐽 fClus 𝐹)) |
2 | | fclstop 22908 |
. . . . 5
⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐽 ∈ Top) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → 𝐽 ∈ Top) |
4 | | simp2 1139 |
. . . . 5
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → 𝑁 ∈ ((nei‘𝐽)‘{𝐴})) |
5 | | eqid 2737 |
. . . . . 6
⊢ ∪ 𝐽 =
∪ 𝐽 |
6 | 5 | neii1 22003 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴})) → 𝑁 ⊆ ∪ 𝐽) |
7 | 3, 4, 6 | syl2anc 587 |
. . . 4
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → 𝑁 ⊆ ∪ 𝐽) |
8 | 5 | ntrss2 21954 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑁 ⊆ ∪ 𝐽)
→ ((int‘𝐽)‘𝑁) ⊆ 𝑁) |
9 | 3, 7, 8 | syl2anc 587 |
. . 3
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → ((int‘𝐽)‘𝑁) ⊆ 𝑁) |
10 | 9 | ssrind 4150 |
. 2
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → (((int‘𝐽)‘𝑁) ∩ 𝑆) ⊆ (𝑁 ∩ 𝑆)) |
11 | 5 | ntropn 21946 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑁 ⊆ ∪ 𝐽)
→ ((int‘𝐽)‘𝑁) ∈ 𝐽) |
12 | 3, 7, 11 | syl2anc 587 |
. . 3
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → ((int‘𝐽)‘𝑁) ∈ 𝐽) |
13 | 5 | fclselbas 22913 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐴 ∈ ∪ 𝐽) |
14 | 1, 13 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → 𝐴 ∈ ∪ 𝐽) |
15 | 14 | snssd 4722 |
. . . . . 6
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → {𝐴} ⊆ ∪ 𝐽) |
16 | 5 | neiint 22001 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ {𝐴} ⊆ ∪ 𝐽
∧ 𝑁 ⊆ ∪ 𝐽)
→ (𝑁 ∈
((nei‘𝐽)‘{𝐴}) ↔ {𝐴} ⊆ ((int‘𝐽)‘𝑁))) |
17 | 3, 15, 7, 16 | syl3anc 1373 |
. . . . 5
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → (𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ↔ {𝐴} ⊆ ((int‘𝐽)‘𝑁))) |
18 | 4, 17 | mpbid 235 |
. . . 4
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → {𝐴} ⊆ ((int‘𝐽)‘𝑁)) |
19 | | snssg 4698 |
. . . . 5
⊢ (𝐴 ∈ ∪ 𝐽
→ (𝐴 ∈
((int‘𝐽)‘𝑁) ↔ {𝐴} ⊆ ((int‘𝐽)‘𝑁))) |
20 | 14, 19 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → (𝐴 ∈ ((int‘𝐽)‘𝑁) ↔ {𝐴} ⊆ ((int‘𝐽)‘𝑁))) |
21 | 18, 20 | mpbird 260 |
. . 3
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → 𝐴 ∈ ((int‘𝐽)‘𝑁)) |
22 | | simp3 1140 |
. . 3
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → 𝑆 ∈ 𝐹) |
23 | | fclsopni 22912 |
. . 3
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ (((int‘𝐽)‘𝑁) ∈ 𝐽 ∧ 𝐴 ∈ ((int‘𝐽)‘𝑁) ∧ 𝑆 ∈ 𝐹)) → (((int‘𝐽)‘𝑁) ∩ 𝑆) ≠ ∅) |
24 | 1, 12, 21, 22, 23 | syl13anc 1374 |
. 2
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → (((int‘𝐽)‘𝑁) ∩ 𝑆) ≠ ∅) |
25 | | ssn0 4315 |
. 2
⊢
(((((int‘𝐽)‘𝑁) ∩ 𝑆) ⊆ (𝑁 ∩ 𝑆) ∧ (((int‘𝐽)‘𝑁) ∩ 𝑆) ≠ ∅) → (𝑁 ∩ 𝑆) ≠ ∅) |
26 | 10, 24, 25 | syl2anc 587 |
1
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → (𝑁 ∩ 𝑆) ≠ ∅) |