Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fmval Unicode version

Theorem fmval 17734
 Description: Introduce a function that takes a function from a filtered domain to a set and produces a filter which consists of supersets of images of filter elements. The functions which are dealt with by this function are similar to nets in topology. For example, suppose we have a sequence filtered by the filter generated by its tails under the usual natural number ordering. Then the elements of this filter are precisely the supersets of tails of this sequence. Under this definition, it is not too difficult to see that the limit of a function in the filter sense captures the notion of convergence of a sequence. As a result, the notion of a filter generalizes many ideas associated with sequences, and this function is one way to make that relationship precise in Metamath. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
Assertion
Ref Expression
fmval
Distinct variable groups:   ,   ,   ,   ,   ,

Proof of Theorem fmval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-fm 17729 . . . . 5
21a1i 10 . . . 4
3 dmeq 4958 . . . . . . . 8
43fveq2d 5609 . . . . . . 7
54adantl 452 . . . . . 6
6 id 19 . . . . . . 7
7 imaeq1 5086 . . . . . . . . 9
87mpteq2dv 4186 . . . . . . . 8
98rneqd 4985 . . . . . . 7
106, 9oveqan12d 5961 . . . . . 6
115, 10mpteq12dv 4177 . . . . 5
12 fdm 5473 . . . . . . . 8
1312fveq2d 5609 . . . . . . 7
14 mpteq1 4179 . . . . . . 7
1513, 14syl 15 . . . . . 6
16153ad2ant3 978 . . . . 5
1711, 16sylan9eqr 2412 . . . 4
18 elex 2872 . . . . 5
19183ad2ant1 976 . . . 4
20 simp3 957 . . . . 5
21 elfvdm 5634 . . . . . 6
22213ad2ant2 977 . . . . 5
23 simp1 955 . . . . 5
24 fex2 5481 . . . . 5
2520, 22, 23, 24syl3anc 1182 . . . 4
26 fvex 5619 . . . . . 6
2726mptex 5829 . . . . 5
2827a1i 10 . . . 4
292, 17, 19, 25, 28ovmpt2d 6059 . . 3
3029fveq1d 5607 . 2
31 mpteq1 4179 . . . . . 6
3231rneqd 4985 . . . . 5
3332oveq2d 5958 . . . 4
34 eqid 2358 . . . 4
35 ovex 5967 . . . 4
3633, 34, 35fvmpt 5682 . . 3