Theorem flfval 20359

Description: Given a function from a filtered set to a topological space, define the set of limit points of the function. (Contributed by Jeff Hankins, 8-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)

Assertion

Ref	Expression
flfval	|- ( ( J e. (TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fLimf L ) ` F ) = ( J fLim ( ( X FilMap F ) ` L ) ) )

Proof of Theorem flfval

Dummy variable f is distinct from all other variables.

Step	Hyp	Ref	Expression
1		toponmax 19298	. . . . 5 |- ( J e. (TopOn ` X ) -> X e. J )
2		filtop 20224	. . . . 5 |- ( L e. ( Fil ` Y ) -> Y e. L )
3		elmapg 7445	. . . . 5 |- ( ( X e. J /\ Y e. L ) -> ( F e. ( X ^m Y ) <-> F : Y --> X ) )
4	1, 2, 3	syl2an 477	. . . 4 |- ( ( J e. (TopOn ` X ) /\ L e. ( Fil ` Y ) ) -> ( F e. ( X ^m Y ) <-> F : Y --> X ) )
5	4	biimpar 485	. . 3 |- ( ( ( J e. (TopOn ` X ) /\ L e. ( Fil ` Y ) ) /\ F : Y --> X ) -> F e. ( X ^m Y ) )
6		flffval 20358	. . . . 5 |- ( ( J e. (TopOn ` X ) /\ L e. ( Fil ` Y ) ) -> ( J fLimf L ) = ( f e. ( X ^m Y ) |-> ( J fLim ( ( X FilMap f ) ` L ) ) ) )
7	6	fveq1d 5874	. . . 4 |- ( ( J e. (TopOn ` X ) /\ L e. ( Fil ` Y ) ) -> ( ( J fLimf L ) ` F ) = ( ( f e. ( X ^m Y ) |-> ( J fLim ( ( X FilMap f ) ` L ) ) ) ` F ) )
8		oveq2 6303	. . . . . . 7 |- ( f = F -> ( X FilMap f ) = ( X FilMap F ) )
9	8	fveq1d 5874	. . . . . 6 |- ( f = F -> ( ( X FilMap f ) ` L ) = ( ( X FilMap F ) ` L ) )
10	9	oveq2d 6311	. . . . 5 |- ( f = F -> ( J fLim ( ( X FilMap f ) ` L ) ) = ( J fLim ( ( X FilMap F ) ` L ) ) )
11		eqid 2467	. . . . 5 |- ( f e. ( X ^m Y ) |-> ( J fLim ( ( X FilMap f ) ` L ) ) ) = ( f e. ( X ^m Y ) |-> ( J fLim ( ( X FilMap f ) ` L ) ) )
12		ovex 6320	. . . . 5 |- ( J fLim ( ( X FilMap F ) ` L ) ) e. _V
13	10, 11, 12	fvmpt 5957	. . . 4 |- ( F e. ( X ^m Y ) -> ( ( f e. ( X ^m Y ) |-> ( J fLim ( ( X FilMap f ) ` L ) ) ) ` F ) = ( J fLim ( ( X FilMap F ) ` L ) ) )
14	7, 13	sylan9eq 2528	. . 3 |- ( ( ( J e. (TopOn ` X ) /\ L e. ( Fil ` Y ) ) /\ F e. ( X ^m Y ) ) -> ( ( J fLimf L ) ` F ) = ( J fLim ( ( X FilMap F ) ` L ) ) )
15	5, 14	syldan 470	. 2 |- ( ( ( J e. (TopOn ` X ) /\ L e. ( Fil ` Y ) ) /\ F : Y --> X ) -> ( ( J fLimf L ) ` F ) = ( J fLim ( ( X FilMap F ) ` L ) ) )
16	15	3impa 1191	1 |- ( ( J e. (TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fLimf L ) ` F ) = ( J fLim ( ( X FilMap F ) ` L ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 973   = wceq 1379   e. wcel 1767   |-> cmpt 4511   -->wf 5590   ` cfv 5594  (class class class)co 6295   ^m cmap 7432  TopOnctopon 19264   Filcfil 20214   FilMap cfm 20302   fLim cflim 20303   fLimf cflf 20304

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-iun 4333  df-br 4454  df-opab 4512  df-mpt 4513  df-id 4801  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-map 7434  df-fbas 18286  df-top 19268  df-topon 19271  df-fil 20215  df-flf 20309

This theorem is referenced by:  flfnei  20360  isflf  20362  hausflf  20366  flfcnp  20373  flfssfcf  20407  uffcfflf  20408  cnpfcf  20410  cnextcn  20435  tsmscls  20504  cnextucn  20674  cmetcaulem  21595  fmcncfil  27738