Theorem parhomid2

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

	Ref	Expression
Hypotheses	parhomval.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
	parhomid.j	⊢ 𝐽 ∈ V
	parhomid.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
	parhomid2.s	⊢ 𝑆 ∈ V
Assertion	parhomid2	⊢ ( 𝜑 → 𝐽 ∈ ( 𝑈 𝐻 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
2		parhomid.j	⊢ 𝐽 ∈ V
3		parhomid.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
4		parhomid2.s	⊢ 𝑆 ∈ V
5	2	snid	⊢ 𝐽 ∈ { 𝐽 }
6	1 4	parhomval	⊢ ( ( 𝑈 ∈ 𝐵 ∧ 𝑈 ∈ 𝐵 ) → ( 𝑈 𝐻 𝑈 ) = if ( 𝑈 = 𝑈 , { 𝐽 } , if ( ( 𝑈 = 𝑋 ∧ 𝑈 = 𝑌 ) , 𝑆 , ∅ ) ) )
7	3 3 6	syl2anc	⊢ ( 𝜑 → ( 𝑈 𝐻 𝑈 ) = if ( 𝑈 = 𝑈 , { 𝐽 } , if ( ( 𝑈 = 𝑋 ∧ 𝑈 = 𝑌 ) , 𝑆 , ∅ ) ) )
8		eqid	⊢ 𝑈 = 𝑈
9	8	iftruei	⊢ if ( 𝑈 = 𝑈 , { 𝐽 } , if ( ( 𝑈 = 𝑋 ∧ 𝑈 = 𝑌 ) , 𝑆 , ∅ ) ) = { 𝐽 }
10	7 9	eqtrdi	⊢ ( 𝜑 → ( 𝑈 𝐻 𝑈 ) = { 𝐽 } )
11	5 10	eleqtrrid	⊢ ( 𝜑 → 𝐽 ∈ ( 𝑈 𝐻 𝑈 ) )