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

Theorem fmval 21741
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 21736 . . . . 5 FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑏 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑦𝑏 ↦ (𝑓𝑦)))))
21a1i 11 . . . 4 ((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑏 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑦𝑏 ↦ (𝑓𝑦))))))
3 dmeq 5322 . . . . . . . 8 (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
43fveq2d 6193 . . . . . . 7 (𝑓 = 𝐹 → (fBas‘dom 𝑓) = (fBas‘dom 𝐹))
54adantl 482 . . . . . 6 ((𝑥 = 𝑋𝑓 = 𝐹) → (fBas‘dom 𝑓) = (fBas‘dom 𝐹))
6 id 22 . . . . . . 7 (𝑥 = 𝑋𝑥 = 𝑋)
7 imaeq1 5459 . . . . . . . . 9 (𝑓 = 𝐹 → (𝑓𝑦) = (𝐹𝑦))
87mpteq2dv 4743 . . . . . . . 8 (𝑓 = 𝐹 → (𝑦𝑏 ↦ (𝑓𝑦)) = (𝑦𝑏 ↦ (𝐹𝑦)))
98rneqd 5351 . . . . . . 7 (𝑓 = 𝐹 → ran (𝑦𝑏 ↦ (𝑓𝑦)) = ran (𝑦𝑏 ↦ (𝐹𝑦)))
106, 9oveqan12d 6666 . . . . . 6 ((𝑥 = 𝑋𝑓 = 𝐹) → (𝑥filGenran (𝑦𝑏 ↦ (𝑓𝑦))) = (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦))))
115, 10mpteq12dv 4731 . . . . 5 ((𝑥 = 𝑋𝑓 = 𝐹) → (𝑏 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑦𝑏 ↦ (𝑓𝑦)))) = (𝑏 ∈ (fBas‘dom 𝐹) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦)))))
12 fdm 6049 . . . . . . . 8 (𝐹:𝑌𝑋 → dom 𝐹 = 𝑌)
1312fveq2d 6193 . . . . . . 7 (𝐹:𝑌𝑋 → (fBas‘dom 𝐹) = (fBas‘𝑌))
1413mpteq1d 4736 . . . . . 6 (𝐹:𝑌𝑋 → (𝑏 ∈ (fBas‘dom 𝐹) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦)))) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦)))))
15143ad2ant3 1083 . . . . 5 ((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝑏 ∈ (fBas‘dom 𝐹) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦)))) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦)))))
1611, 15sylan9eqr 2677 . . . 4 (((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ (𝑥 = 𝑋𝑓 = 𝐹)) → (𝑏 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑦𝑏 ↦ (𝑓𝑦)))) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦)))))
17 elex 3210 . . . . 5 (𝑋𝐴𝑋 ∈ V)
18173ad2ant1 1081 . . . 4 ((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → 𝑋 ∈ V)
19 simp3 1062 . . . . 5 ((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → 𝐹:𝑌𝑋)
20 elfvdm 6218 . . . . . 6 (𝐵 ∈ (fBas‘𝑌) → 𝑌 ∈ dom fBas)
21203ad2ant2 1082 . . . . 5 ((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → 𝑌 ∈ dom fBas)
22 simp1 1060 . . . . 5 ((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → 𝑋𝐴)
23 fex2 7118 . . . . 5 ((𝐹:𝑌𝑋𝑌 ∈ dom fBas ∧ 𝑋𝐴) → 𝐹 ∈ V)
2419, 21, 22, 23syl3anc 1325 . . . 4 ((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → 𝐹 ∈ V)
25 fvex 6199 . . . . . 6 (fBas‘𝑌) ∈ V
2625mptex 6483 . . . . 5 (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦)))) ∈ V
2726a1i 11 . . . 4 ((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦)))) ∈ V)
282, 16, 18, 24, 27ovmpt2d 6785 . . 3 ((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝑋 FilMap 𝐹) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦)))))
2928fveq1d 6191 . 2 ((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → ((𝑋 FilMap 𝐹)‘𝐵) = ((𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦))))‘𝐵))
30 mpteq1 4735 . . . . . 6 (𝑏 = 𝐵 → (𝑦𝑏 ↦ (𝐹𝑦)) = (𝑦𝐵 ↦ (𝐹𝑦)))
3130rneqd 5351 . . . . 5 (𝑏 = 𝐵 → ran (𝑦𝑏 ↦ (𝐹𝑦)) = ran (𝑦𝐵 ↦ (𝐹𝑦)))
3231oveq2d 6663 . . . 4 (𝑏 = 𝐵 → (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦))) = (𝑋filGenran (𝑦𝐵 ↦ (𝐹𝑦))))
33 eqid 2621 . . . 4 (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦)))) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦))))
34 ovex 6675 . . . 4 (𝑋filGenran (𝑦𝐵 ↦ (𝐹𝑦))) ∈ V
3532, 33, 34fvmpt 6280 . . 3 (𝐵 ∈ (fBas‘𝑌) → ((𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦))))‘𝐵) = (𝑋filGenran (𝑦𝐵 ↦ (𝐹𝑦))))
36353ad2ant2 1082 . 2 ((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → ((𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦𝑏 ↦ (𝐹𝑦))))‘𝐵) = (𝑋filGenran (𝑦𝐵 ↦ (𝐹𝑦))))
3729, 36eqtrd 2655 1 ((𝑋𝐴𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → ((𝑋 FilMap 𝐹)‘𝐵) = (𝑋filGenran (𝑦𝐵 ↦ (𝐹𝑦))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1037   = wceq 1482  wcel 1989  Vcvv 3198  cmpt 4727  dom cdm 5112  ran crn 5113  cima 5115  wf 5882  cfv 5886  (class class class)co 6647  cmpt2 6649  fBascfbas 19728  filGencfg 19729   FilMap cfm 21731
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-rep 4769  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-ral 2916  df-rex 2917  df-reu 2918  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-op 4182  df-uni 4435  df-iun 4520  df-br 4652  df-opab 4711  df-mpt 4728  df-id 5022  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-ov 6650  df-oprab 6651  df-mpt2 6652  df-fm 21736
This theorem is referenced by:  fmfil  21742  fmss  21744  elfm  21745  ucnextcn  22102  fmcfil  23064
  Copyright terms: Public domain W3C validator