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	⊢ 𝐵 = ( Base ‘ 𝐶 )
	paridval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	paridval.hv	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
	paridval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	paridval.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
Assertion	paridval	⊢ ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑈 ) = 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		paridval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		paridval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
3		paridval.hv	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
4		paridval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
5		paridval.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
6		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
7	1 2 6 4 5	catidcl	⊢ ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑈 ) ∈ ( 𝑈 𝐻 𝑈 ) )
8		eqidd	⊢ ( 𝜑 → 𝑈 = 𝑈 )
9	3 7 8	parhomideq	⊢ ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑈 ) = 𝐽 )