Metamath Proof Explorer

Theorem fclsopn

Description: Write the cluster point condition in terms of open sets. (Contributed by Jeff Hankins, 10-Nov-2009) (Revised by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion fclsopn ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐹 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) ) )

Proof

Step Hyp Ref Expression
1 isfcls2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) )
2 filn0 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ≠ ∅ )
3 2 adantl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → 𝐹 ≠ ∅ )
4 r19.2z ⊢ ( ( 𝐹 ≠ ∅ ∧ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) → ∃ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) )
5 4 ex ⊢ ( 𝐹 ≠ ∅ → ( ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) → ∃ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) )
6 3 5 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) → ∃ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) )
7 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
8 7 ad2antrr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ 𝐹 ) → 𝐽 ∈ Top )
9 filelss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑠 ∈ 𝐹 ) → 𝑠 ⊆ 𝑋 )
10 9 adantll ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ 𝐹 ) → 𝑠 ⊆ 𝑋 )
11 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
12 11 ad2antrr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ 𝐹 ) → 𝑋 = ∪ 𝐽 )
13 10 12 sseqtrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ 𝐹 ) → 𝑠 ⊆ ∪ 𝐽 )
14 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
15 14 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑠 ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ⊆ ∪ 𝐽 )
16 8 13 15 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ 𝐹 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ⊆ ∪ 𝐽 )
17 16 12 sseqtrrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ 𝐹 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ⊆ 𝑋 )
18 17 sseld ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑠 ∈ 𝐹 ) → ( 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) → 𝐴 ∈ 𝑋 ) )
19 18 rexlimdva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( ∃ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) → 𝐴 ∈ 𝑋 ) )
20 6 19 syld ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) → 𝐴 ∈ 𝑋 ) )
21 20 pm4.71rd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) ) )
22 7 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑠 ∈ 𝐹 ) → 𝐽 ∈ Top )
23 13 adantlr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑠 ∈ 𝐹 ) → 𝑠 ⊆ ∪ 𝐽 )
24 simplr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑠 ∈ 𝐹 ) → 𝐴 ∈ 𝑋 )
25 11 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑠 ∈ 𝐹 ) → 𝑋 = ∪ 𝐽 )
26 24 25 eleqtrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑠 ∈ 𝐹 ) → 𝐴 ∈ ∪ 𝐽 )
27 14 elcls ⊢ ( ( 𝐽 ∈ Top ∧ 𝑠 ⊆ ∪ 𝐽 ∧ 𝐴 ∈ ∪ 𝐽 ) → ( 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) )
28 22 23 26 27 syl3anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑠 ∈ 𝐹 ) → ( 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) )
29 28 ralbidva ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ↔ ∀ 𝑠 ∈ 𝐹 ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) )
30 ralcom ⊢ ( ∀ 𝑠 ∈ 𝐹 ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ↔ ∀ 𝑜 ∈ 𝐽 ∀ 𝑠 ∈ 𝐹 ( 𝐴 ∈ 𝑜 → ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) )
31 r19.21v ⊢ ( ∀ 𝑠 ∈ 𝐹 ( 𝐴 ∈ 𝑜 → ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ↔ ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐹 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) )
32 31 ralbii ⊢ ( ∀ 𝑜 ∈ 𝐽 ∀ 𝑠 ∈ 𝐹 ( 𝐴 ∈ 𝑜 → ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐹 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) )
33 30 32 bitri ⊢ ( ∀ 𝑠 ∈ 𝐹 ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐹 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) )
34 29 33 bitrdi ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐹 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) )
35 34 pm5.32da ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐹 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) ) )
36 1 21 35 3bitrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐹 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) ) )