Theorem parhomssun

Description: Every value of the parallel-arrow hom operation is a subclass of the arrow carrier. (Contributed 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\}$$
Assertion	parhomssun	$$⊢UHV\subseteq 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		ifssun	$$⊢if\left(x=y,\left\{J\right\},if\left(\left(x=X\wedge y=Y\right),S,\varnothing \right)\right)\subseteq \left\{J\right\}\cup if\left(\left(x=X\wedge y=Y\right),S,\varnothing \right)$$
4		ssun2	$$⊢\left\{J\right\}\subseteq S\cup \left\{J\right\}$$
5		ifssun	$$⊢if\left(\left(x=X\wedge y=Y\right),S,\varnothing \right)\subseteq S\cup \varnothing$$
6		un0	$$⊢S\cup \varnothing =S$$
7		ssun1	$$⊢S\subseteq S\cup \left\{J\right\}$$
8	6 7	eqsstri	$$⊢S\cup \varnothing \subseteq S\cup \left\{J\right\}$$
9	5 8	sstri	$$⊢if\left(\left(x=X\wedge y=Y\right),S,\varnothing \right)\subseteq S\cup \left\{J\right\}$$
10	4 9	unssi	$$⊢\left\{J\right\}\cup if\left(\left(x=X\wedge y=Y\right),S,\varnothing \right)\subseteq S\cup \left\{J\right\}$$
11	3 10	sstri	$$⊢if\left(x=y,\left\{J\right\},if\left(\left(x=X\wedge y=Y\right),S,\varnothing \right)\right)\subseteq S\cup \left\{J\right\}$$
12	11	rgen2w	$$⊢\forall x\in B\forall y\in Bif\left(x=y,\left\{J\right\},if\left(\left(x=X\wedge y=Y\right),S,\varnothing \right)\right)\subseteq S\cup \left\{J\right\}$$
13	1	ovmptss	$$⊢\forall x\in B\forall y\in Bif\left(x=y,\left\{J\right\},if\left(\left(x=X\wedge y=Y\right),S,\varnothing \right)\right)\subseteq S\cup \left\{J\right\}\to UHV\subseteq S\cup \left\{J\right\}$$
14	12 13	ax-mp	$$⊢UHV\subseteq S\cup \left\{J\right\}$$
15	14 2	sseqtrri	$$⊢UHV\subseteq K$$