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

Metamath Proof Explorer

Theorem fcfval

Description: The set of cluster points of a function. (Contributed by Jeff Hankins, 24-Nov-2009) (Revised by Stefan O'Rear, 9-Aug-2015)

Ref Expression
Assertion fcfval ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) = ( 𝐽 fClus ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )

Proof

Step Hyp Ref Expression
1 df-fcf ⊢ fClusf = ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ ( 𝑔 ∈ ( ∪ 𝑗 ↑m ∪ 𝑓 ) ↦ ( 𝑗 fClus ( ( ∪ 𝑗 FilMap 𝑔 ) ‘ 𝑓 ) ) ) )
2 1 a1i ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → fClusf = ( 𝑗 ∈ Top , 𝑓 ∈ ∪ ran Fil ↦ ( 𝑔 ∈ ( ∪ 𝑗 ↑m ∪ 𝑓 ) ↦ ( 𝑗 fClus ( ( ∪ 𝑗 FilMap 𝑔 ) ‘ 𝑓 ) ) ) ) )
3 simprl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐿 ) ) → 𝑗 = 𝐽 )
4 3 unieqd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐿 ) ) → ∪ 𝑗 = ∪ 𝐽 )
5 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
6 5 ad2antrr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐿 ) ) → 𝑋 = ∪ 𝐽 )
7 4 6 eqtr4d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐿 ) ) → ∪ 𝑗 = 𝑋 )
8 unieq ⊢ ( 𝑓 = 𝐿 → ∪ 𝑓 = ∪ 𝐿 )
9 8 ad2antll ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐿 ) ) → ∪ 𝑓 = ∪ 𝐿 )
10 filunibas ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑌 ) → ∪ 𝐿 = 𝑌 )
11 10 ad2antlr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐿 ) ) → ∪ 𝐿 = 𝑌 )
12 9 11 eqtrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐿 ) ) → ∪ 𝑓 = 𝑌 )
13 7 12 oveq12d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐿 ) ) → ( ∪ 𝑗 ↑m ∪ 𝑓 ) = ( 𝑋 ↑m 𝑌 ) )
14 7 oveq1d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐿 ) ) → ( ∪ 𝑗 FilMap 𝑔 ) = ( 𝑋 FilMap 𝑔 ) )
15 simprr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐿 ) ) → 𝑓 = 𝐿 )
16 14 15 fveq12d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐿 ) ) → ( ( ∪ 𝑗 FilMap 𝑔 ) ‘ 𝑓 ) = ( ( 𝑋 FilMap 𝑔 ) ‘ 𝐿 ) )
17 3 16 oveq12d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐿 ) ) → ( 𝑗 fClus ( ( ∪ 𝑗 FilMap 𝑔 ) ‘ 𝑓 ) ) = ( 𝐽 fClus ( ( 𝑋 FilMap 𝑔 ) ‘ 𝐿 ) ) )
18 13 17 mpteq12dv ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑓 = 𝐿 ) ) → ( 𝑔 ∈ ( ∪ 𝑗 ↑m ∪ 𝑓 ) ↦ ( 𝑗 fClus ( ( ∪ 𝑗 FilMap 𝑔 ) ‘ 𝑓 ) ) ) = ( 𝑔 ∈ ( 𝑋 ↑m 𝑌 ) ↦ ( 𝐽 fClus ( ( 𝑋 FilMap 𝑔 ) ‘ 𝐿 ) ) ) )
19 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
20 19 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → 𝐽 ∈ Top )
21 fvssunirn ⊢ ( Fil ‘ 𝑌 ) ⊆ ∪ ran Fil
22 21 sseli ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑌 ) → 𝐿 ∈ ∪ ran Fil )
23 22 adantl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → 𝐿 ∈ ∪ ran Fil )
24 ovex ⊢ ( 𝑋 ↑m 𝑌 ) ∈ V
25 24 mptex ⊢ ( 𝑔 ∈ ( 𝑋 ↑m 𝑌 ) ↦ ( 𝐽 fClus ( ( 𝑋 FilMap 𝑔 ) ‘ 𝐿 ) ) ) ∈ V
26 25 a1i ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝑔 ∈ ( 𝑋 ↑m 𝑌 ) ↦ ( 𝐽 fClus ( ( 𝑋 FilMap 𝑔 ) ‘ 𝐿 ) ) ) ∈ V )
27 2 18 20 23 26 ovmpod ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝐽 fClusf 𝐿 ) = ( 𝑔 ∈ ( 𝑋 ↑m 𝑌 ) ↦ ( 𝐽 fClus ( ( 𝑋 FilMap 𝑔 ) ‘ 𝐿 ) ) ) )
28 27 3adant3 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐽 fClusf 𝐿 ) = ( 𝑔 ∈ ( 𝑋 ↑m 𝑌 ) ↦ ( 𝐽 fClus ( ( 𝑋 FilMap 𝑔 ) ‘ 𝐿 ) ) ) )
29 simpr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑔 = 𝐹 ) → 𝑔 = 𝐹 )
30 29 oveq2d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑔 = 𝐹 ) → ( 𝑋 FilMap 𝑔 ) = ( 𝑋 FilMap 𝐹 ) )
31 30 fveq1d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑔 = 𝐹 ) → ( ( 𝑋 FilMap 𝑔 ) ‘ 𝐿 ) = ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) )
32 31 oveq2d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑔 = 𝐹 ) → ( 𝐽 fClus ( ( 𝑋 FilMap 𝑔 ) ‘ 𝐿 ) ) = ( 𝐽 fClus ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )
33 toponmax ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
34 filtop ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑌 ) → 𝑌 ∈ 𝐿 )
35 elmapg ⊢ ( ( 𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐿 ) → ( 𝐹 ∈ ( 𝑋 ↑m 𝑌 ) ↔ 𝐹 : 𝑌 ⟶ 𝑋 ) )
36 33 34 35 syl2an ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝑋 ↑m 𝑌 ) ↔ 𝐹 : 𝑌 ⟶ 𝑋 ) )
37 36 biimp3ar ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → 𝐹 ∈ ( 𝑋 ↑m 𝑌 ) )
38 ovexd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐽 fClus ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ∈ V )
39 28 32 37 38 fvmptd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) = ( 𝐽 fClus ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )