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	|- H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
	parhomid.j	|- J e. _V
	parhomid.u	|- ( ph -> U e. B )
Assertion	parhomid	|- ( ph -> J e. ( U H U ) )

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		parhomid.j	|- J e. _V
3		parhomid.u	|- ( ph -> U e. B )
4	2	snid	|- J e. { J }
5	1	parhomidval	|- ( U e. B -> ( U H U ) = { J } )
6	3 5	syl	|- ( ph -> ( U H U ) = { J } )
7	4 6	eleqtrrid	|- ( ph -> J e. ( U H U ) )