MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fuchom Structured version   Unicode version

Theorem fuchom 14858
Description: The morphisms in the functor category are natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.)
Hypotheses
Ref Expression
fucbas.q  |-  Q  =  ( C FuncCat  D )
fuchom.n  |-  N  =  ( C Nat  D )
Assertion
Ref Expression
fuchom  |-  N  =  ( Hom  `  Q
)

Proof of Theorem fuchom
Dummy variables  a 
b  f  g  h  v  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fucbas.q . . . . 5  |-  Q  =  ( C FuncCat  D )
2 eqid 2437 . . . . 5  |-  ( C 
Func  D )  =  ( C  Func  D )
3 fuchom.n . . . . 5  |-  N  =  ( C Nat  D )
4 eqid 2437 . . . . 5  |-  ( Base `  C )  =  (
Base `  C )
5 eqid 2437 . . . . 5  |-  (comp `  D )  =  (comp `  D )
6 simpl 454 . . . . 5  |-  ( ( C  e.  Cat  /\  D  e.  Cat )  ->  C  e.  Cat )
7 simpr 458 . . . . 5  |-  ( ( C  e.  Cat  /\  D  e.  Cat )  ->  D  e.  Cat )
8 eqid 2437 . . . . . 6  |-  (comp `  Q )  =  (comp `  Q )
91, 2, 3, 4, 5, 6, 7, 8fuccofval 14856 . . . . 5  |-  ( ( C  e.  Cat  /\  D  e.  Cat )  ->  (comp `  Q )  =  ( v  e.  ( ( C  Func  D )  X.  ( C 
Func  D ) ) ,  h  e.  ( C 
Func  D )  |->  [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g N h ) ,  a  e.  ( f N g ) 
|->  ( x  e.  (
Base `  C )  |->  ( ( b `  x ) ( <.
( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  D
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) )
101, 2, 3, 4, 5, 6, 7, 9fucval 14855 . . . 4  |-  ( ( C  e.  Cat  /\  D  e.  Cat )  ->  Q  =  { <. (
Base `  ndx ) ,  ( C  Func  D
) >. ,  <. ( Hom  `  ndx ) ,  N >. ,  <. (comp ` 
ndx ) ,  (comp `  Q ) >. } )
11 catstr 14854 . . . 4  |-  { <. (
Base `  ndx ) ,  ( C  Func  D
) >. ,  <. ( Hom  `  ndx ) ,  N >. ,  <. (comp ` 
ndx ) ,  (comp `  Q ) >. } Struct  <. 1 , ; 1 5 >.
12 homid 14341 . . . 4  |-  Hom  = Slot  ( Hom  `  ndx )
13 snsstp2 4017 . . . 4  |-  { <. ( Hom  `  ndx ) ,  N >. }  C_  { <. (
Base `  ndx ) ,  ( C  Func  D
) >. ,  <. ( Hom  `  ndx ) ,  N >. ,  <. (comp ` 
ndx ) ,  (comp `  Q ) >. }
14 ovex 6109 . . . . . 6  |-  ( C Nat 
D )  e.  _V
153, 14eqeltri 2507 . . . . 5  |-  N  e. 
_V
1615a1i 11 . . . 4  |-  ( ( C  e.  Cat  /\  D  e.  Cat )  ->  N  e.  _V )
17 eqid 2437 . . . 4  |-  ( Hom  `  Q )  =  ( Hom  `  Q )
1810, 11, 12, 13, 16, 17strfv3 14196 . . 3  |-  ( ( C  e.  Cat  /\  D  e.  Cat )  ->  ( Hom  `  Q
)  =  N )
1918eqcomd 2442 . 2  |-  ( ( C  e.  Cat  /\  D  e.  Cat )  ->  N  =  ( Hom  `  Q ) )
20 df-hom 14249 . . . 4  |-  Hom  = Slot ; 1 4
2120str0 14199 . . 3  |-  (/)  =  ( Hom  `  (/) )
223natffn 14846 . . . . 5  |-  N  Fn  ( ( C  Func  D )  X.  ( C 
Func  D ) )
23 funcrcl 14760 . . . . . . . . . 10  |-  ( f  e.  ( C  Func  D )  ->  ( C  e.  Cat  /\  D  e. 
Cat ) )
2423con3i 135 . . . . . . . . 9  |-  ( -.  ( C  e.  Cat  /\  D  e.  Cat )  ->  -.  f  e.  ( C  Func  D )
)
2524eq0rdv 3664 . . . . . . . 8  |-  ( -.  ( C  e.  Cat  /\  D  e.  Cat )  ->  ( C  Func  D
)  =  (/) )
2625xpeq2d 4855 . . . . . . 7  |-  ( -.  ( C  e.  Cat  /\  D  e.  Cat )  ->  ( ( C  Func  D )  X.  ( C 
Func  D ) )  =  ( ( C  Func  D )  X.  (/) ) )
27 xp0 5248 . . . . . . 7  |-  ( ( C  Func  D )  X.  (/) )  =  (/)
2826, 27syl6eq 2485 . . . . . 6  |-  ( -.  ( C  e.  Cat  /\  D  e.  Cat )  ->  ( ( C  Func  D )  X.  ( C 
Func  D ) )  =  (/) )
2928fneq2d 5494 . . . . 5  |-  ( -.  ( C  e.  Cat  /\  D  e.  Cat )  ->  ( N  Fn  (
( C  Func  D
)  X.  ( C 
Func  D ) )  <->  N  Fn  (/) ) )
3022, 29mpbii 211 . . . 4  |-  ( -.  ( C  e.  Cat  /\  D  e.  Cat )  ->  N  Fn  (/) )
31 fn0 5522 . . . 4  |-  ( N  Fn  (/)  <->  N  =  (/) )
3230, 31sylib 196 . . 3  |-  ( -.  ( C  e.  Cat  /\  D  e.  Cat )  ->  N  =  (/) )
33 fnfuc 14842 . . . . . . 7  |- FuncCat  Fn  ( Cat  X.  Cat )
34 fndm 5502 . . . . . . 7  |-  ( FuncCat  Fn  ( Cat  X.  Cat )  ->  dom FuncCat  =  ( Cat  X. 
Cat ) )
3533, 34ax-mp 5 . . . . . 6  |-  dom FuncCat  =  ( Cat  X.  Cat )
3635ndmov 6240 . . . . 5  |-  ( -.  ( C  e.  Cat  /\  D  e.  Cat )  ->  ( C FuncCat  D )  =  (/) )
371, 36syl5eq 2481 . . . 4  |-  ( -.  ( C  e.  Cat  /\  D  e.  Cat )  ->  Q  =  (/) )
3837fveq2d 5687 . . 3  |-  ( -.  ( C  e.  Cat  /\  D  e.  Cat )  ->  ( Hom  `  Q
)  =  ( Hom  `  (/) ) )
3921, 32, 383eqtr4a 2495 . 2  |-  ( -.  ( C  e.  Cat  /\  D  e.  Cat )  ->  N  =  ( Hom  `  Q ) )
4019, 39pm2.61i 164 1  |-  N  =  ( Hom  `  Q
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    /\ wa 369    = wceq 1364    e. wcel 1757   _Vcvv 2966   (/)c0 3629   {ctp 3873   <.cop 3875    X. cxp 4829   dom cdm 4831    Fn wfn 5405   ` cfv 5410  (class class class)co 6084   1c1 9275   4c4 10365   5c5 10366  ;cdc 10747   ndxcnx 14158   Basecbs 14161   Hom chom 14236  compcco 14237   Catccat 14589    Func cfunc 14751   Nat cnat 14838   FuncCat cfuc 14839
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2418  ax-rep 4395  ax-sep 4405  ax-nul 4413  ax-pow 4462  ax-pr 4523  ax-un 6365  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-fal 1370  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2714  df-rex 2715  df-reu 2716  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3281  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-pss 3336  df-nul 3630  df-if 3784  df-pw 3854  df-sn 3870  df-pr 3872  df-tp 3874  df-op 3876  df-uni 4084  df-int 4121  df-iun 4165  df-br 4285  df-opab 4343  df-mpt 4344  df-tr 4378  df-eprel 4623  df-id 4627  df-po 4632  df-so 4633  df-fr 4670  df-we 4672  df-ord 4713  df-on 4714  df-lim 4715  df-suc 4716  df-xp 4837  df-rel 4838  df-cnv 4839  df-co 4840  df-dm 4841  df-rn 4842  df-res 4843  df-ima 4844  df-iota 5373  df-fun 5412  df-fn 5413  df-f 5414  df-f1 5415  df-fo 5416  df-f1o 5417  df-fv 5418  df-riota 6043  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-om 6470  df-1st 6570  df-2nd 6571  df-recs 6822  df-rdg 6856  df-1o 6912  df-oadd 6916  df-er 7093  df-ixp 7256  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-nn 10315  df-2 10372  df-3 10373  df-4 10374  df-5 10375  df-6 10376  df-7 10377  df-8 10378  df-9 10379  df-10 10380  df-n0 10572  df-z 10639  df-dec 10748  df-uz 10854  df-fz 11429  df-struct 14163  df-ndx 14164  df-slot 14165  df-base 14166  df-hom 14249  df-cco 14250  df-func 14755  df-nat 14840  df-fuc 14841
This theorem is referenced by:  fuccatid  14866  fucsect  14869  fuciso  14872  evlfcllem  15018  evlfcl  15019  curfcl  15029  uncf2  15034  curfuncf  15035  diag2cl  15043  curf2ndf  15044  yonedalem21  15070  yonedalem22  15075  yonedalem3b  15076  yonedalem3  15077  yonffthlem  15079
  Copyright terms: Public domain W3C validator