Theorem parhomne2

Description: Variant of parhomne . (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026) (New usage is discouraged.) (Proof modification is discouraged.)

	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 )
	parhomne2.s	|- S e. _V
	parhomne2.j	|- J e. _V
	parhomne2.u	|- ( ph -> U e. B )
	parhomne2.v	|- ( ph -> V e. B )
Assertion	parhomne2	|- ( 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		parhomne2.s	|- S e. _V
5		parhomne2.j	|- J e. _V
6		parhomne2.u	|- ( ph -> U e. B )
7		parhomne2.v	|- ( ph -> V e. B )
8	1 4 5	parhomel	|- ( ( U e. B /\ V e. B ) -> ( F e. ( U H V ) <-> ( ( U = V /\ F = J ) \/ ( -. U = V /\ ( ( U = X /\ V = Y ) /\ F e. S ) ) ) ) )
9	6 7 8	syl2anc	|- ( ph -> ( F e. ( U H V ) <-> ( ( U = V /\ F = J ) \/ ( -. U = V /\ ( ( U = X /\ V = Y ) /\ F e. S ) ) ) ) )
10	2 9	mpbid	|- ( ph -> ( ( U = V /\ F = J ) \/ ( -. U = V /\ ( ( U = X /\ V = Y ) /\ F e. S ) ) ) )
11	3	intnanrd	|- ( ph -> -. ( U = V /\ F = J ) )
12	10 11	orcnd	|- ( ph -> ( -. U = V /\ ( ( U = X /\ V = Y ) /\ F e. S ) ) )
13	12	simprld	|- ( ph -> ( U = X /\ V = Y ) )