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

Theorem fmptco 6511
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 5746 . 2 Rel (𝐺𝐹)
2 mptrel 5356 . 2 Rel (𝑥𝐴𝑇)
3 fmptco.2 . . . . . . . . . . . 12 (𝜑𝐹 = (𝑥𝐴𝑅))
4 fmptco.1 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 𝑅𝐵)
53, 4fmpt3d 6501 . . . . . . . . . . 11 (𝜑𝐹:𝐴𝐵)
65ffund 6162 . . . . . . . . . 10 (𝜑 → Fun 𝐹)
7 funbrfv 6347 . . . . . . . . . . 11 (Fun 𝐹 → (𝑧𝐹𝑢 → (𝐹𝑧) = 𝑢))
87imp 444 . . . . . . . . . 10 ((Fun 𝐹𝑧𝐹𝑢) → (𝐹𝑧) = 𝑢)
96, 8sylan 489 . . . . . . . . 9 ((𝜑𝑧𝐹𝑢) → (𝐹𝑧) = 𝑢)
109eqcomd 2730 . . . . . . . 8 ((𝜑𝑧𝐹𝑢) → 𝑢 = (𝐹𝑧))
1110a1d 25 . . . . . . 7 ((𝜑𝑧𝐹𝑢) → (𝑢𝐺𝑤𝑢 = (𝐹𝑧)))
1211expimpd 630 . . . . . 6 (𝜑 → ((𝑧𝐹𝑢𝑢𝐺𝑤) → 𝑢 = (𝐹𝑧)))
1312pm4.71rd 670 . . . . 5 (𝜑 → ((𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤))))
1413exbidv 1963 . . . 4 (𝜑 → (∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤) ↔ ∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤))))
15 fvex 6314 . . . . . 6 (𝐹𝑧) ∈ V
16 breq2 4764 . . . . . . 7 (𝑢 = (𝐹𝑧) → (𝑧𝐹𝑢𝑧𝐹(𝐹𝑧)))
17 breq1 4763 . . . . . . 7 (𝑢 = (𝐹𝑧) → (𝑢𝐺𝑤 ↔ (𝐹𝑧)𝐺𝑤))
1816, 17anbi12d 749 . . . . . 6 (𝑢 = (𝐹𝑧) → ((𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤)))
1915, 18ceqsexv 3346 . . . . 5 (∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤)) ↔ (𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤))
20 funfvbrb 6445 . . . . . . . . 9 (Fun 𝐹 → (𝑧 ∈ dom 𝐹𝑧𝐹(𝐹𝑧)))
216, 20syl 17 . . . . . . . 8 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐹(𝐹𝑧)))
22 fdm 6164 . . . . . . . . . 10 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
235, 22syl 17 . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝐴)
2423eleq2d 2789 . . . . . . . 8 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐴))
2521, 24bitr3d 270 . . . . . . 7 (𝜑 → (𝑧𝐹(𝐹𝑧) ↔ 𝑧𝐴))
263fveq1d 6306 . . . . . . . 8 (𝜑 → (𝐹𝑧) = ((𝑥𝐴𝑅)‘𝑧))
27 fmptco.3 . . . . . . . 8 (𝜑𝐺 = (𝑦𝐵𝑆))
28 eqidd 2725 . . . . . . . 8 (𝜑𝑤 = 𝑤)
2926, 27, 28breq123d 4774 . . . . . . 7 (𝜑 → ((𝐹𝑧)𝐺𝑤 ↔ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤))
3025, 29anbi12d 749 . . . . . 6 (𝜑 → ((𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤) ↔ (𝑧𝐴 ∧ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤)))
31 nfcv 2866 . . . . . . . . 9 𝑥𝑧
32 nfv 1956 . . . . . . . . . 10 𝑥𝜑
33 nffvmpt1 6312 . . . . . . . . . . . 12 𝑥((𝑥𝐴𝑅)‘𝑧)
34 nfcv 2866 . . . . . . . . . . . 12 𝑥(𝑦𝐵𝑆)
35 nfcv 2866 . . . . . . . . . . . 12 𝑥𝑤
3633, 34, 35nfbr 4807 . . . . . . . . . . 11 𝑥((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤
37 nfcsb1v 3655 . . . . . . . . . . . 12 𝑥𝑧 / 𝑥𝑇
3837nfeq2 2882 . . . . . . . . . . 11 𝑥 𝑤 = 𝑧 / 𝑥𝑇
3936, 38nfbi 1946 . . . . . . . . . 10 𝑥(((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)
4032, 39nfim 1938 . . . . . . . . 9 𝑥(𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))
41 fveq2 6304 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑥𝐴𝑅)‘𝑥) = ((𝑥𝐴𝑅)‘𝑧))
4241breq1d 4770 . . . . . . . . . . 11 (𝑥 = 𝑧 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤 ↔ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤))
43 csbeq1a 3648 . . . . . . . . . . . 12 (𝑥 = 𝑧𝑇 = 𝑧 / 𝑥𝑇)
4443eqeq2d 2734 . . . . . . . . . . 11 (𝑥 = 𝑧 → (𝑤 = 𝑇𝑤 = 𝑧 / 𝑥𝑇))
4542, 44bibi12d 334 . . . . . . . . . 10 (𝑥 = 𝑧 → ((((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇) ↔ (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
4645imbi2d 329 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇)) ↔ (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))))
47 vex 3307 . . . . . . . . . . . 12 𝑤 ∈ V
48 simpl 474 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑅𝑢 = 𝑤) → 𝑦 = 𝑅)
4948eleq1d 2788 . . . . . . . . . . . . . 14 ((𝑦 = 𝑅𝑢 = 𝑤) → (𝑦𝐵𝑅𝐵))
50 id 22 . . . . . . . . . . . . . . 15 (𝑢 = 𝑤𝑢 = 𝑤)
51 fmptco.4 . . . . . . . . . . . . . . 15 (𝑦 = 𝑅𝑆 = 𝑇)
5250, 51eqeqan12rd 2742 . . . . . . . . . . . . . 14 ((𝑦 = 𝑅𝑢 = 𝑤) → (𝑢 = 𝑆𝑤 = 𝑇))
5349, 52anbi12d 749 . . . . . . . . . . . . 13 ((𝑦 = 𝑅𝑢 = 𝑤) → ((𝑦𝐵𝑢 = 𝑆) ↔ (𝑅𝐵𝑤 = 𝑇)))
54 df-mpt 4838 . . . . . . . . . . . . 13 (𝑦𝐵𝑆) = {⟨𝑦, 𝑢⟩ ∣ (𝑦𝐵𝑢 = 𝑆)}
5553, 54brabga 5093 . . . . . . . . . . . 12 ((𝑅𝐵𝑤 ∈ V) → (𝑅(𝑦𝐵𝑆)𝑤 ↔ (𝑅𝐵𝑤 = 𝑇)))
564, 47, 55sylancl 697 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑅(𝑦𝐵𝑆)𝑤 ↔ (𝑅𝐵𝑤 = 𝑇)))
57 id 22 . . . . . . . . . . . . 13 (𝑥𝐴𝑥𝐴)
58 eqid 2724 . . . . . . . . . . . . . 14 (𝑥𝐴𝑅) = (𝑥𝐴𝑅)
5958fvmpt2 6405 . . . . . . . . . . . . 13 ((𝑥𝐴𝑅𝐵) → ((𝑥𝐴𝑅)‘𝑥) = 𝑅)
6057, 4, 59syl2an2 910 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝑥𝐴𝑅)‘𝑥) = 𝑅)
6160breq1d 4770 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑅(𝑦𝐵𝑆)𝑤))
624biantrurd 530 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑤 = 𝑇 ↔ (𝑅𝐵𝑤 = 𝑇)))
6356, 61, 623bitr4d 300 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇))
6463expcom 450 . . . . . . . . 9 (𝑥𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇)))
6531, 40, 46, 64vtoclgaf 3375 . . . . . . . 8 (𝑧𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
6665impcom 445 . . . . . . 7 ((𝜑𝑧𝐴) → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))
6766pm5.32da 676 . . . . . 6 (𝜑 → ((𝑧𝐴 ∧ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
6830, 67bitrd 268 . . . . 5 (𝜑 → ((𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
6919, 68syl5bb 272 . . . 4 (𝜑 → (∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤)) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
7014, 69bitrd 268 . . 3 (𝜑 → (∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
71 vex 3307 . . . 4 𝑧 ∈ V
7271, 47opelco 5401 . . 3 (⟨𝑧, 𝑤⟩ ∈ (𝐺𝐹) ↔ ∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤))
73 df-mpt 4838 . . . . 5 (𝑥𝐴𝑇) = {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)}
7473eleq2i 2795 . . . 4 (⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇) ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)})
75 nfv 1956 . . . . . 6 𝑥 𝑧𝐴
7637nfeq2 2882 . . . . . 6 𝑥 𝑣 = 𝑧 / 𝑥𝑇
7775, 76nfan 1941 . . . . 5 𝑥(𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇)
78 nfv 1956 . . . . 5 𝑣(𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)
79 eleq1 2791 . . . . . 6 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
8043eqeq2d 2734 . . . . . 6 (𝑥 = 𝑧 → (𝑣 = 𝑇𝑣 = 𝑧 / 𝑥𝑇))
8179, 80anbi12d 749 . . . . 5 (𝑥 = 𝑧 → ((𝑥𝐴𝑣 = 𝑇) ↔ (𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇)))
82 eqeq1 2728 . . . . . 6 (𝑣 = 𝑤 → (𝑣 = 𝑧 / 𝑥𝑇𝑤 = 𝑧 / 𝑥𝑇))
8382anbi2d 742 . . . . 5 (𝑣 = 𝑤 → ((𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
8477, 78, 71, 47, 81, 83opelopabf 5104 . . . 4 (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)} ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇))
8574, 84bitri 264 . . 3 (⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇))
8670, 72, 853bitr4g 303 . 2 (𝜑 → (⟨𝑧, 𝑤⟩ ∈ (𝐺𝐹) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇)))
871, 2, 86eqrelrdv 5325 1 (𝜑 → (𝐺𝐹) = (𝑥𝐴𝑇))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1596  wex 1817  wcel 2103  Vcvv 3304  csb 3639  cop 4291   class class class wbr 4760  {copab 4820  cmpt 4837  dom cdm 5218  ccom 5222  Fun wfun 5995  wf 5997  cfv 6001
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-ral 3019  df-rex 3020  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-br 4761  df-opab 4821  df-mpt 4838  df-id 5128  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-fv 6009
This theorem is referenced by:  fmptcof  6512  cofmpt  6514  fcompt  6515  fcoconst  6516  ofco  7034  ccatco  13702  lo1o12  14384  rlimcn1  14439  rlimcn1b  14440  rlimdiv  14496  ackbijnn  14680  setcepi  16860  prf1st  16966  prf2nd  16967  hofcllem  17020  prdsidlem  17444  pws0g  17448  pwsco1mhm  17492  pwsco2mhm  17493  pwsinvg  17650  pwssub  17651  galactghm  17944  efginvrel1  18262  frgpup3lem  18311  gsumzf1o  18434  gsumconst  18455  gsummptshft  18457  gsumzmhm  18458  gsummhm2  18460  gsummptmhm  18461  gsumsub  18469  gsum2dlem2  18491  dprdfsub  18541  lmhmvsca  19168  psrass1lem  19500  psrlinv  19520  psrcom  19532  evlslem2  19635  coe1fval3  19701  psropprmul  19731  coe1z  19756  coe1mul2  19762  coe1tm  19766  ply1coe  19789  evls1sca  19811  frgpcyg  20045  evpmodpmf1o  20065  mhmvlin  20326  ofco2  20380  mdetleib2  20517  mdetralt  20537  smadiadetlem3  20597  ptrescn  21565  lmcn2  21575  qtopeu  21642  flfcnp2  21933  tgpconncomp  22038  tsmsmhm  22071  tsmssub  22074  tsmsxplem1  22078  negfcncf  22844  pcopt  22943  pcopt2  22944  pi1xfrcnvlem  22977  ovolctb  23379  ovolfs2  23460  uniioombllem2  23472  uniioombllem3  23474  ismbf  23517  mbfconst  23522  ismbfcn2  23526  itg1climres  23601  iblabslem  23714  iblabs  23715  bddmulibl  23725  limccnp  23775  limccnp2  23776  limcco  23777  dvcof  23831  dvcjbr  23832  dvcj  23833  dvfre  23834  dvmptcj  23851  dvmptco  23855  dvcnvlem  23859  dvef  23863  dvlip  23876  dvlipcn  23877  itgsubstlem  23931  plypf1  24088  plyco  24117  dgrcolem1  24149  dgrcolem2  24150  dgrco  24151  plycjlem  24152  taylply2  24242  logcn  24513  leibpi  24789  efrlim  24816  jensenlem2  24834  amgmlem  24836  lgamgulmlem2  24876  lgamcvg2  24901  ftalem7  24925  lgseisenlem4  25223  dchrisum0  25329  ofcfval4  30397  eulerpartgbij  30664  dstfrvclim1  30769  cvmliftlem6  31500  cvmliftphtlem  31527  cvmlift3lem5  31533  elmsubrn  31653  msubco  31656  circum  31796  mblfinlem2  33679  volsupnfl  33686  itgaddnc  33702  itgmulc2nc  33710  ftc1anclem1  33717  ftc1anclem2  33718  ftc1anclem3  33719  ftc1anclem4  33720  ftc1anclem5  33721  ftc1anclem7  33723  ftc1anclem8  33724  fnopabco  33749  upixp  33756  mendassa  38183  fsovrfovd  38722  fsovcnvlem  38726  cncfcompt  40516  dvcosax  40561  dirkercncflem4  40743  fourierdlem111  40854  meadjiunlem  41102  meadjiun  41103  amgmwlem  42978  amgmlemALT  42979
  Copyright terms: Public domain W3C validator