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 = ( Base ` C )
	paridval.h	|- H = ( Hom ` C )
	paridval.hv	|- H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
	paridval.c	|- ( ph -> C e. Cat )
	paridval.u	|- ( ph -> U e. B )
Assertion	paridval	|- ( ph -> ( ( Id ` C ) ` U ) = J )

Proof

Step	Hyp	Ref	Expression
1		paridval.b	|- B = ( Base ` C )
2		paridval.h	|- H = ( Hom ` C )
3		paridval.hv	|- H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
4		paridval.c	|- ( ph -> C e. Cat )
5		paridval.u	|- ( ph -> U e. B )
6		eqid	|- ( Id ` C ) = ( Id ` C )
7	1 2 6 4 5	catidcl	|- ( ph -> ( ( Id ` C ) ` U ) e. ( U H U ) )
8		eqidd	|- ( ph -> U = U )
9	3 7 8	parhomideq	|- ( ph -> ( ( Id ` C ) ` U ) = J )