Theorem subcidcl

Description: The identity of the original category is contained in each subcategory. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	subcidcl.j	$$⊢\phi \to J\in \mathrm{Subcat}\left(C\right)$$
	subcidcl.2	$$⊢\phi \to JFn\left(S\times S\right)$$
	subcidcl.x	$$⊢\phi \to X\in S$$
	subcidcl.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
Assertion	subcidcl	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)\in \left(XJX\right)$$

Proof

Step	Hyp	Ref	Expression
1		subcidcl.j	$$⊢\phi \to J\in \mathrm{Subcat}\left(C\right)$$
2		subcidcl.2	$$⊢\phi \to JFn\left(S\times S\right)$$
3		subcidcl.x	$$⊢\phi \to X\in S$$
4		subcidcl.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
5		fveq2	$$⊢x=X\to \underset{\dot{}}{1}\left(x\right)=\underset{\dot{}}{1}\left(X\right)$$
6		id	$$⊢x=X\to x=X$$
7	6 6	oveq12d	$$⊢x=X\to xJx=XJX$$
8	5 7	eleq12d	$$⊢x=X\to \left(\underset{\dot{}}{1}\left(x\right)\in \left(xJx\right)\leftrightarrow \underset{\dot{}}{1}\left(X\right)\in \left(XJX\right)\right)$$
9		eqid	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(C\right)$$
10		eqid	$$⊢\mathrm{comp}\left(C\right)=\mathrm{comp}\left(C\right)$$
11		subcrcl	$$⊢J\in \mathrm{Subcat}\left(C\right)\to C\in \mathrm{Cat}$$
12	1 11	syl	$$⊢\phi \to C\in \mathrm{Cat}$$
13	9 4 10 12 2	issubc2	$$⊢\phi \to \left(J\in \mathrm{Subcat}\left(C\right)\leftrightarrow \left(J{\subseteq }_{\mathrm{cat}}{\mathrm{Hom}}_{𝑓}\left(C\right)\wedge \forall x\in S\left(\underset{\dot{}}{1}\left(x\right)\in \left(xJx\right)\wedge \forall y\in S\forall z\in S\forall f\in \left(xJy\right)\forall g\in \left(yJz\right)g\left(⟨x,y⟩\mathrm{comp}\left(C\right)z\right)f\in \left(xJz\right)\right)\right)\right)$$
14	1 13	mpbid	$$⊢\phi \to \left(J{\subseteq }_{\mathrm{cat}}{\mathrm{Hom}}_{𝑓}\left(C\right)\wedge \forall x\in S\left(\underset{\dot{}}{1}\left(x\right)\in \left(xJx\right)\wedge \forall y\in S\forall z\in S\forall f\in \left(xJy\right)\forall g\in \left(yJz\right)g\left(⟨x,y⟩\mathrm{comp}\left(C\right)z\right)f\in \left(xJz\right)\right)\right)$$
15		simpl	$$⊢\left(\underset{\dot{}}{1}\left(x\right)\in \left(xJx\right)\wedge \forall y\in S\forall z\in S\forall f\in \left(xJy\right)\forall g\in \left(yJz\right)g\left(⟨x,y⟩\mathrm{comp}\left(C\right)z\right)f\in \left(xJz\right)\right)\to \underset{\dot{}}{1}\left(x\right)\in \left(xJx\right)$$
16	15	ralimi	$$⊢\forall x\in S\left(\underset{\dot{}}{1}\left(x\right)\in \left(xJx\right)\wedge \forall y\in S\forall z\in S\forall f\in \left(xJy\right)\forall g\in \left(yJz\right)g\left(⟨x,y⟩\mathrm{comp}\left(C\right)z\right)f\in \left(xJz\right)\right)\to \forall x\in S\underset{\dot{}}{1}\left(x\right)\in \left(xJx\right)$$
17	14 16	simpl2im	$$⊢\phi \to \forall x\in S\underset{\dot{}}{1}\left(x\right)\in \left(xJx\right)$$
18	8 17 3	rspcdva	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)\in \left(XJX\right)$$