Theorem parhomel

Description: Membership in a hom-set of a parallel-arrow category is equivalent to being its identity value on the diagonal, or a member of S at the distinguished source and target. (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
	parhomel.j	|- J e. _V
Assertion	parhomel	|- ( ( U e. B /\ V e. B ) -> ( F e. ( U H V ) <-> ( ( U = V /\ F = J ) \/ ( -. U = V /\ ( ( U = X /\ V = Y ) /\ F e. 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		parhomel.j	|- J e. _V
4	1 2	parhomval	|- ( ( U e. B /\ V e. B ) -> ( U H V ) = if ( U = V , { J } , if ( ( U = X /\ V = Y ) , S , (/) ) ) )
5	4	eleq2d	|- ( ( U e. B /\ V e. B ) -> ( F e. ( U H V ) <-> F e. if ( U = V , { J } , if ( ( U = X /\ V = Y ) , S , (/) ) ) ) )
6		elif	|- ( F e. if ( U = V , { J } , if ( ( U = X /\ V = Y ) , S , (/) ) ) <-> ( ( U = V /\ F e. { J } ) \/ ( -. U = V /\ F e. if ( ( U = X /\ V = Y ) , S , (/) ) ) ) )
7	3	elsn2	|- ( F e. { J } <-> F = J )
8	7	anbi2i	|- ( ( U = V /\ F e. { J } ) <-> ( U = V /\ F = J ) )
9		elif0	|- ( F e. if ( ( U = X /\ V = Y ) , S , (/) ) <-> ( ( U = X /\ V = Y ) /\ F e. S ) )
10	9	anbi2i	|- ( ( -. U = V /\ F e. if ( ( U = X /\ V = Y ) , S , (/) ) ) <-> ( -. U = V /\ ( ( U = X /\ V = Y ) /\ F e. S ) ) )
11	8 10	orbi12i	|- ( ( ( U = V /\ F e. { J } ) \/ ( -. U = V /\ F e. if ( ( U = X /\ V = Y ) , S , (/) ) ) ) <-> ( ( U = V /\ F = J ) \/ ( -. U = V /\ ( ( U = X /\ V = Y ) /\ F e. S ) ) ) )
12	6 11	bitri	|- ( F e. if ( U = V , { J } , if ( ( U = X /\ V = Y ) , S , (/) ) ) <-> ( ( U = V /\ F = J ) \/ ( -. U = V /\ ( ( U = X /\ V = Y ) /\ F e. S ) ) ) )
13	5 12	bitrdi	|- ( ( U e. B /\ V e. B ) -> ( F e. ( U H V ) <-> ( ( U = V /\ F = J ) \/ ( -. U = V /\ ( ( U = X /\ V = Y ) /\ F e. S ) ) ) ) )