Theorem fcoi1 5581

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 5556	. 2
2		df-fn 5420	. . 3
3		eqimss 3433	. . . . 5
4		cnvi 5242	. . . . . . . . . 10
5	4	reseq1i 5110	. . . . . . . . 9
6	5	cnveqi 5018	. . . . . . . 8
7		cnvresid 5485	. . . . . . . 8
8	6, 7	eqtr2i 2502	. . . . . . 7
9	8	coeq2i 5004	. . . . . 6
10		cores2 5349	. . . . . 6
11	9, 10	syl5eq 2525	. . . . 5
12	3, 11	syl 16	. . . 4
13		funrel 5434	. . . . 5
14		coi1 5352	. . . . 5
15	13, 14	syl 16	. . . 4
16	12, 15	sylan9eqr 2535	. . 3
17	2, 16	sylbi 189	. 2
18	1, 17	syl 16	1

Syntax hints:  ->wi 4  /\wa 360  =wceq 1662  C_wss 3353  cid 4634  `'ccnv 4843  domcdm 4844  |`cres 4846  o.ccom 4848  Relwrel 4849  Funwfun 5411  Fnwfn 5412  -->wf 5413

This theorem is referenced by:  fcof1o  5971  mapen  7383  mapfien  7765  hashfacen  11994  cofurid  14579  setccatid  14730  curf2ndf  14835  symgid  15607  pf1mpf  20476  pf1ind  20479  wilthlem3  21362  hoico1  23770  fcobijfs  24647  diophrw  27748  f1omvdco2  28297  psgnunilem1  28322  mendrng  28406  ltrncoidN  32198  trlcoabs2N  32792  trlcoat  32793  cdlemg47a  32804  cdlemg46  32805  trljco  32810  tendo1mulr  32841  tendo0co2  32858  cdlemi2  32889  cdlemk2  32902  cdlemk4  32904  cdlemk8  32908  cdlemk53  33027  cdlemk55a  33029  dvhopN  33187  dihopelvalcpre  33319  dihmeetlem1N  33361  dihglblem5apreN  33362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-9 1728  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462  ax-sep 4423  ax-nul 4431  ax-pr 4538

This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-eu 2309  df-mo 2310  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-ne 2646  df-ral 2756  df-rex 2757  df-rab 2760  df-v 3008  df-dif 3356  df-un 3358  df-in 3360  df-ss 3367  df-nul 3661  df-if 3813  df-sn 3900  df-pr 3901  df-op 3903  df-br 4303  df-opab 4361  df-id 4639  df-xp 4850  df-rel 4851  df-cnv 4852  df-co 4853  df-dm 4854  df-rn 4855  df-res 4856  df-ima 4857  df-fun 5419  df-fn 5420  df-f 5421