Proof of Theorem fclsneii
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp1 1136 | . . . . 5
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → 𝐴 ∈ (𝐽 fClus 𝐹)) | 
| 2 |  | fclstop 24020 | . . . . 5
⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐽 ∈ Top) | 
| 3 | 1, 2 | syl 17 | . . . 4
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → 𝐽 ∈ Top) | 
| 4 |  | simp2 1137 | . . . . 5
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → 𝑁 ∈ ((nei‘𝐽)‘{𝐴})) | 
| 5 |  | eqid 2736 | . . . . . 6
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 6 | 5 | neii1 23115 | . . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴})) → 𝑁 ⊆ ∪ 𝐽) | 
| 7 | 3, 4, 6 | syl2anc 584 | . . . 4
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → 𝑁 ⊆ ∪ 𝐽) | 
| 8 | 5 | ntrss2 23066 | . . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑁 ⊆ ∪ 𝐽)
→ ((int‘𝐽)‘𝑁) ⊆ 𝑁) | 
| 9 | 3, 7, 8 | syl2anc 584 | . . 3
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → ((int‘𝐽)‘𝑁) ⊆ 𝑁) | 
| 10 | 9 | ssrind 4243 | . 2
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → (((int‘𝐽)‘𝑁) ∩ 𝑆) ⊆ (𝑁 ∩ 𝑆)) | 
| 11 | 5 | ntropn 23058 | . . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑁 ⊆ ∪ 𝐽)
→ ((int‘𝐽)‘𝑁) ∈ 𝐽) | 
| 12 | 3, 7, 11 | syl2anc 584 | . . 3
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → ((int‘𝐽)‘𝑁) ∈ 𝐽) | 
| 13 | 5 | fclselbas 24025 | . . . . . . . 8
⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐴 ∈ ∪ 𝐽) | 
| 14 | 1, 13 | syl 17 | . . . . . . 7
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → 𝐴 ∈ ∪ 𝐽) | 
| 15 | 14 | snssd 4808 | . . . . . 6
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → {𝐴} ⊆ ∪ 𝐽) | 
| 16 | 5 | neiint 23113 | . . . . . 6
⊢ ((𝐽 ∈ Top ∧ {𝐴} ⊆ ∪ 𝐽
∧ 𝑁 ⊆ ∪ 𝐽)
→ (𝑁 ∈
((nei‘𝐽)‘{𝐴}) ↔ {𝐴} ⊆ ((int‘𝐽)‘𝑁))) | 
| 17 | 3, 15, 7, 16 | syl3anc 1372 | . . . . 5
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → (𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ↔ {𝐴} ⊆ ((int‘𝐽)‘𝑁))) | 
| 18 | 4, 17 | mpbid 232 | . . . 4
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → {𝐴} ⊆ ((int‘𝐽)‘𝑁)) | 
| 19 |  | snssg 4782 | . . . . 5
⊢ (𝐴 ∈ ∪ 𝐽
→ (𝐴 ∈
((int‘𝐽)‘𝑁) ↔ {𝐴} ⊆ ((int‘𝐽)‘𝑁))) | 
| 20 | 14, 19 | syl 17 | . . . 4
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → (𝐴 ∈ ((int‘𝐽)‘𝑁) ↔ {𝐴} ⊆ ((int‘𝐽)‘𝑁))) | 
| 21 | 18, 20 | mpbird 257 | . . 3
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → 𝐴 ∈ ((int‘𝐽)‘𝑁)) | 
| 22 |  | simp3 1138 | . . 3
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → 𝑆 ∈ 𝐹) | 
| 23 |  | fclsopni 24024 | . . 3
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ (((int‘𝐽)‘𝑁) ∈ 𝐽 ∧ 𝐴 ∈ ((int‘𝐽)‘𝑁) ∧ 𝑆 ∈ 𝐹)) → (((int‘𝐽)‘𝑁) ∩ 𝑆) ≠ ∅) | 
| 24 | 1, 12, 21, 22, 23 | syl13anc 1373 | . 2
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → (((int‘𝐽)‘𝑁) ∩ 𝑆) ≠ ∅) | 
| 25 |  | ssn0 4403 | . 2
⊢
(((((int‘𝐽)‘𝑁) ∩ 𝑆) ⊆ (𝑁 ∩ 𝑆) ∧ (((int‘𝐽)‘𝑁) ∩ 𝑆) ≠ ∅) → (𝑁 ∩ 𝑆) ≠ ∅) | 
| 26 | 10, 24, 25 | syl2anc 584 | 1
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → (𝑁 ∩ 𝑆) ≠ ∅) |