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

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		parhomne.f	|- ( ph -> F e. ( U H V ) )
3		parhomne.n	|- ( ph -> -. U = V )
4	1	parhomvaln0	|- ( F e. ( U H V ) -> ( U H V ) = if ( U = V , { J } , if ( ( U = X /\ V = Y ) , S , (/) ) ) )
5	2 4	syl	|- ( ph -> ( U H V ) = if ( U = V , { J } , if ( ( U = X /\ V = Y ) , S , (/) ) ) )
6	3	iffalsed	|- ( ph -> if ( U = V , { J } , if ( ( U = X /\ V = Y ) , S , (/) ) ) = if ( ( U = X /\ V = Y ) , S , (/) ) )
7	5 6	eqtrd	|- ( ph -> ( U H V ) = if ( ( U = X /\ V = Y ) , S , (/) ) )
8	2 7	eleqtrd	|- ( ph -> F e. if ( ( U = X /\ V = Y ) , S , (/) ) )
9		elif0	|- ( F e. if ( ( U = X /\ V = Y ) , S , (/) ) <-> ( ( U = X /\ V = Y ) /\ F e. S ) )
10	8 9	sylib	|- ( ph -> ( ( U = X /\ V = Y ) /\ F e. S ) )
11	10	simpld	|- ( ph -> ( U = X /\ V = Y ) )