Metamath Proof Explorer

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 
|- H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
parhomssun.k 
|- K = ( S u. { J } )
Assertion parhomssun 
|- ( U H V ) C_ K

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 parhomssun.k 
 |-  K = ( S u. { J } )
3 ifssun 
 |-  if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) C_ ( { J } u. if ( ( x = X /\ y = Y ) , S , (/) ) )
4 ssun2 
 |-  { J } C_ ( S u. { J } )
5 ifssun 
 |-  if ( ( x = X /\ y = Y ) , S , (/) ) C_ ( S u. (/) )
6 un0 
 |-  ( S u. (/) ) = S
7 ssun1 
 |-  S C_ ( S u. { J } )
8 6 7 eqsstri 
 |-  ( S u. (/) ) C_ ( S u. { J } )
9 5 8 sstri 
 |-  if ( ( x = X /\ y = Y ) , S , (/) ) C_ ( S u. { J } )
10 4 9 unssi 
 |-  ( { J } u. if ( ( x = X /\ y = Y ) , S , (/) ) ) C_ ( S u. { J } )
11 3 10 sstri 
 |-  if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) C_ ( S u. { J } )
12 11 rgen2w 
 |-  A. x e. B A. y e. B if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) C_ ( S u. { J } )
13 1 ovmptss 
 |-  ( A. x e. B A. y e. B if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) C_ ( S u. { J } ) -> ( U H V ) C_ ( S u. { J } ) )
14 12 13 ax-mp 
 |-  ( U H V ) C_ ( S u. { J } )
15 14 2 sseqtrri 
 |-  ( U H V ) C_ K