Theorem parhomeqor2

Description: Variant of parhomeqor . (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 , (/) ) ) )
	parhomeqor.f	|- ( ph -> F e. ( U H V ) )
	parhomeqor.g	|- ( ph -> G e. ( V H W ) )
	parhomeqor2.s	|- S e. _V
	parhomeqor2.j	|- J e. _V
	parhomeqor2.n	|- X =/= Y
	parhomeqor2.u	|- ( ph -> U e. B )
	parhomeqor2.v	|- ( ph -> V e. B )
	parhomeqor2.w	|- ( ph -> W e. B )
Assertion	parhomeqor2	|- ( 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		parhomeqor2.s	|- S e. _V
5		parhomeqor2.j	|- J e. _V
6		parhomeqor2.n	|- X =/= Y
7		parhomeqor2.u	|- ( ph -> U e. B )
8		parhomeqor2.v	|- ( ph -> V e. B )
9		parhomeqor2.w	|- ( ph -> W e. B )
10	3	ad2antrr	|- ( ( ( 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	2	adantr	|- ( ( ph /\ -. U = V ) -> F e. ( U H V ) )
15		simpr	|- ( ( ph /\ -. U = V ) -> -. U = V )
16	1 14 15	parhomne	|- ( ( ph /\ -. U = V ) -> ( U = X /\ V = Y ) )
17	16	simprd	|- ( ( ph /\ -. U = V ) -> V = Y )
18	17	adantr	|- ( ( ( ph /\ -. U = V ) /\ -. V = W ) -> V = Y )
19	13 18	eqtr3d	|- ( ( ( ph /\ -. U = V ) /\ -. V = W ) -> X = Y )
20	6	neii	|- -. X = Y
21	20	a1i	|- ( ( ( ph /\ -. U = V ) /\ -. V = W ) -> -. X = Y )
22	19 21	condan	|- ( ( ph /\ -. U = V ) -> V = W )
23	22	ex	|- ( ph -> ( -. U = V -> V = W ) )
24	23	orrd	|- ( ph -> ( U = V \/ V = W ) )