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

Theorem 1stfcl 15012
Description: The first projection functor is a functor onto the left argument. (Contributed by Mario Carneiro, 11-Jan-2017.)
Hypotheses
Ref Expression
1stfcl.t  |-  T  =  ( C  X.c  D )
1stfcl.c  |-  ( ph  ->  C  e.  Cat )
1stfcl.d  |-  ( ph  ->  D  e.  Cat )
1stfcl.p  |-  P  =  ( C  1stF  D )
Assertion
Ref Expression
1stfcl  |-  ( ph  ->  P  e.  ( T 
Func  C ) )

Proof of Theorem 1stfcl
Dummy variables  f 
g  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1stfcl.t . . . 4  |-  T  =  ( C  X.c  D )
2 eqid 2443 . . . . 5  |-  ( Base `  C )  =  (
Base `  C )
3 eqid 2443 . . . . 5  |-  ( Base `  D )  =  (
Base `  D )
41, 2, 3xpcbas 14993 . . . 4  |-  ( (
Base `  C )  X.  ( Base `  D
) )  =  (
Base `  T )
5 eqid 2443 . . . 4  |-  ( Hom  `  T )  =  ( Hom  `  T )
6 1stfcl.c . . . 4  |-  ( ph  ->  C  e.  Cat )
7 1stfcl.d . . . 4  |-  ( ph  ->  D  e.  Cat )
8 1stfcl.p . . . 4  |-  P  =  ( C  1stF  D )
91, 4, 5, 6, 7, 81stfval 15006 . . 3  |-  ( ph  ->  P  =  <. ( 1st  |`  ( ( Base `  C )  X.  ( Base `  D ) ) ) ,  ( x  e.  ( ( Base `  C )  X.  ( Base `  D ) ) ,  y  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  |->  ( 1st  |`  ( x
( Hom  `  T ) y ) ) )
>. )
10 fo1st 6601 . . . . . . . 8  |-  1st : _V -onto-> _V
11 fofun 5626 . . . . . . . 8  |-  ( 1st
: _V -onto-> _V  ->  Fun 
1st )
1210, 11ax-mp 5 . . . . . . 7  |-  Fun  1st
13 fvex 5706 . . . . . . . 8  |-  ( Base `  C )  e.  _V
14 fvex 5706 . . . . . . . 8  |-  ( Base `  D )  e.  _V
1513, 14xpex 6513 . . . . . . 7  |-  ( (
Base `  C )  X.  ( Base `  D
) )  e.  _V
16 resfunexg 5948 . . . . . . 7  |-  ( ( Fun  1st  /\  (
( Base `  C )  X.  ( Base `  D
) )  e.  _V )  ->  ( 1st  |`  (
( Base `  C )  X.  ( Base `  D
) ) )  e. 
_V )
1712, 15, 16mp2an 672 . . . . . 6  |-  ( 1st  |`  ( ( Base `  C
)  X.  ( Base `  D ) ) )  e.  _V
1815, 15mpt2ex 6655 . . . . . 6  |-  ( x  e.  ( ( Base `  C )  X.  ( Base `  D ) ) ,  y  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  |->  ( 1st  |`  ( x
( Hom  `  T ) y ) ) )  e.  _V
1917, 18op2ndd 6593 . . . . 5  |-  ( P  =  <. ( 1st  |`  (
( Base `  C )  X.  ( Base `  D
) ) ) ,  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) ,  y  e.  ( (
Base `  C )  X.  ( Base `  D
) )  |->  ( 1st  |`  ( x ( Hom  `  T ) y ) ) ) >.  ->  ( 2nd `  P )  =  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) ,  y  e.  ( (
Base `  C )  X.  ( Base `  D
) )  |->  ( 1st  |`  ( x ( Hom  `  T ) y ) ) ) )
209, 19syl 16 . . . 4  |-  ( ph  ->  ( 2nd `  P
)  =  ( x  e.  ( ( Base `  C )  X.  ( Base `  D ) ) ,  y  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  |->  ( 1st  |`  ( x
( Hom  `  T ) y ) ) ) )
2120opeq2d 4071 . . 3  |-  ( ph  -> 
<. ( 1st  |`  (
( Base `  C )  X.  ( Base `  D
) ) ) ,  ( 2nd `  P
) >.  =  <. ( 1st  |`  ( ( Base `  C )  X.  ( Base `  D ) ) ) ,  ( x  e.  ( ( Base `  C )  X.  ( Base `  D ) ) ,  y  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  |->  ( 1st  |`  ( x
( Hom  `  T ) y ) ) )
>. )
229, 21eqtr4d 2478 . 2  |-  ( ph  ->  P  =  <. ( 1st  |`  ( ( Base `  C )  X.  ( Base `  D ) ) ) ,  ( 2nd `  P ) >. )
23 eqid 2443 . . . 4  |-  ( Hom  `  C )  =  ( Hom  `  C )
24 eqid 2443 . . . 4  |-  ( Id
`  T )  =  ( Id `  T
)
25 eqid 2443 . . . 4  |-  ( Id
`  C )  =  ( Id `  C
)
26 eqid 2443 . . . 4  |-  (comp `  T )  =  (comp `  T )
27 eqid 2443 . . . 4  |-  (comp `  C )  =  (comp `  C )
281, 6, 7xpccat 15005 . . . 4  |-  ( ph  ->  T  e.  Cat )
29 f1stres 6603 . . . . 5  |-  ( 1st  |`  ( ( Base `  C
)  X.  ( Base `  D ) ) ) : ( ( Base `  C )  X.  ( Base `  D ) ) --> ( Base `  C
)
3029a1i 11 . . . 4  |-  ( ph  ->  ( 1st  |`  (
( Base `  C )  X.  ( Base `  D
) ) ) : ( ( Base `  C
)  X.  ( Base `  D ) ) --> (
Base `  C )
)
31 eqid 2443 . . . . . 6  |-  ( x  e.  ( ( Base `  C )  X.  ( Base `  D ) ) ,  y  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  |->  ( 1st  |`  ( x
( Hom  `  T ) y ) ) )  =  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) ,  y  e.  ( (
Base `  C )  X.  ( Base `  D
) )  |->  ( 1st  |`  ( x ( Hom  `  T ) y ) ) )
32 ovex 6121 . . . . . . 7  |-  ( x ( Hom  `  T
) y )  e. 
_V
33 resfunexg 5948 . . . . . . 7  |-  ( ( Fun  1st  /\  (
x ( Hom  `  T
) y )  e. 
_V )  ->  ( 1st  |`  ( x ( Hom  `  T )
y ) )  e. 
_V )
3412, 32, 33mp2an 672 . . . . . 6  |-  ( 1st  |`  ( x ( Hom  `  T ) y ) )  e.  _V
3531, 34fnmpt2i 6648 . . . . 5  |-  ( x  e.  ( ( Base `  C )  X.  ( Base `  D ) ) ,  y  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  |->  ( 1st  |`  ( x
( Hom  `  T ) y ) ) )  Fn  ( ( (
Base `  C )  X.  ( Base `  D
) )  X.  (
( Base `  C )  X.  ( Base `  D
) ) )
3620fneq1d 5506 . . . . 5  |-  ( ph  ->  ( ( 2nd `  P
)  Fn  ( ( ( Base `  C
)  X.  ( Base `  D ) )  X.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  <-> 
( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) ,  y  e.  ( (
Base `  C )  X.  ( Base `  D
) )  |->  ( 1st  |`  ( x ( Hom  `  T ) y ) ) )  Fn  (
( ( Base `  C
)  X.  ( Base `  D ) )  X.  ( ( Base `  C
)  X.  ( Base `  D ) ) ) ) )
3735, 36mpbiri 233 . . . 4  |-  ( ph  ->  ( 2nd `  P
)  Fn  ( ( ( Base `  C
)  X.  ( Base `  D ) )  X.  ( ( Base `  C
)  X.  ( Base `  D ) ) ) )
38 f1stres 6603 . . . . . 6  |-  ( 1st  |`  ( ( ( 1st `  x ) ( Hom  `  C ) ( 1st `  y ) )  X.  ( ( 2nd `  x
) ( Hom  `  D
) ( 2nd `  y
) ) ) ) : ( ( ( 1st `  x ) ( Hom  `  C
) ( 1st `  y
) )  X.  (
( 2nd `  x
) ( Hom  `  D
) ( 2nd `  y
) ) ) --> ( ( 1st `  x
) ( Hom  `  C
) ( 1st `  y
) )
396adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) ) ) )  ->  C  e.  Cat )
407adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) ) ) )  ->  D  e.  Cat )
41 simprl 755 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) ) ) )  ->  x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )
42 simprr 756 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) ) ) )  ->  y  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )
431, 4, 5, 39, 40, 8, 41, 421stf2 15008 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) ) ) )  ->  ( x ( 2nd `  P ) y )  =  ( 1st  |`  ( x
( Hom  `  T ) y ) ) )
44 eqid 2443 . . . . . . . . . 10  |-  ( Hom  `  D )  =  ( Hom  `  D )
451, 4, 23, 44, 5, 41, 42xpchom 14995 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) ) ) )  ->  ( x ( Hom  `  T )
y )  =  ( ( ( 1st `  x
) ( Hom  `  C
) ( 1st `  y
) )  X.  (
( 2nd `  x
) ( Hom  `  D
) ( 2nd `  y
) ) ) )
4645reseq2d 5115 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) ) ) )  ->  ( 1st  |`  (
x ( Hom  `  T
) y ) )  =  ( 1st  |`  (
( ( 1st `  x
) ( Hom  `  C
) ( 1st `  y
) )  X.  (
( 2nd `  x
) ( Hom  `  D
) ( 2nd `  y
) ) ) ) )
4743, 46eqtrd 2475 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) ) ) )  ->  ( x ( 2nd `  P ) y )  =  ( 1st  |`  ( (
( 1st `  x
) ( Hom  `  C
) ( 1st `  y
) )  X.  (
( 2nd `  x
) ( Hom  `  D
) ( 2nd `  y
) ) ) ) )
4847feq1d 5551 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) ) ) )  ->  ( ( x ( 2nd `  P
) y ) : ( ( ( 1st `  x ) ( Hom  `  C ) ( 1st `  y ) )  X.  ( ( 2nd `  x
) ( Hom  `  D
) ( 2nd `  y
) ) ) --> ( ( 1st `  x
) ( Hom  `  C
) ( 1st `  y
) )  <->  ( 1st  |`  ( ( ( 1st `  x ) ( Hom  `  C ) ( 1st `  y ) )  X.  ( ( 2nd `  x
) ( Hom  `  D
) ( 2nd `  y
) ) ) ) : ( ( ( 1st `  x ) ( Hom  `  C
) ( 1st `  y
) )  X.  (
( 2nd `  x
) ( Hom  `  D
) ( 2nd `  y
) ) ) --> ( ( 1st `  x
) ( Hom  `  C
) ( 1st `  y
) ) ) )
4938, 48mpbiri 233 . . . . 5  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) ) ) )  ->  ( x ( 2nd `  P ) y ) : ( ( ( 1st `  x
) ( Hom  `  C
) ( 1st `  y
) )  X.  (
( 2nd `  x
) ( Hom  `  D
) ( 2nd `  y
) ) ) --> ( ( 1st `  x
) ( Hom  `  C
) ( 1st `  y
) ) )
50 fvres 5709 . . . . . . . 8  |-  ( x  e.  ( ( Base `  C )  X.  ( Base `  D ) )  ->  ( ( 1st  |`  ( ( Base `  C
)  X.  ( Base `  D ) ) ) `
 x )  =  ( 1st `  x
) )
5150ad2antrl 727 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) ) ) )  ->  ( ( 1st  |`  ( ( Base `  C
)  X.  ( Base `  D ) ) ) `
 x )  =  ( 1st `  x
) )
52 fvres 5709 . . . . . . . 8  |-  ( y  e.  ( ( Base `  C )  X.  ( Base `  D ) )  ->  ( ( 1st  |`  ( ( Base `  C
)  X.  ( Base `  D ) ) ) `
 y )  =  ( 1st `  y
) )
5352ad2antll 728 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) ) ) )  ->  ( ( 1st  |`  ( ( Base `  C
)  X.  ( Base `  D ) ) ) `
 y )  =  ( 1st `  y
) )
5451, 53oveq12d 6114 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) ) ) )  ->  ( ( ( 1st  |`  ( ( Base `  C )  X.  ( Base `  D
) ) ) `  x ) ( Hom  `  C ) ( ( 1st  |`  ( ( Base `  C )  X.  ( Base `  D
) ) ) `  y ) )  =  ( ( 1st `  x
) ( Hom  `  C
) ( 1st `  y
) ) )
5545, 54feq23d 5559 . . . . 5  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) ) ) )  ->  ( ( x ( 2nd `  P
) y ) : ( x ( Hom  `  T ) y ) --> ( ( ( 1st  |`  ( ( Base `  C
)  X.  ( Base `  D ) ) ) `
 x ) ( Hom  `  C )
( ( 1st  |`  (
( Base `  C )  X.  ( Base `  D
) ) ) `  y ) )  <->  ( x
( 2nd `  P
) y ) : ( ( ( 1st `  x ) ( Hom  `  C ) ( 1st `  y ) )  X.  ( ( 2nd `  x
) ( Hom  `  D
) ( 2nd `  y
) ) ) --> ( ( 1st `  x
) ( Hom  `  C
) ( 1st `  y
) ) ) )
5649, 55mpbird 232 . . . 4  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) ) ) )  ->  ( x ( 2nd `  P ) y ) : ( x ( Hom  `  T
) y ) --> ( ( ( 1st  |`  (
( Base `  C )  X.  ( Base `  D
) ) ) `  x ) ( Hom  `  C ) ( ( 1st  |`  ( ( Base `  C )  X.  ( Base `  D
) ) ) `  y ) ) )
5728adantr 465 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  ->  T  e.  Cat )
58 simpr 461 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  ->  x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )
594, 5, 24, 57, 58catidcl 14625 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  ->  ( ( Id
`  T ) `  x )  e.  ( x ( Hom  `  T
) x ) )
60 fvres 5709 . . . . . . 7  |-  ( ( ( Id `  T
) `  x )  e.  ( x ( Hom  `  T ) x )  ->  ( ( 1st  |`  ( x ( Hom  `  T ) x ) ) `  ( ( Id `  T ) `
 x ) )  =  ( 1st `  (
( Id `  T
) `  x )
) )
6159, 60syl 16 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  ->  ( ( 1st  |`  ( x ( Hom  `  T ) x ) ) `  ( ( Id `  T ) `
 x ) )  =  ( 1st `  (
( Id `  T
) `  x )
) )
62 1st2nd2 6618 . . . . . . . . . 10  |-  ( x  e.  ( ( Base `  C )  X.  ( Base `  D ) )  ->  x  =  <. ( 1st `  x ) ,  ( 2nd `  x
) >. )
6362adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  ->  x  =  <. ( 1st `  x ) ,  ( 2nd `  x
) >. )
6463fveq2d 5700 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  ->  ( ( Id
`  T ) `  x )  =  ( ( Id `  T
) `  <. ( 1st `  x ) ,  ( 2nd `  x )
>. ) )
656adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  ->  C  e.  Cat )
667adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  ->  D  e.  Cat )
67 eqid 2443 . . . . . . . . 9  |-  ( Id
`  D )  =  ( Id `  D
)
68 xp1st 6611 . . . . . . . . . 10  |-  ( x  e.  ( ( Base `  C )  X.  ( Base `  D ) )  ->  ( 1st `  x
)  e.  ( Base `  C ) )
6968adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  ->  ( 1st `  x
)  e.  ( Base `  C ) )
70 xp2nd 6612 . . . . . . . . . 10  |-  ( x  e.  ( ( Base `  C )  X.  ( Base `  D ) )  ->  ( 2nd `  x
)  e.  ( Base `  D ) )
7170adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  ->  ( 2nd `  x
)  e.  ( Base `  D ) )
721, 65, 66, 2, 3, 25, 67, 24, 69, 71xpcid 15004 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  ->  ( ( Id
`  T ) `  <. ( 1st `  x
) ,  ( 2nd `  x ) >. )  =  <. ( ( Id
`  C ) `  ( 1st `  x ) ) ,  ( ( Id `  D ) `
 ( 2nd `  x
) ) >. )
7364, 72eqtrd 2475 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  ->  ( ( Id
`  T ) `  x )  =  <. ( ( Id `  C
) `  ( 1st `  x ) ) ,  ( ( Id `  D ) `  ( 2nd `  x ) )
>. )
74 fvex 5706 . . . . . . . 8  |-  ( ( Id `  C ) `
 ( 1st `  x
) )  e.  _V
75 fvex 5706 . . . . . . . 8  |-  ( ( Id `  D ) `
 ( 2nd `  x
) )  e.  _V
7674, 75op1std 6592 . . . . . . 7  |-  ( ( ( Id `  T
) `  x )  =  <. ( ( Id
`  C ) `  ( 1st `  x ) ) ,  ( ( Id `  D ) `
 ( 2nd `  x
) ) >.  ->  ( 1st `  ( ( Id
`  T ) `  x ) )  =  ( ( Id `  C ) `  ( 1st `  x ) ) )
7773, 76syl 16 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  ->  ( 1st `  (
( Id `  T
) `  x )
)  =  ( ( Id `  C ) `
 ( 1st `  x
) ) )
7861, 77eqtrd 2475 . . . . 5  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  ->  ( ( 1st  |`  ( x ( Hom  `  T ) x ) ) `  ( ( Id `  T ) `
 x ) )  =  ( ( Id
`  C ) `  ( 1st `  x ) ) )
791, 4, 5, 65, 66, 8, 58, 581stf2 15008 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  ->  ( x ( 2nd `  P ) x )  =  ( 1st  |`  ( x
( Hom  `  T ) x ) ) )
8079fveq1d 5698 . . . . 5  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  ->  ( ( x ( 2nd `  P
) x ) `  ( ( Id `  T ) `  x
) )  =  ( ( 1st  |`  (
x ( Hom  `  T
) x ) ) `
 ( ( Id
`  T ) `  x ) ) )
8150adantl 466 . . . . . 6  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  ->  ( ( 1st  |`  ( ( Base `  C
)  X.  ( Base `  D ) ) ) `
 x )  =  ( 1st `  x
) )
8281fveq2d 5700 . . . . 5  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  ->  ( ( Id
`  C ) `  ( ( 1st  |`  (
( Base `  C )  X.  ( Base `  D
) ) ) `  x ) )  =  ( ( Id `  C ) `  ( 1st `  x ) ) )
8378, 80, 823eqtr4d 2485 . . . 4  |-  ( (
ph  /\  x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  ->  ( ( x ( 2nd `  P
) x ) `  ( ( Id `  T ) `  x
) )  =  ( ( Id `  C
) `  ( ( 1st  |`  ( ( Base `  C )  X.  ( Base `  D ) ) ) `  x ) ) )
84283ad2ant1 1009 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  T  e.  Cat )
85 simp21 1021 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  x  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )
86 simp22 1022 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  y  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )
87 simp23 1023 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )
88 simp3l 1016 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  f  e.  ( x ( Hom  `  T ) y ) )
89 simp3r 1017 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  g  e.  ( y ( Hom  `  T ) z ) )
904, 5, 26, 84, 85, 86, 87, 88, 89catcocl 14628 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  ( g
( <. x ,  y
>. (comp `  T )
z ) f )  e.  ( x ( Hom  `  T )
z ) )
91 fvres 5709 . . . . . . 7  |-  ( ( g ( <. x ,  y >. (comp `  T ) z ) f )  e.  ( x ( Hom  `  T
) z )  -> 
( ( 1st  |`  (
x ( Hom  `  T
) z ) ) `
 ( g (
<. x ,  y >.
(comp `  T )
z ) f ) )  =  ( 1st `  ( g ( <.
x ,  y >.
(comp `  T )
z ) f ) ) )
9290, 91syl 16 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  ( ( 1st  |`  ( x ( Hom  `  T )
z ) ) `  ( g ( <.
x ,  y >.
(comp `  T )
z ) f ) )  =  ( 1st `  ( g ( <.
x ,  y >.
(comp `  T )
z ) f ) ) )
931, 4, 5, 26, 85, 86, 87, 88, 89, 27xpcco1st 14999 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  ( 1st `  ( g ( <.
x ,  y >.
(comp `  T )
z ) f ) )  =  ( ( 1st `  g ) ( <. ( 1st `  x
) ,  ( 1st `  y ) >. (comp `  C ) ( 1st `  z ) ) ( 1st `  f ) ) )
9492, 93eqtrd 2475 . . . . 5  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  ( ( 1st  |`  ( x ( Hom  `  T )
z ) ) `  ( g ( <.
x ,  y >.
(comp `  T )
z ) f ) )  =  ( ( 1st `  g ) ( <. ( 1st `  x
) ,  ( 1st `  y ) >. (comp `  C ) ( 1st `  z ) ) ( 1st `  f ) ) )
9563ad2ant1 1009 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  C  e.  Cat )
9673ad2ant1 1009 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  D  e.  Cat )
971, 4, 5, 95, 96, 8, 85, 871stf2 15008 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  ( x
( 2nd `  P
) z )  =  ( 1st  |`  (
x ( Hom  `  T
) z ) ) )
9897fveq1d 5698 . . . . 5  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  ( (
x ( 2nd `  P
) z ) `  ( g ( <.
x ,  y >.
(comp `  T )
z ) f ) )  =  ( ( 1st  |`  ( x
( Hom  `  T ) z ) ) `  ( g ( <.
x ,  y >.
(comp `  T )
z ) f ) ) )
9985, 50syl 16 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  ( ( 1st  |`  ( ( Base `  C )  X.  ( Base `  D ) ) ) `  x )  =  ( 1st `  x
) )
10086, 52syl 16 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  ( ( 1st  |`  ( ( Base `  C )  X.  ( Base `  D ) ) ) `  y )  =  ( 1st `  y
) )
10199, 100opeq12d 4072 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  <. ( ( 1st  |`  ( ( Base `  C )  X.  ( Base `  D
) ) ) `  x ) ,  ( ( 1st  |`  (
( Base `  C )  X.  ( Base `  D
) ) ) `  y ) >.  =  <. ( 1st `  x ) ,  ( 1st `  y
) >. )
102 fvres 5709 . . . . . . . 8  |-  ( z  e.  ( ( Base `  C )  X.  ( Base `  D ) )  ->  ( ( 1st  |`  ( ( Base `  C
)  X.  ( Base `  D ) ) ) `
 z )  =  ( 1st `  z
) )
10387, 102syl 16 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  ( ( 1st  |`  ( ( Base `  C )  X.  ( Base `  D ) ) ) `  z )  =  ( 1st `  z
) )
104101, 103oveq12d 6114 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  ( <. ( ( 1st  |`  (
( Base `  C )  X.  ( Base `  D
) ) ) `  x ) ,  ( ( 1st  |`  (
( Base `  C )  X.  ( Base `  D
) ) ) `  y ) >. (comp `  C ) ( ( 1st  |`  ( ( Base `  C )  X.  ( Base `  D
) ) ) `  z ) )  =  ( <. ( 1st `  x
) ,  ( 1st `  y ) >. (comp `  C ) ( 1st `  z ) ) )
1051, 4, 5, 95, 96, 8, 86, 871stf2 15008 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  ( y
( 2nd `  P
) z )  =  ( 1st  |`  (
y ( Hom  `  T
) z ) ) )
106105fveq1d 5698 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  ( (
y ( 2nd `  P
) z ) `  g )  =  ( ( 1st  |`  (
y ( Hom  `  T
) z ) ) `
 g ) )
107 fvres 5709 . . . . . . . 8  |-  ( g  e.  ( y ( Hom  `  T )
z )  ->  (
( 1st  |`  ( y ( Hom  `  T
) z ) ) `
 g )  =  ( 1st `  g
) )
10889, 107syl 16 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  ( ( 1st  |`  ( y ( Hom  `  T )
z ) ) `  g )  =  ( 1st `  g ) )
109106, 108eqtrd 2475 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  ( (
y ( 2nd `  P
) z ) `  g )  =  ( 1st `  g ) )
1101, 4, 5, 95, 96, 8, 85, 861stf2 15008 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  ( x
( 2nd `  P
) y )  =  ( 1st  |`  (
x ( Hom  `  T
) y ) ) )
111110fveq1d 5698 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  ( (
x ( 2nd `  P
) y ) `  f )  =  ( ( 1st  |`  (
x ( Hom  `  T
) y ) ) `
 f ) )
112 fvres 5709 . . . . . . . 8  |-  ( f  e.  ( x ( Hom  `  T )
y )  ->  (
( 1st  |`  ( x ( Hom  `  T
) y ) ) `
 f )  =  ( 1st `  f
) )
11388, 112syl 16 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  ( ( 1st  |`  ( x ( Hom  `  T )
y ) ) `  f )  =  ( 1st `  f ) )
114111, 113eqtrd 2475 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  ( (
x ( 2nd `  P
) y ) `  f )  =  ( 1st `  f ) )
115104, 109, 114oveq123d 6117 . . . . 5  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  ( (
( y ( 2nd `  P ) z ) `
 g ) (
<. ( ( 1st  |`  (
( Base `  C )  X.  ( Base `  D
) ) ) `  x ) ,  ( ( 1st  |`  (
( Base `  C )  X.  ( Base `  D
) ) ) `  y ) >. (comp `  C ) ( ( 1st  |`  ( ( Base `  C )  X.  ( Base `  D
) ) ) `  z ) ) ( ( x ( 2nd `  P ) y ) `
 f ) )  =  ( ( 1st `  g ) ( <.
( 1st `  x
) ,  ( 1st `  y ) >. (comp `  C ) ( 1st `  z ) ) ( 1st `  f ) ) )
11694, 98, 1153eqtr4d 2485 . . . 4  |-  ( (
ph  /\  ( x  e.  ( ( Base `  C
)  X.  ( Base `  D ) )  /\  y  e.  ( ( Base `  C )  X.  ( Base `  D
) )  /\  z  e.  ( ( Base `  C
)  X.  ( Base `  D ) ) )  /\  ( f  e.  ( x ( Hom  `  T ) y )  /\  g  e.  ( y ( Hom  `  T
) z ) ) )  ->  ( (
x ( 2nd `  P
) z ) `  ( g ( <.
x ,  y >.
(comp `  T )
z ) f ) )  =  ( ( ( y ( 2nd `  P ) z ) `
 g ) (
<. ( ( 1st  |`  (
( Base `  C )  X.  ( Base `  D
) ) ) `  x ) ,  ( ( 1st  |`  (
( Base `  C )  X.  ( Base `  D
) ) ) `  y ) >. (comp `  C ) ( ( 1st  |`  ( ( Base `  C )  X.  ( Base `  D
) ) ) `  z ) ) ( ( x ( 2nd `  P ) y ) `
 f ) ) )
1174, 2, 5, 23, 24, 25, 26, 27, 28, 6, 30, 37, 56, 83, 116isfuncd 14780 . . 3  |-  ( ph  ->  ( 1st  |`  (
( Base `  C )  X.  ( Base `  D
) ) ) ( T  Func  C )
( 2nd `  P
) )
118 df-br 4298 . . 3  |-  ( ( 1st  |`  ( ( Base `  C )  X.  ( Base `  D
) ) ) ( T  Func  C )
( 2nd `  P
)  <->  <. ( 1st  |`  (
( Base `  C )  X.  ( Base `  D
) ) ) ,  ( 2nd `  P
) >.  e.  ( T 
Func  C ) )
119117, 118sylib 196 . 2  |-  ( ph  -> 
<. ( 1st  |`  (
( Base `  C )  X.  ( Base `  D
) ) ) ,  ( 2nd `  P
) >.  e.  ( T 
Func  C ) )
12022, 119eqeltrd 2517 1  |-  ( ph  ->  P  e.  ( T 
Func  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756   _Vcvv 2977   <.cop 3888   class class class wbr 4297    X. cxp 4843    |` cres 4847   Fun wfun 5417    Fn wfn 5418   -->wf 5419   -onto->wfo 5421   ` cfv 5423  (class class class)co 6096    e. cmpt2 6098   1stc1st 6580   2ndc2nd 6581   Basecbs 14179   Hom chom 14254  compcco 14255   Catccat 14607   Idccid 14608    Func cfunc 14769    X.c cxpc 14983    1stF c1stf 14984
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4408  ax-sep 4418  ax-nul 4426  ax-pow 4475  ax-pr 4536  ax-un 6377  ax-cnex 9343  ax-resscn 9344  ax-1cn 9345  ax-icn 9346  ax-addcl 9347  ax-addrcl 9348  ax-mulcl 9349  ax-mulrcl 9350  ax-mulcom 9351  ax-addass 9352  ax-mulass 9353  ax-distr 9354  ax-i2m1 9355  ax-1ne0 9356  ax-1rid 9357  ax-rnegex 9358  ax-rrecex 9359  ax-cnre 9360  ax-pre-lttri 9361  ax-pre-lttrn 9362  ax-pre-ltadd 9363  ax-pre-mulgt0 9364
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-nel 2614  df-ral 2725  df-rex 2726  df-reu 2727  df-rmo 2728  df-rab 2729  df-v 2979  df-sbc 3192  df-csb 3294  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-pss 3349  df-nul 3643  df-if 3797  df-pw 3867  df-sn 3883  df-pr 3885  df-tp 3887  df-op 3889  df-uni 4097  df-int 4134  df-iun 4178  df-br 4298  df-opab 4356  df-mpt 4357  df-tr 4391  df-eprel 4637  df-id 4641  df-po 4646  df-so 4647  df-fr 4684  df-we 4686  df-ord 4727  df-on 4728  df-lim 4729  df-suc 4730  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5386  df-fun 5425  df-fn 5426  df-f 5427  df-f1 5428  df-fo 5429  df-f1o 5430  df-fv 5431  df-riota 6057  df-ov 6099  df-oprab 6100  df-mpt2 6101  df-om 6482  df-1st 6582  df-2nd 6583  df-recs 6837  df-rdg 6871  df-1o 6925  df-oadd 6929  df-er 7106  df-map 7221  df-ixp 7269  df-en 7316  df-dom 7317  df-sdom 7318  df-fin 7319  df-pnf 9425  df-mnf 9426  df-xr 9427  df-ltxr 9428  df-le 9429  df-sub 9602  df-neg 9603  df-nn 10328  df-2 10385  df-3 10386  df-4 10387  df-5 10388  df-6 10389  df-7 10390  df-8 10391  df-9 10392  df-10 10393  df-n0 10585  df-z 10652  df-dec 10761  df-uz 10867  df-fz 11443  df-struct 14181  df-ndx 14182  df-slot 14183  df-base 14184  df-hom 14267  df-cco 14268  df-cat 14611  df-cid 14612  df-func 14773  df-xpc 14987  df-1stf 14988
This theorem is referenced by:  prf1st  15019  1st2ndprf  15021  uncfcl  15050  uncf1  15051  uncf2  15052  diagcl  15056  diag11  15058  diag12  15059  diag2  15060  yonedalem1  15087  yonedalem21  15088  yonedalem22  15093
  Copyright terms: Public domain W3C validator