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 e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
	parhomeqor.f	|- ( ph -> F e. ( U H V ) )
	parhomeqor.g	|- ( ph -> G e. ( V H W ) )
Assertion	parhomeqor	|- ( ph -> ( U = V \/ V = W ) )

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	|- H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
2		parhomeqor.f	|- ( ph -> F e. ( U H V ) )
3		parhomeqor.g	|- ( ph -> G e. ( V H W ) )
4	2	adantr	|- ( ( ph /\ -. U = V ) -> F e. ( U H V ) )
5		simpr	|- ( ( ph /\ -. U = V ) -> -. U = V )
6	1 4 5	parhomne	|- ( ( ph /\ -. U = V ) -> ( U = X /\ V = Y ) )
7	6	simpld	|- ( ( ph /\ -. U = V ) -> U = X )
8	7	adantr	|- ( ( ( ph /\ -. U = V ) /\ -. V = W ) -> U = X )
9	3	adantr	|- ( ( ph /\ -. U = V ) -> G e. ( V H W ) )
10	9	adantr	|- ( ( ( ph /\ -. U = V ) /\ -. V = W ) -> G e. ( V H W ) )
11		simpr	|- ( ( ( ph /\ -. U = V ) /\ -. V = W ) -> -. V = W )
12	1 10 11	parhomne	|- ( ( ( ph /\ -. U = V ) /\ -. V = W ) -> ( V = X /\ W = Y ) )
13	12	simpld	|- ( ( ( ph /\ -. U = V ) /\ -. V = W ) -> V = X )
14	8 13	eqtr4d	|- ( ( ( ph /\ -. U = V ) /\ -. V = W ) -> U = V )
15	5	adantr	|- ( ( ( ph /\ -. U = V ) /\ -. V = W ) -> -. U = V )
16	14 15	condan	|- ( ( ph /\ -. U = V ) -> V = W )
17	16	ex	|- ( ph -> ( -. U = V -> V = W ) )
18	17	orrd	|- ( ph -> ( U = V \/ V = W ) )