Metamath Proof Explorer

Theorem parhomne2

Description: Variant of parhomne . (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026) (New usage is discouraged.) (Proof modification is discouraged.)

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
parhomne2.s ⊢ S ∈ V
parhomne2.j ⊢ J ∈ V
parhomne2.u ⊢ φ → U ∈ B
parhomne2.v ⊢ φ → V ∈ B
Assertion parhomne2 ⊢ φ → 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 parhomne2.s ⊢ S ∈ V
5 parhomne2.j ⊢ J ∈ V
6 parhomne2.u ⊢ φ → U ∈ B
7 parhomne2.v ⊢ φ → V ∈ B
8 1 4 5 parhomel ⊢ U ∈ B ∧ V ∈ B → F ∈ U H V ↔ U = V ∧ F = J ∨ ¬ U = V ∧ U = X ∧ V = Y ∧ F ∈ S
9 6 7 8 syl2anc ⊢ φ → F ∈ U H V ↔ U = V ∧ F = J ∨ ¬ U = V ∧ U = X ∧ V = Y ∧ F ∈ S
10 2 9 mpbid ⊢ φ → U = V ∧ F = J ∨ ¬ U = V ∧ U = X ∧ V = Y ∧ F ∈ S
11 3 intnanrd ⊢ φ → ¬ U = V ∧ F = J
12 10 11 orcnd ⊢ φ → ¬ U = V ∧ U = X ∧ V = Y ∧ F ∈ S
13 12 simprld ⊢ φ → U = X ∧ V = Y