Theorem parhomssun

Description: Every value of the parallel-arrow hom operation is a subclass of the arrow carrier. (Contributed by Zhi Wang, 16-Sep-2026)

	Ref	Expression
Hypotheses	parhomval.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
	parhomssun.k	⊢ 𝐾 = ( 𝑆 ∪ { 𝐽 } )
Assertion	parhomssun	⊢ ( 𝑈 𝐻 𝑉 ) ⊆ 𝐾

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
2		parhomssun.k	⊢ 𝐾 = ( 𝑆 ∪ { 𝐽 } )
3		ifssun	⊢ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) ⊆ ( { 𝐽 } ∪ if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) )
4		ssun2	⊢ { 𝐽 } ⊆ ( 𝑆 ∪ { 𝐽 } )
5		ifssun	⊢ if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ⊆ ( 𝑆 ∪ ∅ )
6		un0	⊢ ( 𝑆 ∪ ∅ ) = 𝑆
7		ssun1	⊢ 𝑆 ⊆ ( 𝑆 ∪ { 𝐽 } )
8	6 7	eqsstri	⊢ ( 𝑆 ∪ ∅ ) ⊆ ( 𝑆 ∪ { 𝐽 } )
9	5 8	sstri	⊢ if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ⊆ ( 𝑆 ∪ { 𝐽 } )
10	4 9	unssi	⊢ ( { 𝐽 } ∪ if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) ⊆ ( 𝑆 ∪ { 𝐽 } )
11	3 10	sstri	⊢ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) ⊆ ( 𝑆 ∪ { 𝐽 } )
12	11	rgen2w	⊢ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) ⊆ ( 𝑆 ∪ { 𝐽 } )
13	1	ovmptss	⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) ⊆ ( 𝑆 ∪ { 𝐽 } ) → ( 𝑈 𝐻 𝑉 ) ⊆ ( 𝑆 ∪ { 𝐽 } ) )
14	12 13	ax-mp	⊢ ( 𝑈 𝐻 𝑉 ) ⊆ ( 𝑆 ∪ { 𝐽 } )
15	14 2	sseqtrri	⊢ ( 𝑈 𝐻 𝑉 ) ⊆ 𝐾