Metamath Proof Explorer

Theorem parhomeqor

Description: In a composable pair, at least one arrow is an endomorphism. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

		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)$
	Assertion	parhomeqor	$⊢ φ \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	2	adantr	$⊢ (φ \land \neg U = V) \to F \in (U H V)$
5		simpr	$⊢ (φ \land \neg U = V) \to \neg U = V$
6	1 4 5	parhomne	$⊢ (φ \land \neg U = V) \to (U = X \land V = Y)$
7	6	simpld	$⊢ (φ \land \neg U = V) \to U = X$
8	7	adantr	$⊢ ((φ \land \neg U = V) \land \neg V = W) \to U = X$
9	3	adantr	$⊢ (φ \land \neg U = V) \to G \in (V H W)$
10	9	adantr	$⊢ ((φ \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	8 13	eqtr4d	$⊢ ((φ \land \neg U = V) \land \neg V = W) \to U = V$
15	5	adantr	$⊢ ((φ \land \neg U = V) \land \neg V = W) \to \neg U = V$
16	14 15	condan	$⊢ (φ \land \neg U = V) \to V = W$
17	16	ex	$⊢ φ \to (\neg U = V \to V = W)$
18	17	orrd	$⊢ φ \to (U = V \lor V = W)$