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=\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)$$
	parhomss2.s	$$⊢S\in \mathrm{V}$$
	parhomss2.j	$$⊢J\in \mathrm{V}$$
	parhomss2.u	$$⊢\phi \to U\in B$$
	parhomss2.v	$$⊢\phi \to V\in B$$
Assertion	parhomss2	$$⊢\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		parhomss2.s	$$⊢S\in \mathrm{V}$$
5		parhomss2.j	$$⊢J\in \mathrm{V}$$
6		parhomss2.u	$$⊢\phi \to U\in B$$
7		parhomss2.v	$$⊢\phi \to V\in B$$
8		snsspw	$$⊢\left\{J\right\}\subseteq 𝒫J$$
9	2 8	unssi	$$⊢S\cup \left\{J\right\}\subseteq 𝒫J$$
10		eqid	$$⊢S\cup \left\{J\right\}=S\cup \left\{J\right\}$$
11	1 10 3	parhomcl	$$⊢\phi \to F\in \left(S\cup \left\{J\right\}\right)$$
12	9 11	sselid	$$⊢\phi \to F\in 𝒫J$$
13	12	elpwid	$$⊢\phi \to F\subseteq J$$