Metamath Proof Explorer

Theorem catidcl

Description: Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses catidcl.b ⊢B=BaseC
catidcl.h ⊢H=Hom⁡C
catidcl.i ⊢1˙=Id⁡C
catidcl.c ⊢φ→C∈Cat
catidcl.x ⊢φ→X∈B
Assertion catidcl ⊢φ→1˙⁡X∈XHX

Proof

Step Hyp Ref Expression
1 catidcl.b ⊢B=BaseC
2 catidcl.h ⊢H=Hom⁡C
3 catidcl.i ⊢1˙=Id⁡C
4 catidcl.c ⊢φ→C∈Cat
5 catidcl.x ⊢φ→X∈B
6 eqid ⊢comp⁡C=comp⁡C
7 1 2 6 4 3 5 cidval ⊢φ→1˙⁡X=ιg∈XHX|∀y∈B∀f∈yHXgyXcomp⁡CXf=f∧∀f∈XHyfXXcomp⁡Cyg=f
8 1 2 6 4 5 catideu ⊢φ→∃!g∈XHX∀y∈B∀f∈yHXgyXcomp⁡CXf=f∧∀f∈XHyfXXcomp⁡Cyg=f
9 riotacl ⊢∃!g∈XHX∀y∈B∀f∈yHXgyXcomp⁡CXf=f∧∀f∈XHyfXXcomp⁡Cyg=f→ιg∈XHX|∀y∈B∀f∈yHXgyXcomp⁡CXf=f∧∀f∈XHyfXXcomp⁡Cyg=f∈XHX
10 8 9 syl ⊢φ→ιg∈XHX|∀y∈B∀f∈yHXgyXcomp⁡CXf=f∧∀f∈XHyfXXcomp⁡Cyg=f∈XHX
11 7 10 eqeltrd ⊢φ→1˙⁡X∈XHX