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

Theorem fmptco 6064
Description: Composition of two functions expressed as ordered-pair class abstractions. If has the equation and the equation then has the equation . (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:   ,   , ,   ,   ,   ,S   ,

Proof of Theorem fmptco
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relco 5510 . 2
2 funmpt 5629 . . 3
3 funrel 5610 . . 3
42, 3ax-mp 5 . 2
5 fmptco.1 . . . . . . . . . . . . 13
6 eqid 2457 . . . . . . . . . . . . 13
75, 6fmptd 6055 . . . . . . . . . . . 12
8 fmptco.2 . . . . . . . . . . . . 13
98feq1d 5722 . . . . . . . . . . . 12
107, 9mpbird 232 . . . . . . . . . . 11
11 ffun 5738 . . . . . . . . . . 11
1210, 11syl 16 . . . . . . . . . 10
13 funbrfv 5911 . . . . . . . . . . 11
1413imp 429 . . . . . . . . . 10
1512, 14sylan 471 . . . . . . . . 9
1615eqcomd 2465 . . . . . . . 8
1716a1d 25 . . . . . . 7
1817expimpd 603 . . . . . 6
1918pm4.71rd 635 . . . . 5
2019exbidv 1714 . . . 4
21 fvex 5881 . . . . . 6
22 breq2 4456 . . . . . . 7
23 breq1 4455 . . . . . . 7
2422, 23anbi12d 710 . . . . . 6
2521, 24ceqsexv 3146 . . . . 5
26 funfvbrb 6000 . . . . . . . . 9
2712, 26syl 16 . . . . . . . 8
28 fdm 5740 . . . . . . . . . 10
2910, 28syl 16 . . . . . . . . 9
3029eleq2d 2527 . . . . . . . 8
3127, 30bitr3d 255 . . . . . . 7
328fveq1d 5873 . . . . . . . 8
33 fmptco.3 . . . . . . . 8
34 eqidd 2458 . . . . . . . 8
3532, 33, 34breq123d 4466 . . . . . . 7
3631, 35anbi12d 710 . . . . . 6
37 nfcv 2619 . . . . . . . . 9
38 nfv 1707 . . . . . . . . . 10
39 nffvmpt1 5879 . . . . . . . . . . . 12
40 nfcv 2619 . . . . . . . . . . . 12
41 nfcv 2619 . . . . . . . . . . . 12
4239, 40, 41nfbr 4496 . . . . . . . . . . 11
43 nfcsb1v 3450 . . . . . . . . . . . 12
4443nfeq2 2636 . . . . . . . . . . 11
4542, 44nfbi 1934 . . . . . . . . . 10
4638, 45nfim 1920 . . . . . . . . 9
47 fveq2 5871 . . . . . . . . . . . 12
4847breq1d 4462 . . . . . . . . . . 11
49 csbeq1a 3443 . . . . . . . . . . . 12
5049eqeq2d 2471 . . . . . . . . . . 11
5148, 50bibi12d 321 . . . . . . . . . 10
5251imbi2d 316 . . . . . . . . 9
53 vex 3112 . . . . . . . . . . . 12
54 simpl 457 . . . . . . . . . . . . . . 15
5554eleq1d 2526 . . . . . . . . . . . . . 14
56 simpr 461 . . . . . . . . . . . . . . 15
57 fmptco.4 . . . . . . . . . . . . . . . 16
5857adantr 465 . . . . . . . . . . . . . . 15
5956, 58eqeq12d 2479 . . . . . . . . . . . . . 14
6055, 59anbi12d 710 . . . . . . . . . . . . 13
61 df-mpt 4512 . . . . . . . . . . . . 13
6260, 61brabga 4766 . . . . . . . . . . . 12
635, 53, 62sylancl 662 . . . . . . . . . . 11
64 simpr 461 . . . . . . . . . . . . 13
656fvmpt2 5963 . . . . . . . . . . . . 13
6664, 5, 65syl2anc 661 . . . . . . . . . . . 12
6766breq1d 4462 . . . . . . . . . . 11
685biantrurd 508 . . . . . . . . . . 11
6963, 67, 683bitr4d 285 . . . . . . . . . 10
7069expcom 435 . . . . . . . . 9
7137, 46, 52, 70vtoclgaf 3172 . . . . . . . 8
7271impcom 430 . . . . . . 7
7372pm5.32da 641 . . . . . 6
7436, 73bitrd 253 . . . . 5
7525, 74syl5bb 257 . . . 4
7620, 75bitrd 253 . . 3
77 vex 3112 . . . 4
7877, 53opelco 5179 . . 3
79 df-mpt 4512 . . . . 5
8079eleq2i 2535 . . . 4
81 nfv 1707 . . . . . 6
8243nfeq2 2636 . . . . . 6
8381, 82nfan 1928 . . . . 5
84 nfv 1707 . . . . 5
85 eleq1 2529 . . . . . 6
8649eqeq2d 2471 . . . . . 6
8785, 86anbi12d 710 . . . . 5
88 eqeq1 2461 . . . . . 6
8988anbi2d 703 . . . . 5
9083, 84, 77, 53, 87, 89opelopabf 4777 . . . 4
9180, 90bitri 249 . . 3
9276, 78, 913bitr4g 288 . 2
931, 4, 92eqrelrdv 5104 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  E.wex 1612  e.wcel 1818   cvv 3109  [_csb 3434  <.cop 4035   class class class wbr 4452  {copab 4509  e.cmpt 4510  domcdm 5004  o.ccom 5008  Relwrel 5009  Funwfun 5587  -->wf 5589  `cfv 5593
This theorem is referenced by:  fmptcof  6065  fcompt  6067  fcoconst  6068  ofco  6560  ccatco  12801  lo1o12  13356  rlimcn1  13411  rlimcn1b  13412  rlimdiv  13468  ackbijnn  13640  setcepi  15415  prf1st  15473  prf2nd  15474  hofcllem  15527  prdsidlem  15952  pws0g  15956  pwsco1mhm  16001  pwsco2mhm  16002  pwsinvg  16182  pwssub  16183  galactghm  16428  efginvrel1  16746  frgpup3lem  16795  gsumzf1o  16917  gsumzf1oOLD  16920  gsumconst  16954  gsummptshft  16956  gsumzmhm  16957  gsumzmhmOLD  16958  gsummhm2  16961  gsummhm2OLD  16962  gsummptmhm  16963  gsumsub  16974  gsumsubOLD  16975  gsum2dlem2  16998  gsum2dOLD  17000  dprdfsub  17061  dprdfsubOLD  17068  lmhmvsca  17691  psrass1lem  18029  psrlinv  18050  psrcom  18064  evlslem2  18180  coe1fval3  18247  psropprmul  18279  coe1z  18304  coe1mul2  18310  coe1tm  18314  ply1coe  18337  ply1coeOLD  18338  evls1sca  18360  frgpcyg  18612  evpmodpmf1o  18632  mhmvlin  18899  ofco2  18953  mdetleib2  19090  mdetralt  19110  smadiadetlem3  19170  ptrescn  20140  lmcn2  20150  qtopeu  20217  flfcnp2  20508  tgpconcomp  20611  tsmsmhm  20648  tsmssub  20651  tsmsxplem1  20655  negfcncf  21423  pcopt  21522  pcopt2  21523  pi1xfrcnvlem  21556  ovolctb  21901  ovolfs2  21980  uniioombllem2  21992  uniioombllem3  21994  ismbf  22037  mbfconst  22042  ismbfcn2  22046  itg1climres  22121  iblabslem  22234  iblabs  22235  bddmulibl  22245  limccnp  22295  limccnp2  22296  limcco  22297  dvcof  22351  dvcjbr  22352  dvcj  22353  dvfre  22354  dvmptcj  22371  dvmptco  22375  dvcnvlem  22377  dvef  22381  dvlip  22394  dvlipcn  22395  itgsubstlem  22449  plypf1  22609  plyco  22638  dgrcolem1  22670  dgrcolem2  22671  dgrco  22672  plycjlem  22673  taylply2  22763  logcn  23028  leibpi  23273  efrlim  23299  jensenlem2  23317  amgmlem  23319  ftalem7  23352  lgseisenlem4  23627  dchrisum0  23705  cofmpt  27504  ofcfval4  28104  eulerpartgbij  28311  dstfrvclim1  28416  lgamgulmlem2  28572  lgamcvg2  28597  cvmliftlem6  28735  cvmliftphtlem  28762  cvmlift3lem5  28768  elmsubrn  28888  msubco  28891  circum  29040  mblfinlem2  30052  volsupnfl  30059  itgaddnc  30075  itgmulc2nc  30083  ftc1anclem1  30090  ftc1anclem2  30091  ftc1anclem3  30092  ftc1anclem4  30093  ftc1anclem5  30094  ftc1anclem6  30095  ftc1anclem7  30096  ftc1anclem8  30097  fnopabco  30213  upixp  30220  mendassa  31143  cncfcompt  31685  dvcosax  31723  dirkercncflem4  31888  fourierdlem111  32000
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-fv 5601
  Copyright terms: Public domain W3C validator