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	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
	parhomeqor.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
	parhomeqor.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑉 𝐻 𝑊 ) )
Assertion	parhomeqor	⊢ ( 𝜑 → ( 𝑈 = 𝑉 ∨ 𝑉 = 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
2		parhomeqor.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
3		parhomeqor.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑉 𝐻 𝑊 ) )
4	2	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
5		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → ¬ 𝑈 = 𝑉 )
6	1 4 5	parhomne	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) )
7	6	simpld	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → 𝑈 = 𝑋 )
8	7	adantr	⊢ ( ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) ∧ ¬ 𝑉 = 𝑊 ) → 𝑈 = 𝑋 )
9	3	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → 𝐺 ∈ ( 𝑉 𝐻 𝑊 ) )
10	9	adantr	⊢ ( ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) ∧ ¬ 𝑉 = 𝑊 ) → 𝐺 ∈ ( 𝑉 𝐻 𝑊 ) )
11		simpr	⊢ ( ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) ∧ ¬ 𝑉 = 𝑊 ) → ¬ 𝑉 = 𝑊 )
12	1 10 11	parhomne	⊢ ( ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) ∧ ¬ 𝑉 = 𝑊 ) → ( 𝑉 = 𝑋 ∧ 𝑊 = 𝑌 ) )
13	12	simpld	⊢ ( ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) ∧ ¬ 𝑉 = 𝑊 ) → 𝑉 = 𝑋 )
14	8 13	eqtr4d	⊢ ( ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) ∧ ¬ 𝑉 = 𝑊 ) → 𝑈 = 𝑉 )
15	5	adantr	⊢ ( ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) ∧ ¬ 𝑉 = 𝑊 ) → ¬ 𝑈 = 𝑉 )
16	14 15	condan	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → 𝑉 = 𝑊 )
17	16	ex	⊢ ( 𝜑 → ( ¬ 𝑈 = 𝑉 → 𝑉 = 𝑊 ) )
18	17	orrd	⊢ ( 𝜑 → ( 𝑈 = 𝑉 ∨ 𝑉 = 𝑊 ) )