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	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
	parhomss.p	⊢ 𝑆 ⊆ 𝒫 𝐽
	parhomss.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
	parhomss2.s	⊢ 𝑆 ∈ V
	parhomss2.j	⊢ 𝐽 ∈ V
	parhomss2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
	parhomss2.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
Assertion	parhomss2	⊢ ( 𝜑 → 𝐹 ⊆ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
2		parhomss.p	⊢ 𝑆 ⊆ 𝒫 𝐽
3		parhomss.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
4		parhomss2.s	⊢ 𝑆 ∈ V
5		parhomss2.j	⊢ 𝐽 ∈ V
6		parhomss2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
7		parhomss2.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
8		snsspw	⊢ { 𝐽 } ⊆ 𝒫 𝐽
9	2 8	unssi	⊢ ( 𝑆 ∪ { 𝐽 } ) ⊆ 𝒫 𝐽
10		eqid	⊢ ( 𝑆 ∪ { 𝐽 } ) = ( 𝑆 ∪ { 𝐽 } )
11	1 10 3	parhomcl	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 ∪ { 𝐽 } ) )
12	9 11	sselid	⊢ ( 𝜑 → 𝐹 ∈ 𝒫 𝐽 )
13	12	elpwid	⊢ ( 𝜑 → 𝐹 ⊆ 𝐽 )