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 = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
	parhomssun.k	|- K = ( S u. { J } )
	parhomcl.f	|- ( ph -> F e. ( U H V ) )
Assertion	parhomcl	|- ( ph -> F e. K )

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	|- H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
2		parhomssun.k	|- K = ( S u. { J } )
3		parhomcl.f	|- ( ph -> F e. ( U H V ) )
4	1 2	parhomssun	|- ( U H V ) C_ K
5	4 3	sselid	|- ( ph -> F e. K )