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	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
	parhomval.s	⊢ 𝑆 ∈ V
	parhomel.j	⊢ 𝐽 ∈ V
Assertion	parhomel	⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) ↔ ( ( 𝑈 = 𝑉 ∧ 𝐹 = 𝐽 ) ∨ ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
2		parhomval.s	⊢ 𝑆 ∈ V
3		parhomel.j	⊢ 𝐽 ∈ V
4	1 2	parhomval	⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( 𝑈 𝐻 𝑉 ) = if ( 𝑈 = 𝑉 , { 𝐽 } , if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ) )
5	4	eleq2d	⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) ↔ 𝐹 ∈ if ( 𝑈 = 𝑉 , { 𝐽 } , if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ) ) )
6		elif	⊢ ( 𝐹 ∈ if ( 𝑈 = 𝑉 , { 𝐽 } , if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ) ↔ ( ( 𝑈 = 𝑉 ∧ 𝐹 ∈ { 𝐽 } ) ∨ ( ¬ 𝑈 = 𝑉 ∧ 𝐹 ∈ if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ) ) )
7	3	elsn2	⊢ ( 𝐹 ∈ { 𝐽 } ↔ 𝐹 = 𝐽 )
8	7	anbi2i	⊢ ( ( 𝑈 = 𝑉 ∧ 𝐹 ∈ { 𝐽 } ) ↔ ( 𝑈 = 𝑉 ∧ 𝐹 = 𝐽 ) )
9		elif0	⊢ ( 𝐹 ∈ if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ↔ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) )
10	9	anbi2i	⊢ ( ( ¬ 𝑈 = 𝑉 ∧ 𝐹 ∈ if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ) ↔ ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) ) )
11	8 10	orbi12i	⊢ ( ( ( 𝑈 = 𝑉 ∧ 𝐹 ∈ { 𝐽 } ) ∨ ( ¬ 𝑈 = 𝑉 ∧ 𝐹 ∈ if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ) ) ↔ ( ( 𝑈 = 𝑉 ∧ 𝐹 = 𝐽 ) ∨ ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) ) ) )
12	6 11	bitri	⊢ ( 𝐹 ∈ if ( 𝑈 = 𝑉 , { 𝐽 } , if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ) ↔ ( ( 𝑈 = 𝑉 ∧ 𝐹 = 𝐽 ) ∨ ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) ) ) )
13	5 12	bitrdi	⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) ↔ ( ( 𝑈 = 𝑉 ∧ 𝐹 = 𝐽 ) ∨ ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) ) ) ) )