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 ‘ 𝐷 ) ‘ 𝑋 ) )