Metamath Proof Explorer


Theorem fclsopni

Description: An open neighborhood of a cluster point of a filter intersects any element of that filter. (Contributed by Mario Carneiro, 11-Apr-2015) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Assertion fclsopni ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ ( 𝑈𝐽𝐴𝑈𝑆𝐹 ) ) → ( 𝑈𝑆 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 eqid 𝐽 = 𝐽
2 1 fclsfil ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → 𝐹 ∈ ( Fil ‘ 𝐽 ) )
3 fclstopon ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → ( 𝐽 ∈ ( TopOn ‘ 𝐽 ) ↔ 𝐹 ∈ ( Fil ‘ 𝐽 ) ) )
4 2 3 mpbird ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → 𝐽 ∈ ( TopOn ‘ 𝐽 ) )
5 fclsopn ( ( 𝐽 ∈ ( TopOn ‘ 𝐽 ) ∧ 𝐹 ∈ ( Fil ‘ 𝐽 ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝐴 𝐽 ∧ ∀ 𝑜𝐽 ( 𝐴𝑜 → ∀ 𝑠𝐹 ( 𝑜𝑠 ) ≠ ∅ ) ) ) )
6 4 2 5 syl2anc ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝐴 𝐽 ∧ ∀ 𝑜𝐽 ( 𝐴𝑜 → ∀ 𝑠𝐹 ( 𝑜𝑠 ) ≠ ∅ ) ) ) )
7 6 ibi ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → ( 𝐴 𝐽 ∧ ∀ 𝑜𝐽 ( 𝐴𝑜 → ∀ 𝑠𝐹 ( 𝑜𝑠 ) ≠ ∅ ) ) )
8 eleq2 ( 𝑜 = 𝑈 → ( 𝐴𝑜𝐴𝑈 ) )
9 ineq1 ( 𝑜 = 𝑈 → ( 𝑜𝑠 ) = ( 𝑈𝑠 ) )
10 9 neeq1d ( 𝑜 = 𝑈 → ( ( 𝑜𝑠 ) ≠ ∅ ↔ ( 𝑈𝑠 ) ≠ ∅ ) )
11 10 ralbidv ( 𝑜 = 𝑈 → ( ∀ 𝑠𝐹 ( 𝑜𝑠 ) ≠ ∅ ↔ ∀ 𝑠𝐹 ( 𝑈𝑠 ) ≠ ∅ ) )
12 8 11 imbi12d ( 𝑜 = 𝑈 → ( ( 𝐴𝑜 → ∀ 𝑠𝐹 ( 𝑜𝑠 ) ≠ ∅ ) ↔ ( 𝐴𝑈 → ∀ 𝑠𝐹 ( 𝑈𝑠 ) ≠ ∅ ) ) )
13 12 rspccv ( ∀ 𝑜𝐽 ( 𝐴𝑜 → ∀ 𝑠𝐹 ( 𝑜𝑠 ) ≠ ∅ ) → ( 𝑈𝐽 → ( 𝐴𝑈 → ∀ 𝑠𝐹 ( 𝑈𝑠 ) ≠ ∅ ) ) )
14 7 13 simpl2im ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → ( 𝑈𝐽 → ( 𝐴𝑈 → ∀ 𝑠𝐹 ( 𝑈𝑠 ) ≠ ∅ ) ) )
15 ineq2 ( 𝑠 = 𝑆 → ( 𝑈𝑠 ) = ( 𝑈𝑆 ) )
16 15 neeq1d ( 𝑠 = 𝑆 → ( ( 𝑈𝑠 ) ≠ ∅ ↔ ( 𝑈𝑆 ) ≠ ∅ ) )
17 16 rspccv ( ∀ 𝑠𝐹 ( 𝑈𝑠 ) ≠ ∅ → ( 𝑆𝐹 → ( 𝑈𝑆 ) ≠ ∅ ) )
18 14 17 syl8 ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → ( 𝑈𝐽 → ( 𝐴𝑈 → ( 𝑆𝐹 → ( 𝑈𝑆 ) ≠ ∅ ) ) ) )
19 18 3imp2 ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ ( 𝑈𝐽𝐴𝑈𝑆𝐹 ) ) → ( 𝑈𝑆 ) ≠ ∅ )