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

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
2		parhomeqor.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
3		parhomeqor.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑉 𝐻 𝑊 ) )
4		parhomeqor2.s	⊢ 𝑆 ∈ V
5		parhomeqor2.j	⊢ 𝐽 ∈ V
6		parhomeqor2.n	⊢ 𝑋 ≠ 𝑌
7		parhomeqor2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
8		parhomeqor2.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
9		parhomeqor2.w	⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
10	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) ∧ ¬ 𝑉 = 𝑊 ) → 𝐺 ∈ ( 𝑉 𝐻 𝑊 ) )
11		simpr	⊢ ( ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) ∧ ¬ 𝑉 = 𝑊 ) → ¬ 𝑉 = 𝑊 )
12	1 10 11	parhomne	⊢ ( ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) ∧ ¬ 𝑉 = 𝑊 ) → ( 𝑉 = 𝑋 ∧ 𝑊 = 𝑌 ) )
13	12	simpld	⊢ ( ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) ∧ ¬ 𝑉 = 𝑊 ) → 𝑉 = 𝑋 )
14	2	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
15		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → ¬ 𝑈 = 𝑉 )
16	1 14 15	parhomne	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) )
17	16	simprd	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → 𝑉 = 𝑌 )
18	17	adantr	⊢ ( ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) ∧ ¬ 𝑉 = 𝑊 ) → 𝑉 = 𝑌 )
19	13 18	eqtr3d	⊢ ( ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) ∧ ¬ 𝑉 = 𝑊 ) → 𝑋 = 𝑌 )
20	6	neii	⊢ ¬ 𝑋 = 𝑌
21	20	a1i	⊢ ( ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) ∧ ¬ 𝑉 = 𝑊 ) → ¬ 𝑋 = 𝑌 )
22	19 21	condan	⊢ ( ( 𝜑 ∧ ¬ 𝑈 = 𝑉 ) → 𝑉 = 𝑊 )
23	22	ex	⊢ ( 𝜑 → ( ¬ 𝑈 = 𝑉 → 𝑉 = 𝑊 ) )
24	23	orrd	⊢ ( 𝜑 → ( 𝑈 = 𝑉 ∨ 𝑉 = 𝑊 ) )