Theorem parhomid

Description: The identity value belongs to each endomorphism hom-set. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 16-Sep-2026)

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

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
2		parhomid.j	⊢ 𝐽 ∈ V
3		parhomid.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
4	2	snid	⊢ 𝐽 ∈ { 𝐽 }
5	1	parhomidval	⊢ ( 𝑈 ∈ 𝐵 → ( 𝑈 𝐻 𝑈 ) = { 𝐽 } )
6	3 5	syl	⊢ ( 𝜑 → ( 𝑈 𝐻 𝑈 ) = { 𝐽 } )
7	4 6	eleqtrrid	⊢ ( 𝜑 → 𝐽 ∈ ( 𝑈 𝐻 𝑈 ) )