Metamath Proof Explorer

Theorem isfcls2

Description: A cluster point of a filter. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion isfcls2 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) )

Proof

Step Hyp Ref Expression
1 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
2 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
3 2 fveq2d ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( Fil ‘ 𝑋 ) = ( Fil ‘ ∪ 𝐽 ) )
4 3 eleq2d ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ↔ 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) ) )
5 4 biimpa ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) )
6 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
7 6 isfcls ⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) ∧ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) )
8 df-3an ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) ∧ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) ) ∧ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) )
9 7 8 bitri ⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) ) ∧ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) )
10 9 baib ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) )
11 1 5 10 syl2an2r ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) )