Theorem parhomval

Description: At objects in the base, the hom operation has value { J } on the diagonal, S from the distinguished source to target, and the empty set otherwise. (Contributed by Zhi Wang, 14-Sep-2026)

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

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
2		parhomval.s	⊢ 𝑆 ∈ V
3		eqeq12	⊢ ( ( 𝑥 = 𝑈 ∧ 𝑦 = 𝑉 ) → ( 𝑥 = 𝑦 ↔ 𝑈 = 𝑉 ) )
4		simpl	⊢ ( ( 𝑥 = 𝑈 ∧ 𝑦 = 𝑉 ) → 𝑥 = 𝑈 )
5	4	eqeq1d	⊢ ( ( 𝑥 = 𝑈 ∧ 𝑦 = 𝑉 ) → ( 𝑥 = 𝑋 ↔ 𝑈 = 𝑋 ) )
6		simpr	⊢ ( ( 𝑥 = 𝑈 ∧ 𝑦 = 𝑉 ) → 𝑦 = 𝑉 )
7	6	eqeq1d	⊢ ( ( 𝑥 = 𝑈 ∧ 𝑦 = 𝑉 ) → ( 𝑦 = 𝑌 ↔ 𝑉 = 𝑌 ) )
8	5 7	anbi12d	⊢ ( ( 𝑥 = 𝑈 ∧ 𝑦 = 𝑉 ) → ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ↔ ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ) )
9	8	ifbid	⊢ ( ( 𝑥 = 𝑈 ∧ 𝑦 = 𝑉 ) → if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) = if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) )
10	3 9	ifbieq2d	⊢ ( ( 𝑥 = 𝑈 ∧ 𝑦 = 𝑉 ) → if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) = if ( 𝑈 = 𝑉 , { 𝐽 } , if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ) )
11		snex	⊢ { 𝐽 } ∈ V
12		0ex	⊢ ∅ ∈ V
13	2 12	ifex	⊢ if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ∈ V
14	11 13	ifex	⊢ if ( 𝑈 = 𝑉 , { 𝐽 } , if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ) ∈ V
15	10 1 14	ovmpoa	⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( 𝑈 𝐻 𝑉 ) = if ( 𝑈 = 𝑉 , { 𝐽 } , if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ) )