Theorem resccatlem

Description: Lemma for resccat . (Contributed by Zhi Wang, 6-Nov-2025)

	Ref	Expression
Hypotheses	resccat.d	$$⊢D=C{\upharpoonright }_{\mathrm{cat}}J$$
	resccat.b	$$⊢B={\mathrm{Base}}_C$$
	resccat.s	$$⊢S={\mathrm{Base}}_E$$
	resccat.j	$$⊢J={\mathrm{Hom}}_{𝑓}\left(E\right)$$
	resccat.x	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
	resccat.xb	$$⊢\underset{\dot{}}{\bullet }=\mathrm{comp}\left(E\right)$$
	resccat.1	$$⊢\left(\left(\phi \wedge \left(x\in S\wedge y\in S\wedge z\in S\right)\right)\wedge \left(f\in \left(xJy\right)\wedge g\in \left(yJz\right)\right)\right)\to g\left(⟨x,y⟩\underset{\dot{}}{·}z\right)f=g\left(⟨x,y⟩\underset{\dot{}}{\bullet }z\right)f$$
	resccat.e	$$⊢\phi \to E\in V$$
	resccat.ss	$$⊢\phi \to S\subseteq B$$
	resccatlem.c	$$⊢\phi \to C\in U$$
Assertion	resccatlem	$$⊢\phi \to \left(D\in \mathrm{Cat}\leftrightarrow E\in \mathrm{Cat}\right)$$

Proof

Step	Hyp	Ref	Expression
1		resccat.d	$$⊢D=C{\upharpoonright }_{\mathrm{cat}}J$$
2		resccat.b	$$⊢B={\mathrm{Base}}_C$$
3		resccat.s	$$⊢S={\mathrm{Base}}_E$$
4		resccat.j	$$⊢J={\mathrm{Hom}}_{𝑓}\left(E\right)$$
5		resccat.x	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
6		resccat.xb	$$⊢\underset{\dot{}}{\bullet }=\mathrm{comp}\left(E\right)$$
7		resccat.1	$$⊢\left(\left(\phi \wedge \left(x\in S\wedge y\in S\wedge z\in S\right)\right)\wedge \left(f\in \left(xJy\right)\wedge g\in \left(yJz\right)\right)\right)\to g\left(⟨x,y⟩\underset{\dot{}}{·}z\right)f=g\left(⟨x,y⟩\underset{\dot{}}{\bullet }z\right)f$$
8		resccat.e	$$⊢\phi \to E\in V$$
9		resccat.ss	$$⊢\phi \to S\subseteq B$$
10		resccatlem.c	$$⊢\phi \to C\in U$$
11	4 3	homffn	$$⊢JFn\left(S\times S\right)$$
12	11	a1i	$$⊢\phi \to JFn\left(S\times S\right)$$
13	1 2 10 12 9	reschomf	$$⊢\phi \to J={\mathrm{Hom}}_{𝑓}\left(D\right)$$
14	13 4	eqtr3di	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(D\right)={\mathrm{Hom}}_{𝑓}\left(E\right)$$
15	7	ralrimivva	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\wedge z\in S\right)\right)\to \forall f\in \left(xJy\right)\forall g\in \left(yJz\right)g\left(⟨x,y⟩\underset{\dot{}}{·}z\right)f=g\left(⟨x,y⟩\underset{\dot{}}{\bullet }z\right)f$$
16	15	ralrimivvva	$$⊢\phi \to \forall x\in S\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=g\left(⟨x,y⟩\underset{\dot{}}{\bullet }z\right)f$$
17		eqid	$$⊢\mathrm{comp}\left(D\right)=\mathrm{comp}\left(D\right)$$
18		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
19	1 2 10 12 9	rescbas	$$⊢\phi \to S={\mathrm{Base}}_D$$
20	3	a1i	$$⊢\phi \to S={\mathrm{Base}}_E$$
21	17 6 18 19 20 14	comfeq	$$⊢\phi \to \left({\mathrm{comp}}_{𝑓}\left(D\right)={\mathrm{comp}}_{𝑓}\left(E\right)\leftrightarrow \forall x\in S\forall y\in S\forall z\in S\forall f\in \left(x\mathrm{Hom}\left(D\right)y\right)\forall g\in \left(y\mathrm{Hom}\left(D\right)z\right)g\left(⟨x,y⟩\mathrm{comp}\left(D\right)z\right)f=g\left(⟨x,y⟩\underset{\dot{}}{\bullet }z\right)f\right)$$
22	1 2 10 12 9	reschom	$$⊢\phi \to J=\mathrm{Hom}\left(D\right)$$
23	22	oveqd	$$⊢\phi \to xJy=x\mathrm{Hom}\left(D\right)y$$
24	22	oveqd	$$⊢\phi \to yJz=y\mathrm{Hom}\left(D\right)z$$
25	1 2 10 12 9 5	rescco	$$⊢\phi \to \underset{\dot{}}{·}=\mathrm{comp}\left(D\right)$$
26	25	oveqd	$$⊢\phi \to ⟨x,y⟩\underset{\dot{}}{·}z=⟨x,y⟩\mathrm{comp}\left(D\right)z$$
27	26	oveqd	$$⊢\phi \to g\left(⟨x,y⟩\underset{\dot{}}{·}z\right)f=g\left(⟨x,y⟩\mathrm{comp}\left(D\right)z\right)f$$
28	27	eqeq1d	$$⊢\phi \to \left(g\left(⟨x,y⟩\underset{\dot{}}{·}z\right)f=g\left(⟨x,y⟩\underset{\dot{}}{\bullet }z\right)f\leftrightarrow g\left(⟨x,y⟩\mathrm{comp}\left(D\right)z\right)f=g\left(⟨x,y⟩\underset{\dot{}}{\bullet }z\right)f\right)$$
29	24 28	raleqbidv	$$⊢\phi \to \left(\forall g\in \left(yJz\right)g\left(⟨x,y⟩\underset{\dot{}}{·}z\right)f=g\left(⟨x,y⟩\underset{\dot{}}{\bullet }z\right)f\leftrightarrow \forall g\in \left(y\mathrm{Hom}\left(D\right)z\right)g\left(⟨x,y⟩\mathrm{comp}\left(D\right)z\right)f=g\left(⟨x,y⟩\underset{\dot{}}{\bullet }z\right)f\right)$$
30	23 29	raleqbidv	$$⊢\phi \to \left(\forall f\in \left(xJy\right)\forall g\in \left(yJz\right)g\left(⟨x,y⟩\underset{\dot{}}{·}z\right)f=g\left(⟨x,y⟩\underset{\dot{}}{\bullet }z\right)f\leftrightarrow \forall f\in \left(x\mathrm{Hom}\left(D\right)y\right)\forall g\in \left(y\mathrm{Hom}\left(D\right)z\right)g\left(⟨x,y⟩\mathrm{comp}\left(D\right)z\right)f=g\left(⟨x,y⟩\underset{\dot{}}{\bullet }z\right)f\right)$$
31	30	3ralbidv	$$⊢\phi \to \left(\forall x\in S\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=g\left(⟨x,y⟩\underset{\dot{}}{\bullet }z\right)f\leftrightarrow \forall x\in S\forall y\in S\forall z\in S\forall f\in \left(x\mathrm{Hom}\left(D\right)y\right)\forall g\in \left(y\mathrm{Hom}\left(D\right)z\right)g\left(⟨x,y⟩\mathrm{comp}\left(D\right)z\right)f=g\left(⟨x,y⟩\underset{\dot{}}{\bullet }z\right)f\right)$$
32	21 31	bitr4d	$$⊢\phi \to \left({\mathrm{comp}}_{𝑓}\left(D\right)={\mathrm{comp}}_{𝑓}\left(E\right)\leftrightarrow \forall x\in S\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=g\left(⟨x,y⟩\underset{\dot{}}{\bullet }z\right)f\right)$$
33	16 32	mpbird	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(D\right)={\mathrm{comp}}_{𝑓}\left(E\right)$$
34	1	ovexi	$$⊢D\in \mathrm{V}$$
35	34	a1i	$$⊢\phi \to D\in \mathrm{V}$$
36	14 33 35 8	catpropd	$$⊢\phi \to \left(D\in \mathrm{Cat}\leftrightarrow E\in \mathrm{Cat}\right)$$