Theorem flimclsi

Description: The convergent points of a filter are a subset of the closure of any of the filter sets. (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Stefan O'Rear, 9-Aug-2015)

	Ref	Expression
Assertion	flimclsi	⊢ ( 𝑆 ∈ 𝐹 → ( 𝐽 fLim 𝐹 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
2	1	flimfil	⊢ ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) → 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) )
3	2	ad2antlr	⊢ ( ( ( 𝑆 ∈ 𝐹 ∧ 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) )
4		flimnei	⊢ ( ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → 𝑦 ∈ 𝐹 )
5	4	adantll	⊢ ( ( ( 𝑆 ∈ 𝐹 ∧ 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → 𝑦 ∈ 𝐹 )
6		simpll	⊢ ( ( ( 𝑆 ∈ 𝐹 ∧ 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → 𝑆 ∈ 𝐹 )
7		filinn0	⊢ ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) ∧ 𝑦 ∈ 𝐹 ∧ 𝑆 ∈ 𝐹 ) → ( 𝑦 ∩ 𝑆 ) ≠ ∅ )
8	3 5 6 7	syl3anc	⊢ ( ( ( 𝑆 ∈ 𝐹 ∧ 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → ( 𝑦 ∩ 𝑆 ) ≠ ∅ )
9	8	ralrimiva	⊢ ( ( 𝑆 ∈ 𝐹 ∧ 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) → ∀ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑦 ∩ 𝑆 ) ≠ ∅ )
10		flimtop	⊢ ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) → 𝐽 ∈ Top )
11	10	adantl	⊢ ( ( 𝑆 ∈ 𝐹 ∧ 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) → 𝐽 ∈ Top )
12		filelss	⊢ ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) ∧ 𝑆 ∈ 𝐹 ) → 𝑆 ⊆ ∪ 𝐽 )
13	12	ancoms	⊢ ( ( 𝑆 ∈ 𝐹 ∧ 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) ) → 𝑆 ⊆ ∪ 𝐽 )
14	2 13	sylan2	⊢ ( ( 𝑆 ∈ 𝐹 ∧ 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) → 𝑆 ⊆ ∪ 𝐽 )
15	1	flimelbas	⊢ ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) → 𝑥 ∈ ∪ 𝐽 )
16	15	adantl	⊢ ( ( 𝑆 ∈ 𝐹 ∧ 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) → 𝑥 ∈ ∪ 𝐽 )
17	1	neindisj2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ∧ 𝑥 ∈ ∪ 𝐽 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) )
18	11 14 16 17	syl3anc	⊢ ( ( 𝑆 ∈ 𝐹 ∧ 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝑦 ∩ 𝑆 ) ≠ ∅ ) )
19	9 18	mpbird	⊢ ( ( 𝑆 ∈ 𝐹 ∧ 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
20	19	ex	⊢ ( 𝑆 ∈ 𝐹 → ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
21	20	ssrdv	⊢ ( 𝑆 ∈ 𝐹 → ( 𝐽 fLim 𝐹 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )