parhomeqor2

Description: Variant of parhomeqor . (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 \in B, y \in B ⟼ if (x = y, \{J\}, if ((x = X \land y = Y), S, \emptyset)))$
	parhomeqor.f	$⊢ φ \to F \in (U H V)$
	parhomeqor.g	$⊢ φ \to G \in (V H W)$
	parhomeqor2.s	$⊢ S \in V$
	parhomeqor2.j	$⊢ J \in V$
	parhomeqor2.n	$⊢ X \neq Y$
	parhomeqor2.u	$⊢ φ \to U \in B$
	parhomeqor2.v	$⊢ φ \to V \in B$
	parhomeqor2.w	$⊢ φ \to W \in B$
Assertion	parhomeqor2	$⊢ φ \to (U = V \lor V = W)$

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	$⊢ H = (x \in B, y \in B ⟼ if (x = y, \{J\}, if ((x = X \land y = Y), S, \emptyset)))$
2		parhomeqor.f	$⊢ φ \to F \in (U H V)$
3		parhomeqor.g	$⊢ φ \to G \in (V H W)$
4		parhomeqor2.s	$⊢ S \in V$
5		parhomeqor2.j	$⊢ J \in V$
6		parhomeqor2.n	$⊢ X \neq Y$
7		parhomeqor2.u	$⊢ φ \to U \in B$
8		parhomeqor2.v	$⊢ φ \to V \in B$
9		parhomeqor2.w	$⊢ φ \to W \in B$
10	3	ad2antrr	$⊢ ((φ \land \neg U = V) \land \neg V = W) \to G \in (V H W)$
11		simpr	$⊢ ((φ \land \neg U = V) \land \neg V = W) \to \neg V = W$
12	1 10 11	parhomne	$⊢ ((φ \land \neg U = V) \land \neg V = W) \to (V = X \land W = Y)$
13	12	simpld	$⊢ ((φ \land \neg U = V) \land \neg V = W) \to V = X$
14	2	adantr	$⊢ (φ \land \neg U = V) \to F \in (U H V)$
15		simpr	$⊢ (φ \land \neg U = V) \to \neg U = V$
16	1 14 15	parhomne	$⊢ (φ \land \neg U = V) \to (U = X \land V = Y)$
17	16	simprd	$⊢ (φ \land \neg U = V) \to V = Y$
18	17	adantr	$⊢ ((φ \land \neg U = V) \land \neg V = W) \to V = Y$
19	13 18	eqtr3d	$⊢ ((φ \land \neg U = V) \land \neg V = W) \to X = Y$
20	6	neii	$⊢ \neg X = Y$
21	20	a1i	$⊢ ((φ \land \neg U = V) \land \neg V = W) \to \neg X = Y$
22	19 21	condan	$⊢ (φ \land \neg U = V) \to V = W$
23	22	ex	$⊢ φ \to (\neg U = V \to V = W)$
24	23	orrd	$⊢ φ \to (U = V \lor V = W)$

Metamath Proof Explorer

Theorem parhomeqor2

Proof