Metamath Proof Explorer


Definition df-idfu

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

Ref Expression
Assertion df-idfu idfunc = ( 𝑡 ∈ Cat ↦ ( Base ‘ 𝑡 ) / 𝑏 ⟨ ( I ↾ 𝑏 ) , ( 𝑧 ∈ ( 𝑏 × 𝑏 ) ↦ ( I ↾ ( ( Hom ‘ 𝑡 ) ‘ 𝑧 ) ) ) ⟩ )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cidfu idfunc
1 vt 𝑡
2 ccat Cat
3 cbs Base
4 1 cv 𝑡
5 4 3 cfv ( Base ‘ 𝑡 )
6 vb 𝑏
7 cid I
8 6 cv 𝑏
9 7 8 cres ( I ↾ 𝑏 )
10 vz 𝑧
11 8 8 cxp ( 𝑏 × 𝑏 )
12 chom Hom
13 4 12 cfv ( Hom ‘ 𝑡 )
14 10 cv 𝑧
15 14 13 cfv ( ( Hom ‘ 𝑡 ) ‘ 𝑧 )
16 7 15 cres ( I ↾ ( ( Hom ‘ 𝑡 ) ‘ 𝑧 ) )
17 10 11 16 cmpt ( 𝑧 ∈ ( 𝑏 × 𝑏 ) ↦ ( I ↾ ( ( Hom ‘ 𝑡 ) ‘ 𝑧 ) ) )
18 9 17 cop ⟨ ( I ↾ 𝑏 ) , ( 𝑧 ∈ ( 𝑏 × 𝑏 ) ↦ ( I ↾ ( ( Hom ‘ 𝑡 ) ‘ 𝑧 ) ) ) ⟩
19 6 5 18 csb ( Base ‘ 𝑡 ) / 𝑏 ⟨ ( I ↾ 𝑏 ) , ( 𝑧 ∈ ( 𝑏 × 𝑏 ) ↦ ( I ↾ ( ( Hom ‘ 𝑡 ) ‘ 𝑧 ) ) ) ⟩
20 1 2 19 cmpt ( 𝑡 ∈ Cat ↦ ( Base ‘ 𝑡 ) / 𝑏 ⟨ ( I ↾ 𝑏 ) , ( 𝑧 ∈ ( 𝑏 × 𝑏 ) ↦ ( I ↾ ( ( Hom ‘ 𝑡 ) ‘ 𝑧 ) ) ) ⟩ )
21 0 20 wceq idfunc = ( 𝑡 ∈ Cat ↦ ( Base ‘ 𝑡 ) / 𝑏 ⟨ ( I ↾ 𝑏 ) , ( 𝑧 ∈ ( 𝑏 × 𝑏 ) ↦ ( I ↾ ( ( Hom ‘ 𝑡 ) ‘ 𝑧 ) ) ) ⟩ )