Theorem issubc2

Description: Elementhood in the set of subcategories. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	issubc.h	$$⊢H={\mathrm{Hom}}_{𝑓}\left(C\right)$$
	issubc.i	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
	issubc.o	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
	issubc.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	issubc2.a	$$⊢\phi \to JFn\left(S\times S\right)$$
Assertion	issubc2	$$⊢\phi \to \left(J\in \mathrm{Subcat}\left(C\right)\leftrightarrow \left(J{\subseteq }_{\mathrm{cat}}H\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⟩\underset{\dot{}}{·}z\right)f\in \left(xJz\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		issubc.h	$$⊢H={\mathrm{Hom}}_{𝑓}\left(C\right)$$
2		issubc.i	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
3		issubc.o	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
4		issubc.c	$$⊢\phi \to C\in \mathrm{Cat}$$
5		issubc2.a	$$⊢\phi \to JFn\left(S\times S\right)$$
6	5	fndmd	$$⊢\phi \to \mathrm{dom}J=S\times S$$
7	6	dmeqd	$$⊢\phi \to \mathrm{dom}\mathrm{dom}J=\mathrm{dom}\left(S\times S\right)$$
8		dmxpid	$$⊢\mathrm{dom}\left(S\times S\right)=S$$
9	7 8	eqtr2di	$$⊢\phi \to S=\mathrm{dom}\mathrm{dom}J$$
10	1 2 3 4 9	issubc	$$⊢\phi \to \left(J\in \mathrm{Subcat}\left(C\right)\leftrightarrow \left(J{\subseteq }_{\mathrm{cat}}H\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⟩\underset{\dot{}}{·}z\right)f\in \left(xJz\right)\right)\right)\right)$$