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=\left(x\in B,y\in B⟼if\left(x=y,\left\{J\right\},if\left(\left(x=X\wedge y=Y\right),S,\varnothing \right)\right)\right)$$
	parhomid.j	$$⊢J\in \mathrm{V}$$
	parhomid.u	$$⊢\phi \to U\in B$$
Assertion	parhomid	$$⊢\phi \to J\in \left(UHU\right)$$

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	$$⊢H=\left(x\in B,y\in B⟼if\left(x=y,\left\{J\right\},if\left(\left(x=X\wedge y=Y\right),S,\varnothing \right)\right)\right)$$
2		parhomid.j	$$⊢J\in \mathrm{V}$$
3		parhomid.u	$$⊢\phi \to U\in B$$
4	2	snid	$$⊢J\in \left\{J\right\}$$
5	1	parhomidval	$$⊢U\in B\to UHU=\left\{J\right\}$$
6	3 5	syl	$$⊢\phi \to UHU=\left\{J\right\}$$
7	4 6	eleqtrrid	$$⊢\phi \to J\in \left(UHU\right)$$