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 = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
	parhomss.p	|- S C_ ~P J
	parhomss.f	|- ( ph -> F e. ( U H V ) )
Assertion	parhomss	|- ( ph -> F C_ J )

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		parhomss.p	|- S C_ ~P J
3		parhomss.f	|- ( ph -> F e. ( U H V ) )
4		snsspw	|- { J } C_ ~P J
5	2 4	unssi	|- ( S u. { J } ) C_ ~P J
6		eqid	|- ( S u. { J } ) = ( S u. { J } )
7	1 6 3	parhomcl	|- ( ph -> F e. ( S u. { J } ) )
8	5 7	sselid	|- ( ph -> F e. ~P J )
9	8	elpwid	|- ( ph -> F C_ J )