Theorem parhomne

Description: A morphism between different objects has the distinguished source and target. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

	Ref	Expression
Hypotheses	parhomval.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
	parhomne.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
	parhomne.n	⊢ ( 𝜑 → ¬ 𝑈 = 𝑉 )
Assertion	parhomne	⊢ ( 𝜑 → ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
2		parhomne.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
3		parhomne.n	⊢ ( 𝜑 → ¬ 𝑈 = 𝑉 )
4	1	parhomvaln0	⊢ ( 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) → ( 𝑈 𝐻 𝑉 ) = if ( 𝑈 = 𝑉 , { 𝐽 } , if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ) )
5	2 4	syl	⊢ ( 𝜑 → ( 𝑈 𝐻 𝑉 ) = if ( 𝑈 = 𝑉 , { 𝐽 } , if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ) )
6	3	iffalsed	⊢ ( 𝜑 → if ( 𝑈 = 𝑉 , { 𝐽 } , if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ) = if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) )
7	5 6	eqtrd	⊢ ( 𝜑 → ( 𝑈 𝐻 𝑉 ) = if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) )
8	2 7	eleqtrd	⊢ ( 𝜑 → 𝐹 ∈ if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) )
9		elif0	⊢ ( 𝐹 ∈ if ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) , 𝑆 , ∅ ) ↔ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) )
10	8 9	sylib	⊢ ( 𝜑 → ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) )
11	10	simpld	⊢ ( 𝜑 → ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) )