Step |
Hyp |
Ref |
Expression |
1 |
|
simp1 |
⊢ ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆 ∈ 𝐹 ) → 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) |
2 |
|
fclstop |
⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → 𝐽 ∈ Top ) |
3 |
1 2
|
syl |
⊢ ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆 ∈ 𝐹 ) → 𝐽 ∈ Top ) |
4 |
|
simp2 |
⊢ ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆 ∈ 𝐹 ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) |
5 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
6 |
5
|
neii1 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝑁 ⊆ ∪ 𝐽 ) |
7 |
3 4 6
|
syl2anc |
⊢ ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆 ∈ 𝐹 ) → 𝑁 ⊆ ∪ 𝐽 ) |
8 |
5
|
ntrss2 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ⊆ ∪ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ⊆ 𝑁 ) |
9 |
3 7 8
|
syl2anc |
⊢ ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆 ∈ 𝐹 ) → ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ⊆ 𝑁 ) |
10 |
9
|
ssrind |
⊢ ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆 ∈ 𝐹 ) → ( ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ∩ 𝑆 ) ⊆ ( 𝑁 ∩ 𝑆 ) ) |
11 |
5
|
ntropn |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ⊆ ∪ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ∈ 𝐽 ) |
12 |
3 7 11
|
syl2anc |
⊢ ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆 ∈ 𝐹 ) → ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ∈ 𝐽 ) |
13 |
5
|
fclselbas |
⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → 𝐴 ∈ ∪ 𝐽 ) |
14 |
1 13
|
syl |
⊢ ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆 ∈ 𝐹 ) → 𝐴 ∈ ∪ 𝐽 ) |
15 |
14
|
snssd |
⊢ ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆 ∈ 𝐹 ) → { 𝐴 } ⊆ ∪ 𝐽 ) |
16 |
5
|
neiint |
⊢ ( ( 𝐽 ∈ Top ∧ { 𝐴 } ⊆ ∪ 𝐽 ∧ 𝑁 ⊆ ∪ 𝐽 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ↔ { 𝐴 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) ) |
17 |
3 15 7 16
|
syl3anc |
⊢ ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆 ∈ 𝐹 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ↔ { 𝐴 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) ) |
18 |
4 17
|
mpbid |
⊢ ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆 ∈ 𝐹 ) → { 𝐴 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) |
19 |
|
snssg |
⊢ ( 𝐴 ∈ ∪ 𝐽 → ( 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ↔ { 𝐴 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) ) |
20 |
14 19
|
syl |
⊢ ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆 ∈ 𝐹 ) → ( 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ↔ { 𝐴 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) ) |
21 |
18 20
|
mpbird |
⊢ ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆 ∈ 𝐹 ) → 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) |
22 |
|
simp3 |
⊢ ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆 ∈ 𝐹 ) → 𝑆 ∈ 𝐹 ) |
23 |
|
fclsopni |
⊢ ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ ( ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ∈ 𝐽 ∧ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ∧ 𝑆 ∈ 𝐹 ) ) → ( ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ∩ 𝑆 ) ≠ ∅ ) |
24 |
1 12 21 22 23
|
syl13anc |
⊢ ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆 ∈ 𝐹 ) → ( ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ∩ 𝑆 ) ≠ ∅ ) |
25 |
|
ssn0 |
⊢ ( ( ( ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ∩ 𝑆 ) ⊆ ( 𝑁 ∩ 𝑆 ) ∧ ( ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ∩ 𝑆 ) ≠ ∅ ) → ( 𝑁 ∩ 𝑆 ) ≠ ∅ ) |
26 |
10 24 25
|
syl2anc |
⊢ ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑆 ∈ 𝐹 ) → ( 𝑁 ∩ 𝑆 ) ≠ ∅ ) |