Theorem parhomidval

Description: On the diagonal, the parallel-arrow hom operation has value { J } . (Contributed by Zhi Wang, 16-Sep-2026)

	Ref	Expression
Hypothesis	parhomval.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
Assertion	parhomidval	⊢ ( 𝑈 ∈ 𝐵 → ( 𝑈 𝐻 𝑈 ) = { 𝐽 } )

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
2		eqtr3	⊢ ( ( 𝑥 = 𝑈 ∧ 𝑦 = 𝑈 ) → 𝑥 = 𝑦 )
3	2	iftrued	⊢ ( ( 𝑥 = 𝑈 ∧ 𝑦 = 𝑈 ) → if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) = { 𝐽 } )
4		snex	⊢ { 𝐽 } ∈ V
5	3 1 4	ovmpoa	⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝑈 ∈ 𝐵 ) → ( 𝑈 𝐻 𝑈 ) = { 𝐽 } )
6	5	anidms	⊢ ( 𝑈 ∈ 𝐵 → ( 𝑈 𝐻 𝑈 ) = { 𝐽 } )