Metamath Proof Explorer

Theorem wunnat

Description: A weak universe is closed under the natural transformation operation. (Contributed by Mario Carneiro, 12-Jan-2017) (Proof shortened by AV, 13-Oct-2024)

Ref Expression
Hypotheses wunnat.1 
|- ( ph -> U e. WUni )
wunnat.2 
|- ( ph -> C e. U )
wunnat.3 
|- ( ph -> D e. U )
Assertion wunnat 
|- ( ph -> ( C Nat D ) e. U )

Proof

Step Hyp Ref Expression
1 wunnat.1 
 |-  ( ph -> U e. WUni )
2 wunnat.2 
 |-  ( ph -> C e. U )
3 wunnat.3 
 |-  ( ph -> D e. U )
4 1 2 3 wunfunc 
 |-  ( ph -> ( C Func D ) e. U )
5 1 4 4 wunxp 
 |-  ( ph -> ( ( C Func D ) X. ( C Func D ) ) e. U )
6 homid 
 |-  Hom = Slot ( Hom ` ndx )
7 6 1 3 wunstr 
 |-  ( ph -> ( Hom ` D ) e. U )
8 1 7 wunrn 
 |-  ( ph -> ran ( Hom ` D ) e. U )
9 1 8 wununi 
 |-  ( ph -> U. ran ( Hom ` D ) e. U )
10 baseid 
 |-  Base = Slot ( Base ` ndx )
11 10 1 2 wunstr 
 |-  ( ph -> ( Base ` C ) e. U )
12 1 9 11 wunmap 
 |-  ( ph -> ( U. ran ( Hom ` D ) ^m ( Base ` C ) ) e. U )
13 1 12 wunpw 
 |-  ( ph -> ~P ( U. ran ( Hom ` D ) ^m ( Base ` C ) ) e. U )
14 fvex 
 |-  ( 1st ` f ) e. _V
15 fvex 
 |-  ( 1st ` g ) e. _V
16 ovex 
 |-  ( U. ran ( Hom ` D ) ^m ( Base ` C ) ) e. _V
17 ssrab2 
 |-  { a e. X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. z e. ( x ( Hom ` C ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` z ) ) = ( ( ( x ( 2nd ` g ) y ) ` z ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } C_ X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) )
18 ovssunirn 
 |-  ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) C_ U. ran ( Hom ` D )
19 18 rgenw 
 |-  A. x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) C_ U. ran ( Hom ` D )
20 ss2ixp 
 |-  ( A. x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) C_ U. ran ( Hom ` D ) -> X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) C_ X_ x e. ( Base ` C ) U. ran ( Hom ` D ) )
21 19 20 ax-mp 
 |-  X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) C_ X_ x e. ( Base ` C ) U. ran ( Hom ` D )
22 fvex 
 |-  ( Base ` C ) e. _V
23 fvex 
 |-  ( Hom ` D ) e. _V
24 23 rnex 
 |-  ran ( Hom ` D ) e. _V
25 24 uniex 
 |-  U. ran ( Hom ` D ) e. _V
26 22 25 ixpconst 
 |-  X_ x e. ( Base ` C ) U. ran ( Hom ` D ) = ( U. ran ( Hom ` D ) ^m ( Base ` C ) )
27 21 26 sseqtri 
 |-  X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) C_ ( U. ran ( Hom ` D ) ^m ( Base ` C ) )
28 17 27 sstri 
 |-  { a e. X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. z e. ( x ( Hom ` C ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` z ) ) = ( ( ( x ( 2nd ` g ) y ) ` z ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } C_ ( U. ran ( Hom ` D ) ^m ( Base ` C ) )
29 16 28 elpwi2 
 |-  { a e. X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. z e. ( x ( Hom ` C ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` z ) ) = ( ( ( x ( 2nd ` g ) y ) ` z ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } e. ~P ( U. ran ( Hom ` D ) ^m ( Base ` C ) )
30 29 sbcth 
 |-  ( ( 1st ` g ) e. _V -> [. ( 1st ` g ) / s ]. { a e. X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. z e. ( x ( Hom ` C ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` z ) ) = ( ( ( x ( 2nd ` g ) y ) ` z ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } e. ~P ( U. ran ( Hom ` D ) ^m ( Base ` C ) ) )
31 sbcel1g 
 |-  ( ( 1st ` g ) e. _V -> ( [. ( 1st ` g ) / s ]. { a e. X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. z e. ( x ( Hom ` C ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` z ) ) = ( ( ( x ( 2nd ` g ) y ) ` z ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } e. ~P ( U. ran ( Hom ` D ) ^m ( Base ` C ) ) <-> [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. z e. ( x ( Hom ` C ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` z ) ) = ( ( ( x ( 2nd ` g ) y ) ` z ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } e. ~P ( U. ran ( Hom ` D ) ^m ( Base ` C ) ) ) )
32 30 31 mpbid 
 |-  ( ( 1st ` g ) e. _V -> [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. z e. ( x ( Hom ` C ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` z ) ) = ( ( ( x ( 2nd ` g ) y ) ` z ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } e. ~P ( U. ran ( Hom ` D ) ^m ( Base ` C ) ) )
33 15 32 ax-mp 
 |-  [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. z e. ( x ( Hom ` C ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` z ) ) = ( ( ( x ( 2nd ` g ) y ) ` z ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } e. ~P ( U. ran ( Hom ` D ) ^m ( Base ` C ) )
34 33 sbcth 
 |-  ( ( 1st ` f ) e. _V -> [. ( 1st ` f ) / r ]. [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. z e. ( x ( Hom ` C ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` z ) ) = ( ( ( x ( 2nd ` g ) y ) ` z ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } e. ~P ( U. ran ( Hom ` D ) ^m ( Base ` C ) ) )
35 sbcel1g 
 |-  ( ( 1st ` f ) e. _V -> ( [. ( 1st ` f ) / r ]. [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. z e. ( x ( Hom ` C ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` z ) ) = ( ( ( x ( 2nd ` g ) y ) ` z ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } e. ~P ( U. ran ( Hom ` D ) ^m ( Base ` C ) ) <-> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. z e. ( x ( Hom ` C ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` z ) ) = ( ( ( x ( 2nd ` g ) y ) ` z ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } e. ~P ( U. ran ( Hom ` D ) ^m ( Base ` C ) ) ) )
36 34 35 mpbid 
 |-  ( ( 1st ` f ) e. _V -> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. z e. ( x ( Hom ` C ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` z ) ) = ( ( ( x ( 2nd ` g ) y ) ` z ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } e. ~P ( U. ran ( Hom ` D ) ^m ( Base ` C ) ) )
37 14 36 ax-mp 
 |-  [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. z e. ( x ( Hom ` C ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` z ) ) = ( ( ( x ( 2nd ` g ) y ) ` z ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } e. ~P ( U. ran ( Hom ` D ) ^m ( Base ` C ) )
38 37 rgen2w 
 |-  A. f e. ( C Func D ) A. g e. ( C Func D ) [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. z e. ( x ( Hom ` C ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` z ) ) = ( ( ( x ( 2nd ` g ) y ) ` z ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } e. ~P ( U. ran ( Hom ` D ) ^m ( Base ` C ) )
39 eqid 
 |-  ( C Nat D ) = ( C Nat D )
40 eqid 
 |-  ( Base ` C ) = ( Base ` C )
41 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
42 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
43 eqid 
 |-  ( comp ` D ) = ( comp ` D )
44 39 40 41 42 43 natfval 
 |-  ( C Nat D ) = ( f e. ( C Func D ) , g e. ( C Func D ) |-> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. z e. ( x ( Hom ` C ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` z ) ) = ( ( ( x ( 2nd ` g ) y ) ` z ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } )
45 44 fmpo 
 |-  ( A. f e. ( C Func D ) A. g e. ( C Func D ) [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. z e. ( x ( Hom ` C ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` z ) ) = ( ( ( x ( 2nd ` g ) y ) ` z ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } e. ~P ( U. ran ( Hom ` D ) ^m ( Base ` C ) ) <-> ( C Nat D ) : ( ( C Func D ) X. ( C Func D ) ) --> ~P ( U. ran ( Hom ` D ) ^m ( Base ` C ) ) )
46 38 45 mpbi 
 |-  ( C Nat D ) : ( ( C Func D ) X. ( C Func D ) ) --> ~P ( U. ran ( Hom ` D ) ^m ( Base ` C ) )
47 46 a1i 
 |-  ( ph -> ( C Nat D ) : ( ( C Func D ) X. ( C Func D ) ) --> ~P ( U. ran ( Hom ` D ) ^m ( Base ` C ) ) )
48 1 5 13 47 wunf 
 |-  ( ph -> ( C Nat D ) e. U )