Metamath Proof Explorer

Theorem prdsvallem

Description: Lemma for prdsval . (Contributed by Stefan O'Rear, 3-Jan-2015) Extracted from the former proof of prdsval , dependency on df-hom removed. (Revised by AV, 13-Oct-2024)

Ref Expression
Assertion prdsvallem 
|- ( f e. v , g e. v |-> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) ) e. _V

Proof

Step Hyp Ref Expression
1 vex 
 |-  v e. _V
2 ovex 
 |-  ( U. ran U. ran U. ran r ^m dom r ) e. _V
3 2 pwex 
 |-  ~P ( U. ran U. ran U. ran r ^m dom r ) e. _V
4 ovssunirn 
 |-  ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) C_ U. ran ( Hom ` ( r ` x ) )
5 homid 
 |-  Hom = Slot ( Hom ` ndx )
6 5 strfvss 
 |-  ( Hom ` ( r ` x ) ) C_ U. ran ( r ` x )
7 fvssunirn 
 |-  ( r ` x ) C_ U. ran r
8 rnss 
 |-  ( ( r ` x ) C_ U. ran r -> ran ( r ` x ) C_ ran U. ran r )
9 uniss 
 |-  ( ran ( r ` x ) C_ ran U. ran r -> U. ran ( r ` x ) C_ U. ran U. ran r )
10 7 8 9 mp2b 
 |-  U. ran ( r ` x ) C_ U. ran U. ran r
11 6 10 sstri 
 |-  ( Hom ` ( r ` x ) ) C_ U. ran U. ran r
12 rnss 
 |-  ( ( Hom ` ( r ` x ) ) C_ U. ran U. ran r -> ran ( Hom ` ( r ` x ) ) C_ ran U. ran U. ran r )
13 uniss 
 |-  ( ran ( Hom ` ( r ` x ) ) C_ ran U. ran U. ran r -> U. ran ( Hom ` ( r ` x ) ) C_ U. ran U. ran U. ran r )
14 11 12 13 mp2b 
 |-  U. ran ( Hom ` ( r ` x ) ) C_ U. ran U. ran U. ran r
15 4 14 sstri 
 |-  ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) C_ U. ran U. ran U. ran r
16 15 rgenw 
 |-  A. x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) C_ U. ran U. ran U. ran r
17 ss2ixp 
 |-  ( A. x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) C_ U. ran U. ran U. ran r -> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) C_ X_ x e. dom r U. ran U. ran U. ran r )
18 16 17 ax-mp 
 |-  X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) C_ X_ x e. dom r U. ran U. ran U. ran r
19 vex 
 |-  r e. _V
20 19 dmex 
 |-  dom r e. _V
21 19 rnex 
 |-  ran r e. _V
22 21 uniex 
 |-  U. ran r e. _V
23 22 rnex 
 |-  ran U. ran r e. _V
24 23 uniex 
 |-  U. ran U. ran r e. _V
25 24 rnex 
 |-  ran U. ran U. ran r e. _V
26 25 uniex 
 |-  U. ran U. ran U. ran r e. _V
27 20 26 ixpconst 
 |-  X_ x e. dom r U. ran U. ran U. ran r = ( U. ran U. ran U. ran r ^m dom r )
28 18 27 sseqtri 
 |-  X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) C_ ( U. ran U. ran U. ran r ^m dom r )
29 2 28 elpwi2 
 |-  X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) e. ~P ( U. ran U. ran U. ran r ^m dom r )
30 29 rgen2w 
 |-  A. f e. v A. g e. v X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) e. ~P ( U. ran U. ran U. ran r ^m dom r )
31 1 1 3 30 mpoexw 
 |-  ( f e. v , g e. v |-> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) ) e. _V