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

Theorem fmptco 6303
 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 5550 . 2 Rel (𝐺𝐹)
2 mptrel 5170 . 2 Rel (𝑥𝐴𝑇)
3 fmptco.2 . . . . . . . . . . . 12 (𝜑𝐹 = (𝑥𝐴𝑅))
4 fmptco.1 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 𝑅𝐵)
53, 4fmpt3d 6293 . . . . . . . . . . 11 (𝜑𝐹:𝐴𝐵)
65ffund 5962 . . . . . . . . . 10 (𝜑 → Fun 𝐹)
7 funbrfv 6144 . . . . . . . . . . 11 (Fun 𝐹 → (𝑧𝐹𝑢 → (𝐹𝑧) = 𝑢))
87imp 444 . . . . . . . . . 10 ((Fun 𝐹𝑧𝐹𝑢) → (𝐹𝑧) = 𝑢)
96, 8sylan 487 . . . . . . . . 9 ((𝜑𝑧𝐹𝑢) → (𝐹𝑧) = 𝑢)
109eqcomd 2616 . . . . . . . 8 ((𝜑𝑧𝐹𝑢) → 𝑢 = (𝐹𝑧))
1110a1d 25 . . . . . . 7 ((𝜑𝑧𝐹𝑢) → (𝑢𝐺𝑤𝑢 = (𝐹𝑧)))
1211expimpd 627 . . . . . 6 (𝜑 → ((𝑧𝐹𝑢𝑢𝐺𝑤) → 𝑢 = (𝐹𝑧)))
1312pm4.71rd 665 . . . . 5 (𝜑 → ((𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤))))
1413exbidv 1837 . . . 4 (𝜑 → (∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤) ↔ ∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤))))
15 fvex 6113 . . . . . 6 (𝐹𝑧) ∈ V
16 breq2 4587 . . . . . . 7 (𝑢 = (𝐹𝑧) → (𝑧𝐹𝑢𝑧𝐹(𝐹𝑧)))
17 breq1 4586 . . . . . . 7 (𝑢 = (𝐹𝑧) → (𝑢𝐺𝑤 ↔ (𝐹𝑧)𝐺𝑤))
1816, 17anbi12d 743 . . . . . 6 (𝑢 = (𝐹𝑧) → ((𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤)))
1915, 18ceqsexv 3215 . . . . 5 (∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤)) ↔ (𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤))
20 funfvbrb 6238 . . . . . . . . 9 (Fun 𝐹 → (𝑧 ∈ dom 𝐹𝑧𝐹(𝐹𝑧)))
216, 20syl 17 . . . . . . . 8 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐹(𝐹𝑧)))
22 fdm 5964 . . . . . . . . . 10 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
235, 22syl 17 . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝐴)
2423eleq2d 2673 . . . . . . . 8 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐴))
2521, 24bitr3d 269 . . . . . . 7 (𝜑 → (𝑧𝐹(𝐹𝑧) ↔ 𝑧𝐴))
263fveq1d 6105 . . . . . . . 8 (𝜑 → (𝐹𝑧) = ((𝑥𝐴𝑅)‘𝑧))
27 fmptco.3 . . . . . . . 8 (𝜑𝐺 = (𝑦𝐵𝑆))
28 eqidd 2611 . . . . . . . 8 (𝜑𝑤 = 𝑤)
2926, 27, 28breq123d 4597 . . . . . . 7 (𝜑 → ((𝐹𝑧)𝐺𝑤 ↔ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤))
3025, 29anbi12d 743 . . . . . 6 (𝜑 → ((𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤) ↔ (𝑧𝐴 ∧ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤)))
31 nfcv 2751 . . . . . . . . 9 𝑥𝑧
32 nfv 1830 . . . . . . . . . 10 𝑥𝜑
33 nffvmpt1 6111 . . . . . . . . . . . 12 𝑥((𝑥𝐴𝑅)‘𝑧)
34 nfcv 2751 . . . . . . . . . . . 12 𝑥(𝑦𝐵𝑆)
35 nfcv 2751 . . . . . . . . . . . 12 𝑥𝑤
3633, 34, 35nfbr 4629 . . . . . . . . . . 11 𝑥((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤
37 nfcsb1v 3515 . . . . . . . . . . . 12 𝑥𝑧 / 𝑥𝑇
3837nfeq2 2766 . . . . . . . . . . 11 𝑥 𝑤 = 𝑧 / 𝑥𝑇
3936, 38nfbi 1821 . . . . . . . . . 10 𝑥(((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)
4032, 39nfim 1813 . . . . . . . . 9 𝑥(𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))
41 fveq2 6103 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑥𝐴𝑅)‘𝑥) = ((𝑥𝐴𝑅)‘𝑧))
4241breq1d 4593 . . . . . . . . . . 11 (𝑥 = 𝑧 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤 ↔ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤))
43 csbeq1a 3508 . . . . . . . . . . . 12 (𝑥 = 𝑧𝑇 = 𝑧 / 𝑥𝑇)
4443eqeq2d 2620 . . . . . . . . . . 11 (𝑥 = 𝑧 → (𝑤 = 𝑇𝑤 = 𝑧 / 𝑥𝑇))
4542, 44bibi12d 334 . . . . . . . . . 10 (𝑥 = 𝑧 → ((((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇) ↔ (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
4645imbi2d 329 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇)) ↔ (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))))
47 vex 3176 . . . . . . . . . . . 12 𝑤 ∈ V
48 simpl 472 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑅𝑢 = 𝑤) → 𝑦 = 𝑅)
4948eleq1d 2672 . . . . . . . . . . . . . 14 ((𝑦 = 𝑅𝑢 = 𝑤) → (𝑦𝐵𝑅𝐵))
50 id 22 . . . . . . . . . . . . . . 15 (𝑢 = 𝑤𝑢 = 𝑤)
51 fmptco.4 . . . . . . . . . . . . . . 15 (𝑦 = 𝑅𝑆 = 𝑇)
5250, 51eqeqan12rd 2628 . . . . . . . . . . . . . 14 ((𝑦 = 𝑅𝑢 = 𝑤) → (𝑢 = 𝑆𝑤 = 𝑇))
5349, 52anbi12d 743 . . . . . . . . . . . . 13 ((𝑦 = 𝑅𝑢 = 𝑤) → ((𝑦𝐵𝑢 = 𝑆) ↔ (𝑅𝐵𝑤 = 𝑇)))
54 df-mpt 4645 . . . . . . . . . . . . 13 (𝑦𝐵𝑆) = {⟨𝑦, 𝑢⟩ ∣ (𝑦𝐵𝑢 = 𝑆)}
5553, 54brabga 4914 . . . . . . . . . . . 12 ((𝑅𝐵𝑤 ∈ V) → (𝑅(𝑦𝐵𝑆)𝑤 ↔ (𝑅𝐵𝑤 = 𝑇)))
564, 47, 55sylancl 693 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑅(𝑦𝐵𝑆)𝑤 ↔ (𝑅𝐵𝑤 = 𝑇)))
57 id 22 . . . . . . . . . . . . 13 (𝑥𝐴𝑥𝐴)
58 eqid 2610 . . . . . . . . . . . . . 14 (𝑥𝐴𝑅) = (𝑥𝐴𝑅)
5958fvmpt2 6200 . . . . . . . . . . . . 13 ((𝑥𝐴𝑅𝐵) → ((𝑥𝐴𝑅)‘𝑥) = 𝑅)
6057, 4, 59syl2an2 871 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝑥𝐴𝑅)‘𝑥) = 𝑅)
6160breq1d 4593 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑅(𝑦𝐵𝑆)𝑤))
624biantrurd 528 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑤 = 𝑇 ↔ (𝑅𝐵𝑤 = 𝑇)))
6356, 61, 623bitr4d 299 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇))
6463expcom 450 . . . . . . . . 9 (𝑥𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇)))
6531, 40, 46, 64vtoclgaf 3244 . . . . . . . 8 (𝑧𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
6665impcom 445 . . . . . . 7 ((𝜑𝑧𝐴) → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))
6766pm5.32da 671 . . . . . 6 (𝜑 → ((𝑧𝐴 ∧ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
6830, 67bitrd 267 . . . . 5 (𝜑 → ((𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
6919, 68syl5bb 271 . . . 4 (𝜑 → (∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤)) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
7014, 69bitrd 267 . . 3 (𝜑 → (∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
71 vex 3176 . . . 4 𝑧 ∈ V
7271, 47opelco 5215 . . 3 (⟨𝑧, 𝑤⟩ ∈ (𝐺𝐹) ↔ ∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤))
73 df-mpt 4645 . . . . 5 (𝑥𝐴𝑇) = {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)}
7473eleq2i 2680 . . . 4 (⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇) ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)})
75 nfv 1830 . . . . . 6 𝑥 𝑧𝐴
7637nfeq2 2766 . . . . . 6 𝑥 𝑣 = 𝑧 / 𝑥𝑇
7775, 76nfan 1816 . . . . 5 𝑥(𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇)
78 nfv 1830 . . . . 5 𝑣(𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)
79 eleq1 2676 . . . . . 6 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
8043eqeq2d 2620 . . . . . 6 (𝑥 = 𝑧 → (𝑣 = 𝑇𝑣 = 𝑧 / 𝑥𝑇))
8179, 80anbi12d 743 . . . . 5 (𝑥 = 𝑧 → ((𝑥𝐴𝑣 = 𝑇) ↔ (𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇)))
82 eqeq1 2614 . . . . . 6 (𝑣 = 𝑤 → (𝑣 = 𝑧 / 𝑥𝑇𝑤 = 𝑧 / 𝑥𝑇))
8382anbi2d 736 . . . . 5 (𝑣 = 𝑤 → ((𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
8477, 78, 71, 47, 81, 83opelopabf 4925 . . . 4 (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)} ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇))
8574, 84bitri 263 . . 3 (⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇))
8670, 72, 853bitr4g 302 . 2 (𝜑 → (⟨𝑧, 𝑤⟩ ∈ (𝐺𝐹) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇)))
871, 2, 86eqrelrdv 5139 1 (𝜑 → (𝐺𝐹) = (𝑥𝐴𝑇))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977  Vcvv 3173  ⦋csb 3499  ⟨cop 4131   class class class wbr 4583  {copab 4642   ↦ cmpt 4643  dom cdm 5038   ∘ ccom 5042  Fun wfun 5798  ⟶wf 5800  ‘cfv 5804 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812 This theorem is referenced by:  fmptcof  6304  fcompt  6306  fcoconst  6307  ofco  6815  ccatco  13432  lo1o12  14112  rlimcn1  14167  rlimcn1b  14168  rlimdiv  14224  ackbijnn  14399  setcepi  16561  prf1st  16667  prf2nd  16668  hofcllem  16721  prdsidlem  17145  pws0g  17149  pwsco1mhm  17193  pwsco2mhm  17194  pwsinvg  17351  pwssub  17352  galactghm  17646  efginvrel1  17964  frgpup3lem  18013  gsumzf1o  18136  gsumconst  18157  gsummptshft  18159  gsumzmhm  18160  gsummhm2  18162  gsummptmhm  18163  gsumsub  18171  gsum2dlem2  18193  dprdfsub  18243  lmhmvsca  18866  psrass1lem  19198  psrlinv  19218  psrcom  19230  evlslem2  19333  coe1fval3  19399  psropprmul  19429  coe1z  19454  coe1mul2  19460  coe1tm  19464  ply1coe  19487  evls1sca  19509  frgpcyg  19741  evpmodpmf1o  19761  mhmvlin  20022  ofco2  20076  mdetleib2  20213  mdetralt  20233  smadiadetlem3  20293  ptrescn  21252  lmcn2  21262  qtopeu  21329  flfcnp2  21621  tgpconcomp  21726  tsmsmhm  21759  tsmssub  21762  tsmsxplem1  21766  negfcncf  22530  pcopt  22630  pcopt2  22631  pi1xfrcnvlem  22664  ovolctb  23065  ovolfs2  23145  uniioombllem2  23157  uniioombllem3  23159  ismbf  23203  mbfconst  23208  ismbfcn2  23212  itg1climres  23287  iblabslem  23400  iblabs  23401  bddmulibl  23411  limccnp  23461  limccnp2  23462  limcco  23463  dvcof  23517  dvcjbr  23518  dvcj  23519  dvfre  23520  dvmptcj  23537  dvmptco  23541  dvcnvlem  23543  dvef  23547  dvlip  23560  dvlipcn  23561  itgsubstlem  23615  plypf1  23772  plyco  23801  dgrcolem1  23833  dgrcolem2  23834  dgrco  23835  plycjlem  23836  taylply2  23926  logcn  24193  leibpi  24469  efrlim  24496  jensenlem2  24514  amgmlem  24516  lgamgulmlem2  24556  lgamcvg2  24581  ftalem7  24605  lgseisenlem4  24903  dchrisum0  25009  cofmpt  28846  ofcfval4  29494  eulerpartgbij  29761  dstfrvclim1  29866  cvmliftlem6  30526  cvmliftphtlem  30553  cvmlift3lem5  30559  elmsubrn  30679  msubco  30682  circum  30822  mblfinlem2  32617  volsupnfl  32624  itgaddnc  32640  itgmulc2nc  32648  ftc1anclem1  32655  ftc1anclem2  32656  ftc1anclem3  32657  ftc1anclem4  32658  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anclem8  32662  fnopabco  32687  upixp  32694  mendassa  36783  fsovrfovd  37323  fsovcnvlem  37327  cncfcompt  38768  dvcosax  38816  dirkercncflem4  38999  fourierdlem111  39110  meadjiunlem  39358  meadjiun  39359  amgmwlem  42357  amgmlemALT  42358
 Copyright terms: Public domain W3C validator