Metamath Proof Explorer

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 ∈ B , y ∈ B ⟼ if x = y J if x = X ∧ y = Y S ∅
parhomval.s ⊢ S ∈ V
parhomel.j ⊢ J ∈ V
Assertion parhomel ⊢ U ∈ B ∧ V ∈ B → F ∈ U H V ↔ U = V ∧ F = J ∨ ¬ U = V ∧ U = X ∧ V = Y ∧ F ∈ S

Proof

Step Hyp Ref Expression
1 parhomval.h ⊢ H = x ∈ B , y ∈ B ⟼ if x = y J if x = X ∧ y = Y S ∅
2 parhomval.s ⊢ S ∈ V
3 parhomel.j ⊢ J ∈ V
4 1 2 parhomval ⊢ U ∈ B ∧ V ∈ B → U H V = if U = V J if U = X ∧ V = Y S ∅
5 4 eleq2d ⊢ U ∈ B ∧ V ∈ B → F ∈ U H V ↔ F ∈ if U = V J if U = X ∧ V = Y S ∅
6 elif ⊢ F ∈ if U = V J if U = X ∧ V = Y S ∅ ↔ U = V ∧ F ∈ J ∨ ¬ U = V ∧ F ∈ if U = X ∧ V = Y S ∅
7 3 elsn2 ⊢ F ∈ J ↔ F = J
8 7 anbi2i ⊢ U = V ∧ F ∈ J ↔ U = V ∧ F = J
9 elif0 ⊢ F ∈ if U = X ∧ V = Y S ∅ ↔ U = X ∧ V = Y ∧ F ∈ S
10 9 anbi2i ⊢ ¬ U = V ∧ F ∈ if U = X ∧ V = Y S ∅ ↔ ¬ U = V ∧ U = X ∧ V = Y ∧ F ∈ S
11 8 10 orbi12i ⊢ U = V ∧ F ∈ J ∨ ¬ U = V ∧ F ∈ if U = X ∧ V = Y S ∅ ↔ U = V ∧ F = J ∨ ¬ U = V ∧ U = X ∧ V = Y ∧ F ∈ S
12 6 11 bitri ⊢ F ∈ if U = V J if U = X ∧ V = Y S ∅ ↔ U = V ∧ F = J ∨ ¬ U = V ∧ U = X ∧ V = Y ∧ F ∈ S
13 5 12 bitrdi ⊢ U ∈ B ∧ V ∈ B → F ∈ U H V ↔ U = V ∧ F = J ∨ ¬ U = V ∧ U = X ∧ V = Y ∧ F ∈ S