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

Theorem fmptco 6887
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 6095 . 2 Rel (𝐺𝐹)
2 mptrel 5696 . 2 Rel (𝑥𝐴𝑇)
3 fmptco.2 . . . . . . . . . . . 12 (𝜑𝐹 = (𝑥𝐴𝑅))
4 fmptco.1 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 𝑅𝐵)
53, 4fmpt3d 6876 . . . . . . . . . . 11 (𝜑𝐹:𝐴𝐵)
65ffund 6515 . . . . . . . . . 10 (𝜑 → Fun 𝐹)
7 funbrfv 6713 . . . . . . . . . . 11 (Fun 𝐹 → (𝑧𝐹𝑢 → (𝐹𝑧) = 𝑢))
87imp 407 . . . . . . . . . 10 ((Fun 𝐹𝑧𝐹𝑢) → (𝐹𝑧) = 𝑢)
96, 8sylan 580 . . . . . . . . 9 ((𝜑𝑧𝐹𝑢) → (𝐹𝑧) = 𝑢)
109eqcomd 2832 . . . . . . . 8 ((𝜑𝑧𝐹𝑢) → 𝑢 = (𝐹𝑧))
1110a1d 25 . . . . . . 7 ((𝜑𝑧𝐹𝑢) → (𝑢𝐺𝑤𝑢 = (𝐹𝑧)))
1211expimpd 454 . . . . . 6 (𝜑 → ((𝑧𝐹𝑢𝑢𝐺𝑤) → 𝑢 = (𝐹𝑧)))
1312pm4.71rd 563 . . . . 5 (𝜑 → ((𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤))))
1413exbidv 1915 . . . 4 (𝜑 → (∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤) ↔ ∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤))))
15 fvex 6680 . . . . . 6 (𝐹𝑧) ∈ V
16 breq2 5067 . . . . . . 7 (𝑢 = (𝐹𝑧) → (𝑧𝐹𝑢𝑧𝐹(𝐹𝑧)))
17 breq1 5066 . . . . . . 7 (𝑢 = (𝐹𝑧) → (𝑢𝐺𝑤 ↔ (𝐹𝑧)𝐺𝑤))
1816, 17anbi12d 630 . . . . . 6 (𝑢 = (𝐹𝑧) → ((𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤)))
1915, 18ceqsexv 3547 . . . . 5 (∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤)) ↔ (𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤))
20 funfvbrb 6817 . . . . . . . . 9 (Fun 𝐹 → (𝑧 ∈ dom 𝐹𝑧𝐹(𝐹𝑧)))
216, 20syl 17 . . . . . . . 8 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐹(𝐹𝑧)))
225fdmd 6520 . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝐴)
2322eleq2d 2903 . . . . . . . 8 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐴))
2421, 23bitr3d 282 . . . . . . 7 (𝜑 → (𝑧𝐹(𝐹𝑧) ↔ 𝑧𝐴))
253fveq1d 6669 . . . . . . . 8 (𝜑 → (𝐹𝑧) = ((𝑥𝐴𝑅)‘𝑧))
26 fmptco.3 . . . . . . . 8 (𝜑𝐺 = (𝑦𝐵𝑆))
27 eqidd 2827 . . . . . . . 8 (𝜑𝑤 = 𝑤)
2825, 26, 27breq123d 5077 . . . . . . 7 (𝜑 → ((𝐹𝑧)𝐺𝑤 ↔ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤))
2924, 28anbi12d 630 . . . . . 6 (𝜑 → ((𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤) ↔ (𝑧𝐴 ∧ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤)))
30 nfcv 2982 . . . . . . . . 9 𝑥𝑧
31 nfv 1908 . . . . . . . . . 10 𝑥𝜑
32 nffvmpt1 6678 . . . . . . . . . . . 12 𝑥((𝑥𝐴𝑅)‘𝑧)
33 nfcv 2982 . . . . . . . . . . . 12 𝑥(𝑦𝐵𝑆)
34 nfcv 2982 . . . . . . . . . . . 12 𝑥𝑤
3532, 33, 34nfbr 5110 . . . . . . . . . . 11 𝑥((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤
36 nfcsb1v 3911 . . . . . . . . . . . 12 𝑥𝑧 / 𝑥𝑇
3736nfeq2 3000 . . . . . . . . . . 11 𝑥 𝑤 = 𝑧 / 𝑥𝑇
3835, 37nfbi 1897 . . . . . . . . . 10 𝑥(((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)
3931, 38nfim 1890 . . . . . . . . 9 𝑥(𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))
40 fveq2 6667 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑥𝐴𝑅)‘𝑥) = ((𝑥𝐴𝑅)‘𝑧))
4140breq1d 5073 . . . . . . . . . . 11 (𝑥 = 𝑧 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤 ↔ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤))
42 csbeq1a 3901 . . . . . . . . . . . 12 (𝑥 = 𝑧𝑇 = 𝑧 / 𝑥𝑇)
4342eqeq2d 2837 . . . . . . . . . . 11 (𝑥 = 𝑧 → (𝑤 = 𝑇𝑤 = 𝑧 / 𝑥𝑇))
4441, 43bibi12d 347 . . . . . . . . . 10 (𝑥 = 𝑧 → ((((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇) ↔ (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
4544imbi2d 342 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇)) ↔ (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))))
46 vex 3503 . . . . . . . . . . . 12 𝑤 ∈ V
47 simpl 483 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑅𝑢 = 𝑤) → 𝑦 = 𝑅)
4847eleq1d 2902 . . . . . . . . . . . . . 14 ((𝑦 = 𝑅𝑢 = 𝑤) → (𝑦𝐵𝑅𝐵))
49 id 22 . . . . . . . . . . . . . . 15 (𝑢 = 𝑤𝑢 = 𝑤)
50 fmptco.4 . . . . . . . . . . . . . . 15 (𝑦 = 𝑅𝑆 = 𝑇)
5149, 50eqeqan12rd 2845 . . . . . . . . . . . . . 14 ((𝑦 = 𝑅𝑢 = 𝑤) → (𝑢 = 𝑆𝑤 = 𝑇))
5248, 51anbi12d 630 . . . . . . . . . . . . 13 ((𝑦 = 𝑅𝑢 = 𝑤) → ((𝑦𝐵𝑢 = 𝑆) ↔ (𝑅𝐵𝑤 = 𝑇)))
53 df-mpt 5144 . . . . . . . . . . . . 13 (𝑦𝐵𝑆) = {⟨𝑦, 𝑢⟩ ∣ (𝑦𝐵𝑢 = 𝑆)}
5452, 53brabga 5418 . . . . . . . . . . . 12 ((𝑅𝐵𝑤 ∈ V) → (𝑅(𝑦𝐵𝑆)𝑤 ↔ (𝑅𝐵𝑤 = 𝑇)))
554, 46, 54sylancl 586 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑅(𝑦𝐵𝑆)𝑤 ↔ (𝑅𝐵𝑤 = 𝑇)))
56 id 22 . . . . . . . . . . . . 13 (𝑥𝐴𝑥𝐴)
57 eqid 2826 . . . . . . . . . . . . . 14 (𝑥𝐴𝑅) = (𝑥𝐴𝑅)
5857fvmpt2 6775 . . . . . . . . . . . . 13 ((𝑥𝐴𝑅𝐵) → ((𝑥𝐴𝑅)‘𝑥) = 𝑅)
5956, 4, 58syl2an2 682 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝑥𝐴𝑅)‘𝑥) = 𝑅)
6059breq1d 5073 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑅(𝑦𝐵𝑆)𝑤))
614biantrurd 533 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑤 = 𝑇 ↔ (𝑅𝐵𝑤 = 𝑇)))
6255, 60, 613bitr4d 312 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇))
6362expcom 414 . . . . . . . . 9 (𝑥𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇)))
6430, 39, 45, 63vtoclgaf 3578 . . . . . . . 8 (𝑧𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
6564impcom 408 . . . . . . 7 ((𝜑𝑧𝐴) → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))
6665pm5.32da 579 . . . . . 6 (𝜑 → ((𝑧𝐴 ∧ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
6729, 66bitrd 280 . . . . 5 (𝜑 → ((𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
6819, 67syl5bb 284 . . . 4 (𝜑 → (∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤)) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
6914, 68bitrd 280 . . 3 (𝜑 → (∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
70 vex 3503 . . . 4 𝑧 ∈ V
7170, 46opelco 5741 . . 3 (⟨𝑧, 𝑤⟩ ∈ (𝐺𝐹) ↔ ∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤))
72 df-mpt 5144 . . . . 5 (𝑥𝐴𝑇) = {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)}
7372eleq2i 2909 . . . 4 (⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇) ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)})
74 nfv 1908 . . . . . 6 𝑥 𝑧𝐴
7536nfeq2 3000 . . . . . 6 𝑥 𝑣 = 𝑧 / 𝑥𝑇
7674, 75nfan 1893 . . . . 5 𝑥(𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇)
77 nfv 1908 . . . . 5 𝑣(𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)
78 eleq1w 2900 . . . . . 6 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
7942eqeq2d 2837 . . . . . 6 (𝑥 = 𝑧 → (𝑣 = 𝑇𝑣 = 𝑧 / 𝑥𝑇))
8078, 79anbi12d 630 . . . . 5 (𝑥 = 𝑧 → ((𝑥𝐴𝑣 = 𝑇) ↔ (𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇)))
81 eqeq1 2830 . . . . . 6 (𝑣 = 𝑤 → (𝑣 = 𝑧 / 𝑥𝑇𝑤 = 𝑧 / 𝑥𝑇))
8281anbi2d 628 . . . . 5 (𝑣 = 𝑤 → ((𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
8376, 77, 70, 46, 80, 82opelopabf 5429 . . . 4 (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)} ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇))
8473, 83bitri 276 . . 3 (⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇))
8569, 71, 843bitr4g 315 . 2 (𝜑 → (⟨𝑧, 𝑤⟩ ∈ (𝐺𝐹) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇)))
861, 2, 85eqrelrdv 5664 1 (𝜑 → (𝐺𝐹) = (𝑥𝐴𝑇))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1530  wex 1773  wcel 2107  Vcvv 3500  csb 3887  cop 4570   class class class wbr 5063  {copab 5125  cmpt 5143  dom cdm 5554  ccom 5558  Fun wfun 6346  cfv 6352
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-fv 6360
This theorem is referenced by:  fmptcof  6888  cofmpt  6890  fcompt  6891  fcoconst  6892  ofco  7419  ccatco  14187  rlimcn1  14935  rlimdiv  14992  ackbijnn  15173  setcepi  17338  prf1st  17444  prf2nd  17445  hofcllem  17498  prdsidlem  17931  pws0g  17935  pwsco1mhm  17979  pwsco2mhm  17980  pwsinvg  18142  pwssub  18143  galactghm  18451  efginvrel1  18774  frgpup3lem  18823  gsumzf1o  18952  gsumconst  18974  gsummptshft  18976  gsumzmhm  18977  gsummhm2  18979  gsummptmhm  18980  gsumsub  18988  gsum2dlem2  19011  dprdfsub  19063  lmhmvsca  19737  psrass1lem  20076  psrlinv  20096  psrcom  20108  evlslem2  20211  coe1fval3  20295  psropprmul  20325  coe1z  20350  coe1mul2  20356  coe1tm  20360  ply1coe  20383  evls1sca  20405  frgpcyg  20639  evpmodpmf1o  20659  mhmvlin  20927  ofco2  20979  mdetleib2  21116  mdetralt  21136  smadiadetlem3  21196  ptrescn  22166  lmcn2  22176  qtopeu  22243  flfcnp2  22534  tgpconncomp  22639  tsmssub  22675  tsmsxplem1  22679  negfcncf  23445  pcopt  23544  pcopt2  23545  pi1xfrcnvlem  23578  ovolctb  24009  ovolfs2  24090  uniioombllem2  24102  ismbf  24147  mbfconst  24152  limccnp2  24408  limcco  24409  dvcof  24463  dvcj  24465  dvfre  24466  dvmptcj  24483  dvmptco  24487  dvcnvlem  24491  dvlip  24508  dvlipcn  24509  itgsubstlem  24563  plyco  24749  dgrcolem1  24781  dgrcolem2  24782  dgrco  24783  plycjlem  24784  taylply2  24874  logcn  25146  leibpi  25437  efrlim  25464  jensenlem2  25482  amgmlem  25484  ftalem7  25573  dchrisum0  26013  ofcfval4  31253  eulerpartgbij  31519  dstfrvclim1  31624  cvmliftlem6  32424  cvmliftphtlem  32451  cvmlift3lem5  32457  elmsubrn  32662  msubco  32665  circum  32804  mblfinlem2  34800  volsupnfl  34807  itgaddnc  34822  itgmulc2nc  34830  ftc1anclem1  34837  ftc1anclem2  34838  ftc1anclem3  34839  ftc1anclem4  34840  ftc1anclem5  34841  ftc1anclem7  34843  ftc1anclem8  34844  fnopabco  34869  upixp  34875  mendassa  39662  fsovrfovd  40223  fsovcnvlem  40227  cncfcompt  42034  dvcosax  42079  dirkercncflem4  42260  fourierdlem111  42371  meadjiunlem  42616  meadjiun  42617  amgmwlem  44738  amgmlemALT  44739
  Copyright terms: Public domain W3C validator