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

Metamath Proof Explorer

Theorem subcid

Description: The identity in a subcategory is the same as the original category. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses subccat.1 ⊢ D = C ↾ cat J
subccat.j ⊢ φ → J ∈ Subcat ⁡ C
subccatid.1 ⊢ φ → J Fn S × S
subccatid.2 ⊢ 1 ˙ = Id ⁡ C
subcid.x ⊢ φ → X ∈ S
Assertion subcid ⊢ φ → 1 ˙ ⁡ X = Id ⁡ D ⁡ X

Proof

Step Hyp Ref Expression
1 subccat.1 ⊢ D = C ↾ cat J
2 subccat.j ⊢ φ → J ∈ Subcat ⁡ C
3 subccatid.1 ⊢ φ → J Fn S × S
4 subccatid.2 ⊢ 1 ˙ = Id ⁡ C
5 subcid.x ⊢ φ → X ∈ S
6 1 2 3 4 subccatid ⊢ φ → D ∈ Cat ∧ Id ⁡ D = x ∈ S ⟼ 1 ˙ ⁡ x
7 6 simprd ⊢ φ → Id ⁡ D = x ∈ S ⟼ 1 ˙ ⁡ x
8 simpr ⊢ φ ∧ x = X → x = X
9 8 fveq2d ⊢ φ ∧ x = X → 1 ˙ ⁡ x = 1 ˙ ⁡ X
10 fvexd ⊢ φ → 1 ˙ ⁡ X ∈ V
11 7 9 5 10 fvmptd ⊢ φ → Id ⁡ D ⁡ X = 1 ˙ ⁡ X
12 11 eqcomd ⊢ φ → 1 ˙ ⁡ X = Id ⁡ D ⁡ X