Theorem parhomcl

Description: All hom-sets of the parallel-arrow construction lie in its arrow carrier. (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)$$
	parhomssun.k	$$⊢K=S\cup \left\{J\right\}$$
	parhomcl.f	$$⊢\phi \to F\in \left(UHV\right)$$
Assertion	parhomcl	$$⊢\phi \to F\in K$$

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		parhomssun.k	$$⊢K=S\cup \left\{J\right\}$$
3		parhomcl.f	$$⊢\phi \to F\in \left(UHV\right)$$
4	1 2	parhomssun	$$⊢UHV\subseteq K$$
5	4 3	sselid	$$⊢\phi \to F\in K$$