Theorem parhomss

Description: When every member of the parallel-arrow class S is a subset of J , every arrow in a hom-set is a subset of its identity value J . The subset hypothesis is essential; it does not follow from the hom-set definition alone. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-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)$$
	parhomss.p	$$⊢S\subseteq 𝒫J$$
	parhomss.f	$$⊢\phi \to F\in \left(UHV\right)$$
Assertion	parhomss	$$⊢\phi \to F\subseteq 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		parhomss.p	$$⊢S\subseteq 𝒫J$$
3		parhomss.f	$$⊢\phi \to F\in \left(UHV\right)$$
4		snsspw	$$⊢\left\{J\right\}\subseteq 𝒫J$$
5	2 4	unssi	$$⊢S\cup \left\{J\right\}\subseteq 𝒫J$$
6		eqid	$$⊢S\cup \left\{J\right\}=S\cup \left\{J\right\}$$
7	1 6 3	parhomcl	$$⊢\phi \to F\in \left(S\cup \left\{J\right\}\right)$$
8	5 7	sselid	$$⊢\phi \to F\in 𝒫J$$
9	8	elpwid	$$⊢\phi \to F\subseteq J$$