Metamath Proof Explorer


Theorem catcid

Description: The identity arrow in the category of categories is the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses catccatid.c C = CatCat U
catccatid.b B = Base C
catcid.o 1 ˙ = Id C
catcid.i I = id func X
catcid.u φ U V
catcid.x φ X B
Assertion catcid φ 1 ˙ X = I

Proof

Step Hyp Ref Expression
1 catccatid.c C = CatCat U
2 catccatid.b B = Base C
3 catcid.o 1 ˙ = Id C
4 catcid.i I = id func X
5 catcid.u φ U V
6 catcid.x φ X B
7 1 2 catccatid U V C Cat Id C = x B id func x
8 5 7 syl φ C Cat Id C = x B id func x
9 8 simprd φ Id C = x B id func x
10 3 9 eqtrid φ 1 ˙ = x B id func x
11 simpr φ x = X x = X
12 11 fveq2d φ x = X id func x = id func X
13 fvexd φ id func X V
14 10 12 6 13 fvmptd φ 1 ˙ X = id func X
15 14 4 eqtr4di φ 1 ˙ X = I