Metamath Proof Explorer


Definition df-idfu

Description: Define the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Assertion df-idfu id func = t Cat Base t / b I b z b × b I Hom t z

Detailed syntax breakdown

Step Hyp Ref Expression
0 cidfu class id func
1 vt setvar t
2 ccat class Cat
3 cbs class Base
4 1 cv setvar t
5 4 3 cfv class Base t
6 vb setvar b
7 cid class I
8 6 cv setvar b
9 7 8 cres class I b
10 vz setvar z
11 8 8 cxp class b × b
12 chom class Hom
13 4 12 cfv class Hom t
14 10 cv setvar z
15 14 13 cfv class Hom t z
16 7 15 cres class I Hom t z
17 10 11 16 cmpt class z b × b I Hom t z
18 9 17 cop class I b z b × b I Hom t z
19 6 5 18 csb class Base t / b I b z b × b I Hom t z
20 1 2 19 cmpt class t Cat Base t / b I b z b × b I Hom t z
21 0 20 wceq wff id func = t Cat Base t / b I b z b × b I Hom t z