Metamath Proof Explorer

Theorem cidfn

Description: The identity arrow operator is a function from objects to arrows. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses cidfn.b ⊢B=BaseC
cidfn.i ⊢1˙=Id⁡C
Assertion cidfn ⊢C∈Cat→1˙FnB

Proof

Step Hyp Ref Expression
1 cidfn.b ⊢B=BaseC
2 cidfn.i ⊢1˙=Id⁡C
3 riotaex ⊢ιg∈xHom⁡Cx|∀y∈B∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∈V
4 eqid ⊢x∈B⟼ιg∈xHom⁡Cx|∀y∈B∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f=x∈B⟼ιg∈xHom⁡Cx|∀y∈B∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f
5 3 4 fnmpti ⊢x∈B⟼ιg∈xHom⁡Cx|∀y∈B∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=fFnB
6 eqid ⊢Hom⁡C=Hom⁡C
7 eqid ⊢comp⁡C=comp⁡C
8 id ⊢C∈Cat→C∈Cat
9 1 6 7 8 2 cidfval ⊢C∈Cat→1˙=x∈B⟼ιg∈xHom⁡Cx|∀y∈B∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f
10 9 fneq1d ⊢C∈Cat→1˙FnB↔x∈B⟼ιg∈xHom⁡Cx|∀y∈B∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=fFnB
11 5 10 mpbiri ⊢C∈Cat→1˙FnB