This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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