Theorem mptfvmpt 7179

Description: A function in maps-to notation as the value of another function in maps-to notation. (Contributed by AV, 20-Aug-2022.)

Hypotheses

Ref	Expression
mptfvmpt.y	⊢ (𝑦 = 𝑌 → 𝑀 = (𝑥 ∈ 𝑉 ↦ 𝐴))
mptfvmpt.g	⊢ 𝐺 = (𝑦 ∈ 𝑊 ↦ 𝑀)
mptfvmpt.v	⊢ 𝑉 = (𝐹‘𝑋)

Assertion

Ref	Expression
mptfvmpt	⊢ (𝑌 ∈ 𝑊 → (𝐺‘𝑌) = (𝑥 ∈ 𝑉 ↦ 𝐴))

Distinct variable groups:   𝑦,𝐴   𝑥,𝑉,𝑦   𝑦,𝑊   𝑦,𝑌

Allowed substitution hints:   𝐴(𝑥)   𝐹(𝑥,𝑦)   𝐺(𝑥,𝑦)   𝑀(𝑥,𝑦)   𝑊(𝑥)   𝑋(𝑥,𝑦)   𝑌(𝑥)

Proof of Theorem mptfvmpt

Step	Hyp	Ref	Expression
1		mptfvmpt.y	. 2 ⊢ (𝑦 = 𝑌 → 𝑀 = (𝑥 ∈ 𝑉 ↦ 𝐴))
2		mptfvmpt.g	. 2 ⊢ 𝐺 = (𝑦 ∈ 𝑊 ↦ 𝑀)
3		mptfvmpt.v	. . . 4 ⊢ 𝑉 = (𝐹‘𝑋)
4	3	fvexi 6848	. . 3 ⊢ 𝑉 ∈ V
5	4	mptex 7174	. 2 ⊢ (𝑥 ∈ 𝑉 ↦ 𝐴) ∈ V
6	1, 2, 5	fvmpt 6942	1 ⊢ (𝑌 ∈ 𝑊 → (𝐺‘𝑌) = (𝑥 ∈ 𝑉 ↦ 𝐴))

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119   ↦ cmpt 5160  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-rep 5206  ax-sep 5225  ax-nul 5235  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500

This theorem is referenced by:  cidfval  17640  idafval  18022  grpinvfvalALT  18953  grplactfval  19015  odfvalALT  19506  asclfval  21860  ig1pval  26166  ishlg  28695  htthlem  31013  sgnsv  33248  mvrsval  35734  mvhfval  35762  msrfval  35766  lkrfval  39580  pmapfval  40249  watfvalN  40485  ldilfset  40601  ltrnfset  40610  dilfsetN  40645  trnfsetN  40648  trlfset  40653  tgrpfset  41237  tendofset  41251  tendoi  41287  erngfset  41292  erngfset-rN  41300  dvafset  41497  diaffval  41523  dvhfset  41573  docaffvalN  41614  djaffvalN  41626  dibffval  41633  dicffval  41667  dihffval  41723  dihfval  41724  dochffval  41842  djhffval  41889  lcfrlem8  42042  lcdfval  42081  mapdffval  42119  mapdfval  42120  hvmapffval  42251  hdmap1ffval  42288  hdmapffval  42319  hdmapfval  42320  hgmapffval  42378  hgmapfval  42379  hbtlem1  43569  hbtlem7  43571