Theorem parhomideq

Description: An endomorphism in the parallel-arrow construction has the identity value. (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)$$
	parhomideq.f	$$⊢\phi \to F\in \left(UHV\right)$$
	parhomideq.e	$$⊢\phi \to U=V$$
Assertion	parhomideq	$$⊢\phi \to F=J$$

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		parhomideq.f	$$⊢\phi \to F\in \left(UHV\right)$$
3		parhomideq.e	$$⊢\phi \to U=V$$
4	3	oveq2d	$$⊢\phi \to UHU=UHV$$
5	2 4	eleqtrrd	$$⊢\phi \to F\in \left(UHU\right)$$
6	1	elmpocl1	$$⊢F\in \left(UHV\right)\to U\in B$$
7	1	parhomidval	$$⊢U\in B\to UHU=\left\{J\right\}$$
8	2 6 7	3syl	$$⊢\phi \to UHU=\left\{J\right\}$$
9	5 8	eleqtrd	$$⊢\phi \to F\in \left\{J\right\}$$
10	9	elsnd	$$⊢\phi \to F=J$$