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 𝑓 ) ) ) )