This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem flimcls

Description: Closure in terms of filter convergence. (Contributed by Jeff Hankins, 28-Nov-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Assertion flimcls ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝑆 ∈ 𝑓 ∧ 𝐴 ∈ ( 𝐽 fLim 𝑓 ) ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) = ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) )
2 1 flimclslem ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) ∈ ( Fil ‘ 𝑋 ) ∧ 𝑆 ∈ ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) ∧ 𝐴 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) ) ) )
3 3anass ⊢ ( ( ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) ∈ ( Fil ‘ 𝑋 ) ∧ 𝑆 ∈ ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) ∧ 𝐴 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) ) ) ↔ ( ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑆 ∈ ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) ∧ 𝐴 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) ) ) ) )
4 2 3 sylib ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑆 ∈ ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) ∧ 𝐴 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) ) ) ) )
5 eleq2 ⊢ ( 𝑓 = ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) → ( 𝑆 ∈ 𝑓 ↔ 𝑆 ∈ ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) ) )
6 oveq2 ⊢ ( 𝑓 = ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) → ( 𝐽 fLim 𝑓 ) = ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) ) )
7 6 eleq2d ⊢ ( 𝑓 = ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) → ( 𝐴 ∈ ( 𝐽 fLim 𝑓 ) ↔ 𝐴 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) ) ) )
8 5 7 anbi12d ⊢ ( 𝑓 = ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) → ( ( 𝑆 ∈ 𝑓 ∧ 𝐴 ∈ ( 𝐽 fLim 𝑓 ) ) ↔ ( 𝑆 ∈ ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) ∧ 𝐴 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) ) ) ) )
9 8 rspcev ⊢ ( ( ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑆 ∈ ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) ∧ 𝐴 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∪ { 𝑆 } ) ) ) ) ) ) → ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝑆 ∈ 𝑓 ∧ 𝐴 ∈ ( 𝐽 fLim 𝑓 ) ) )
10 4 9 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝑆 ∈ 𝑓 ∧ 𝐴 ∈ ( 𝐽 fLim 𝑓 ) ) )
11 10 3expia ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) → ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝑆 ∈ 𝑓 ∧ 𝐴 ∈ ( 𝐽 fLim 𝑓 ) ) ) )
12 flimclsi ⊢ ( 𝑆 ∈ 𝑓 → ( 𝐽 fLim 𝑓 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
13 12 sselda ⊢ ( ( 𝑆 ∈ 𝑓 ∧ 𝐴 ∈ ( 𝐽 fLim 𝑓 ) ) → 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
14 13 rexlimivw ⊢ ( ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝑆 ∈ 𝑓 ∧ 𝐴 ∈ ( 𝐽 fLim 𝑓 ) ) → 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
15 11 14 impbid1 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝑆 ∈ 𝑓 ∧ 𝐴 ∈ ( 𝐽 fLim 𝑓 ) ) ) )