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 ⊢ 𝐷 = ( 𝐶 ↾cat 𝐽 )
subccat.j ⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
subccatid.1 ⊢ ( 𝜑 → 𝐽 Fn ( 𝑆 × 𝑆 ) )
subccatid.2 ⊢ 1 = ( Id ‘ 𝐶 )
subcid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
Assertion subcid ( 𝜑 → ( 1 ‘ 𝑋 ) = ( ( Id ‘ 𝐷 ) ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 subccat.1 ⊢ 𝐷 = ( 𝐶 ↾cat 𝐽 )
2 subccat.j ⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
3 subccatid.1 ⊢ ( 𝜑 → 𝐽 Fn ( 𝑆 × 𝑆 ) )
4 subccatid.2 ⊢ 1 = ( Id ‘ 𝐶 )
5 subcid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
6 1 2 3 4 subccatid ⊢ ( 𝜑 → ( 𝐷 ∈ Cat ∧ ( Id ‘ 𝐷 ) = ( 𝑥 ∈ 𝑆 ↦ ( 1 ‘ 𝑥 ) ) ) )
7 6 simprd ⊢ ( 𝜑 → ( Id ‘ 𝐷 ) = ( 𝑥 ∈ 𝑆 ↦ ( 1 ‘ 𝑥 ) ) )
8 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
9 8 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 1 ‘ 𝑥 ) = ( 1 ‘ 𝑋 ) )
10 fvexd ⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) ∈ V )
11 7 9 5 10 fvmptd ⊢ ( 𝜑 → ( ( Id ‘ 𝐷 ) ‘ 𝑋 ) = ( 1 ‘ 𝑋 ) )
12 11 eqcomd ⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) = ( ( Id ‘ 𝐷 ) ‘ 𝑋 ) )