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 𝐹 ) ↔ ( 𝐴𝑋 ∧ ∀ 𝑜𝐽 ( 𝐴𝑜 → ∀ 𝑠𝐹 ( 𝑜𝑠 ) ≠ ∅ ) ) ) )