Metamath Proof Explorer


Theorem wunnatOLD

Description: Obsolete proof of wunnat as of 13-Oct-2024. (Contributed by Mario Carneiro, 12-Jan-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses wunnat.1
|- ( ph -> U e. WUni )
wunnat.2
|- ( ph -> C e. U )
wunnat.3
|- ( ph -> D e. U )
Assertion wunnatOLD
|- ( 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 df-hom
 |-  Hom = Slot ; 1 4
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 df-base
 |-  Base = Slot 1
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 )