Theorem fclsbas

Description: Cluster points in terms of filter bases. (Contributed by Jeff Hankins, 13-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

	Ref	Expression
Hypothesis	fclsbas.f	⊢ 𝐹 = ( 𝑋 filGen 𝐵 )
Assertion	fclsbas	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fclsbas.f	⊢ 𝐹 = ( 𝑋 filGen 𝐵 )
2		fgcl	⊢ ( 𝐵 ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen 𝐵 ) ∈ ( Fil ‘ 𝑋 ) )
3	2	adantl	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( 𝑋 filGen 𝐵 ) ∈ ( Fil ‘ 𝑋 ) )
4	1 3	eqeltrid	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
5		fclsopn	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑡 ∈ 𝐹 ( 𝑜 ∩ 𝑡 ) ≠ ∅ ) ) ) )
6	4 5	syldan	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑡 ∈ 𝐹 ( 𝑜 ∩ 𝑡 ) ≠ ∅ ) ) ) )
7		ssfg	⊢ ( 𝐵 ∈ ( fBas ‘ 𝑋 ) → 𝐵 ⊆ ( 𝑋 filGen 𝐵 ) )
8	7	ad3antlr	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) → 𝐵 ⊆ ( 𝑋 filGen 𝐵 ) )
9	8 1	sseqtrrdi	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) → 𝐵 ⊆ 𝐹 )
10		ssralv	⊢ ( 𝐵 ⊆ 𝐹 → ( ∀ 𝑡 ∈ 𝐹 ( 𝑜 ∩ 𝑡 ) ≠ ∅ → ∀ 𝑡 ∈ 𝐵 ( 𝑜 ∩ 𝑡 ) ≠ ∅ ) )
11	9 10	syl	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) → ( ∀ 𝑡 ∈ 𝐹 ( 𝑜 ∩ 𝑡 ) ≠ ∅ → ∀ 𝑡 ∈ 𝐵 ( 𝑜 ∩ 𝑡 ) ≠ ∅ ) )
12		ineq2	⊢ ( 𝑡 = 𝑠 → ( 𝑜 ∩ 𝑡 ) = ( 𝑜 ∩ 𝑠 ) )
13	12	neeq1d	⊢ ( 𝑡 = 𝑠 → ( ( 𝑜 ∩ 𝑡 ) ≠ ∅ ↔ ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) )
14	13	cbvralvw	⊢ ( ∀ 𝑡 ∈ 𝐵 ( 𝑜 ∩ 𝑡 ) ≠ ∅ ↔ ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ )
15	11 14	syl6ib	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) → ( ∀ 𝑡 ∈ 𝐹 ( 𝑜 ∩ 𝑡 ) ≠ ∅ → ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) )
16	1	eleq2i	⊢ ( 𝑡 ∈ 𝐹 ↔ 𝑡 ∈ ( 𝑋 filGen 𝐵 ) )
17		elfg	⊢ ( 𝐵 ∈ ( fBas ‘ 𝑋 ) → ( 𝑡 ∈ ( 𝑋 filGen 𝐵 ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡 ) ) )
18	17	ad3antlr	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) → ( 𝑡 ∈ ( 𝑋 filGen 𝐵 ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡 ) ) )
19	16 18	syl5bb	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) → ( 𝑡 ∈ 𝐹 ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡 ) ) )
20	19	simplbda	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) ∧ 𝑡 ∈ 𝐹 ) → ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡 )
21		r19.29r	⊢ ( ( ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡 ∧ ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) → ∃ 𝑠 ∈ 𝐵 ( 𝑠 ⊆ 𝑡 ∧ ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) )
22		sslin	⊢ ( 𝑠 ⊆ 𝑡 → ( 𝑜 ∩ 𝑠 ) ⊆ ( 𝑜 ∩ 𝑡 ) )
23		ssn0	⊢ ( ( ( 𝑜 ∩ 𝑠 ) ⊆ ( 𝑜 ∩ 𝑡 ) ∧ ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) → ( 𝑜 ∩ 𝑡 ) ≠ ∅ )
24	22 23	sylan	⊢ ( ( 𝑠 ⊆ 𝑡 ∧ ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) → ( 𝑜 ∩ 𝑡 ) ≠ ∅ )
25	24	rexlimivw	⊢ ( ∃ 𝑠 ∈ 𝐵 ( 𝑠 ⊆ 𝑡 ∧ ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) → ( 𝑜 ∩ 𝑡 ) ≠ ∅ )
26	21 25	syl	⊢ ( ( ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡 ∧ ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) → ( 𝑜 ∩ 𝑡 ) ≠ ∅ )
27	26	ex	⊢ ( ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡 → ( ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ → ( 𝑜 ∩ 𝑡 ) ≠ ∅ ) )
28	20 27	syl	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) ∧ 𝑡 ∈ 𝐹 ) → ( ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ → ( 𝑜 ∩ 𝑡 ) ≠ ∅ ) )
29	28	ralrimdva	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) → ( ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ → ∀ 𝑡 ∈ 𝐹 ( 𝑜 ∩ 𝑡 ) ≠ ∅ ) )
30	15 29	impbid	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) → ( ∀ 𝑡 ∈ 𝐹 ( 𝑜 ∩ 𝑡 ) ≠ ∅ ↔ ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) )
31	30	anassrs	⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝐴 ∈ 𝑜 ) → ( ∀ 𝑡 ∈ 𝐹 ( 𝑜 ∩ 𝑡 ) ≠ ∅ ↔ ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) )
32	31	pm5.74da	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( ( 𝐴 ∈ 𝑜 → ∀ 𝑡 ∈ 𝐹 ( 𝑜 ∩ 𝑡 ) ≠ ∅ ) ↔ ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) )
33	32	ralbidva	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑡 ∈ 𝐹 ( 𝑜 ∩ 𝑡 ) ≠ ∅ ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) )
34	33	pm5.32da	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑡 ∈ 𝐹 ( 𝑜 ∩ 𝑡 ) ≠ ∅ ) ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) ) )
35	6 34	bitrd	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) ) )