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

Theorem fmval 23769
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 positive integer 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 ((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → ((𝑋 FilMap 𝐹)‘𝐵) = (𝑋filGenran (𝑦𝐵 ↦ (𝐹𝑦))))
Distinct variable groups:   𝑦,𝐵   𝑦,𝐹   𝑦,𝑋   𝑦,𝑌   𝑦,𝐴

Proof of Theorem fmval
Dummy variables 𝑓 𝑏 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-fm 23764 . . . . 5 FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑏 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑦𝑏 ↦ (𝑓𝑦)))))
21a1i 11 . . . 4 ((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑏 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑦𝑏 ↦ (𝑓𝑦))))))
3 dmeq 5893 . . . . . . . 8 (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
43fveq2d 6885 . . . . . . 7 (𝑓 = 𝐹 → (fBas‘dom 𝑓) = (fBas‘dom 𝐹))
54adantl 481 . . . . . 6 ((𝑥 = 𝑋𝑓 = 𝐹) → (fBas‘dom 𝑓) = (fBas‘dom 𝐹))
6 id 22 . . . . . . 7 (𝑥 = 𝑋𝑥 = 𝑋)
7 imaeq1 6044 . . . . . . . . 9 (𝑓 = 𝐹 → (𝑓𝑦) = (𝐹𝑦))
87mpteq2dv 5240 . . . . . . . 8 (𝑓 = 𝐹 → (𝑦𝑏 ↦ (𝑓𝑦)) = (𝑦𝑏 ↦ (𝐹𝑦)))
98rneqd 5927 . . . . . . 7 (𝑓 = 𝐹 → ran (𝑦𝑏 ↦ (𝑓𝑦)) = ran (𝑦𝑏 ↦ (𝐹𝑦)))
106, 9oveqan12d 7420 . . . . . 6 ((𝑥 = 𝑋𝑓 = 𝐹) → (𝑥filGenran (𝑦𝑏 ↦ (𝑓𝑦))) = (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦))))
115, 10mpteq12dv 5229 . . . . 5 ((𝑥 = 𝑋𝑓 = 𝐹) → (𝑏 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑦𝑏 ↦ (𝑓𝑦)))) = (𝑏 ∈ (fBas‘dom 𝐹) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦)))))
12 fdm 6716 . . . . . . . 8 (𝐹:𝑌𝑋 → dom 𝐹 = 𝑌)
1312fveq2d 6885 . . . . . . 7 (𝐹:𝑌𝑋 → (fBas‘dom 𝐹) = (fBas‘𝑌))
1413mpteq1d 5233 . . . . . 6 (𝐹:𝑌𝑋 → (𝑏 ∈ (fBas‘dom 𝐹) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦)))) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦)))))
15143ad2ant3 1132 . . . . 5 ((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝑏 ∈ (fBas‘dom 𝐹) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦)))) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦)))))
1611, 15sylan9eqr 2786 . . . 4 (((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ (𝑥 = 𝑋𝑓 = 𝐹)) → (𝑏 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑦𝑏 ↦ (𝑓𝑦)))) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦)))))
17 elex 3485 . . . . 5 (𝑋𝐴𝑋 ∈ V)
18173ad2ant1 1130 . . . 4 ((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → 𝑋 ∈ V)
19 simp3 1135 . . . . 5 ((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → 𝐹:𝑌𝑋)
20 elfvdm 6918 . . . . . 6 (𝐵 ∈ (fBas‘𝑌) → 𝑌 ∈ dom fBas)
21203ad2ant2 1131 . . . . 5 ((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → 𝑌 ∈ dom fBas)
2219, 21fexd 7220 . . . 4 ((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → 𝐹 ∈ V)
23 fvex 6894 . . . . . 6 (fBas‘𝑌) ∈ V
2423mptex 7216 . . . . 5 (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦)))) ∈ V
2524a1i 11 . . . 4 ((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦)))) ∈ V)
262, 16, 18, 22, 25ovmpod 7552 . . 3 ((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝑋 FilMap 𝐹) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦)))))
2726fveq1d 6883 . 2 ((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → ((𝑋 FilMap 𝐹)‘𝐵) = ((𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦))))‘𝐵))
28 mpteq1 5231 . . . . . 6 (𝑏 = 𝐵 → (𝑦𝑏 ↦ (𝐹𝑦)) = (𝑦𝐵 ↦ (𝐹𝑦)))
2928rneqd 5927 . . . . 5 (𝑏 = 𝐵 → ran (𝑦𝑏 ↦ (𝐹𝑦)) = ran (𝑦𝐵 ↦ (𝐹𝑦)))
3029oveq2d 7417 . . . 4 (𝑏 = 𝐵 → (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦))) = (𝑋filGenran (𝑦𝐵 ↦ (𝐹𝑦))))
31 eqid 2724 . . . 4 (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦)))) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦))))
32 ovex 7434 . . . 4 (𝑋filGenran (𝑦𝐵 ↦ (𝐹𝑦))) ∈ V
3330, 31, 32fvmpt 6988 . . 3 (𝐵 ∈ (fBas‘𝑌) → ((𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦))))‘𝐵) = (𝑋filGenran (𝑦𝐵 ↦ (𝐹𝑦))))
34333ad2ant2 1131 . 2 ((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → ((𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦))))‘𝐵) = (𝑋filGenran (𝑦𝐵 ↦ (𝐹𝑦))))
3527, 34eqtrd 2764 1 ((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → ((𝑋 FilMap 𝐹)‘𝐵) = (𝑋filGenran (𝑦𝐵 ↦ (𝐹𝑦))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1084   = wceq 1533  wcel 2098  Vcvv 3466  cmpt 5221  dom cdm 5666  ran crn 5667  cima 5669  wf 6529  cfv 6533  (class class class)co 7401  cmpo 7403  fBascfbas 21216  filGencfg 21217   FilMap cfm 23759
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pr 5417
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7404  df-oprab 7405  df-mpo 7406  df-fm 23764
This theorem is referenced by:  fmfil  23770  fmss  23772  elfm  23773  ucnextcn  24131  fmcfil  25122
  Copyright terms: Public domain W3C validator