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{\upharpoonright }_{\mathrm{cat}}J$$
	subccat.j	$$⊢\phi \to J\in \mathrm{Subcat}\left(C\right)$$
	subccatid.1	$$⊢\phi \to JFn\left(S\times S\right)$$
	subccatid.2	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
	subcid.x	$$⊢\phi \to X\in S$$
Assertion	subcid	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)=\mathrm{Id}\left(D\right)\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		subccat.1	$$⊢D=C{\upharpoonright }_{\mathrm{cat}}J$$
2		subccat.j	$$⊢\phi \to J\in \mathrm{Subcat}\left(C\right)$$
3		subccatid.1	$$⊢\phi \to JFn\left(S\times S\right)$$
4		subccatid.2	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
5		subcid.x	$$⊢\phi \to X\in S$$
6	1 2 3 4	subccatid	$$⊢\phi \to \left(D\in \mathrm{Cat}\wedge \mathrm{Id}\left(D\right)=\left(x\in S⟼\underset{\dot{}}{1}\left(x\right)\right)\right)$$
7	6	simprd	$$⊢\phi \to \mathrm{Id}\left(D\right)=\left(x\in S⟼\underset{\dot{}}{1}\left(x\right)\right)$$
8		simpr	$$⊢\left(\phi \wedge x=X\right)\to x=X$$
9	8	fveq2d	$$⊢\left(\phi \wedge x=X\right)\to \underset{\dot{}}{1}\left(x\right)=\underset{\dot{}}{1}\left(X\right)$$
10		fvexd	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)\in \mathrm{V}$$
11	7 9 5 10	fvmptd	$$⊢\phi \to \mathrm{Id}\left(D\right)\left(X\right)=\underset{\dot{}}{1}\left(X\right)$$
12	11	eqcomd	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)=\mathrm{Id}\left(D\right)\left(X\right)$$