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	|- H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
	parhomval.s	|- S e. _V
Assertion	parhomval	|- ( ( U e. B /\ V e. B ) -> ( U H V ) = if ( U = V , { J } , if ( ( U = X /\ V = Y ) , S , (/) ) ) )

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	|- H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
2		parhomval.s	|- S e. _V
3		eqeq12	|- ( ( x = U /\ y = V ) -> ( x = y <-> U = V ) )
4		simpl	|- ( ( x = U /\ y = V ) -> x = U )
5	4	eqeq1d	|- ( ( x = U /\ y = V ) -> ( x = X <-> U = X ) )
6		simpr	|- ( ( x = U /\ y = V ) -> y = V )
7	6	eqeq1d	|- ( ( x = U /\ y = V ) -> ( y = Y <-> V = Y ) )
8	5 7	anbi12d	|- ( ( x = U /\ y = V ) -> ( ( x = X /\ y = Y ) <-> ( U = X /\ V = Y ) ) )
9	8	ifbid	|- ( ( x = U /\ y = V ) -> if ( ( x = X /\ y = Y ) , S , (/) ) = if ( ( U = X /\ V = Y ) , S , (/) ) )
10	3 9	ifbieq2d	|- ( ( x = U /\ y = V ) -> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) = if ( U = V , { J } , if ( ( U = X /\ V = Y ) , S , (/) ) ) )
11		snex	|- { J } e. _V
12		0ex	|- (/) e. _V
13	2 12	ifex	|- if ( ( U = X /\ V = Y ) , S , (/) ) e. _V
14	11 13	ifex	|- if ( U = V , { J } , if ( ( U = X /\ V = Y ) , S , (/) ) ) e. _V
15	10 1 14	ovmpoa	|- ( ( U e. B /\ V e. B ) -> ( U H V ) = if ( U = V , { J } , if ( ( U = X /\ V = Y ) , S , (/) ) ) )