This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem catcid

Description: The identity arrow in the category of categories is the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses catccatid.c ⊢ C = CatCat ⁡ U
catccatid.b ⊢ B = Base C
catcid.o ⊢ 1 ˙ = Id ⁡ C
catcid.i ⊢ I = id func ⁡ X
catcid.u ⊢ φ → U ∈ V
catcid.x ⊢ φ → X ∈ B
Assertion catcid ⊢ φ → 1 ˙ ⁡ X = I

Proof

Step Hyp Ref Expression
1 catccatid.c ⊢ C = CatCat ⁡ U
2 catccatid.b ⊢ B = Base C
3 catcid.o ⊢ 1 ˙ = Id ⁡ C
4 catcid.i ⊢ I = id func ⁡ X
5 catcid.u ⊢ φ → U ∈ V
6 catcid.x ⊢ φ → X ∈ B
7 1 2 catccatid ⊢ U ∈ V → C ∈ Cat ∧ Id ⁡ C = x ∈ B ⟼ id func ⁡ x
8 5 7 syl ⊢ φ → C ∈ Cat ∧ Id ⁡ C = x ∈ B ⟼ id func ⁡ x
9 8 simprd ⊢ φ → Id ⁡ C = x ∈ B ⟼ id func ⁡ x
10 3 9 eqtrid ⊢ φ → 1 ˙ = x ∈ B ⟼ id func ⁡ x
11 simpr ⊢ φ ∧ x = X → x = X
12 11 fveq2d ⊢ φ ∧ x = X → id func ⁡ x = id func ⁡ X
13 fvexd ⊢ φ → id func ⁡ X ∈ V
14 10 12 6 13 fvmptd ⊢ φ → 1 ˙ ⁡ X = id func ⁡ X
15 14 4 eqtr4di ⊢ φ → 1 ˙ ⁡ X = I