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

Theorem fmptco 7123
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 6104 . 2 Rel (𝐺𝐹)
2 mptrel 5823 . 2 Rel (𝑥𝐴𝑇)
3 fmptco.2 . . . . . . . . . . . 12 (𝜑𝐹 = (𝑥𝐴𝑅))
4 fmptco.1 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 𝑅𝐵)
53, 4fmpt3d 7112 . . . . . . . . . . 11 (𝜑𝐹:𝐴𝐵)
65ffund 6718 . . . . . . . . . 10 (𝜑 → Fun 𝐹)
7 funbrfv 6939 . . . . . . . . . . 11 (Fun 𝐹 → (𝑧𝐹𝑢 → (𝐹𝑧) = 𝑢))
87imp 407 . . . . . . . . . 10 ((Fun 𝐹𝑧𝐹𝑢) → (𝐹𝑧) = 𝑢)
96, 8sylan 580 . . . . . . . . 9 ((𝜑𝑧𝐹𝑢) → (𝐹𝑧) = 𝑢)
109eqcomd 2738 . . . . . . . 8 ((𝜑𝑧𝐹𝑢) → 𝑢 = (𝐹𝑧))
1110a1d 25 . . . . . . 7 ((𝜑𝑧𝐹𝑢) → (𝑢𝐺𝑤𝑢 = (𝐹𝑧)))
1211expimpd 454 . . . . . 6 (𝜑 → ((𝑧𝐹𝑢𝑢𝐺𝑤) → 𝑢 = (𝐹𝑧)))
1312pm4.71rd 563 . . . . 5 (𝜑 → ((𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤))))
1413exbidv 1924 . . . 4 (𝜑 → (∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤) ↔ ∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤))))
15 fvex 6901 . . . . . 6 (𝐹𝑧) ∈ V
16 breq2 5151 . . . . . . 7 (𝑢 = (𝐹𝑧) → (𝑧𝐹𝑢𝑧𝐹(𝐹𝑧)))
17 breq1 5150 . . . . . . 7 (𝑢 = (𝐹𝑧) → (𝑢𝐺𝑤 ↔ (𝐹𝑧)𝐺𝑤))
1816, 17anbi12d 631 . . . . . 6 (𝑢 = (𝐹𝑧) → ((𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤)))
1915, 18ceqsexv 3525 . . . . 5 (∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤)) ↔ (𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤))
20 funfvbrb 7049 . . . . . . . . 9 (Fun 𝐹 → (𝑧 ∈ dom 𝐹𝑧𝐹(𝐹𝑧)))
216, 20syl 17 . . . . . . . 8 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐹(𝐹𝑧)))
225fdmd 6725 . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝐴)
2322eleq2d 2819 . . . . . . . 8 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐴))
2421, 23bitr3d 280 . . . . . . 7 (𝜑 → (𝑧𝐹(𝐹𝑧) ↔ 𝑧𝐴))
253fveq1d 6890 . . . . . . . 8 (𝜑 → (𝐹𝑧) = ((𝑥𝐴𝑅)‘𝑧))
26 fmptco.3 . . . . . . . 8 (𝜑𝐺 = (𝑦𝐵𝑆))
27 eqidd 2733 . . . . . . . 8 (𝜑𝑤 = 𝑤)
2825, 26, 27breq123d 5161 . . . . . . 7 (𝜑 → ((𝐹𝑧)𝐺𝑤 ↔ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤))
2924, 28anbi12d 631 . . . . . 6 (𝜑 → ((𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤) ↔ (𝑧𝐴 ∧ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤)))
30 nfcv 2903 . . . . . . . . 9 𝑥𝑧
31 nfv 1917 . . . . . . . . . 10 𝑥𝜑
32 nffvmpt1 6899 . . . . . . . . . . . 12 𝑥((𝑥𝐴𝑅)‘𝑧)
33 nfcv 2903 . . . . . . . . . . . 12 𝑥(𝑦𝐵𝑆)
34 nfcv 2903 . . . . . . . . . . . 12 𝑥𝑤
3532, 33, 34nfbr 5194 . . . . . . . . . . 11 𝑥((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤
36 nfcsb1v 3917 . . . . . . . . . . . 12 𝑥𝑧 / 𝑥𝑇
3736nfeq2 2920 . . . . . . . . . . 11 𝑥 𝑤 = 𝑧 / 𝑥𝑇
3835, 37nfbi 1906 . . . . . . . . . 10 𝑥(((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)
3931, 38nfim 1899 . . . . . . . . 9 𝑥(𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))
40 fveq2 6888 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑥𝐴𝑅)‘𝑥) = ((𝑥𝐴𝑅)‘𝑧))
4140breq1d 5157 . . . . . . . . . . 11 (𝑥 = 𝑧 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤 ↔ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤))
42 csbeq1a 3906 . . . . . . . . . . . 12 (𝑥 = 𝑧𝑇 = 𝑧 / 𝑥𝑇)
4342eqeq2d 2743 . . . . . . . . . . 11 (𝑥 = 𝑧 → (𝑤 = 𝑇𝑤 = 𝑧 / 𝑥𝑇))
4441, 43bibi12d 345 . . . . . . . . . 10 (𝑥 = 𝑧 → ((((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇) ↔ (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
4544imbi2d 340 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇)) ↔ (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))))
46 vex 3478 . . . . . . . . . . . 12 𝑤 ∈ V
47 simpl 483 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑅𝑢 = 𝑤) → 𝑦 = 𝑅)
4847eleq1d 2818 . . . . . . . . . . . . . 14 ((𝑦 = 𝑅𝑢 = 𝑤) → (𝑦𝐵𝑅𝐵))
49 id 22 . . . . . . . . . . . . . . 15 (𝑢 = 𝑤𝑢 = 𝑤)
50 fmptco.4 . . . . . . . . . . . . . . 15 (𝑦 = 𝑅𝑆 = 𝑇)
5149, 50eqeqan12rd 2747 . . . . . . . . . . . . . 14 ((𝑦 = 𝑅𝑢 = 𝑤) → (𝑢 = 𝑆𝑤 = 𝑇))
5248, 51anbi12d 631 . . . . . . . . . . . . 13 ((𝑦 = 𝑅𝑢 = 𝑤) → ((𝑦𝐵𝑢 = 𝑆) ↔ (𝑅𝐵𝑤 = 𝑇)))
53 df-mpt 5231 . . . . . . . . . . . . 13 (𝑦𝐵𝑆) = {⟨𝑦, 𝑢⟩ ∣ (𝑦𝐵𝑢 = 𝑆)}
5452, 53brabga 5533 . . . . . . . . . . . 12 ((𝑅𝐵𝑤 ∈ V) → (𝑅(𝑦𝐵𝑆)𝑤 ↔ (𝑅𝐵𝑤 = 𝑇)))
554, 46, 54sylancl 586 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑅(𝑦𝐵𝑆)𝑤 ↔ (𝑅𝐵𝑤 = 𝑇)))
56 id 22 . . . . . . . . . . . . 13 (𝑥𝐴𝑥𝐴)
57 eqid 2732 . . . . . . . . . . . . . 14 (𝑥𝐴𝑅) = (𝑥𝐴𝑅)
5857fvmpt2 7006 . . . . . . . . . . . . 13 ((𝑥𝐴𝑅𝐵) → ((𝑥𝐴𝑅)‘𝑥) = 𝑅)
5956, 4, 58syl2an2 684 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝑥𝐴𝑅)‘𝑥) = 𝑅)
6059breq1d 5157 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑅(𝑦𝐵𝑆)𝑤))
614biantrurd 533 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑤 = 𝑇 ↔ (𝑅𝐵𝑤 = 𝑇)))
6255, 60, 613bitr4d 310 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇))
6362expcom 414 . . . . . . . . 9 (𝑥𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇)))
6430, 39, 45, 63vtoclgaf 3564 . . . . . . . 8 (𝑧𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
6564impcom 408 . . . . . . 7 ((𝜑𝑧𝐴) → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))
6665pm5.32da 579 . . . . . 6 (𝜑 → ((𝑧𝐴 ∧ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
6729, 66bitrd 278 . . . . 5 (𝜑 → ((𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
6819, 67bitrid 282 . . . 4 (𝜑 → (∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤)) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
6914, 68bitrd 278 . . 3 (𝜑 → (∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
70 vex 3478 . . . 4 𝑧 ∈ V
7170, 46opelco 5869 . . 3 (⟨𝑧, 𝑤⟩ ∈ (𝐺𝐹) ↔ ∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤))
72 df-mpt 5231 . . . . 5 (𝑥𝐴𝑇) = {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)}
7372eleq2i 2825 . . . 4 (⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇) ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)})
74 nfv 1917 . . . . . 6 𝑥 𝑧𝐴
7536nfeq2 2920 . . . . . 6 𝑥 𝑣 = 𝑧 / 𝑥𝑇
7674, 75nfan 1902 . . . . 5 𝑥(𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇)
77 nfv 1917 . . . . 5 𝑣(𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)
78 eleq1w 2816 . . . . . 6 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
7942eqeq2d 2743 . . . . . 6 (𝑥 = 𝑧 → (𝑣 = 𝑇𝑣 = 𝑧 / 𝑥𝑇))
8078, 79anbi12d 631 . . . . 5 (𝑥 = 𝑧 → ((𝑥𝐴𝑣 = 𝑇) ↔ (𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇)))
81 eqeq1 2736 . . . . . 6 (𝑣 = 𝑤 → (𝑣 = 𝑧 / 𝑥𝑇𝑤 = 𝑧 / 𝑥𝑇))
8281anbi2d 629 . . . . 5 (𝑣 = 𝑤 → ((𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
8376, 77, 70, 46, 80, 82opelopabf 5544 . . . 4 (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)} ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇))
8473, 83bitri 274 . . 3 (⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇))
8569, 71, 843bitr4g 313 . 2 (𝜑 → (⟨𝑧, 𝑤⟩ ∈ (𝐺𝐹) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇)))
861, 2, 85eqrelrdv 5790 1 (𝜑 → (𝐺𝐹) = (𝑥𝐴𝑇))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wex 1781  wcel 2106  Vcvv 3474  csb 3892  cop 4633   class class class wbr 5147  {copab 5209  cmpt 5230  dom cdm 5675  ccom 5679  Fun wfun 6534  cfv 6540
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548
This theorem is referenced by:  fmptcof  7124  cofmpt  7126  fcompt  7127  fcoconst  7128  ofco  7689  ccatco  14782  rlimcn1  15528  rlimdiv  15588  ackbijnn  15770  setcepi  18034  prf1st  18152  prf2nd  18153  hofcllem  18207  prdsidlem  18653  pws0g  18657  pwsco1mhm  18709  pwsco2mhm  18710  smndex1iidm  18778  smndex2dlinvh  18794  pwsinvg  18932  pwssub  18933  galactghm  19266  efginvrel1  19590  frgpup3lem  19639  gsumzf1o  19774  gsumconst  19796  gsummptshft  19798  gsumzmhm  19799  gsummhm2  19801  gsummptmhm  19802  gsumsub  19810  gsum2dlem2  19833  dprdfsub  19885  lmhmvsca  20648  frgpcyg  21120  evpmodpmf1o  21140  psrass1lemOLD  21484  psrass1lem  21487  psrlinv  21507  psrcom  21520  evlslem2  21633  coe1fval3  21723  psropprmul  21751  coe1z  21776  coe1mul2  21782  coe1tm  21786  ply1coe  21811  evls1sca  21833  mhmvlin  21890  ofco2  21944  mdetleib2  22081  mdetralt  22101  smadiadetlem3  22161  ptrescn  23134  lmcn2  23144  qtopeu  23211  flfcnp2  23502  tgpconncomp  23608  tsmssub  23644  tsmsxplem1  23648  negfcncf  24430  pcopt  24529  pcopt2  24530  pi1xfrcnvlem  24563  ovolctb  24998  ovolfs2  25079  uniioombllem2  25091  ismbf  25136  mbfconst  25141  limccnp2  25400  limcco  25401  dvcof  25456  dvcj  25458  dvfre  25459  dvmptcj  25476  dvmptco  25480  dvcnvlem  25484  dvlip  25501  dvlipcn  25502  itgsubstlem  25556  plyco  25746  dgrcolem1  25778  dgrcolem2  25779  dgrco  25780  plycjlem  25781  taylply2  25871  logcn  26146  leibpi  26436  efrlim  26463  jensenlem2  26481  amgmlem  26483  ftalem7  26572  dchrisum0  27012  ghmquskerco  32517  ofcfval4  33091  eulerpartgbij  33359  dstfrvclim1  33464  cvmliftlem6  34269  cvmliftphtlem  34296  cvmlift3lem5  34302  elmsubrn  34507  msubco  34510  circum  34647  mblfinlem2  36514  volsupnfl  36521  itgaddnc  36536  itgmulc2nc  36544  ftc1anclem1  36549  ftc1anclem2  36550  ftc1anclem3  36551  ftc1anclem4  36552  ftc1anclem5  36553  ftc1anclem7  36555  ftc1anclem8  36556  fnopabco  36579  upixp  36585  selvvvval  41154  evlselv  41156  mendassa  41921  fsovrfovd  42745  fsovcnvlem  42749  cncfcompt  44585  dvcosax  44628  dirkercncflem4  44808  fourierdlem111  44919  meadjiunlem  45167  meadjiun  45168  fundcmpsurbijinjpreimafv  46061  itcovalpclem2  47310  itcovalt2lem2  47315  amgmwlem  47802  amgmlemALT  47803
  Copyright terms: Public domain W3C validator