Theorem fcoi1 5602

Description: Composition of a mapping and restricted identity. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)

Assertion

Ref	Expression
fcoi1

Proof of Theorem fcoi1

Step	Hyp	Ref	Expression
1		ffn 5577	. 2
2		df-fn 5441	. . 3
3		eqimss 3445	. . . . 5
4		cnvi 5263	. . . . . . . . . 10
5	4	reseq1i 5128	. . . . . . . . 9
6	5	cnveqi 5036	. . . . . . . 8
7		cnvresid 5506	. . . . . . . 8
8	6, 7	eqtr2i 2510	. . . . . . 7
9	8	coeq2i 5022	. . . . . 6
10		cores2 5370	. . . . . 6
11	9, 10	syl5eq 2533	. . . . 5
12	3, 11	syl 16	. . . 4
13		funrel 5455	. . . . 5
14		coi1 5373	. . . . 5
15	13, 14	syl 16	. . . 4
16	12, 15	sylan9eqr 2543	. . 3
17	2, 16	sylbi 189	. 2
18	1, 17	syl 16	1

Syntax hints:  ->wi 4  /\wa 360  =wceq 1670  C_wss 3365  cid 4652  `'ccnv 4861  domcdm 4862  |`cres 4864  o.ccom 4866  Relwrel 4867  Funwfun 5432  Fnwfn 5433  -->wf 5434

This theorem is referenced by:  fcof1o  6007  mapen  7436  mapfien  7820  hashfacen  12054  cofurid  14642  setccatid  14793  curf2ndf  14898  symgid  15687  f1omvdco2  17605  psgnunilem1  17646  pf1mpf  20987  pf1ind  20990  wilthlem3  21874  hoico1  24282  fcobijfs  25156  diophrw  28245  mendrng  28731  ltrncoidN  32475  trlcoabs2N  33069  trlcoat  33070  cdlemg47a  33081  cdlemg46  33082  trljco  33087  tendo1mulr  33118  tendo0co2  33135  cdlemi2  33166  cdlemk2  33179  cdlemk4  33181  cdlemk8  33185  cdlemk53  33304  cdlemk55a  33306  dvhopN  33464  dihopelvalcpre  33596  dihmeetlem1N  33638  dihglblem5apreN  33639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-9 1736  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-sep 4439  ax-nul 4447  ax-pr 4554

This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-eu 2317  df-mo 2318  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-ral 2764  df-rex 2765  df-rab 2768  df-v 3017  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-nul 3674  df-if 3826  df-sn 3915  df-pr 3916  df-op 3918  df-br 4319  df-opab 4377  df-id 4657  df-xp 4868  df-rel 4869  df-cnv 4870  df-co 4871  df-dm 4872  df-rn 4873  df-res 4874  df-ima 4875  df-fun 5440  df-fn 5441  df-f 5442