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 = Base C
catidcl.h ⊢ H = Hom ⁡ C
catidcl.i ⊢ 1 ˙ = Id ⁡ C
catidcl.c ⊢ φ → C ∈ Cat
catidcl.x ⊢ φ → X ∈ B
Assertion catidcl ⊢ φ → 1 ˙ ⁡ X ∈ X H X

Proof

Step Hyp Ref Expression
1 catidcl.b ⊢ B = Base C
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 ∈ X H X | ∀ y ∈ B ∀ f ∈ y H X g y X comp ⁡ C X f = f ∧ ∀ f ∈ X H y f X X comp ⁡ C y g = f
8 1 2 6 4 5 catideu ⊢ φ → ∃! g ∈ X H X ∀ y ∈ B ∀ f ∈ y H X g y X comp ⁡ C X f = f ∧ ∀ f ∈ X H y f X X comp ⁡ C y g = f
9 riotacl ⊢ ∃! g ∈ X H X ∀ y ∈ B ∀ f ∈ y H X g y X comp ⁡ C X f = f ∧ ∀ f ∈ X H y f X X comp ⁡ C y g = f → ι g ∈ X H X | ∀ y ∈ B ∀ f ∈ y H X g y X comp ⁡ C X f = f ∧ ∀ f ∈ X H y f X X comp ⁡ C y g = f ∈ X H X
10 8 9 syl ⊢ φ → ι g ∈ X H X | ∀ y ∈ B ∀ f ∈ y H X g y X comp ⁡ C X f = f ∧ ∀ f ∈ X H y f X X comp ⁡ C y g = f ∈ X H X
11 7 10 eqeltrd ⊢ φ → 1 ˙ ⁡ X ∈ X H X