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 ‘ 𝑡 ) ‘ 𝑧 ) ) ) ⟩ )