Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isfunb Unicode version

Theorem isfunb 25835
Description: The predicate "is a functor" . (Contributed by FL, 10-Feb-2008.)
Hypotheses
Ref Expression
isfunb.1  |-  O1  =  dom  ( id_ `  T
)
isfunb.2  |-  M1  =  dom  ( dom_ `  T
)
isfunb.3  |-  D1  =  ( dom_ `  T )
isfunb.4  |-  C1  =  ( cod_ `  T )
isfunb.5  |-  I1  =  ( id_ `  T )
isfunb.6  |-  Ro 1  =  ( o_ `  T )
isfunb.7  |-  O 2  =  dom  ( id_ `  U
)
isfunb.8  |-  M 2  =  dom  ( dom_ `  U
)
isfunb.9  |-  D 2  =  ( dom_ `  U
)
isfunb.10  |-  C 2  =  ( cod_ `  U
)
isfunb.11  |-  I 2  =  ( id_ `  U
)
isfunb.12  |-  Ro 2  =  ( o_ `  U )
Assertion
Ref Expression
isfunb  |-  ( ( T  e.  Cat OLD  /\  U  e.  Cat OLD  )  ->  ( F  e.  ( Func OLD `  <. T ,  U >. )  <->  ( F : M1 --> M 2  /\  ( A. o  e.  O1  E. p  e.  O 2  ( F `  ( I1 `  o ) )  =  ( I 2 `  p )  /\  ( A. m  e.  M1  ( F `  ( I1 `  ( D1 `  m ) ) )  =  ( I 2 `  ( D 2 `  ( F `  m ) ) )  /\  A. m  e.  M1  ( F `
 ( I1 `  ( C1 `  m ) ) )  =  ( I 2 `  ( C 2 `  ( F `
 m ) ) ) )  /\  A. m  e.  M1  A. n  e.  M1  ( ( C1 `  n )  =  (
D1 `  m )  ->  ( F `  (
m Ro 1 n
) )  =  ( ( F `  m
) Ro 2 ( F `  n )
) ) ) ) ) )
Distinct variable groups:    m, n, M1    o, O1    p, O 2    m, o, p, F, n    T, m, n, o, p    U, m, n, o, p
Allowed substitution hints:    O1( m, n, p)    M1( o, p)    O 2( m, n, o)    M 2( m, n, o, p)    I1( m, n, o, p)    D1( m, n, o, p)    C1( m, n, o, p)    Ro 1( m, n, o, p)    I 2( m, n, o, p)    D 2( m, n, o, p)    C 2( m, n, o, p)    Ro 2( m, n, o, p)

Proof of Theorem isfunb
Dummy variable  f is distinct from all other variables.
StepHypRef Expression
1 isfunb.1 . . . 4  |-  O1  =  dom  ( id_ `  T
)
2 isfunb.2 . . . 4  |-  M1  =  dom  ( dom_ `  T
)
3 isfunb.3 . . . 4  |-  D1  =  ( dom_ `  T )
4 isfunb.4 . . . 4  |-  C1  =  ( cod_ `  T )
5 isfunb.5 . . . 4  |-  I1  =  ( id_ `  T )
6 isfunb.6 . . . 4  |-  Ro 1  =  ( o_ `  T )
7 isfunb.7 . . . 4  |-  O 2  =  dom  ( id_ `  U
)
8 isfunb.8 . . . 4  |-  M 2  =  dom  ( dom_ `  U
)
9 isfunb.9 . . . 4  |-  D 2  =  ( dom_ `  U
)
10 isfunb.10 . . . 4  |-  C 2  =  ( cod_ `  U
)
11 isfunb.11 . . . 4  |-  I 2  =  ( id_ `  U
)
12 isfunb.12 . . . 4  |-  Ro 2  =  ( o_ `  U )
131, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12isfuna 25834 . . 3  |-  ( ( T  e.  Cat OLD  /\  U  e.  Cat OLD  )  ->  ( Func OLD ` 
<. T ,  U >. )  =  { f  e.  ( M 2  ^m  M1 )  |  ( A. o  e.  O1  E. p  e.  O 2  ( f `
 ( I1 `  o
) )  =  ( I 2 `  p
)  /\  ( A. m  e.  M1  ( f `
 ( I1 `  ( D1 `  m ) ) )  =  ( I 2 `  ( D 2 `  ( f `
 m ) ) )  /\  A. m  e.  M1  ( f `  ( I1 `  ( C1 `  m ) ) )  =  ( I 2 `  ( C 2 `  ( f `  m
) ) ) )  /\  A. m  e.  M1  A. n  e.  M1  ( ( C1 `  n
)  =  ( D1 `  m )  ->  (
f `  ( m Ro 1 n ) )  =  ( ( f `
 m ) Ro
2 ( f `  n ) ) ) ) } )
1413eleq2d 2350 . 2  |-  ( ( T  e.  Cat OLD  /\  U  e.  Cat OLD  )  ->  ( F  e.  ( Func OLD `  <. T ,  U >. )  <->  F  e.  { f  e.  ( M 2  ^m  M1 )  |  ( A. o  e.  O1  E. p  e.  O 2  ( f `
 ( I1 `  o
) )  =  ( I 2 `  p
)  /\  ( A. m  e.  M1  ( f `
 ( I1 `  ( D1 `  m ) ) )  =  ( I 2 `  ( D 2 `  ( f `
 m ) ) )  /\  A. m  e.  M1  ( f `  ( I1 `  ( C1 `  m ) ) )  =  ( I 2 `  ( C 2 `  ( f `  m
) ) ) )  /\  A. m  e.  M1  A. n  e.  M1  ( ( C1 `  n
)  =  ( D1 `  m )  ->  (
f `  ( m Ro 1 n ) )  =  ( ( f `
 m ) Ro
2 ( f `  n ) ) ) ) } ) )
15 fveq1 5524 . . . . . . . 8  |-  ( f  =  F  ->  (
f `  ( I1 `  o
) )  =  ( F `  ( I1 `  o ) ) )
1615eqeq1d 2291 . . . . . . 7  |-  ( f  =  F  ->  (
( f `  ( I1 `  o ) )  =  ( I 2 `  p )  <->  ( F `  ( I1 `  o
) )  =  ( I 2 `  p
) ) )
1716rexbidv 2564 . . . . . 6  |-  ( f  =  F  ->  ( E. p  e.  O 2  ( f `  ( I1 `  o ) )  =  ( I 2 `  p )  <->  E. p  e.  O 2  ( F `  ( I1 `  o ) )  =  ( I 2 `  p ) ) )
1817ralbidv 2563 . . . . 5  |-  ( f  =  F  ->  ( A. o  e.  O1  E. p  e.  O 2  ( f `
 ( I1 `  o
) )  =  ( I 2 `  p
)  <->  A. o  e.  O1  E. p  e.  O 2 
( F `  ( I1 `  o ) )  =  ( I 2 `  p ) ) )
19 fveq1 5524 . . . . . . . 8  |-  ( f  =  F  ->  (
f `  ( I1 `  ( D1 `  m ) ) )  =  ( F `
 ( I1 `  ( D1 `  m ) ) ) )
20 fveq1 5524 . . . . . . . . . 10  |-  ( f  =  F  ->  (
f `  m )  =  ( F `  m ) )
2120fveq2d 5529 . . . . . . . . 9  |-  ( f  =  F  ->  ( D 2 `  ( f `
 m ) )  =  ( D 2 `  ( F `  m
) ) )
2221fveq2d 5529 . . . . . . . 8  |-  ( f  =  F  ->  (
I 2 `  ( D 2 `  ( f `
 m ) ) )  =  ( I 2 `  ( D 2 `  ( F `
 m ) ) ) )
2319, 22eqeq12d 2297 . . . . . . 7  |-  ( f  =  F  ->  (
( f `  ( I1 `  ( D1 `  m
) ) )  =  ( I 2 `  ( D 2 `  (
f `  m )
) )  <->  ( F `  ( I1 `  ( D1 `  m ) ) )  =  ( I 2 `  ( D 2 `  ( F `
 m ) ) ) ) )
2423ralbidv 2563 . . . . . 6  |-  ( f  =  F  ->  ( A. m  e.  M1  (
f `  ( I1 `  ( D1 `  m ) ) )  =  ( I 2 `  ( D 2 `  ( f `
 m ) ) )  <->  A. m  e.  M1  ( F `  ( I1 `  ( D1 `  m
) ) )  =  ( I 2 `  ( D 2 `  ( F `  m )
) ) ) )
25 fveq1 5524 . . . . . . . 8  |-  ( f  =  F  ->  (
f `  ( I1 `  ( C1 `  m ) ) )  =  ( F `
 ( I1 `  ( C1 `  m ) ) ) )
2620fveq2d 5529 . . . . . . . . 9  |-  ( f  =  F  ->  ( C 2 `  ( f `
 m ) )  =  ( C 2 `  ( F `  m
) ) )
2726fveq2d 5529 . . . . . . . 8  |-  ( f  =  F  ->  (
I 2 `  ( C 2 `  ( f `
 m ) ) )  =  ( I 2 `  ( C 2 `  ( F `
 m ) ) ) )
2825, 27eqeq12d 2297 . . . . . . 7  |-  ( f  =  F  ->  (
( f `  ( I1 `  ( C1 `  m
) ) )  =  ( I 2 `  ( C 2 `  (
f `  m )
) )  <->  ( F `  ( I1 `  ( C1 `  m ) ) )  =  ( I 2 `  ( C 2 `  ( F `
 m ) ) ) ) )
2928ralbidv 2563 . . . . . 6  |-  ( f  =  F  ->  ( A. m  e.  M1  (
f `  ( I1 `  ( C1 `  m ) ) )  =  ( I 2 `  ( C 2 `  ( f `
 m ) ) )  <->  A. m  e.  M1  ( F `  ( I1 `  ( C1 `  m
) ) )  =  ( I 2 `  ( C 2 `  ( F `  m )
) ) ) )
3024, 29anbi12d 691 . . . . 5  |-  ( f  =  F  ->  (
( A. m  e.  M1  ( f `  ( I1 `  ( D1 `  m
) ) )  =  ( I 2 `  ( D 2 `  (
f `  m )
) )  /\  A. m  e.  M1  ( f `
 ( I1 `  ( C1 `  m ) ) )  =  ( I 2 `  ( C 2 `  ( f `
 m ) ) ) )  <->  ( A. m  e.  M1  ( F `
 ( I1 `  ( D1 `  m ) ) )  =  ( I 2 `  ( D 2 `  ( F `
 m ) ) )  /\  A. m  e.  M1  ( F `  ( I1 `  ( C1 `  m ) ) )  =  ( I 2 `  ( C 2 `  ( F `  m ) ) ) ) ) )
31 fveq1 5524 . . . . . . . 8  |-  ( f  =  F  ->  (
f `  ( m Ro 1 n ) )  =  ( F `  ( m Ro 1
n ) ) )
32 fveq1 5524 . . . . . . . . 9  |-  ( f  =  F  ->  (
f `  n )  =  ( F `  n ) )
3320, 32oveq12d 5876 . . . . . . . 8  |-  ( f  =  F  ->  (
( f `  m
) Ro 2 (
f `  n )
)  =  ( ( F `  m ) Ro 2 ( F `
 n ) ) )
3431, 33eqeq12d 2297 . . . . . . 7  |-  ( f  =  F  ->  (
( f `  (
m Ro 1 n
) )  =  ( ( f `  m
) Ro 2 (
f `  n )
)  <->  ( F `  ( m Ro 1
n ) )  =  ( ( F `  m ) Ro 2
( F `  n
) ) ) )
3534imbi2d 307 . . . . . 6  |-  ( f  =  F  ->  (
( ( C1 `  n
)  =  ( D1 `  m )  ->  (
f `  ( m Ro 1 n ) )  =  ( ( f `
 m ) Ro
2 ( f `  n ) ) )  <-> 
( ( C1 `  n
)  =  ( D1 `  m )  ->  ( F `  ( m Ro 1 n ) )  =  ( ( F `
 m ) Ro
2 ( F `  n ) ) ) ) )
36352ralbidv 2585 . . . . 5  |-  ( f  =  F  ->  ( A. m  e.  M1  A. n  e.  M1  ( ( C1 `  n )  =  (
D1 `  m )  ->  ( f `  (
m Ro 1 n
) )  =  ( ( f `  m
) Ro 2 (
f `  n )
) )  <->  A. m  e.  M1  A. n  e.  M1  ( ( C1 `  n
)  =  ( D1 `  m )  ->  ( F `  ( m Ro 1 n ) )  =  ( ( F `
 m ) Ro
2 ( F `  n ) ) ) ) )
3718, 30, 363anbi123d 1252 . . . 4  |-  ( f  =  F  ->  (
( A. o  e.  O1  E. p  e.  O 2  ( f `  ( I1 `  o ) )  =  ( I 2 `  p )  /\  ( A. m  e.  M1  ( f `  ( I1 `  ( D1 `  m ) ) )  =  ( I 2 `  ( D 2 `  ( f `  m
) ) )  /\  A. m  e.  M1  (
f `  ( I1 `  ( C1 `  m ) ) )  =  ( I 2 `  ( C 2 `  ( f `
 m ) ) ) )  /\  A. m  e.  M1  A. n  e.  M1  ( ( C1 `  n )  =  (
D1 `  m )  ->  ( f `  (
m Ro 1 n
) )  =  ( ( f `  m
) Ro 2 (
f `  n )
) ) )  <->  ( A. o  e.  O1  E. p  e.  O 2  ( F `
 ( I1 `  o
) )  =  ( I 2 `  p
)  /\  ( A. m  e.  M1  ( F `
 ( I1 `  ( D1 `  m ) ) )  =  ( I 2 `  ( D 2 `  ( F `
 m ) ) )  /\  A. m  e.  M1  ( F `  ( I1 `  ( C1 `  m ) ) )  =  ( I 2 `  ( C 2 `  ( F `  m ) ) ) )  /\  A. m  e.  M1  A. n  e.  M1  ( ( C1 `  n )  =  (
D1 `  m )  ->  ( F `  (
m Ro 1 n
) )  =  ( ( F `  m
) Ro 2 ( F `  n )
) ) ) ) )
3837elrab 2923 . . 3  |-  ( F  e.  { f  e.  ( M 2  ^m  M1 )  |  ( A. o  e.  O1  E. p  e.  O 2  ( f `
 ( I1 `  o
) )  =  ( I 2 `  p
)  /\  ( A. m  e.  M1  ( f `
 ( I1 `  ( D1 `  m ) ) )  =  ( I 2 `  ( D 2 `  ( f `
 m ) ) )  /\  A. m  e.  M1  ( f `  ( I1 `  ( C1 `  m ) ) )  =  ( I 2 `  ( C 2 `  ( f `  m
) ) ) )  /\  A. m  e.  M1  A. n  e.  M1  ( ( C1 `  n
)  =  ( D1 `  m )  ->  (
f `  ( m Ro 1 n ) )  =  ( ( f `
 m ) Ro
2 ( f `  n ) ) ) ) }  <->  ( F  e.  ( M 2  ^m  M1 )  /\  ( A. o  e.  O1  E. p  e.  O 2  ( F `
 ( I1 `  o
) )  =  ( I 2 `  p
)  /\  ( A. m  e.  M1  ( F `
 ( I1 `  ( D1 `  m ) ) )  =  ( I 2 `  ( D 2 `  ( F `
 m ) ) )  /\  A. m  e.  M1  ( F `  ( I1 `  ( C1 `  m ) ) )  =  ( I 2 `  ( C 2 `  ( F `  m ) ) ) )  /\  A. m  e.  M1  A. n  e.  M1  ( ( C1 `  n )  =  (
D1 `  m )  ->  ( F `  (
m Ro 1 n
) )  =  ( ( F `  m
) Ro 2 ( F `  n )
) ) ) ) )
39 fvex 5539 . . . . . . 7  |-  ( dom_ `  U )  e.  _V
4039dmex 4941 . . . . . 6  |-  dom  ( dom_ `  U )  e. 
_V
418, 40eqeltri 2353 . . . . 5  |-  M 2  e.  _V
42 fvex 5539 . . . . . . 7  |-  ( dom_ `  T )  e.  _V
4342dmex 4941 . . . . . 6  |-  dom  ( dom_ `  T )  e. 
_V
442, 43eqeltri 2353 . . . . 5  |-  M1  e.  _V
4541, 44elmap 6796 . . . 4  |-  ( F  e.  ( M 2  ^m  M1 )  <->  F : M1
--> M 2 )
4645anbi1i 676 . . 3  |-  ( ( F  e.  ( M 2  ^m  M1 )  /\  ( A. o  e.  O1  E. p  e.  O 2  ( F `  ( I1 `  o ) )  =  ( I 2 `  p )  /\  ( A. m  e.  M1  ( F `  ( I1 `  ( D1 `  m ) ) )  =  ( I 2 `  ( D 2 `  ( F `  m ) ) )  /\  A. m  e.  M1  ( F `
 ( I1 `  ( C1 `  m ) ) )  =  ( I 2 `  ( C 2 `  ( F `
 m ) ) ) )  /\  A. m  e.  M1  A. n  e.  M1  ( ( C1 `  n )  =  (
D1 `  m )  ->  ( F `  (
m Ro 1 n
) )  =  ( ( F `  m
) Ro 2 ( F `  n )
) ) ) )  <-> 
( F : M1 --> M 2  /\  ( A. o  e.  O1  E. p  e.  O 2  ( F `
 ( I1 `  o
) )  =  ( I 2 `  p
)  /\  ( A. m  e.  M1  ( F `
 ( I1 `  ( D1 `  m ) ) )  =  ( I 2 `  ( D 2 `  ( F `
 m ) ) )  /\  A. m  e.  M1  ( F `  ( I1 `  ( C1 `  m ) ) )  =  ( I 2 `  ( C 2 `  ( F `  m ) ) ) )  /\  A. m  e.  M1  A. n  e.  M1  ( ( C1 `  n )  =  (
D1 `  m )  ->  ( F `  (
m Ro 1 n
) )  =  ( ( F `  m
) Ro 2 ( F `  n )
) ) ) ) )
4738, 46bitri 240 . 2  |-  ( F  e.  { f  e.  ( M 2  ^m  M1 )  |  ( A. o  e.  O1  E. p  e.  O 2  ( f `
 ( I1 `  o
) )  =  ( I 2 `  p
)  /\  ( A. m  e.  M1  ( f `
 ( I1 `  ( D1 `  m ) ) )  =  ( I 2 `  ( D 2 `  ( f `
 m ) ) )  /\  A. m  e.  M1  ( f `  ( I1 `  ( C1 `  m ) ) )  =  ( I 2 `  ( C 2 `  ( f `  m
) ) ) )  /\  A. m  e.  M1  A. n  e.  M1  ( ( C1 `  n
)  =  ( D1 `  m )  ->  (
f `  ( m Ro 1 n ) )  =  ( ( f `
 m ) Ro
2 ( f `  n ) ) ) ) }  <->  ( F : M1 --> M 2  /\  ( A. o  e.  O1  E. p  e.  O 2 
( F `  ( I1 `  o ) )  =  ( I 2 `  p )  /\  ( A. m  e.  M1  ( F `  ( I1 `  ( D1 `  m ) ) )  =  ( I 2 `  ( D 2 `  ( F `
 m ) ) )  /\  A. m  e.  M1  ( F `  ( I1 `  ( C1 `  m ) ) )  =  ( I 2 `  ( C 2 `  ( F `  m ) ) ) )  /\  A. m  e.  M1  A. n  e.  M1  ( ( C1 `  n )  =  (
D1 `  m )  ->  ( F `  (
m Ro 1 n
) )  =  ( ( F `  m
) Ro 2 ( F `  n )
) ) ) ) )
4814, 47syl6bb 252 1  |-  ( ( T  e.  Cat OLD  /\  U  e.  Cat OLD  )  ->  ( F  e.  ( Func OLD `  <. T ,  U >. )  <->  ( F : M1 --> M 2  /\  ( A. o  e.  O1  E. p  e.  O 2  ( F `  ( I1 `  o ) )  =  ( I 2 `  p )  /\  ( A. m  e.  M1  ( F `  ( I1 `  ( D1 `  m ) ) )  =  ( I 2 `  ( D 2 `  ( F `  m ) ) )  /\  A. m  e.  M1  ( F `
 ( I1 `  ( C1 `  m ) ) )  =  ( I 2 `  ( C 2 `  ( F `
 m ) ) ) )  /\  A. m  e.  M1  A. n  e.  M1  ( ( C1 `  n )  =  (
D1 `  m )  ->  ( F `  (
m Ro 1 n
) )  =  ( ( F `  m
) Ro 2 ( F `  n )
) ) ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934    = wceq 1623    e. wcel 1684   A.wral 2543   E.wrex 2544   {crab 2547   _Vcvv 2788   <.cop 3643   dom cdm 4689   -->wf 5251   ` cfv 5255  (class class class)co 5858    ^m cmap 6772   dom_cdom_ 25712   cod_ccod_ 25713   id_cid_ 25714   o_co_ 25715    Cat
OLD ccatOLD 25752   Func
OLDcfuncOLD 25831
This theorem is referenced by:  fmamo  25836  vidfunid  25837  iddvvidd  25838  idcvvidc  25839  fmp  25840  idfisf  25841  idsubfun  25858
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-map 6774  df-funcOLD 25833
  Copyright terms: Public domain W3C validator