Metamath Proof Explorer

Theorem isfcls

Description: A cluster point of a filter. (Contributed by Jeff Hankins, 10-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Hypothesis fclsval.x ⊢ 𝑋 = ∪ 𝐽
Assertion isfcls ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) )

Proof

Step Hyp Ref Expression
1 fclsval.x ⊢ 𝑋 = ∪ 𝐽
2 anass ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) ∧ 𝑋 = ∪ 𝐹 ) ∧ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) ∧ ( 𝑋 = ∪ 𝐹 ∧ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) ) )
3 fvssunirn ⊢ ( Fil ‘ 𝑋 ) ⊆ ∪ ran Fil
4 3 sseli ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ∪ ran Fil )
5 filunibas ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∪ 𝐹 = 𝑋 )
6 5 eqcomd ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 = ∪ 𝐹 )
7 4 6 jca ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐹 ∈ ∪ ran Fil ∧ 𝑋 = ∪ 𝐹 ) )
8 filunirn ⊢ ( 𝐹 ∈ ∪ ran Fil ↔ 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) )
9 fveq2 ⊢ ( 𝑋 = ∪ 𝐹 → ( Fil ‘ 𝑋 ) = ( Fil ‘ ∪ 𝐹 ) )
10 9 eleq2d ⊢ ( 𝑋 = ∪ 𝐹 → ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ↔ 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ) )
11 10 biimparc ⊢ ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑋 = ∪ 𝐹 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
12 8 11 sylanb ⊢ ( ( 𝐹 ∈ ∪ ran Fil ∧ 𝑋 = ∪ 𝐹 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
13 7 12 impbii ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ↔ ( 𝐹 ∈ ∪ ran Fil ∧ 𝑋 = ∪ 𝐹 ) )
14 13 anbi2i ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ↔ ( 𝐽 ∈ Top ∧ ( 𝐹 ∈ ∪ ran Fil ∧ 𝑋 = ∪ 𝐹 ) ) )
15 14 anbi1i ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) ↔ ( ( 𝐽 ∈ Top ∧ ( 𝐹 ∈ ∪ ran Fil ∧ 𝑋 = ∪ 𝐹 ) ) ∧ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) )
16 df-3an ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) )
17 anass ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) ∧ 𝑋 = ∪ 𝐹 ) ↔ ( 𝐽 ∈ Top ∧ ( 𝐹 ∈ ∪ ran Fil ∧ 𝑋 = ∪ 𝐹 ) ) )
18 17 anbi1i ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) ∧ 𝑋 = ∪ 𝐹 ) ∧ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) ↔ ( ( 𝐽 ∈ Top ∧ ( 𝐹 ∈ ∪ ran Fil ∧ 𝑋 = ∪ 𝐹 ) ) ∧ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) )
19 15 16 18 3bitr4i ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) ↔ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) ∧ 𝑋 = ∪ 𝐹 ) ∧ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) )
20 df-fcls ⊢ fClus = ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ if ( ∪ 𝑗 = ∪ 𝑓 , ∩ 𝑥 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑥 ) , ∅ ) )
21 20 elmpocl ⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) )
22 1 fclsval ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ) → ( 𝐽 fClus 𝐹 ) = if ( 𝑋 = ∪ 𝐹 , ∩ 𝑠 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) , ∅ ) )
23 8 22 sylan2b ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) → ( 𝐽 fClus 𝐹 ) = if ( 𝑋 = ∪ 𝐹 , ∩ 𝑠 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) , ∅ ) )
24 23 eleq2d ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ 𝐴 ∈ if ( 𝑋 = ∪ 𝐹 , ∩ 𝑠 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) , ∅ ) ) )
25 n0i ⊢ ( 𝐴 ∈ if ( 𝑋 = ∪ 𝐹 , ∩ 𝑠 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) , ∅ ) → ¬ if ( 𝑋 = ∪ 𝐹 , ∩ 𝑠 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) , ∅ ) = ∅ )
26 iffalse ⊢ ( ¬ 𝑋 = ∪ 𝐹 → if ( 𝑋 = ∪ 𝐹 , ∩ 𝑠 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) , ∅ ) = ∅ )
27 25 26 nsyl2 ⊢ ( 𝐴 ∈ if ( 𝑋 = ∪ 𝐹 , ∩ 𝑠 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) , ∅ ) → 𝑋 = ∪ 𝐹 )
28 27 a1i ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) → ( 𝐴 ∈ if ( 𝑋 = ∪ 𝐹 , ∩ 𝑠 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) , ∅ ) → 𝑋 = ∪ 𝐹 ) )
29 28 pm4.71rd ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) → ( 𝐴 ∈ if ( 𝑋 = ∪ 𝐹 , ∩ 𝑠 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) , ∅ ) ↔ ( 𝑋 = ∪ 𝐹 ∧ 𝐴 ∈ if ( 𝑋 = ∪ 𝐹 , ∩ 𝑠 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) , ∅ ) ) ) )
30 iftrue ⊢ ( 𝑋 = ∪ 𝐹 → if ( 𝑋 = ∪ 𝐹 , ∩ 𝑠 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) , ∅ ) = ∩ 𝑠 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) )
31 30 adantl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) ∧ 𝑋 = ∪ 𝐹 ) → if ( 𝑋 = ∪ 𝐹 , ∩ 𝑠 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) , ∅ ) = ∩ 𝑠 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) )
32 31 eleq2d ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) ∧ 𝑋 = ∪ 𝐹 ) → ( 𝐴 ∈ if ( 𝑋 = ∪ 𝐹 , ∩ 𝑠 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) , ∅ ) ↔ 𝐴 ∈ ∩ 𝑠 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) )
33 elex ⊢ ( 𝐴 ∈ ∩ 𝑠 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) → 𝐴 ∈ V )
34 33 a1i ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) ∧ 𝑋 = ∪ 𝐹 ) → ( 𝐴 ∈ ∩ 𝑠 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) → 𝐴 ∈ V ) )
35 filn0 ⊢ ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) → 𝐹 ≠ ∅ )
36 8 35 sylbi ⊢ ( 𝐹 ∈ ∪ ran Fil → 𝐹 ≠ ∅ )
37 36 ad2antlr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) ∧ 𝑋 = ∪ 𝐹 ) → 𝐹 ≠ ∅ )
38 r19.2z ⊢ ( ( 𝐹 ≠ ∅ ∧ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) → ∃ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) )
39 38 ex ⊢ ( 𝐹 ≠ ∅ → ( ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) → ∃ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) )
40 37 39 syl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) ∧ 𝑋 = ∪ 𝐹 ) → ( ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) → ∃ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) )
41 elex ⊢ ( 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) → 𝐴 ∈ V )
42 41 rexlimivw ⊢ ( ∃ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) → 𝐴 ∈ V )
43 40 42 syl6 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) ∧ 𝑋 = ∪ 𝐹 ) → ( ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) → 𝐴 ∈ V ) )
44 eliin ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ ∩ 𝑠 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ↔ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) )
45 44 a1i ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) ∧ 𝑋 = ∪ 𝐹 ) → ( 𝐴 ∈ V → ( 𝐴 ∈ ∩ 𝑠 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ↔ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) ) )
46 34 43 45 pm5.21ndd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) ∧ 𝑋 = ∪ 𝐹 ) → ( 𝐴 ∈ ∩ 𝑠 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ↔ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) )
47 32 46 bitrd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) ∧ 𝑋 = ∪ 𝐹 ) → ( 𝐴 ∈ if ( 𝑋 = ∪ 𝐹 , ∩ 𝑠 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) , ∅ ) ↔ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) )
48 47 pm5.32da ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) → ( ( 𝑋 = ∪ 𝐹 ∧ 𝐴 ∈ if ( 𝑋 = ∪ 𝐹 , ∩ 𝑠 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) , ∅ ) ) ↔ ( 𝑋 = ∪ 𝐹 ∧ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) ) )
49 24 29 48 3bitrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝑋 = ∪ 𝐹 ∧ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) ) )
50 21 49 biadanii ⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ) ∧ ( 𝑋 = ∪ 𝐹 ∧ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) ) )
51 2 19 50 3bitr4ri ⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝐹 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ) )