This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fclsval

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

Ref Expression
Hypothesis fclsval.x ⊢ 𝑋 = ∪ 𝐽
Assertion fclsval ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝐽 fClus 𝐹 ) = if ( 𝑋 = 𝑌 , ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) , ∅ ) )

Proof

Step Hyp Ref Expression
1 fclsval.x ⊢ 𝑋 = ∪ 𝐽
2 simpl ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑌 ) ) → 𝐽 ∈ Top )
3 fvssunirn ⊢ ( Fil ‘ 𝑌 ) ⊆ ∪ ran Fil
4 3 sseli ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑌 ) → 𝐹 ∈ ∪ ran Fil )
5 4 adantl ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑌 ) ) → 𝐹 ∈ ∪ ran Fil )
6 filn0 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑌 ) → 𝐹 ≠ ∅ )
7 6 adantl ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑌 ) ) → 𝐹 ≠ ∅ )
8 fvex ⊢ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ∈ V
9 8 rgenw ⊢ ∀ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ∈ V
10 iinexg ⊢ ( ( 𝐹 ≠ ∅ ∧ ∀ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ∈ V ) → ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ∈ V )
11 7 9 10 sylancl ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑌 ) ) → ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ∈ V )
12 0ex ⊢ ∅ ∈ V
13 ifcl ⊢ ( ( ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ∈ V ∧ ∅ ∈ V ) → if ( 𝑋 = ∪ 𝐹 , ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) , ∅ ) ∈ V )
14 11 12 13 sylancl ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑌 ) ) → if ( 𝑋 = ∪ 𝐹 , ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) , ∅ ) ∈ V )
15 unieq ⊢ ( 𝑗 = 𝐽 → ∪ 𝑗 = ∪ 𝐽 )
16 15 1 eqtr4di ⊢ ( 𝑗 = 𝐽 → ∪ 𝑗 = 𝑋 )
17 unieq ⊢ ( 𝑓 = 𝐹 → ∪ 𝑓 = ∪ 𝐹 )
18 16 17 eqeqan12d ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ( ∪ 𝑗 = ∪ 𝑓 ↔ 𝑋 = ∪ 𝐹 ) )
19 iineq1 ⊢ ( 𝑓 = 𝐹 → ∩ 𝑡 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑡 ) = ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝑗 ) ‘ 𝑡 ) )
20 19 adantl ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ∩ 𝑡 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑡 ) = ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝑗 ) ‘ 𝑡 ) )
21 simpll ⊢ ( ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) ∧ 𝑡 ∈ 𝐹 ) → 𝑗 = 𝐽 )
22 21 fveq2d ⊢ ( ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) ∧ 𝑡 ∈ 𝐹 ) → ( cls ‘ 𝑗 ) = ( cls ‘ 𝐽 ) )
23 22 fveq1d ⊢ ( ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) ∧ 𝑡 ∈ 𝐹 ) → ( ( cls ‘ 𝑗 ) ‘ 𝑡 ) = ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) )
24 23 iineq2dv ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝑗 ) ‘ 𝑡 ) = ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) )
25 20 24 eqtrd ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → ∩ 𝑡 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑡 ) = ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) )
26 18 25 ifbieq1d ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐹 ) → if ( ∪ 𝑗 = ∪ 𝑓 , ∩ 𝑡 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑡 ) , ∅ ) = if ( 𝑋 = ∪ 𝐹 , ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) , ∅ ) )
27 df-fcls ⊢ fClus = ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ if ( ∪ 𝑗 = ∪ 𝑓 , ∩ 𝑡 ∈ 𝑓 ( ( cls ‘ 𝑗 ) ‘ 𝑡 ) , ∅ ) )
28 26 27 ovmpoga ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ∧ if ( 𝑋 = ∪ 𝐹 , ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) , ∅ ) ∈ V ) → ( 𝐽 fClus 𝐹 ) = if ( 𝑋 = ∪ 𝐹 , ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) , ∅ ) )
29 2 5 14 28 syl3anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝐽 fClus 𝐹 ) = if ( 𝑋 = ∪ 𝐹 , ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) , ∅ ) )
30 filunibas ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑌 ) → ∪ 𝐹 = 𝑌 )
31 30 eqeq2d ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑌 ) → ( 𝑋 = ∪ 𝐹 ↔ 𝑋 = 𝑌 ) )
32 31 adantl ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝑋 = ∪ 𝐹 ↔ 𝑋 = 𝑌 ) )
33 32 ifbid ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑌 ) ) → if ( 𝑋 = ∪ 𝐹 , ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) , ∅ ) = if ( 𝑋 = 𝑌 , ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) , ∅ ) )
34 29 33 eqtrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝐽 fClus 𝐹 ) = if ( 𝑋 = 𝑌 , ∩ 𝑡 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) , ∅ ) )