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

Theorem catcocl 14734
Description: Closure of a composition arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
catcocl.b  |-  B  =  ( Base `  C
)
catcocl.h  |-  H  =  ( Hom  `  C
)
catcocl.o  |-  .x.  =  (comp `  C )
catcocl.c  |-  ( ph  ->  C  e.  Cat )
catcocl.x  |-  ( ph  ->  X  e.  B )
catcocl.y  |-  ( ph  ->  Y  e.  B )
catcocl.z  |-  ( ph  ->  Z  e.  B )
catcocl.f  |-  ( ph  ->  F  e.  ( X H Y ) )
catcocl.g  |-  ( ph  ->  G  e.  ( Y H Z ) )
Assertion
Ref Expression
catcocl  |-  ( ph  ->  ( G ( <. X ,  Y >.  .x. 
Z ) F )  e.  ( X H Z ) )

Proof of Theorem catcocl
Dummy variables  f 
g  v  w  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 catcocl.c . . 3  |-  ( ph  ->  C  e.  Cat )
2 catcocl.b . . . . 5  |-  B  =  ( Base `  C
)
3 catcocl.h . . . . 5  |-  H  =  ( Hom  `  C
)
4 catcocl.o . . . . 5  |-  .x.  =  (comp `  C )
52, 3, 4iscat 14721 . . . 4  |-  ( C  e.  Cat  ->  ( C  e.  Cat  <->  A. x  e.  B  ( E. g  e.  ( x H x ) A. y  e.  B  ( A. f  e.  (
y H x ) ( g ( <.
y ,  x >.  .x.  x ) f )  =  f  /\  A. f  e.  ( x H y ) ( f ( <. x ,  x >.  .x.  y ) g )  =  f )  /\  A. y  e.  B  A. z  e.  B  A. f  e.  ( x H y ) A. g  e.  ( y H z ) ( ( g ( <. x ,  y
>.  .x.  z ) f )  e.  ( x H z )  /\  A. w  e.  B  A. v  e.  ( z H w ) ( ( v ( <.
y ,  z >.  .x.  w ) g ) ( <. x ,  y
>.  .x.  w ) f )  =  ( v ( <. x ,  z
>.  .x.  w ) ( g ( <. x ,  y >.  .x.  z
) f ) ) ) ) ) )
65ibi 241 . . 3  |-  ( C  e.  Cat  ->  A. x  e.  B  ( E. g  e.  ( x H x ) A. y  e.  B  ( A. f  e.  (
y H x ) ( g ( <.
y ,  x >.  .x.  x ) f )  =  f  /\  A. f  e.  ( x H y ) ( f ( <. x ,  x >.  .x.  y ) g )  =  f )  /\  A. y  e.  B  A. z  e.  B  A. f  e.  ( x H y ) A. g  e.  ( y H z ) ( ( g ( <. x ,  y
>.  .x.  z ) f )  e.  ( x H z )  /\  A. w  e.  B  A. v  e.  ( z H w ) ( ( v ( <.
y ,  z >.  .x.  w ) g ) ( <. x ,  y
>.  .x.  w ) f )  =  ( v ( <. x ,  z
>.  .x.  w ) ( g ( <. x ,  y >.  .x.  z
) f ) ) ) ) )
7 simpl 457 . . . . . . . . 9  |-  ( ( ( g ( <.
x ,  y >.  .x.  z ) f )  e.  ( x H z )  /\  A. w  e.  B  A. v  e.  ( z H w ) ( ( v ( <.
y ,  z >.  .x.  w ) g ) ( <. x ,  y
>.  .x.  w ) f )  =  ( v ( <. x ,  z
>.  .x.  w ) ( g ( <. x ,  y >.  .x.  z
) f ) ) )  ->  ( g
( <. x ,  y
>.  .x.  z ) f )  e.  ( x H z ) )
87ralimi 2814 . . . . . . . 8  |-  ( A. g  e.  ( y H z ) ( ( g ( <.
x ,  y >.  .x.  z ) f )  e.  ( x H z )  /\  A. w  e.  B  A. v  e.  ( z H w ) ( ( v ( <.
y ,  z >.  .x.  w ) g ) ( <. x ,  y
>.  .x.  w ) f )  =  ( v ( <. x ,  z
>.  .x.  w ) ( g ( <. x ,  y >.  .x.  z
) f ) ) )  ->  A. g  e.  ( y H z ) ( g (
<. x ,  y >.  .x.  z ) f )  e.  ( x H z ) )
98ralimi 2814 . . . . . . 7  |-  ( A. f  e.  ( x H y ) A. g  e.  ( y H z ) ( ( g ( <.
x ,  y >.  .x.  z ) f )  e.  ( x H z )  /\  A. w  e.  B  A. v  e.  ( z H w ) ( ( v ( <.
y ,  z >.  .x.  w ) g ) ( <. x ,  y
>.  .x.  w ) f )  =  ( v ( <. x ,  z
>.  .x.  w ) ( g ( <. x ,  y >.  .x.  z
) f ) ) )  ->  A. f  e.  ( x H y ) A. g  e.  ( y H z ) ( g (
<. x ,  y >.  .x.  z ) f )  e.  ( x H z ) )
109ralimi 2814 . . . . . 6  |-  ( A. z  e.  B  A. f  e.  ( x H y ) A. g  e.  ( y H z ) ( ( g ( <.
x ,  y >.  .x.  z ) f )  e.  ( x H z )  /\  A. w  e.  B  A. v  e.  ( z H w ) ( ( v ( <.
y ,  z >.  .x.  w ) g ) ( <. x ,  y
>.  .x.  w ) f )  =  ( v ( <. x ,  z
>.  .x.  w ) ( g ( <. x ,  y >.  .x.  z
) f ) ) )  ->  A. z  e.  B  A. f  e.  ( x H y ) A. g  e.  ( y H z ) ( g (
<. x ,  y >.  .x.  z ) f )  e.  ( x H z ) )
1110ralimi 2814 . . . . 5  |-  ( A. y  e.  B  A. z  e.  B  A. f  e.  ( x H y ) A. g  e.  ( y H z ) ( ( g ( <.
x ,  y >.  .x.  z ) f )  e.  ( x H z )  /\  A. w  e.  B  A. v  e.  ( z H w ) ( ( v ( <.
y ,  z >.  .x.  w ) g ) ( <. x ,  y
>.  .x.  w ) f )  =  ( v ( <. x ,  z
>.  .x.  w ) ( g ( <. x ,  y >.  .x.  z
) f ) ) )  ->  A. y  e.  B  A. z  e.  B  A. f  e.  ( x H y ) A. g  e.  ( y H z ) ( g (
<. x ,  y >.  .x.  z ) f )  e.  ( x H z ) )
1211adantl 466 . . . 4  |-  ( ( E. g  e.  ( x H x ) A. y  e.  B  ( A. f  e.  ( y H x ) ( g ( <.
y ,  x >.  .x.  x ) f )  =  f  /\  A. f  e.  ( x H y ) ( f ( <. x ,  x >.  .x.  y ) g )  =  f )  /\  A. y  e.  B  A. z  e.  B  A. f  e.  ( x H y ) A. g  e.  ( y H z ) ( ( g ( <. x ,  y
>.  .x.  z ) f )  e.  ( x H z )  /\  A. w  e.  B  A. v  e.  ( z H w ) ( ( v ( <.
y ,  z >.  .x.  w ) g ) ( <. x ,  y
>.  .x.  w ) f )  =  ( v ( <. x ,  z
>.  .x.  w ) ( g ( <. x ,  y >.  .x.  z
) f ) ) ) )  ->  A. y  e.  B  A. z  e.  B  A. f  e.  ( x H y ) A. g  e.  ( y H z ) ( g (
<. x ,  y >.  .x.  z ) f )  e.  ( x H z ) )
1312ralimi 2814 . . 3  |-  ( A. x  e.  B  ( E. g  e.  (
x H x ) A. y  e.  B  ( A. f  e.  ( y H x ) ( g ( <.
y ,  x >.  .x.  x ) f )  =  f  /\  A. f  e.  ( x H y ) ( f ( <. x ,  x >.  .x.  y ) g )  =  f )  /\  A. y  e.  B  A. z  e.  B  A. f  e.  ( x H y ) A. g  e.  ( y H z ) ( ( g ( <. x ,  y
>.  .x.  z ) f )  e.  ( x H z )  /\  A. w  e.  B  A. v  e.  ( z H w ) ( ( v ( <.
y ,  z >.  .x.  w ) g ) ( <. x ,  y
>.  .x.  w ) f )  =  ( v ( <. x ,  z
>.  .x.  w ) ( g ( <. x ,  y >.  .x.  z
) f ) ) ) )  ->  A. x  e.  B  A. y  e.  B  A. z  e.  B  A. f  e.  ( x H y ) A. g  e.  ( y H z ) ( g (
<. x ,  y >.  .x.  z ) f )  e.  ( x H z ) )
141, 6, 133syl 20 . 2  |-  ( ph  ->  A. x  e.  B  A. y  e.  B  A. z  e.  B  A. f  e.  (
x H y ) A. g  e.  ( y H z ) ( g ( <.
x ,  y >.  .x.  z ) f )  e.  ( x H z ) )
15 catcocl.x . . 3  |-  ( ph  ->  X  e.  B )
16 catcocl.y . . . . 5  |-  ( ph  ->  Y  e.  B )
1716adantr 465 . . . 4  |-  ( (
ph  /\  x  =  X )  ->  Y  e.  B )
18 catcocl.z . . . . . 6  |-  ( ph  ->  Z  e.  B )
1918ad2antrr 725 . . . . 5  |-  ( ( ( ph  /\  x  =  X )  /\  y  =  Y )  ->  Z  e.  B )
20 catcocl.f . . . . . . . 8  |-  ( ph  ->  F  e.  ( X H Y ) )
2120ad3antrrr 729 . . . . . . 7  |-  ( ( ( ( ph  /\  x  =  X )  /\  y  =  Y
)  /\  z  =  Z )  ->  F  e.  ( X H Y ) )
22 simpllr 758 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  =  X )  /\  y  =  Y
)  /\  z  =  Z )  ->  x  =  X )
23 simplr 754 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  =  X )  /\  y  =  Y
)  /\  z  =  Z )  ->  y  =  Y )
2422, 23oveq12d 6211 . . . . . . 7  |-  ( ( ( ( ph  /\  x  =  X )  /\  y  =  Y
)  /\  z  =  Z )  ->  (
x H y )  =  ( X H Y ) )
2521, 24eleqtrrd 2542 . . . . . 6  |-  ( ( ( ( ph  /\  x  =  X )  /\  y  =  Y
)  /\  z  =  Z )  ->  F  e.  ( x H y ) )
26 catcocl.g . . . . . . . . . 10  |-  ( ph  ->  G  e.  ( Y H Z ) )
2726ad3antrrr 729 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  =  X )  /\  y  =  Y
)  /\  z  =  Z )  ->  G  e.  ( Y H Z ) )
28 simpr 461 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  =  X )  /\  y  =  Y
)  /\  z  =  Z )  ->  z  =  Z )
2923, 28oveq12d 6211 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  =  X )  /\  y  =  Y
)  /\  z  =  Z )  ->  (
y H z )  =  ( Y H Z ) )
3027, 29eleqtrrd 2542 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  =  X )  /\  y  =  Y
)  /\  z  =  Z )  ->  G  e.  ( y H z ) )
3130adantr 465 . . . . . . 7  |-  ( ( ( ( ( ph  /\  x  =  X )  /\  y  =  Y )  /\  z  =  Z )  /\  f  =  F )  ->  G  e.  ( y H z ) )
32 simp-5r 768 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  x  =  X )  /\  y  =  Y )  /\  z  =  Z )  /\  f  =  F )  /\  g  =  G )  ->  x  =  X )
33 simp-4r 766 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  x  =  X )  /\  y  =  Y )  /\  z  =  Z )  /\  f  =  F )  /\  g  =  G )  ->  y  =  Y )
3432, 33opeq12d 4168 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  x  =  X )  /\  y  =  Y )  /\  z  =  Z )  /\  f  =  F )  /\  g  =  G )  ->  <. x ,  y >.  =  <. X ,  Y >. )
35 simpllr 758 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  x  =  X )  /\  y  =  Y )  /\  z  =  Z )  /\  f  =  F )  /\  g  =  G )  ->  z  =  Z )
3634, 35oveq12d 6211 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  x  =  X )  /\  y  =  Y )  /\  z  =  Z )  /\  f  =  F )  /\  g  =  G )  ->  ( <. x ,  y >.  .x.  z )  =  (
<. X ,  Y >.  .x. 
Z ) )
37 simpr 461 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  x  =  X )  /\  y  =  Y )  /\  z  =  Z )  /\  f  =  F )  /\  g  =  G )  ->  g  =  G )
38 simplr 754 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  x  =  X )  /\  y  =  Y )  /\  z  =  Z )  /\  f  =  F )  /\  g  =  G )  ->  f  =  F )
3936, 37, 38oveq123d 6214 . . . . . . . 8  |-  ( ( ( ( ( (
ph  /\  x  =  X )  /\  y  =  Y )  /\  z  =  Z )  /\  f  =  F )  /\  g  =  G )  ->  (
g ( <. x ,  y >.  .x.  z
) f )  =  ( G ( <. X ,  Y >.  .x. 
Z ) F ) )
4032, 35oveq12d 6211 . . . . . . . 8  |-  ( ( ( ( ( (
ph  /\  x  =  X )  /\  y  =  Y )  /\  z  =  Z )  /\  f  =  F )  /\  g  =  G )  ->  (
x H z )  =  ( X H Z ) )
4139, 40eleq12d 2533 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  x  =  X )  /\  y  =  Y )  /\  z  =  Z )  /\  f  =  F )  /\  g  =  G )  ->  (
( g ( <.
x ,  y >.  .x.  z ) f )  e.  ( x H z )  <->  ( G
( <. X ,  Y >.  .x.  Z ) F )  e.  ( X H Z ) ) )
4231, 41rspcdv 3175 . . . . . 6  |-  ( ( ( ( ( ph  /\  x  =  X )  /\  y  =  Y )  /\  z  =  Z )  /\  f  =  F )  ->  ( A. g  e.  (
y H z ) ( g ( <.
x ,  y >.  .x.  z ) f )  e.  ( x H z )  ->  ( G ( <. X ,  Y >.  .x.  Z ) F )  e.  ( X H Z ) ) )
4325, 42rspcimdv 3173 . . . . 5  |-  ( ( ( ( ph  /\  x  =  X )  /\  y  =  Y
)  /\  z  =  Z )  ->  ( A. f  e.  (
x H y ) A. g  e.  ( y H z ) ( g ( <.
x ,  y >.  .x.  z ) f )  e.  ( x H z )  ->  ( G ( <. X ,  Y >.  .x.  Z ) F )  e.  ( X H Z ) ) )
4419, 43rspcimdv 3173 . . . 4  |-  ( ( ( ph  /\  x  =  X )  /\  y  =  Y )  ->  ( A. z  e.  B  A. f  e.  (
x H y ) A. g  e.  ( y H z ) ( g ( <.
x ,  y >.  .x.  z ) f )  e.  ( x H z )  ->  ( G ( <. X ,  Y >.  .x.  Z ) F )  e.  ( X H Z ) ) )
4517, 44rspcimdv 3173 . . 3  |-  ( (
ph  /\  x  =  X )  ->  ( A. y  e.  B  A. z  e.  B  A. f  e.  (
x H y ) A. g  e.  ( y H z ) ( g ( <.
x ,  y >.  .x.  z ) f )  e.  ( x H z )  ->  ( G ( <. X ,  Y >.  .x.  Z ) F )  e.  ( X H Z ) ) )
4615, 45rspcimdv 3173 . 2  |-  ( ph  ->  ( A. x  e.  B  A. y  e.  B  A. z  e.  B  A. f  e.  ( x H y ) A. g  e.  ( y H z ) ( g (
<. x ,  y >.  .x.  z ) f )  e.  ( x H z )  ->  ( G ( <. X ,  Y >.  .x.  Z ) F )  e.  ( X H Z ) ) )
4714, 46mpd 15 1  |-  ( ph  ->  ( G ( <. X ,  Y >.  .x. 
Z ) F )  e.  ( X H Z ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1370    e. wcel 1758   A.wral 2795   E.wrex 2796   <.cop 3984   ` cfv 5519  (class class class)co 6193   Basecbs 14285   Hom chom 14360  compcco 14361   Catccat 14713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-nul 4522
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3073  df-sbc 3288  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-sn 3979  df-pr 3981  df-op 3985  df-uni 4193  df-br 4394  df-iota 5482  df-fv 5527  df-ov 6196  df-cat 14717
This theorem is referenced by:  oppccatid  14769  ismon2  14784  isepi2  14791  sectco  14806  monsect  14828  issubc3  14870  fullsubc  14871  idfucl  14902  cofucl  14909  fthsect  14946  fthmon  14948  fuccocl  14985  invfuc  14995  coahom  15049  catcisolem  15085  xpccatid  15109  1stfcl  15118  2ndfcl  15119  prfcl  15124  evlfcllem  15142  evlfcl  15143  curf1cl  15149  curfcl  15153  hofcllem  15179  hofcl  15180  yon12  15186  hofpropd  15188  yonedalem4c  15198
  Copyright terms: Public domain W3C validator