Metamath Proof Explorer

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 ∈ B , y ∈ B ⟼ if x = y J if x = X ∧ y = Y S ∅
parhomval.s ⊢ S ∈ V
Assertion parhomval ⊢ U ∈ B ∧ V ∈ B → U H V = if U = V J if U = X ∧ V = Y 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 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 ∈ V
12 0ex ⊢ ∅ ∈ V
13 2 12 ifex ⊢ if U = X ∧ V = Y S ∅ ∈ V
14 11 13 ifex ⊢ if U = V J if U = X ∧ V = Y S ∅ ∈ V
15 10 1 14 ovmpoa ⊢ U ∈ B ∧ V ∈ B → U H V = if U = V J if U = X ∧ V = Y S ∅