Metamath Proof Explorer


Theorem setcid

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

Ref Expression
Hypotheses setccat.c C = SetCat U
setcid.o 1 ˙ = Id C
setcid.u φ U V
setcid.x φ X U
Assertion setcid φ 1 ˙ X = I X

Proof

Step Hyp Ref Expression
1 setccat.c C = SetCat U
2 setcid.o 1 ˙ = Id C
3 setcid.u φ U V
4 setcid.x φ X U
5 1 setccatid U V C Cat Id C = x U I x
6 3 5 syl φ C Cat Id C = x U I x
7 6 simprd φ Id C = x U I x
8 2 7 eqtrid φ 1 ˙ = x U I x
9 simpr φ x = X x = X
10 9 reseq2d φ x = X I x = I X
11 4 resiexd φ I X V
12 8 10 4 11 fvmptd φ 1 ˙ X = I X