Theorem parhomss2

Description: Variant of parhomss . (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026) (New usage is discouraged.) (Proof modification is discouraged.)

	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 ) )
	parhomss2.s	|- S e. _V
	parhomss2.j	|- J e. _V
	parhomss2.u	|- ( ph -> U e. B )
	parhomss2.v	|- ( ph -> V e. B )
Assertion	parhomss2	|- ( 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		parhomss2.s	|- S e. _V
5		parhomss2.j	|- J e. _V
6		parhomss2.u	|- ( ph -> U e. B )
7		parhomss2.v	|- ( ph -> V e. B )
8		snsspw	|- { J } C_ ~P J
9	2 8	unssi	|- ( S u. { J } ) C_ ~P J
10		eqid	|- ( S u. { J } ) = ( S u. { J } )
11	1 10 3	parhomcl	|- ( ph -> F e. ( S u. { J } ) )
12	9 11	sselid	|- ( ph -> F e. ~P J )
13	12	elpwid	|- ( ph -> F C_ J )