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	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
	parhomne.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
	parhomne.n	⊢ ( 𝜑 → ¬ 𝑈 = 𝑉 )
	parhomne2.s	⊢ 𝑆 ∈ V
	parhomne2.j	⊢ 𝐽 ∈ V
	parhomne2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
	parhomne2.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
Assertion	parhomne2	⊢ ( 𝜑 → ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
2		parhomne.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
3		parhomne.n	⊢ ( 𝜑 → ¬ 𝑈 = 𝑉 )
4		parhomne2.s	⊢ 𝑆 ∈ V
5		parhomne2.j	⊢ 𝐽 ∈ V
6		parhomne2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
7		parhomne2.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
8	1 4 5	parhomel	⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) ↔ ( ( 𝑈 = 𝑉 ∧ 𝐹 = 𝐽 ) ∨ ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) ) ) ) )
9	6 7 8	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) ↔ ( ( 𝑈 = 𝑉 ∧ 𝐹 = 𝐽 ) ∨ ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) ) ) ) )
10	2 9	mpbid	⊢ ( 𝜑 → ( ( 𝑈 = 𝑉 ∧ 𝐹 = 𝐽 ) ∨ ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) ) ) )
11	3	intnanrd	⊢ ( 𝜑 → ¬ ( 𝑈 = 𝑉 ∧ 𝐹 = 𝐽 ) )
12	10 11	orcnd	⊢ ( 𝜑 → ( ¬ 𝑈 = 𝑉 ∧ ( ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) ∧ 𝐹 ∈ 𝑆 ) ) )
13	12	simprld	⊢ ( 𝜑 → ( 𝑈 = 𝑋 ∧ 𝑉 = 𝑌 ) )