Metamath Proof Explorer

Theorem parhomne

Description: A morphism between different objects has the distinguished source and target. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

Ref Expression
Hypotheses parhomval.h ⊢ H = x ∈ B , y ∈ B ⟼ if x = y J if x = X ∧ y = Y S ∅
parhomne.f ⊢ φ → F ∈ U H V
parhomne.n ⊢ φ → ¬ U = V
Assertion parhomne ⊢ φ → U = X ∧ V = Y

Proof

Step Hyp Ref Expression
1 parhomval.h ⊢ H = x ∈ B , y ∈ B ⟼ if x = y J if x = X ∧ y = Y S ∅
2 parhomne.f ⊢ φ → F ∈ U H V
3 parhomne.n ⊢ φ → ¬ U = V
4 1 parhomvaln0 ⊢ F ∈ U H V → U H V = if U = V J if U = X ∧ V = Y S ∅
5 2 4 syl ⊢ φ → U H V = if U = V J if U = X ∧ V = Y S ∅
6 3 iffalsed ⊢ φ → if U = V J if U = X ∧ V = Y S ∅ = if U = X ∧ V = Y S ∅
7 5 6 eqtrd ⊢ φ → U H V = if U = X ∧ V = Y S ∅
8 2 7 eleqtrd ⊢ φ → F ∈ if U = X ∧ V = Y S ∅
9 elif0 ⊢ F ∈ if U = X ∧ V = Y S ∅ ↔ U = X ∧ V = Y ∧ F ∈ S
10 8 9 sylib ⊢ φ → U = X ∧ V = Y ∧ F ∈ S
11 10 simpld ⊢ φ → U = X ∧ V = Y