Theorem parhomidval

Description: On the diagonal, the parallel-arrow hom operation has value { J } . (Contributed by Zhi Wang, 16-Sep-2026)

	Ref	Expression
Hypothesis	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)$$
Assertion	parhomidval	$$⊢U\in B\to UHU=\left\{J\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		eqtr3	$$⊢\left(x=U\wedge y=U\right)\to x=y$$
3	2	iftrued	$$⊢\left(x=U\wedge y=U\right)\to if\left(x=y,\left\{J\right\},if\left(\left(x=X\wedge y=Y\right),S,\varnothing \right)\right)=\left\{J\right\}$$
4		snex	$$⊢\left\{J\right\}\in \mathrm{V}$$
5	3 1 4	ovmpoa	$$⊢\left(U\in B\wedge U\in B\right)\to UHU=\left\{J\right\}$$
6	5	anidms	$$⊢U\in B\to UHU=\left\{J\right\}$$