Theorem fcompt 6067

Description: Express composition of two functions as a maps-to applying both in sequence. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Proof shortened by Mario Carneiro, 27-Dec-2014.)

Assertion

Ref	Expression
fcompt

Distinct variable groups:   ,   ,   ,   ,   ,

Proof of Theorem fcompt

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ffvelrn 6029	. . 3
2	1	adantll 713	. 2
3		ffn 5736	. . . 4
4	3	adantl 466	. . 3
5		dffn5 5918	. . 3
6	4, 5	sylib 196	. 2
7		ffn 5736	. . . 4
8	7	adantr 465	. . 3
9		dffn5 5918	. . 3
10	8, 9	sylib 196	. 2
11		fveq2 5871	. 2
12	2, 6, 10, 11	fmptco 6064	1

Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  e.cmpt 4510  o.ccom 5008  Fnwfn 5588  -->wf 5589  `cfv 5593

This theorem is referenced by:  2fvcoidd  6200  revco  12800  repsco  12805  caucvgrlem2  13497  fucidcl  15334  fucsect  15341  prf1st  15473  prf2nd  15474  curfcl  15501  yonedalem4c  15546  yonedalem3b  15548  yonedainv  15550  frmdup3  16035  efginvrel1  16746  frgpup3lem  16795  frgpup3  16796  dprdfinv  17059  dprdfinvOLD  17066  grpvlinv  18897  grpvrinv  18898  mhmvlin  18899  chcoeffeqlem  19386  prdstps  20130  imasdsf1olem  20876  meascnbl  28190  gamcvg2lem  28601  elmrsubrn  28880  mzprename  30682  mendassa  31143  mulc1cncfg  31583  expcnfg  31586  cncficcgt0  31691  dvsinax  31708  dirkercncflem2  31886  fourierdlem18  31907  fourierdlem53  31942  fourierdlem93  31982  fourierdlem101  31990  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