Metamath Proof Explorer

Theorem cidffn

Description: The identity arrow construction is a function on categories. (Contributed by Mario Carneiro, 17-Jan-2017)

Ref Expression
Assertion cidffn ⊢IdFnCat

Proof

Step Hyp Ref Expression
1 vex ⊢b∈V
2 1 mptex ⊢x∈b⟼ιg∈xhx|∀y∈b∀f∈yhxgyxoxf=f∧∀f∈xhyfxxoyg=f∈V
3 2 csbex ⊢⦋comp⁡c/o⦌x∈b⟼ιg∈xhx|∀y∈b∀f∈yhxgyxoxf=f∧∀f∈xhyfxxoyg=f∈V
4 3 csbex ⊢⦋Hom⁡c/h⦌⦋comp⁡c/o⦌x∈b⟼ιg∈xhx|∀y∈b∀f∈yhxgyxoxf=f∧∀f∈xhyfxxoyg=f∈V
5 4 csbex ⊢⦋Basec/b⦌⦋Hom⁡c/h⦌⦋comp⁡c/o⦌x∈b⟼ιg∈xhx|∀y∈b∀f∈yhxgyxoxf=f∧∀f∈xhyfxxoyg=f∈V
6 df-cid ⊢Id=c∈Cat⟼⦋Basec/b⦌⦋Hom⁡c/h⦌⦋comp⁡c/o⦌x∈b⟼ιg∈xhx|∀y∈b∀f∈yhxgyxoxf=f∧∀f∈xhyfxxoyg=f
7 5 6 fnmpti ⊢IdFnCat