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

Theorem fmptco 7127
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 6108 . 2 Rel (𝐺𝐹)
2 mptrel 5826 . 2 Rel (𝑥𝐴𝑇)
3 fmptco.2 . . . . . . . . . . . 12 (𝜑𝐹 = (𝑥𝐴𝑅))
4 fmptco.1 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 𝑅𝐵)
53, 4fmpt3d 7116 . . . . . . . . . . 11 (𝜑𝐹:𝐴𝐵)
65ffund 6722 . . . . . . . . . 10 (𝜑 → Fun 𝐹)
7 funbrfv 6943 . . . . . . . . . . 11 (Fun 𝐹 → (𝑧𝐹𝑢 → (𝐹𝑧) = 𝑢))
87imp 408 . . . . . . . . . 10 ((Fun 𝐹𝑧𝐹𝑢) → (𝐹𝑧) = 𝑢)
96, 8sylan 581 . . . . . . . . 9 ((𝜑𝑧𝐹𝑢) → (𝐹𝑧) = 𝑢)
109eqcomd 2739 . . . . . . . 8 ((𝜑𝑧𝐹𝑢) → 𝑢 = (𝐹𝑧))
1110a1d 25 . . . . . . 7 ((𝜑𝑧𝐹𝑢) → (𝑢𝐺𝑤𝑢 = (𝐹𝑧)))
1211expimpd 455 . . . . . 6 (𝜑 → ((𝑧𝐹𝑢𝑢𝐺𝑤) → 𝑢 = (𝐹𝑧)))
1312pm4.71rd 564 . . . . 5 (𝜑 → ((𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤))))
1413exbidv 1925 . . . 4 (𝜑 → (∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤) ↔ ∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤))))
15 fvex 6905 . . . . . 6 (𝐹𝑧) ∈ V
16 breq2 5153 . . . . . . 7 (𝑢 = (𝐹𝑧) → (𝑧𝐹𝑢𝑧𝐹(𝐹𝑧)))
17 breq1 5152 . . . . . . 7 (𝑢 = (𝐹𝑧) → (𝑢𝐺𝑤 ↔ (𝐹𝑧)𝐺𝑤))
1816, 17anbi12d 632 . . . . . 6 (𝑢 = (𝐹𝑧) → ((𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤)))
1915, 18ceqsexv 3526 . . . . 5 (∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤)) ↔ (𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤))
20 funfvbrb 7053 . . . . . . . . 9 (Fun 𝐹 → (𝑧 ∈ dom 𝐹𝑧𝐹(𝐹𝑧)))
216, 20syl 17 . . . . . . . 8 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐹(𝐹𝑧)))
225fdmd 6729 . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝐴)
2322eleq2d 2820 . . . . . . . 8 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐴))
2421, 23bitr3d 281 . . . . . . 7 (𝜑 → (𝑧𝐹(𝐹𝑧) ↔ 𝑧𝐴))
253fveq1d 6894 . . . . . . . 8 (𝜑 → (𝐹𝑧) = ((𝑥𝐴𝑅)‘𝑧))
26 fmptco.3 . . . . . . . 8 (𝜑𝐺 = (𝑦𝐵𝑆))
27 eqidd 2734 . . . . . . . 8 (𝜑𝑤 = 𝑤)
2825, 26, 27breq123d 5163 . . . . . . 7 (𝜑 → ((𝐹𝑧)𝐺𝑤 ↔ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤))
2924, 28anbi12d 632 . . . . . 6 (𝜑 → ((𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤) ↔ (𝑧𝐴 ∧ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤)))
30 nfcv 2904 . . . . . . . . 9 𝑥𝑧
31 nfv 1918 . . . . . . . . . 10 𝑥𝜑
32 nffvmpt1 6903 . . . . . . . . . . . 12 𝑥((𝑥𝐴𝑅)‘𝑧)
33 nfcv 2904 . . . . . . . . . . . 12 𝑥(𝑦𝐵𝑆)
34 nfcv 2904 . . . . . . . . . . . 12 𝑥𝑤
3532, 33, 34nfbr 5196 . . . . . . . . . . 11 𝑥((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤
36 nfcsb1v 3919 . . . . . . . . . . . 12 𝑥𝑧 / 𝑥𝑇
3736nfeq2 2921 . . . . . . . . . . 11 𝑥 𝑤 = 𝑧 / 𝑥𝑇
3835, 37nfbi 1907 . . . . . . . . . 10 𝑥(((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)
3931, 38nfim 1900 . . . . . . . . 9 𝑥(𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))
40 fveq2 6892 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑥𝐴𝑅)‘𝑥) = ((𝑥𝐴𝑅)‘𝑧))
4140breq1d 5159 . . . . . . . . . . 11 (𝑥 = 𝑧 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤 ↔ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤))
42 csbeq1a 3908 . . . . . . . . . . . 12 (𝑥 = 𝑧𝑇 = 𝑧 / 𝑥𝑇)
4342eqeq2d 2744 . . . . . . . . . . 11 (𝑥 = 𝑧 → (𝑤 = 𝑇𝑤 = 𝑧 / 𝑥𝑇))
4441, 43bibi12d 346 . . . . . . . . . 10 (𝑥 = 𝑧 → ((((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇) ↔ (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
4544imbi2d 341 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇)) ↔ (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))))
46 vex 3479 . . . . . . . . . . . 12 𝑤 ∈ V
47 simpl 484 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑅𝑢 = 𝑤) → 𝑦 = 𝑅)
4847eleq1d 2819 . . . . . . . . . . . . . 14 ((𝑦 = 𝑅𝑢 = 𝑤) → (𝑦𝐵𝑅𝐵))
49 id 22 . . . . . . . . . . . . . . 15 (𝑢 = 𝑤𝑢 = 𝑤)
50 fmptco.4 . . . . . . . . . . . . . . 15 (𝑦 = 𝑅𝑆 = 𝑇)
5149, 50eqeqan12rd 2748 . . . . . . . . . . . . . 14 ((𝑦 = 𝑅𝑢 = 𝑤) → (𝑢 = 𝑆𝑤 = 𝑇))
5248, 51anbi12d 632 . . . . . . . . . . . . 13 ((𝑦 = 𝑅𝑢 = 𝑤) → ((𝑦𝐵𝑢 = 𝑆) ↔ (𝑅𝐵𝑤 = 𝑇)))
53 df-mpt 5233 . . . . . . . . . . . . 13 (𝑦𝐵𝑆) = {⟨𝑦, 𝑢⟩ ∣ (𝑦𝐵𝑢 = 𝑆)}
5452, 53brabga 5535 . . . . . . . . . . . 12 ((𝑅𝐵𝑤 ∈ V) → (𝑅(𝑦𝐵𝑆)𝑤 ↔ (𝑅𝐵𝑤 = 𝑇)))
554, 46, 54sylancl 587 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑅(𝑦𝐵𝑆)𝑤 ↔ (𝑅𝐵𝑤 = 𝑇)))
56 id 22 . . . . . . . . . . . . 13 (𝑥𝐴𝑥𝐴)
57 eqid 2733 . . . . . . . . . . . . . 14 (𝑥𝐴𝑅) = (𝑥𝐴𝑅)
5857fvmpt2 7010 . . . . . . . . . . . . 13 ((𝑥𝐴𝑅𝐵) → ((𝑥𝐴𝑅)‘𝑥) = 𝑅)
5956, 4, 58syl2an2 685 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝑥𝐴𝑅)‘𝑥) = 𝑅)
6059breq1d 5159 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑅(𝑦𝐵𝑆)𝑤))
614biantrurd 534 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑤 = 𝑇 ↔ (𝑅𝐵𝑤 = 𝑇)))
6255, 60, 613bitr4d 311 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇))
6362expcom 415 . . . . . . . . 9 (𝑥𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇)))
6430, 39, 45, 63vtoclgaf 3565 . . . . . . . 8 (𝑧𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
6564impcom 409 . . . . . . 7 ((𝜑𝑧𝐴) → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))
6665pm5.32da 580 . . . . . 6 (𝜑 → ((𝑧𝐴 ∧ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
6729, 66bitrd 279 . . . . 5 (𝜑 → ((𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
6819, 67bitrid 283 . . . 4 (𝜑 → (∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤)) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
6914, 68bitrd 279 . . 3 (𝜑 → (∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
70 vex 3479 . . . 4 𝑧 ∈ V
7170, 46opelco 5872 . . 3 (⟨𝑧, 𝑤⟩ ∈ (𝐺𝐹) ↔ ∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤))
72 df-mpt 5233 . . . . 5 (𝑥𝐴𝑇) = {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)}
7372eleq2i 2826 . . . 4 (⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇) ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)})
74 nfv 1918 . . . . . 6 𝑥 𝑧𝐴
7536nfeq2 2921 . . . . . 6 𝑥 𝑣 = 𝑧 / 𝑥𝑇
7674, 75nfan 1903 . . . . 5 𝑥(𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇)
77 nfv 1918 . . . . 5 𝑣(𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)
78 eleq1w 2817 . . . . . 6 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
7942eqeq2d 2744 . . . . . 6 (𝑥 = 𝑧 → (𝑣 = 𝑇𝑣 = 𝑧 / 𝑥𝑇))
8078, 79anbi12d 632 . . . . 5 (𝑥 = 𝑧 → ((𝑥𝐴𝑣 = 𝑇) ↔ (𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇)))
81 eqeq1 2737 . . . . . 6 (𝑣 = 𝑤 → (𝑣 = 𝑧 / 𝑥𝑇𝑤 = 𝑧 / 𝑥𝑇))
8281anbi2d 630 . . . . 5 (𝑣 = 𝑤 → ((𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
8376, 77, 70, 46, 80, 82opelopabf 5546 . . . 4 (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)} ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇))
8473, 83bitri 275 . . 3 (⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇))
8569, 71, 843bitr4g 314 . 2 (𝜑 → (⟨𝑧, 𝑤⟩ ∈ (𝐺𝐹) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇)))
861, 2, 85eqrelrdv 5793 1 (𝜑 → (𝐺𝐹) = (𝑥𝐴𝑇))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wex 1782  wcel 2107  Vcvv 3475  csb 3894  cop 4635   class class class wbr 5149  {copab 5211  cmpt 5232  dom cdm 5677  ccom 5681  Fun wfun 6538  cfv 6544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552
This theorem is referenced by:  fmptcof  7128  cofmpt  7130  fcompt  7131  fcoconst  7132  ofco  7693  ccatco  14786  rlimcn1  15532  rlimdiv  15592  ackbijnn  15774  setcepi  18038  prf1st  18156  prf2nd  18157  hofcllem  18211  prdsidlem  18657  pws0g  18661  pwsco1mhm  18713  pwsco2mhm  18714  smndex1iidm  18782  smndex2dlinvh  18798  pwsinvg  18936  pwssub  18937  galactghm  19272  efginvrel1  19596  frgpup3lem  19645  gsumzf1o  19780  gsumconst  19802  gsummptshft  19804  gsumzmhm  19805  gsummhm2  19807  gsummptmhm  19808  gsumsub  19816  gsum2dlem2  19839  dprdfsub  19891  lmhmvsca  20656  frgpcyg  21129  evpmodpmf1o  21149  psrass1lemOLD  21493  psrass1lem  21496  psrlinv  21516  psrcom  21529  evlslem2  21642  coe1fval3  21732  psropprmul  21760  coe1z  21785  coe1mul2  21791  coe1tm  21795  ply1coe  21820  evls1sca  21842  mhmvlin  21899  ofco2  21953  mdetleib2  22090  mdetralt  22110  smadiadetlem3  22170  ptrescn  23143  lmcn2  23153  qtopeu  23220  flfcnp2  23511  tgpconncomp  23617  tsmssub  23653  tsmsxplem1  23657  negfcncf  24439  pcopt  24538  pcopt2  24539  pi1xfrcnvlem  24572  ovolctb  25007  ovolfs2  25088  uniioombllem2  25100  ismbf  25145  mbfconst  25150  limccnp2  25409  limcco  25410  dvcof  25465  dvcj  25467  dvfre  25468  dvmptcj  25485  dvmptco  25489  dvcnvlem  25493  dvlip  25510  dvlipcn  25511  itgsubstlem  25565  plyco  25755  dgrcolem1  25787  dgrcolem2  25788  dgrco  25789  plycjlem  25790  taylply2  25880  logcn  26155  leibpi  26447  efrlim  26474  jensenlem2  26492  amgmlem  26494  ftalem7  26583  dchrisum0  27023  ghmquskerco  32529  ofcfval4  33103  eulerpartgbij  33371  dstfrvclim1  33476  cvmliftlem6  34281  cvmliftphtlem  34308  cvmlift3lem5  34314  elmsubrn  34519  msubco  34522  circum  34659  mblfinlem2  36526  volsupnfl  36533  itgaddnc  36548  itgmulc2nc  36556  ftc1anclem1  36561  ftc1anclem2  36562  ftc1anclem3  36563  ftc1anclem4  36564  ftc1anclem5  36565  ftc1anclem7  36567  ftc1anclem8  36568  fnopabco  36591  upixp  36597  selvvvval  41157  evlselv  41159  mendassa  41936  fsovrfovd  42760  fsovcnvlem  42764  cncfcompt  44599  dvcosax  44642  dirkercncflem4  44822  fourierdlem111  44933  meadjiunlem  45181  meadjiun  45182  fundcmpsurbijinjpreimafv  46075  itcovalpclem2  47357  itcovalt2lem2  47362  amgmwlem  47849  amgmlemALT  47850
  Copyright terms: Public domain W3C validator