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

Theorem fmptco 6882
 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 6074 . 2 Rel (𝐺𝐹)
2 mptrel 5666 . 2 Rel (𝑥𝐴𝑇)
3 fmptco.2 . . . . . . . . . . . 12 (𝜑𝐹 = (𝑥𝐴𝑅))
4 fmptco.1 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 𝑅𝐵)
53, 4fmpt3d 6871 . . . . . . . . . . 11 (𝜑𝐹:𝐴𝐵)
65ffund 6502 . . . . . . . . . 10 (𝜑 → Fun 𝐹)
7 funbrfv 6704 . . . . . . . . . . 11 (Fun 𝐹 → (𝑧𝐹𝑢 → (𝐹𝑧) = 𝑢))
87imp 410 . . . . . . . . . 10 ((Fun 𝐹𝑧𝐹𝑢) → (𝐹𝑧) = 𝑢)
96, 8sylan 583 . . . . . . . . 9 ((𝜑𝑧𝐹𝑢) → (𝐹𝑧) = 𝑢)
109eqcomd 2764 . . . . . . . 8 ((𝜑𝑧𝐹𝑢) → 𝑢 = (𝐹𝑧))
1110a1d 25 . . . . . . 7 ((𝜑𝑧𝐹𝑢) → (𝑢𝐺𝑤𝑢 = (𝐹𝑧)))
1211expimpd 457 . . . . . 6 (𝜑 → ((𝑧𝐹𝑢𝑢𝐺𝑤) → 𝑢 = (𝐹𝑧)))
1312pm4.71rd 566 . . . . 5 (𝜑 → ((𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤))))
1413exbidv 1922 . . . 4 (𝜑 → (∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤) ↔ ∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤))))
15 fvex 6671 . . . . . 6 (𝐹𝑧) ∈ V
16 breq2 5036 . . . . . . 7 (𝑢 = (𝐹𝑧) → (𝑧𝐹𝑢𝑧𝐹(𝐹𝑧)))
17 breq1 5035 . . . . . . 7 (𝑢 = (𝐹𝑧) → (𝑢𝐺𝑤 ↔ (𝐹𝑧)𝐺𝑤))
1816, 17anbi12d 633 . . . . . 6 (𝑢 = (𝐹𝑧) → ((𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤)))
1915, 18ceqsexv 3458 . . . . 5 (∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤)) ↔ (𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤))
20 funfvbrb 6812 . . . . . . . . 9 (Fun 𝐹 → (𝑧 ∈ dom 𝐹𝑧𝐹(𝐹𝑧)))
216, 20syl 17 . . . . . . . 8 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐹(𝐹𝑧)))
225fdmd 6508 . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝐴)
2322eleq2d 2837 . . . . . . . 8 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐴))
2421, 23bitr3d 284 . . . . . . 7 (𝜑 → (𝑧𝐹(𝐹𝑧) ↔ 𝑧𝐴))
253fveq1d 6660 . . . . . . . 8 (𝜑 → (𝐹𝑧) = ((𝑥𝐴𝑅)‘𝑧))
26 fmptco.3 . . . . . . . 8 (𝜑𝐺 = (𝑦𝐵𝑆))
27 eqidd 2759 . . . . . . . 8 (𝜑𝑤 = 𝑤)
2825, 26, 27breq123d 5046 . . . . . . 7 (𝜑 → ((𝐹𝑧)𝐺𝑤 ↔ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤))
2924, 28anbi12d 633 . . . . . 6 (𝜑 → ((𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤) ↔ (𝑧𝐴 ∧ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤)))
30 nfcv 2919 . . . . . . . . 9 𝑥𝑧
31 nfv 1915 . . . . . . . . . 10 𝑥𝜑
32 nffvmpt1 6669 . . . . . . . . . . . 12 𝑥((𝑥𝐴𝑅)‘𝑧)
33 nfcv 2919 . . . . . . . . . . . 12 𝑥(𝑦𝐵𝑆)
34 nfcv 2919 . . . . . . . . . . . 12 𝑥𝑤
3532, 33, 34nfbr 5079 . . . . . . . . . . 11 𝑥((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤
36 nfcsb1v 3829 . . . . . . . . . . . 12 𝑥𝑧 / 𝑥𝑇
3736nfeq2 2936 . . . . . . . . . . 11 𝑥 𝑤 = 𝑧 / 𝑥𝑇
3835, 37nfbi 1904 . . . . . . . . . 10 𝑥(((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)
3931, 38nfim 1897 . . . . . . . . 9 𝑥(𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))
40 fveq2 6658 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑥𝐴𝑅)‘𝑥) = ((𝑥𝐴𝑅)‘𝑧))
4140breq1d 5042 . . . . . . . . . . 11 (𝑥 = 𝑧 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤 ↔ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤))
42 csbeq1a 3819 . . . . . . . . . . . 12 (𝑥 = 𝑧𝑇 = 𝑧 / 𝑥𝑇)
4342eqeq2d 2769 . . . . . . . . . . 11 (𝑥 = 𝑧 → (𝑤 = 𝑇𝑤 = 𝑧 / 𝑥𝑇))
4441, 43bibi12d 349 . . . . . . . . . 10 (𝑥 = 𝑧 → ((((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇) ↔ (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
4544imbi2d 344 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇)) ↔ (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))))
46 vex 3413 . . . . . . . . . . . 12 𝑤 ∈ V
47 simpl 486 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑅𝑢 = 𝑤) → 𝑦 = 𝑅)
4847eleq1d 2836 . . . . . . . . . . . . . 14 ((𝑦 = 𝑅𝑢 = 𝑤) → (𝑦𝐵𝑅𝐵))
49 id 22 . . . . . . . . . . . . . . 15 (𝑢 = 𝑤𝑢 = 𝑤)
50 fmptco.4 . . . . . . . . . . . . . . 15 (𝑦 = 𝑅𝑆 = 𝑇)
5149, 50eqeqan12rd 2777 . . . . . . . . . . . . . 14 ((𝑦 = 𝑅𝑢 = 𝑤) → (𝑢 = 𝑆𝑤 = 𝑇))
5248, 51anbi12d 633 . . . . . . . . . . . . 13 ((𝑦 = 𝑅𝑢 = 𝑤) → ((𝑦𝐵𝑢 = 𝑆) ↔ (𝑅𝐵𝑤 = 𝑇)))
53 df-mpt 5113 . . . . . . . . . . . . 13 (𝑦𝐵𝑆) = {⟨𝑦, 𝑢⟩ ∣ (𝑦𝐵𝑢 = 𝑆)}
5452, 53brabga 5391 . . . . . . . . . . . 12 ((𝑅𝐵𝑤 ∈ V) → (𝑅(𝑦𝐵𝑆)𝑤 ↔ (𝑅𝐵𝑤 = 𝑇)))
554, 46, 54sylancl 589 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑅(𝑦𝐵𝑆)𝑤 ↔ (𝑅𝐵𝑤 = 𝑇)))
56 id 22 . . . . . . . . . . . . 13 (𝑥𝐴𝑥𝐴)
57 eqid 2758 . . . . . . . . . . . . . 14 (𝑥𝐴𝑅) = (𝑥𝐴𝑅)
5857fvmpt2 6770 . . . . . . . . . . . . 13 ((𝑥𝐴𝑅𝐵) → ((𝑥𝐴𝑅)‘𝑥) = 𝑅)
5956, 4, 58syl2an2 685 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝑥𝐴𝑅)‘𝑥) = 𝑅)
6059breq1d 5042 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑅(𝑦𝐵𝑆)𝑤))
614biantrurd 536 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑤 = 𝑇 ↔ (𝑅𝐵𝑤 = 𝑇)))
6255, 60, 613bitr4d 314 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇))
6362expcom 417 . . . . . . . . 9 (𝑥𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇)))
6430, 39, 45, 63vtoclgaf 3491 . . . . . . . 8 (𝑧𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
6564impcom 411 . . . . . . 7 ((𝜑𝑧𝐴) → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))
6665pm5.32da 582 . . . . . 6 (𝜑 → ((𝑧𝐴 ∧ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
6729, 66bitrd 282 . . . . 5 (𝜑 → ((𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
6819, 67syl5bb 286 . . . 4 (𝜑 → (∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤)) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
6914, 68bitrd 282 . . 3 (𝜑 → (∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
70 vex 3413 . . . 4 𝑧 ∈ V
7170, 46opelco 5711 . . 3 (⟨𝑧, 𝑤⟩ ∈ (𝐺𝐹) ↔ ∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤))
72 df-mpt 5113 . . . . 5 (𝑥𝐴𝑇) = {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)}
7372eleq2i 2843 . . . 4 (⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇) ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)})
74 nfv 1915 . . . . . 6 𝑥 𝑧𝐴
7536nfeq2 2936 . . . . . 6 𝑥 𝑣 = 𝑧 / 𝑥𝑇
7674, 75nfan 1900 . . . . 5 𝑥(𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇)
77 nfv 1915 . . . . 5 𝑣(𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)
78 eleq1w 2834 . . . . . 6 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
7942eqeq2d 2769 . . . . . 6 (𝑥 = 𝑧 → (𝑣 = 𝑇𝑣 = 𝑧 / 𝑥𝑇))
8078, 79anbi12d 633 . . . . 5 (𝑥 = 𝑧 → ((𝑥𝐴𝑣 = 𝑇) ↔ (𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇)))
81 eqeq1 2762 . . . . . 6 (𝑣 = 𝑤 → (𝑣 = 𝑧 / 𝑥𝑇𝑤 = 𝑧 / 𝑥𝑇))
8281anbi2d 631 . . . . 5 (𝑣 = 𝑤 → ((𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
8376, 77, 70, 46, 80, 82opelopabf 5402 . . . 4 (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)} ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇))
8473, 83bitri 278 . . 3 (⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇))
8569, 71, 843bitr4g 317 . 2 (𝜑 → (⟨𝑧, 𝑤⟩ ∈ (𝐺𝐹) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇)))
861, 2, 85eqrelrdv 5634 1 (𝜑 → (𝐺𝐹) = (𝑥𝐴𝑇))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  Vcvv 3409  ⦋csb 3805  ⟨cop 4528   class class class wbr 5032  {copab 5094   ↦ cmpt 5112  dom cdm 5524   ∘ ccom 5528  Fun wfun 6329  ‘cfv 6335 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-fv 6343 This theorem is referenced by:  fmptcof  6883  cofmpt  6885  fcompt  6886  fcoconst  6887  ofco  7427  ccatco  14244  rlimcn1  14993  rlimdiv  15050  ackbijnn  15231  setcepi  17414  prf1st  17520  prf2nd  17521  hofcllem  17574  prdsidlem  18009  pws0g  18013  pwsco1mhm  18062  pwsco2mhm  18063  smndex1iidm  18132  smndex2dlinvh  18148  pwsinvg  18279  pwssub  18280  galactghm  18599  efginvrel1  18921  frgpup3lem  18970  gsumzf1o  19100  gsumconst  19122  gsummptshft  19124  gsumzmhm  19125  gsummhm2  19127  gsummptmhm  19128  gsumsub  19136  gsum2dlem2  19159  dprdfsub  19211  lmhmvsca  19885  frgpcyg  20341  evpmodpmf1o  20361  psrass1lemOLD  20702  psrass1lem  20705  psrlinv  20725  psrcom  20737  evlslem2  20842  coe1fval3  20932  psropprmul  20962  coe1z  20987  coe1mul2  20993  coe1tm  20997  ply1coe  21020  evls1sca  21042  mhmvlin  21099  ofco2  21151  mdetleib2  21288  mdetralt  21308  smadiadetlem3  21368  ptrescn  22339  lmcn2  22349  qtopeu  22416  flfcnp2  22707  tgpconncomp  22813  tsmssub  22849  tsmsxplem1  22853  negfcncf  23624  pcopt  23723  pcopt2  23724  pi1xfrcnvlem  23757  ovolctb  24190  ovolfs2  24271  uniioombllem2  24283  ismbf  24328  mbfconst  24333  limccnp2  24591  limcco  24592  dvcof  24647  dvcj  24649  dvfre  24650  dvmptcj  24667  dvmptco  24671  dvcnvlem  24675  dvlip  24692  dvlipcn  24693  itgsubstlem  24747  plyco  24937  dgrcolem1  24969  dgrcolem2  24970  dgrco  24971  plycjlem  24972  taylply2  25062  logcn  25337  leibpi  25627  efrlim  25654  jensenlem2  25672  amgmlem  25674  ftalem7  25763  dchrisum0  26203  ofcfval4  31592  eulerpartgbij  31858  dstfrvclim1  31963  cvmliftlem6  32768  cvmliftphtlem  32795  cvmlift3lem5  32801  elmsubrn  33006  msubco  33009  circum  33148  mblfinlem2  35375  volsupnfl  35382  itgaddnc  35397  itgmulc2nc  35405  ftc1anclem1  35410  ftc1anclem2  35411  ftc1anclem3  35412  ftc1anclem4  35413  ftc1anclem5  35414  ftc1anclem7  35416  ftc1anclem8  35417  fnopabco  35441  upixp  35447  mendassa  40511  fsovrfovd  41083  fsovcnvlem  41087  cncfcompt  42891  dvcosax  42934  dirkercncflem4  43114  fourierdlem111  43225  meadjiunlem  43470  meadjiun  43471  fundcmpsurbijinjpreimafv  44292  itcovalpclem2  45450  itcovalt2lem2  45455  amgmwlem  45721  amgmlemALT  45722
 Copyright terms: Public domain W3C validator