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

Theorem fmptco 6357
Description: Composition of two functions expressed as ordered-pair class abstractions. If 𝐹 has the equation (𝑥 + 2) and 𝐺 the equation (3∗𝑧) then (𝐺𝐹) has the equation (3∗(𝑥 + 2)). (Contributed by FL, 21-Jun-2012.) (Revised by Mario Carneiro, 24-Jul-2014.)
Hypotheses
Ref Expression
fmptco.1 ((𝜑𝑥𝐴) → 𝑅𝐵)
fmptco.2 (𝜑𝐹 = (𝑥𝐴𝑅))
fmptco.3 (𝜑𝐺 = (𝑦𝐵𝑆))
fmptco.4 (𝑦 = 𝑅𝑆 = 𝑇)
Assertion
Ref Expression
fmptco (𝜑 → (𝐺𝐹) = (𝑥𝐴𝑇))
Distinct variable groups:   𝑥,𝐴   𝑥,𝑦,𝐵   𝑦,𝑅   𝜑,𝑥   𝑥,𝑆   𝑦,𝑇
Allowed substitution hints:   𝜑(𝑦)   𝐴(𝑦)   𝑅(𝑥)   𝑆(𝑦)   𝑇(𝑥)   𝐹(𝑥,𝑦)   𝐺(𝑥,𝑦)

Proof of Theorem fmptco
Dummy variables 𝑣 𝑢 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relco 5597 . 2 Rel (𝐺𝐹)
2 mptrel 5213 . 2 Rel (𝑥𝐴𝑇)
3 fmptco.2 . . . . . . . . . . . 12 (𝜑𝐹 = (𝑥𝐴𝑅))
4 fmptco.1 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 𝑅𝐵)
53, 4fmpt3d 6347 . . . . . . . . . . 11 (𝜑𝐹:𝐴𝐵)
65ffund 6011 . . . . . . . . . 10 (𝜑 → Fun 𝐹)
7 funbrfv 6196 . . . . . . . . . . 11 (Fun 𝐹 → (𝑧𝐹𝑢 → (𝐹𝑧) = 𝑢))
87imp 445 . . . . . . . . . 10 ((Fun 𝐹𝑧𝐹𝑢) → (𝐹𝑧) = 𝑢)
96, 8sylan 488 . . . . . . . . 9 ((𝜑𝑧𝐹𝑢) → (𝐹𝑧) = 𝑢)
109eqcomd 2627 . . . . . . . 8 ((𝜑𝑧𝐹𝑢) → 𝑢 = (𝐹𝑧))
1110a1d 25 . . . . . . 7 ((𝜑𝑧𝐹𝑢) → (𝑢𝐺𝑤𝑢 = (𝐹𝑧)))
1211expimpd 628 . . . . . 6 (𝜑 → ((𝑧𝐹𝑢𝑢𝐺𝑤) → 𝑢 = (𝐹𝑧)))
1312pm4.71rd 666 . . . . 5 (𝜑 → ((𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤))))
1413exbidv 1847 . . . 4 (𝜑 → (∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤) ↔ ∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤))))
15 fvex 6163 . . . . . 6 (𝐹𝑧) ∈ V
16 breq2 4622 . . . . . . 7 (𝑢 = (𝐹𝑧) → (𝑧𝐹𝑢𝑧𝐹(𝐹𝑧)))
17 breq1 4621 . . . . . . 7 (𝑢 = (𝐹𝑧) → (𝑢𝐺𝑤 ↔ (𝐹𝑧)𝐺𝑤))
1816, 17anbi12d 746 . . . . . 6 (𝑢 = (𝐹𝑧) → ((𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤)))
1915, 18ceqsexv 3231 . . . . 5 (∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤)) ↔ (𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤))
20 funfvbrb 6291 . . . . . . . . 9 (Fun 𝐹 → (𝑧 ∈ dom 𝐹𝑧𝐹(𝐹𝑧)))
216, 20syl 17 . . . . . . . 8 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐹(𝐹𝑧)))
22 fdm 6013 . . . . . . . . . 10 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
235, 22syl 17 . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝐴)
2423eleq2d 2684 . . . . . . . 8 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐴))
2521, 24bitr3d 270 . . . . . . 7 (𝜑 → (𝑧𝐹(𝐹𝑧) ↔ 𝑧𝐴))
263fveq1d 6155 . . . . . . . 8 (𝜑 → (𝐹𝑧) = ((𝑥𝐴𝑅)‘𝑧))
27 fmptco.3 . . . . . . . 8 (𝜑𝐺 = (𝑦𝐵𝑆))
28 eqidd 2622 . . . . . . . 8 (𝜑𝑤 = 𝑤)
2926, 27, 28breq123d 4632 . . . . . . 7 (𝜑 → ((𝐹𝑧)𝐺𝑤 ↔ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤))
3025, 29anbi12d 746 . . . . . 6 (𝜑 → ((𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤) ↔ (𝑧𝐴 ∧ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤)))
31 nfcv 2761 . . . . . . . . 9 𝑥𝑧
32 nfv 1840 . . . . . . . . . 10 𝑥𝜑
33 nffvmpt1 6161 . . . . . . . . . . . 12 𝑥((𝑥𝐴𝑅)‘𝑧)
34 nfcv 2761 . . . . . . . . . . . 12 𝑥(𝑦𝐵𝑆)
35 nfcv 2761 . . . . . . . . . . . 12 𝑥𝑤
3633, 34, 35nfbr 4664 . . . . . . . . . . 11 𝑥((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤
37 nfcsb1v 3534 . . . . . . . . . . . 12 𝑥𝑧 / 𝑥𝑇
3837nfeq2 2776 . . . . . . . . . . 11 𝑥 𝑤 = 𝑧 / 𝑥𝑇
3936, 38nfbi 1830 . . . . . . . . . 10 𝑥(((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)
4032, 39nfim 1822 . . . . . . . . 9 𝑥(𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))
41 fveq2 6153 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑥𝐴𝑅)‘𝑥) = ((𝑥𝐴𝑅)‘𝑧))
4241breq1d 4628 . . . . . . . . . . 11 (𝑥 = 𝑧 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤 ↔ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤))
43 csbeq1a 3527 . . . . . . . . . . . 12 (𝑥 = 𝑧𝑇 = 𝑧 / 𝑥𝑇)
4443eqeq2d 2631 . . . . . . . . . . 11 (𝑥 = 𝑧 → (𝑤 = 𝑇𝑤 = 𝑧 / 𝑥𝑇))
4542, 44bibi12d 335 . . . . . . . . . 10 (𝑥 = 𝑧 → ((((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇) ↔ (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
4645imbi2d 330 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇)) ↔ (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))))
47 vex 3192 . . . . . . . . . . . 12 𝑤 ∈ V
48 simpl 473 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑅𝑢 = 𝑤) → 𝑦 = 𝑅)
4948eleq1d 2683 . . . . . . . . . . . . . 14 ((𝑦 = 𝑅𝑢 = 𝑤) → (𝑦𝐵𝑅𝐵))
50 id 22 . . . . . . . . . . . . . . 15 (𝑢 = 𝑤𝑢 = 𝑤)
51 fmptco.4 . . . . . . . . . . . . . . 15 (𝑦 = 𝑅𝑆 = 𝑇)
5250, 51eqeqan12rd 2639 . . . . . . . . . . . . . 14 ((𝑦 = 𝑅𝑢 = 𝑤) → (𝑢 = 𝑆𝑤 = 𝑇))
5349, 52anbi12d 746 . . . . . . . . . . . . 13 ((𝑦 = 𝑅𝑢 = 𝑤) → ((𝑦𝐵𝑢 = 𝑆) ↔ (𝑅𝐵𝑤 = 𝑇)))
54 df-mpt 4680 . . . . . . . . . . . . 13 (𝑦𝐵𝑆) = {⟨𝑦, 𝑢⟩ ∣ (𝑦𝐵𝑢 = 𝑆)}
5553, 54brabga 4954 . . . . . . . . . . . 12 ((𝑅𝐵𝑤 ∈ V) → (𝑅(𝑦𝐵𝑆)𝑤 ↔ (𝑅𝐵𝑤 = 𝑇)))
564, 47, 55sylancl 693 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑅(𝑦𝐵𝑆)𝑤 ↔ (𝑅𝐵𝑤 = 𝑇)))
57 id 22 . . . . . . . . . . . . 13 (𝑥𝐴𝑥𝐴)
58 eqid 2621 . . . . . . . . . . . . . 14 (𝑥𝐴𝑅) = (𝑥𝐴𝑅)
5958fvmpt2 6253 . . . . . . . . . . . . 13 ((𝑥𝐴𝑅𝐵) → ((𝑥𝐴𝑅)‘𝑥) = 𝑅)
6057, 4, 59syl2an2 874 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝑥𝐴𝑅)‘𝑥) = 𝑅)
6160breq1d 4628 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑅(𝑦𝐵𝑆)𝑤))
624biantrurd 529 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑤 = 𝑇 ↔ (𝑅𝐵𝑤 = 𝑇)))
6356, 61, 623bitr4d 300 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇))
6463expcom 451 . . . . . . . . 9 (𝑥𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇)))
6531, 40, 46, 64vtoclgaf 3260 . . . . . . . 8 (𝑧𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
6665impcom 446 . . . . . . 7 ((𝜑𝑧𝐴) → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))
6766pm5.32da 672 . . . . . 6 (𝜑 → ((𝑧𝐴 ∧ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
6830, 67bitrd 268 . . . . 5 (𝜑 → ((𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
6919, 68syl5bb 272 . . . 4 (𝜑 → (∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤)) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
7014, 69bitrd 268 . . 3 (𝜑 → (∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
71 vex 3192 . . . 4 𝑧 ∈ V
7271, 47opelco 5258 . . 3 (⟨𝑧, 𝑤⟩ ∈ (𝐺𝐹) ↔ ∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤))
73 df-mpt 4680 . . . . 5 (𝑥𝐴𝑇) = {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)}
7473eleq2i 2690 . . . 4 (⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇) ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)})
75 nfv 1840 . . . . . 6 𝑥 𝑧𝐴
7637nfeq2 2776 . . . . . 6 𝑥 𝑣 = 𝑧 / 𝑥𝑇
7775, 76nfan 1825 . . . . 5 𝑥(𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇)
78 nfv 1840 . . . . 5 𝑣(𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)
79 eleq1 2686 . . . . . 6 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
8043eqeq2d 2631 . . . . . 6 (𝑥 = 𝑧 → (𝑣 = 𝑇𝑣 = 𝑧 / 𝑥𝑇))
8179, 80anbi12d 746 . . . . 5 (𝑥 = 𝑧 → ((𝑥𝐴𝑣 = 𝑇) ↔ (𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇)))
82 eqeq1 2625 . . . . . 6 (𝑣 = 𝑤 → (𝑣 = 𝑧 / 𝑥𝑇𝑤 = 𝑧 / 𝑥𝑇))
8382anbi2d 739 . . . . 5 (𝑣 = 𝑤 → ((𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
8477, 78, 71, 47, 81, 83opelopabf 4965 . . . 4 (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)} ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇))
8574, 84bitri 264 . . 3 (⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇))
8670, 72, 853bitr4g 303 . 2 (𝜑 → (⟨𝑧, 𝑤⟩ ∈ (𝐺𝐹) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇)))
871, 2, 86eqrelrdv 5182 1 (𝜑 → (𝐺𝐹) = (𝑥𝐴𝑇))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wex 1701  wcel 1987  Vcvv 3189  csb 3518  cop 4159   class class class wbr 4618  {copab 4677  cmpt 4678  dom cdm 5079  ccom 5083  Fun wfun 5846  wf 5848  cfv 5852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-fv 5860
This theorem is referenced by:  fmptcof  6358  fcompt  6360  fcoconst  6361  ofco  6877  ccatco  13526  lo1o12  14206  rlimcn1  14261  rlimcn1b  14262  rlimdiv  14318  ackbijnn  14496  setcepi  16670  prf1st  16776  prf2nd  16777  hofcllem  16830  prdsidlem  17254  pws0g  17258  pwsco1mhm  17302  pwsco2mhm  17303  pwsinvg  17460  pwssub  17461  galactghm  17755  efginvrel1  18073  frgpup3lem  18122  gsumzf1o  18245  gsumconst  18266  gsummptshft  18268  gsumzmhm  18269  gsummhm2  18271  gsummptmhm  18272  gsumsub  18280  gsum2dlem2  18302  dprdfsub  18352  lmhmvsca  18977  psrass1lem  19309  psrlinv  19329  psrcom  19341  evlslem2  19444  coe1fval3  19510  psropprmul  19540  coe1z  19565  coe1mul2  19571  coe1tm  19575  ply1coe  19598  evls1sca  19620  frgpcyg  19854  evpmodpmf1o  19874  mhmvlin  20135  ofco2  20189  mdetleib2  20326  mdetralt  20346  smadiadetlem3  20406  ptrescn  21365  lmcn2  21375  qtopeu  21442  flfcnp2  21734  tgpconncomp  21839  tsmsmhm  21872  tsmssub  21875  tsmsxplem1  21879  negfcncf  22645  pcopt  22745  pcopt2  22746  pi1xfrcnvlem  22779  ovolctb  23181  ovolfs2  23262  uniioombllem2  23274  uniioombllem3  23276  ismbf  23320  mbfconst  23325  ismbfcn2  23329  itg1climres  23404  iblabslem  23517  iblabs  23518  bddmulibl  23528  limccnp  23578  limccnp2  23579  limcco  23580  dvcof  23634  dvcjbr  23635  dvcj  23636  dvfre  23637  dvmptcj  23654  dvmptco  23658  dvcnvlem  23660  dvef  23664  dvlip  23677  dvlipcn  23678  itgsubstlem  23732  plypf1  23889  plyco  23918  dgrcolem1  23950  dgrcolem2  23951  dgrco  23952  plycjlem  23953  taylply2  24043  logcn  24310  leibpi  24586  efrlim  24613  jensenlem2  24631  amgmlem  24633  lgamgulmlem2  24673  lgamcvg2  24698  ftalem7  24722  lgseisenlem4  25020  dchrisum0  25126  cofmpt  29329  ofcfval4  29972  eulerpartgbij  30239  dstfrvclim1  30344  cvmliftlem6  31015  cvmliftphtlem  31042  cvmlift3lem5  31048  elmsubrn  31168  msubco  31171  circum  31311  mblfinlem2  33114  volsupnfl  33121  itgaddnc  33137  itgmulc2nc  33145  ftc1anclem1  33152  ftc1anclem2  33153  ftc1anclem3  33154  ftc1anclem4  33155  ftc1anclem5  33156  ftc1anclem6  33157  ftc1anclem7  33158  ftc1anclem8  33159  fnopabco  33184  upixp  33191  mendassa  37280  fsovrfovd  37820  fsovcnvlem  37824  cncfcompt  39427  dvcosax  39474  dirkercncflem4  39656  fourierdlem111  39767  meadjiunlem  40015  meadjiun  40016  amgmwlem  41877  amgmlemALT  41878
  Copyright terms: Public domain W3C validator