Metamath Proof Explorer

Theorem parhomvaln0

Description: Evaluate an inhabited parallel-arrow hom-set. Membership certifies the selected branch even when sethood hypotheses are unavailable. Compare parhomval for evaluation throughout the object domain. (Contributed by Zhi Wang, 17-Sep-2026)

Ref Expression
Hypothesis parhomval.h ⊢ H = x ∈ B , y ∈ B ⟼ if x = y J if x = X ∧ y = Y S ∅
Assertion parhomvaln0 ⊢ F ∈ U H V → 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 nfcv ⊢ Ⅎ _ a if x = y J if x = X ∧ y = Y S ∅
3 nfcv ⊢ Ⅎ _ b if x = y J if x = X ∧ y = Y S ∅
4 nfcv ⊢ Ⅎ _ x if a = b J if a = X ∧ b = Y S ∅
5 nfcv ⊢ Ⅎ _ y if a = b J if a = X ∧ b = Y S ∅
6 eqeq12 ⊢ x = a ∧ y = b → x = y ↔ a = b
7 simpl ⊢ x = a ∧ y = b → x = a
8 7 eqeq1d ⊢ x = a ∧ y = b → x = X ↔ a = X
9 simpr ⊢ x = a ∧ y = b → y = b
10 9 eqeq1d ⊢ x = a ∧ y = b → y = Y ↔ b = Y
11 8 10 anbi12d ⊢ x = a ∧ y = b → x = X ∧ y = Y ↔ a = X ∧ b = Y
12 11 ifbid ⊢ x = a ∧ y = b → if x = X ∧ y = Y S ∅ = if a = X ∧ b = Y S ∅
13 6 12 ifbieq2d ⊢ x = a ∧ y = b → if x = y J if x = X ∧ y = Y S ∅ = if a = b J if a = X ∧ b = Y S ∅
14 2 3 4 5 13 cbvmpo ⊢ x ∈ B , y ∈ B ⟼ if x = y J if x = X ∧ y = Y S ∅ = a ∈ B , b ∈ B ⟼ if a = b J if a = X ∧ b = Y S ∅
15 1 14 eqtri ⊢ H = a ∈ B , b ∈ B ⟼ if a = b J if a = X ∧ b = Y S ∅
16 eqeq12 ⊢ a = U ∧ b = V → a = b ↔ U = V
17 simpl ⊢ a = U ∧ b = V → a = U
18 17 eqeq1d ⊢ a = U ∧ b = V → a = X ↔ U = X
19 simpr ⊢ a = U ∧ b = V → b = V
20 19 eqeq1d ⊢ a = U ∧ b = V → b = Y ↔ V = Y
21 18 20 anbi12d ⊢ a = U ∧ b = V → a = X ∧ b = Y ↔ U = X ∧ V = Y
22 21 ifbid ⊢ a = U ∧ b = V → if a = X ∧ b = Y S ∅ = if U = X ∧ V = Y S ∅
23 16 22 ifbieq2d ⊢ a = U ∧ b = V → if a = b J if a = X ∧ b = Y S ∅ = if U = V J if U = X ∧ V = Y S ∅
24 15 23 elovmpoeq ⊢ F ∈ U H V → U H V = if U = V J if U = X ∧ V = Y S ∅