Theorem fcoi1 6716

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	⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹)

Proof of Theorem fcoi1

Step	Hyp	Ref	Expression
1		ffn 6670	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		df-fn 6503	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
3		eqimss 3994	. . . . 5 ⊢ (dom 𝐹 = 𝐴 → dom 𝐹 ⊆ 𝐴)
4		cnvi 6107	. . . . . . . . . 10 ⊢ ◡ I = I
5	4	reseq1i 5942	. . . . . . . . 9 ⊢ (◡ I ↾ 𝐴) = ( I ↾ 𝐴)
6	5	cnveqi 5831	. . . . . . . 8 ⊢ ◡(◡ I ↾ 𝐴) = ◡( I ↾ 𝐴)
7		cnvresid 6579	. . . . . . . 8 ⊢ ◡( I ↾ 𝐴) = ( I ↾ 𝐴)
8	6, 7	eqtr2i 2761	. . . . . . 7 ⊢ ( I ↾ 𝐴) = ◡(◡ I ↾ 𝐴)
9	8	coeq2i 5817	. . . . . 6 ⊢ (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹 ∘ ◡(◡ I ↾ 𝐴))
10		cores2 6226	. . . . . 6 ⊢ (dom 𝐹 ⊆ 𝐴 → (𝐹 ∘ ◡(◡ I ↾ 𝐴)) = (𝐹 ∘ I ))
11	9, 10	eqtrid 2784	. . . . 5 ⊢ (dom 𝐹 ⊆ 𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹 ∘ I ))
12	3, 11	syl 17	. . . 4 ⊢ (dom 𝐹 = 𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = (𝐹 ∘ I ))
13		funrel 6517	. . . . 5 ⊢ (Fun 𝐹 → Rel 𝐹)
14		coi1 6229	. . . . 5 ⊢ (Rel 𝐹 → (𝐹 ∘ I ) = 𝐹)
15	13, 14	syl 17	. . . 4 ⊢ (Fun 𝐹 → (𝐹 ∘ I ) = 𝐹)
16	12, 15	sylan9eqr 2794	. . 3 ⊢ ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹)
17	2, 16	sylbi 217	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹)
18	1, 17	syl 17	1 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ⊆ wss 3903   I cid 5526  ^◡ccnv 5631  dom cdm 5632   ↾ cres 5634   ∘ ccom 5636  Rel wrel 5637  Fun wfun 6494   Fn wfn 6495  ⟶wf 6496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-fun 6502  df-fn 6503  df-f 6504

This theorem is referenced by:  fcof1oinvd  7249  mapen  9081  mapfien  9323  hashfacen  14389  cofurid  17827  setccatid  18020  estrccatid  18067  curf2ndf  18182  efmndid  18825  efmndmnd  18826  f1omvdco2  19389  psgnunilem1  19434  pf1mpf  22308  pf1ind  22311  wilthlem3  27048  hoico1  31844  fmptco1f1o  32723  fcobijfs  32811  cocnvf1o  32819  cycpmconjslem2  33249  cycpmconjs  33250  cyc3conja  33251  1arithidomlem2  33629  mplvrpmga  33722  mplvrpmrhm  33724  reprpmtf1o  34804  ltrncoidN  40504  trlcoabs2N  41098  trlcoat  41099  cdlemg47a  41110  cdlemg46  41111  trljco  41116  tendo1mulr  41147  tendo0co2  41164  cdlemi2  41195  cdlemk2  41208  cdlemk4  41210  cdlemk8  41214  cdlemk53  41333  cdlemk55a  41335  dvhopN  41492  dihopelvalcpre  41624  dihmeetlem1N  41666  dihglblem5apreN  41667  diophrw  43116  mendring  43545  rngccatidALTV  48632  ringccatidALTV  48666