Metamath Proof Explorer


Theorem cidffn

Description: The identity arrow construction is a function on categories. (Contributed by Mario Carneiro, 17-Jan-2017)

Ref Expression
Assertion cidffn IdFnCat

Proof

Step Hyp Ref Expression
1 vex bV
2 1 mptex xbιgxhx|ybfyhxgyxoxf=ffxhyfxxoyg=fV
3 2 csbex compc/oxbιgxhx|ybfyhxgyxoxf=ffxhyfxxoyg=fV
4 3 csbex Homc/hcompc/oxbιgxhx|ybfyhxgyxoxf=ffxhyfxxoyg=fV
5 4 csbex Basec/bHomc/hcompc/oxbιgxhx|ybfyhxgyxoxf=ffxhyfxxoyg=fV
6 df-cid Id=cCatBasec/bHomc/hcompc/oxbιgxhx|ybfyhxgyxoxf=ffxhyfxxoyg=f
7 5 6 fnmpti IdFnCat