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	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
	parhomssun.k	⊢ 𝐾 = ( 𝑆 ∪ { 𝐽 } )
	parhomcl.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
Assertion	parhomcl	⊢ ( 𝜑 → 𝐹 ∈ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
2		parhomssun.k	⊢ 𝐾 = ( 𝑆 ∪ { 𝐽 } )
3		parhomcl.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
4	1 2	parhomssun	⊢ ( 𝑈 𝐻 𝑉 ) ⊆ 𝐾
5	4 3	sselid	⊢ ( 𝜑 → 𝐹 ∈ 𝐾 )