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 ⊢ 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