Theorem paridval

Description: The identity at any object of a category with the parallel-arrow hom construction is J . (Contributed by Zhi Wang, 17-Sep-2026)

	Ref	Expression
Hypotheses	paridval.b	$$⊢B={\mathrm{Base}}_C$$
	paridval.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	paridval.hv	$$⊢H=\left(x\in B,y\in B⟼if\left(x=y,\left\{J\right\},if\left(\left(x=X\wedge y=Y\right),S,\varnothing \right)\right)\right)$$
	paridval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	paridval.u	$$⊢\phi \to U\in B$$
Assertion	paridval	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(U\right)=J$$

Proof

Step	Hyp	Ref	Expression
1		paridval.b	$$⊢B={\mathrm{Base}}_C$$
2		paridval.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
3		paridval.hv	$$⊢H=\left(x\in B,y\in B⟼if\left(x=y,\left\{J\right\},if\left(\left(x=X\wedge y=Y\right),S,\varnothing \right)\right)\right)$$
4		paridval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
5		paridval.u	$$⊢\phi \to U\in B$$
6		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
7	1 2 6 4 5	catidcl	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(U\right)\in \left(UHU\right)$$
8		eqidd	$$⊢\phi \to U=U$$
9	3 7 8	parhomideq	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(U\right)=J$$