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

Theorem catcisolem 14254
Description: Lemma for catciso 14255. (Contributed by Mario Carneiro, 29-Jan-2017.)
Hypotheses
Ref Expression
catciso.c  |-  C  =  (CatCat `  U )
catciso.b  |-  B  =  ( Base `  C
)
catciso.r  |-  R  =  ( Base `  X
)
catciso.s  |-  S  =  ( Base `  Y
)
catciso.u  |-  ( ph  ->  U  e.  V )
catciso.x  |-  ( ph  ->  X  e.  B )
catciso.y  |-  ( ph  ->  Y  e.  B )
catcisolem.i  |-  I  =  (Inv `  C )
catcisolem.g  |-  H  =  ( x  e.  S ,  y  e.  S  |->  `' ( ( `' F `  x ) G ( `' F `  y ) ) )
catcisolem.1  |-  ( ph  ->  F ( ( X Full 
Y )  i^i  ( X Faith  Y ) ) G )
catcisolem.2  |-  ( ph  ->  F : R -1-1-onto-> S )
Assertion
Ref Expression
catcisolem  |-  ( ph  -> 
<. F ,  G >. ( X I Y )
<. `' F ,  H >. )
Distinct variable groups:    x, y, C    x, F, y    x, G, y    ph, x, y   
x, I, y    x, R, y    x, S, y   
x, X, y    x, Y, y
Allowed substitution hints:    B( x, y)    U( x, y)    H( x, y)    V( x, y)

Proof of Theorem catcisolem
Dummy variables  f 
g  u  v  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 catcisolem.2 . . . . . . 7  |-  ( ph  ->  F : R -1-1-onto-> S )
2 f1ococnv1 5697 . . . . . . 7  |-  ( F : R -1-1-onto-> S  ->  ( `' F  o.  F )  =  (  _I  |`  R ) )
31, 2syl 16 . . . . . 6  |-  ( ph  ->  ( `' F  o.  F )  =  (  _I  |`  R )
)
413ad2ant1 978 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  F : R
-1-1-onto-> S )
5 f1of 5667 . . . . . . . . . . . . . 14  |-  ( F : R -1-1-onto-> S  ->  F : R
--> S )
64, 5syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  F : R
--> S )
7 simp2 958 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  u  e.  R )
86, 7ffvelrnd 5864 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( F `  u )  e.  S
)
9 simp3 959 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  v  e.  R )
106, 9ffvelrnd 5864 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( F `  v )  e.  S
)
11 simpl 444 . . . . . . . . . . . . . . . 16  |-  ( ( x  =  ( F `
 u )  /\  y  =  ( F `  v ) )  ->  x  =  ( F `  u ) )
1211fveq2d 5725 . . . . . . . . . . . . . . 15  |-  ( ( x  =  ( F `
 u )  /\  y  =  ( F `  v ) )  -> 
( `' F `  x )  =  ( `' F `  ( F `
 u ) ) )
13 simpr 448 . . . . . . . . . . . . . . . 16  |-  ( ( x  =  ( F `
 u )  /\  y  =  ( F `  v ) )  -> 
y  =  ( F `
 v ) )
1413fveq2d 5725 . . . . . . . . . . . . . . 15  |-  ( ( x  =  ( F `
 u )  /\  y  =  ( F `  v ) )  -> 
( `' F `  y )  =  ( `' F `  ( F `
 v ) ) )
1512, 14oveq12d 6092 . . . . . . . . . . . . . 14  |-  ( ( x  =  ( F `
 u )  /\  y  =  ( F `  v ) )  -> 
( ( `' F `  x ) G ( `' F `  y ) )  =  ( ( `' F `  ( F `
 u ) ) G ( `' F `  ( F `  v
) ) ) )
1615cnveqd 5041 . . . . . . . . . . . . 13  |-  ( ( x  =  ( F `
 u )  /\  y  =  ( F `  v ) )  ->  `' ( ( `' F `  x ) G ( `' F `  y ) )  =  `' ( ( `' F `  ( F `
 u ) ) G ( `' F `  ( F `  v
) ) ) )
17 catcisolem.g . . . . . . . . . . . . 13  |-  H  =  ( x  e.  S ,  y  e.  S  |->  `' ( ( `' F `  x ) G ( `' F `  y ) ) )
18 ovex 6099 . . . . . . . . . . . . . 14  |-  ( ( `' F `  ( F `
 u ) ) G ( `' F `  ( F `  v
) ) )  e. 
_V
1918cnvex 5399 . . . . . . . . . . . . 13  |-  `' ( ( `' F `  ( F `  u ) ) G ( `' F `  ( F `
 v ) ) )  e.  _V
2016, 17, 19ovmpt2a 6197 . . . . . . . . . . . 12  |-  ( ( ( F `  u
)  e.  S  /\  ( F `  v )  e.  S )  -> 
( ( F `  u ) H ( F `  v ) )  =  `' ( ( `' F `  ( F `  u ) ) G ( `' F `  ( F `
 v ) ) ) )
218, 10, 20syl2anc 643 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( ( F `  u ) H ( F `  v ) )  =  `' ( ( `' F `  ( F `
 u ) ) G ( `' F `  ( F `  v
) ) ) )
22 f1ocnvfv1 6007 . . . . . . . . . . . . . 14  |-  ( ( F : R -1-1-onto-> S  /\  u  e.  R )  ->  ( `' F `  ( F `  u ) )  =  u )
234, 7, 22syl2anc 643 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( `' F `  ( F `  u ) )  =  u )
24 f1ocnvfv1 6007 . . . . . . . . . . . . . 14  |-  ( ( F : R -1-1-onto-> S  /\  v  e.  R )  ->  ( `' F `  ( F `  v ) )  =  v )
254, 9, 24syl2anc 643 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( `' F `  ( F `  v ) )  =  v )
2623, 25oveq12d 6092 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( ( `' F `  ( F `
 u ) ) G ( `' F `  ( F `  v
) ) )  =  ( u G v ) )
2726cnveqd 5041 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  `' (
( `' F `  ( F `  u ) ) G ( `' F `  ( F `
 v ) ) )  =  `' ( u G v ) )
2821, 27eqtrd 2468 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( ( F `  u ) H ( F `  v ) )  =  `' ( u G v ) )
2928coeq1d 5027 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( (
( F `  u
) H ( F `
 v ) )  o.  ( u G v ) )  =  ( `' ( u G v )  o.  ( u G v ) ) )
30 catciso.r . . . . . . . . . . 11  |-  R  =  ( Base `  X
)
31 eqid 2436 . . . . . . . . . . 11  |-  (  Hom  `  X )  =  (  Hom  `  X )
32 eqid 2436 . . . . . . . . . . 11  |-  (  Hom  `  Y )  =  (  Hom  `  Y )
33 catcisolem.1 . . . . . . . . . . . 12  |-  ( ph  ->  F ( ( X Full 
Y )  i^i  ( X Faith  Y ) ) G )
34333ad2ant1 978 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  F (
( X Full  Y )  i^i  ( X Faith  Y ) ) G )
3530, 31, 32, 34, 7, 9ffthf1o 14109 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( u G v ) : ( u (  Hom  `  X ) v ) -1-1-onto-> ( ( F `  u
) (  Hom  `  Y
) ( F `  v ) ) )
36 f1ococnv1 5697 . . . . . . . . . 10  |-  ( ( u G v ) : ( u (  Hom  `  X )
v ) -1-1-onto-> ( ( F `  u ) (  Hom  `  Y ) ( F `
 v ) )  ->  ( `' ( u G v )  o.  ( u G v ) )  =  (  _I  |`  (
u (  Hom  `  X
) v ) ) )
3735, 36syl 16 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( `' ( u G v )  o.  ( u G v ) )  =  (  _I  |`  (
u (  Hom  `  X
) v ) ) )
3829, 37eqtrd 2468 . . . . . . . 8  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( (
( F `  u
) H ( F `
 v ) )  o.  ( u G v ) )  =  (  _I  |`  (
u (  Hom  `  X
) v ) ) )
3938mpt2eq3dva 6131 . . . . . . 7  |-  ( ph  ->  ( u  e.  R ,  v  e.  R  |->  ( ( ( F `
 u ) H ( F `  v
) )  o.  (
u G v ) ) )  =  ( u  e.  R , 
v  e.  R  |->  (  _I  |`  ( u
(  Hom  `  X ) v ) ) ) )
40 fveq2 5721 . . . . . . . . . 10  |-  ( z  =  <. u ,  v
>.  ->  ( (  Hom  `  X ) `  z
)  =  ( (  Hom  `  X ) `  <. u ,  v
>. ) )
41 df-ov 6077 . . . . . . . . . 10  |-  ( u (  Hom  `  X
) v )  =  ( (  Hom  `  X
) `  <. u ,  v >. )
4240, 41syl6eqr 2486 . . . . . . . . 9  |-  ( z  =  <. u ,  v
>.  ->  ( (  Hom  `  X ) `  z
)  =  ( u (  Hom  `  X
) v ) )
4342reseq2d 5139 . . . . . . . 8  |-  ( z  =  <. u ,  v
>.  ->  (  _I  |`  (
(  Hom  `  X ) `
 z ) )  =  (  _I  |`  (
u (  Hom  `  X
) v ) ) )
4443mpt2mpt 6158 . . . . . . 7  |-  ( z  e.  ( R  X.  R )  |->  (  _I  |`  ( (  Hom  `  X
) `  z )
) )  =  ( u  e.  R , 
v  e.  R  |->  (  _I  |`  ( u
(  Hom  `  X ) v ) ) )
4539, 44syl6eqr 2486 . . . . . 6  |-  ( ph  ->  ( u  e.  R ,  v  e.  R  |->  ( ( ( F `
 u ) H ( F `  v
) )  o.  (
u G v ) ) )  =  ( z  e.  ( R  X.  R )  |->  (  _I  |`  ( (  Hom  `  X ) `  z ) ) ) )
463, 45opeq12d 3985 . . . . 5  |-  ( ph  -> 
<. ( `' F  o.  F ) ,  ( u  e.  R , 
v  e.  R  |->  ( ( ( F `  u ) H ( F `  v ) )  o.  ( u G v ) ) ) >.  =  <. (  _I  |`  R ) ,  ( z  e.  ( R  X.  R
)  |->  (  _I  |`  (
(  Hom  `  X ) `
 z ) ) ) >. )
47 inss1 3554 . . . . . . . . 9  |-  ( ( X Full  Y )  i^i  ( X Faith  Y ) )  C_  ( X Full  Y )
48 fullfunc 14096 . . . . . . . . 9  |-  ( X Full 
Y )  C_  ( X  Func  Y )
4947, 48sstri 3350 . . . . . . . 8  |-  ( ( X Full  Y )  i^i  ( X Faith  Y ) )  C_  ( X  Func  Y )
5049ssbri 4247 . . . . . . 7  |-  ( F ( ( X Full  Y
)  i^i  ( X Faith  Y ) ) G  ->  F ( X  Func  Y ) G )
5133, 50syl 16 . . . . . 6  |-  ( ph  ->  F ( X  Func  Y ) G )
52 catciso.s . . . . . . 7  |-  S  =  ( Base `  Y
)
53 eqid 2436 . . . . . . 7  |-  ( Id
`  Y )  =  ( Id `  Y
)
54 eqid 2436 . . . . . . 7  |-  ( Id
`  X )  =  ( Id `  X
)
55 eqid 2436 . . . . . . 7  |-  (comp `  Y )  =  (comp `  Y )
56 eqid 2436 . . . . . . 7  |-  (comp `  X )  =  (comp `  X )
57 catciso.c . . . . . . . . . 10  |-  C  =  (CatCat `  U )
58 catciso.b . . . . . . . . . 10  |-  B  =  ( Base `  C
)
59 catciso.u . . . . . . . . . 10  |-  ( ph  ->  U  e.  V )
6057, 58, 59catcbas 14245 . . . . . . . . 9  |-  ( ph  ->  B  =  ( U  i^i  Cat ) )
61 inss2 3555 . . . . . . . . 9  |-  ( U  i^i  Cat )  C_  Cat
6260, 61syl6eqss 3391 . . . . . . . 8  |-  ( ph  ->  B  C_  Cat )
63 catciso.y . . . . . . . 8  |-  ( ph  ->  Y  e.  B )
6462, 63sseldd 3342 . . . . . . 7  |-  ( ph  ->  Y  e.  Cat )
65 catciso.x . . . . . . . 8  |-  ( ph  ->  X  e.  B )
6662, 65sseldd 3342 . . . . . . 7  |-  ( ph  ->  X  e.  Cat )
67 f1ocnv 5680 . . . . . . . 8  |-  ( F : R -1-1-onto-> S  ->  `' F : S -1-1-onto-> R )
68 f1of 5667 . . . . . . . 8  |-  ( `' F : S -1-1-onto-> R  ->  `' F : S --> R )
691, 67, 683syl 19 . . . . . . 7  |-  ( ph  ->  `' F : S --> R )
70 ovex 6099 . . . . . . . . . 10  |-  ( ( `' F `  x ) G ( `' F `  y ) )  e. 
_V
7170cnvex 5399 . . . . . . . . 9  |-  `' ( ( `' F `  x ) G ( `' F `  y ) )  e.  _V
7217, 71fnmpt2i 6413 . . . . . . . 8  |-  H  Fn  ( S  X.  S
)
7372a1i 11 . . . . . . 7  |-  ( ph  ->  H  Fn  ( S  X.  S ) )
7433adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  ->  F ( ( X Full 
Y )  i^i  ( X Faith  Y ) ) G )
7569ffvelrnda 5863 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  S )  ->  ( `' F `  u )  e.  R )
7675adantrr 698 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( `' F `  u )  e.  R
)
7769ffvelrnda 5863 . . . . . . . . . . 11  |-  ( (
ph  /\  v  e.  S )  ->  ( `' F `  v )  e.  R )
7877adantrl 697 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( `' F `  v )  e.  R
)
7930, 31, 32, 74, 76, 78ffthf1o 14109 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( ( `' F `  u ) G ( `' F `  v ) ) : ( ( `' F `  u ) (  Hom  `  X
) ( `' F `  v ) ) -1-1-onto-> ( ( F `  ( `' F `  u ) ) (  Hom  `  Y
) ( F `  ( `' F `  v ) ) ) )
80 f1ocnv 5680 . . . . . . . . 9  |-  ( ( ( `' F `  u ) G ( `' F `  v ) ) : ( ( `' F `  u ) (  Hom  `  X
) ( `' F `  v ) ) -1-1-onto-> ( ( F `  ( `' F `  u ) ) (  Hom  `  Y
) ( F `  ( `' F `  v ) ) )  ->  `' ( ( `' F `  u ) G ( `' F `  v ) ) : ( ( F `  ( `' F `  u ) ) (  Hom  `  Y
) ( F `  ( `' F `  v ) ) ) -1-1-onto-> ( ( `' F `  u ) (  Hom  `  X ) ( `' F `  v ) ) )
81 f1of 5667 . . . . . . . . 9  |-  ( `' ( ( `' F `  u ) G ( `' F `  v ) ) : ( ( F `  ( `' F `  u ) ) (  Hom  `  Y
) ( F `  ( `' F `  v ) ) ) -1-1-onto-> ( ( `' F `  u ) (  Hom  `  X ) ( `' F `  v ) )  ->  `' (
( `' F `  u ) G ( `' F `  v ) ) : ( ( F `  ( `' F `  u ) ) (  Hom  `  Y
) ( F `  ( `' F `  v ) ) ) --> ( ( `' F `  u ) (  Hom  `  X
) ( `' F `  v ) ) )
8279, 80, 813syl 19 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  ->  `' ( ( `' F `  u ) G ( `' F `  v ) ) : ( ( F `  ( `' F `  u ) ) (  Hom  `  Y
) ( F `  ( `' F `  v ) ) ) --> ( ( `' F `  u ) (  Hom  `  X
) ( `' F `  v ) ) )
83 simpl 444 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  v )  ->  x  =  u )
8483fveq2d 5725 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  v )  ->  ( `' F `  x )  =  ( `' F `  u ) )
85 simpr 448 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  v )  ->  y  =  v )
8685fveq2d 5725 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  v )  ->  ( `' F `  y )  =  ( `' F `  v ) )
8784, 86oveq12d 6092 . . . . . . . . . . . 12  |-  ( ( x  =  u  /\  y  =  v )  ->  ( ( `' F `  x ) G ( `' F `  y ) )  =  ( ( `' F `  u ) G ( `' F `  v ) ) )
8887cnveqd 5041 . . . . . . . . . . 11  |-  ( ( x  =  u  /\  y  =  v )  ->  `' ( ( `' F `  x ) G ( `' F `  y ) )  =  `' ( ( `' F `  u ) G ( `' F `  v ) ) )
89 ovex 6099 . . . . . . . . . . . 12  |-  ( ( `' F `  u ) G ( `' F `  v ) )  e. 
_V
9089cnvex 5399 . . . . . . . . . . 11  |-  `' ( ( `' F `  u ) G ( `' F `  v ) )  e.  _V
9188, 17, 90ovmpt2a 6197 . . . . . . . . . 10  |-  ( ( u  e.  S  /\  v  e.  S )  ->  ( u H v )  =  `' ( ( `' F `  u ) G ( `' F `  v ) ) )
9291adantl 453 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( u H v )  =  `' ( ( `' F `  u ) G ( `' F `  v ) ) )
931adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  ->  F : R -1-1-onto-> S )
94 simprl 733 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  ->  u  e.  S )
95 f1ocnvfv2 6008 . . . . . . . . . . . 12  |-  ( ( F : R -1-1-onto-> S  /\  u  e.  S )  ->  ( F `  ( `' F `  u ) )  =  u )
9693, 94, 95syl2anc 643 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( F `  ( `' F `  u ) )  =  u )
97 simprr 734 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
v  e.  S )
98 f1ocnvfv2 6008 . . . . . . . . . . . 12  |-  ( ( F : R -1-1-onto-> S  /\  v  e.  S )  ->  ( F `  ( `' F `  v ) )  =  v )
9993, 97, 98syl2anc 643 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( F `  ( `' F `  v ) )  =  v )
10096, 99oveq12d 6092 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( ( F `  ( `' F `  u ) ) (  Hom  `  Y
) ( F `  ( `' F `  v ) ) )  =  ( u (  Hom  `  Y
) v ) )
101100eqcomd 2441 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( u (  Hom  `  Y ) v )  =  ( ( F `
 ( `' F `  u ) ) (  Hom  `  Y )
( F `  ( `' F `  v ) ) ) )
10292, 101feq12d 5575 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( ( u H v ) : ( u (  Hom  `  Y
) v ) --> ( ( `' F `  u ) (  Hom  `  X ) ( `' F `  v ) )  <->  `' ( ( `' F `  u ) G ( `' F `  v ) ) : ( ( F `  ( `' F `  u ) ) (  Hom  `  Y
) ( F `  ( `' F `  v ) ) ) --> ( ( `' F `  u ) (  Hom  `  X
) ( `' F `  v ) ) ) )
10382, 102mpbird 224 . . . . . . 7  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( u H v ) : ( u (  Hom  `  Y
) v ) --> ( ( `' F `  u ) (  Hom  `  X ) ( `' F `  v ) ) )
104 simpr 448 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  S )  ->  u  e.  S )
105 simpl 444 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  u )  ->  x  =  u )
106105fveq2d 5725 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  u )  ->  ( `' F `  x )  =  ( `' F `  u ) )
107 simpr 448 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  u )  ->  y  =  u )
108107fveq2d 5725 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  u )  ->  ( `' F `  y )  =  ( `' F `  u ) )
109106, 108oveq12d 6092 . . . . . . . . . . . 12  |-  ( ( x  =  u  /\  y  =  u )  ->  ( ( `' F `  x ) G ( `' F `  y ) )  =  ( ( `' F `  u ) G ( `' F `  u ) ) )
110109cnveqd 5041 . . . . . . . . . . 11  |-  ( ( x  =  u  /\  y  =  u )  ->  `' ( ( `' F `  x ) G ( `' F `  y ) )  =  `' ( ( `' F `  u ) G ( `' F `  u ) ) )
111 ovex 6099 . . . . . . . . . . . 12  |-  ( ( `' F `  u ) G ( `' F `  u ) )  e. 
_V
112111cnvex 5399 . . . . . . . . . . 11  |-  `' ( ( `' F `  u ) G ( `' F `  u ) )  e.  _V
113110, 17, 112ovmpt2a 6197 . . . . . . . . . 10  |-  ( ( u  e.  S  /\  u  e.  S )  ->  ( u H u )  =  `' ( ( `' F `  u ) G ( `' F `  u ) ) )
114104, 104, 113syl2anc 643 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  S )  ->  (
u H u )  =  `' ( ( `' F `  u ) G ( `' F `  u ) ) )
115114fveq1d 5723 . . . . . . . 8  |-  ( (
ph  /\  u  e.  S )  ->  (
( u H u ) `  ( ( Id `  Y ) `
 u ) )  =  ( `' ( ( `' F `  u ) G ( `' F `  u ) ) `  ( ( Id `  Y ) `
 u ) ) )
11651adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  S )  ->  F
( X  Func  Y
) G )
11730, 54, 53, 116, 75funcid 14060 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  S )  ->  (
( ( `' F `  u ) G ( `' F `  u ) ) `  ( ( Id `  X ) `
 ( `' F `  u ) ) )  =  ( ( Id
`  Y ) `  ( F `  ( `' F `  u ) ) ) )
1181, 95sylan 458 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  S )  ->  ( F `  ( `' F `  u )
)  =  u )
119118fveq2d 5725 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  S )  ->  (
( Id `  Y
) `  ( F `  ( `' F `  u ) ) )  =  ( ( Id
`  Y ) `  u ) )
120117, 119eqtrd 2468 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  S )  ->  (
( ( `' F `  u ) G ( `' F `  u ) ) `  ( ( Id `  X ) `
 ( `' F `  u ) ) )  =  ( ( Id
`  Y ) `  u ) )
12133adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  S )  ->  F
( ( X Full  Y
)  i^i  ( X Faith  Y ) ) G )
12230, 31, 32, 121, 75, 75ffthf1o 14109 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  S )  ->  (
( `' F `  u ) G ( `' F `  u ) ) : ( ( `' F `  u ) (  Hom  `  X
) ( `' F `  u ) ) -1-1-onto-> ( ( F `  ( `' F `  u ) ) (  Hom  `  Y
) ( F `  ( `' F `  u ) ) ) )
12366adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  S )  ->  X  e.  Cat )
12430, 31, 54, 123, 75catidcl 13900 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  S )  ->  (
( Id `  X
) `  ( `' F `  u )
)  e.  ( ( `' F `  u ) (  Hom  `  X
) ( `' F `  u ) ) )
125 f1ocnvfv 6009 . . . . . . . . . 10  |-  ( ( ( ( `' F `  u ) G ( `' F `  u ) ) : ( ( `' F `  u ) (  Hom  `  X
) ( `' F `  u ) ) -1-1-onto-> ( ( F `  ( `' F `  u ) ) (  Hom  `  Y
) ( F `  ( `' F `  u ) ) )  /\  (
( Id `  X
) `  ( `' F `  u )
)  e.  ( ( `' F `  u ) (  Hom  `  X
) ( `' F `  u ) ) )  ->  ( ( ( ( `' F `  u ) G ( `' F `  u ) ) `  ( ( Id `  X ) `
 ( `' F `  u ) ) )  =  ( ( Id
`  Y ) `  u )  ->  ( `' ( ( `' F `  u ) G ( `' F `  u ) ) `  ( ( Id `  Y ) `  u
) )  =  ( ( Id `  X
) `  ( `' F `  u )
) ) )
126122, 124, 125syl2anc 643 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  S )  ->  (
( ( ( `' F `  u ) G ( `' F `  u ) ) `  ( ( Id `  X ) `  ( `' F `  u ) ) )  =  ( ( Id `  Y
) `  u )  ->  ( `' ( ( `' F `  u ) G ( `' F `  u ) ) `  ( ( Id `  Y ) `  u
) )  =  ( ( Id `  X
) `  ( `' F `  u )
) ) )
127120, 126mpd 15 . . . . . . . 8  |-  ( (
ph  /\  u  e.  S )  ->  ( `' ( ( `' F `  u ) G ( `' F `  u ) ) `  ( ( Id `  Y ) `  u
) )  =  ( ( Id `  X
) `  ( `' F `  u )
) )
128115, 127eqtrd 2468 . . . . . . 7  |-  ( (
ph  /\  u  e.  S )  ->  (
( u H u ) `  ( ( Id `  Y ) `
 u ) )  =  ( ( Id
`  X ) `  ( `' F `  u ) ) )
129513ad2ant1 978 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  F ( X 
Func  Y ) G )
130693ad2ant1 978 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  `' F : S
--> R )
131 simp21 990 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  u  e.  S
)
132130, 131ffvelrnd 5864 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( `' F `  u )  e.  R
)
133 simp22 991 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  v  e.  S
)
134130, 133ffvelrnd 5864 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( `' F `  v )  e.  R
)
135 simp23 992 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  z  e.  S
)
136130, 135ffvelrnd 5864 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( `' F `  z )  e.  R
)
137333ad2ant1 978 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  F ( ( X Full  Y )  i^i  ( X Faith  Y ) ) G )
13830, 31, 32, 137, 132, 134ffthf1o 14109 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( ( `' F `  u ) G ( `' F `  v ) ) : ( ( `' F `  u ) (  Hom  `  X ) ( `' F `  v ) ) -1-1-onto-> ( ( F `  ( `' F `  u ) ) (  Hom  `  Y
) ( F `  ( `' F `  v ) ) ) )
13913ad2ant1 978 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  F : R -1-1-onto-> S
)
140139, 131, 95syl2anc 643 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( F `  ( `' F `  u ) )  =  u )
141139, 133, 98syl2anc 643 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( F `  ( `' F `  v ) )  =  v )
142140, 141oveq12d 6092 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( ( F `
 ( `' F `  u ) ) (  Hom  `  Y )
( F `  ( `' F `  v ) ) )  =  ( u (  Hom  `  Y
) v ) )
143 f1oeq3 5660 . . . . . . . . . . . . . . 15  |-  ( ( ( F `  ( `' F `  u ) ) (  Hom  `  Y
) ( F `  ( `' F `  v ) ) )  =  ( u (  Hom  `  Y
) v )  -> 
( ( ( `' F `  u ) G ( `' F `  v ) ) : ( ( `' F `  u ) (  Hom  `  X ) ( `' F `  v ) ) -1-1-onto-> ( ( F `  ( `' F `  u ) ) (  Hom  `  Y
) ( F `  ( `' F `  v ) ) )  <->  ( ( `' F `  u ) G ( `' F `  v ) ) : ( ( `' F `  u ) (  Hom  `  X ) ( `' F `  v ) ) -1-1-onto-> ( u (  Hom  `  Y ) v ) ) )
144142, 143syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( ( ( `' F `  u ) G ( `' F `  v ) ) : ( ( `' F `  u ) (  Hom  `  X ) ( `' F `  v ) ) -1-1-onto-> ( ( F `  ( `' F `  u ) ) (  Hom  `  Y
) ( F `  ( `' F `  v ) ) )  <->  ( ( `' F `  u ) G ( `' F `  v ) ) : ( ( `' F `  u ) (  Hom  `  X ) ( `' F `  v ) ) -1-1-onto-> ( u (  Hom  `  Y ) v ) ) )
145138, 144mpbid 202 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( ( `' F `  u ) G ( `' F `  v ) ) : ( ( `' F `  u ) (  Hom  `  X ) ( `' F `  v ) ) -1-1-onto-> ( u (  Hom  `  Y ) v ) )
146 f1ocnv 5680 . . . . . . . . . . . . 13  |-  ( ( ( `' F `  u ) G ( `' F `  v ) ) : ( ( `' F `  u ) (  Hom  `  X
) ( `' F `  v ) ) -1-1-onto-> ( u (  Hom  `  Y
) v )  ->  `' ( ( `' F `  u ) G ( `' F `  v ) ) : ( u (  Hom  `  Y ) v ) -1-1-onto-> ( ( `' F `  u ) (  Hom  `  X ) ( `' F `  v ) ) )
147 f1of 5667 . . . . . . . . . . . . 13  |-  ( `' ( ( `' F `  u ) G ( `' F `  v ) ) : ( u (  Hom  `  Y
) v ) -1-1-onto-> ( ( `' F `  u ) (  Hom  `  X
) ( `' F `  v ) )  ->  `' ( ( `' F `  u ) G ( `' F `  v ) ) : ( u (  Hom  `  Y ) v ) --> ( ( `' F `  u ) (  Hom  `  X ) ( `' F `  v ) ) )
148145, 146, 1473syl 19 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  `' ( ( `' F `  u ) G ( `' F `  v ) ) : ( u (  Hom  `  Y ) v ) --> ( ( `' F `  u ) (  Hom  `  X ) ( `' F `  v ) ) )
149 simp3l 985 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  f  e.  ( u (  Hom  `  Y
) v ) )
150148, 149ffvelrnd 5864 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( `' ( ( `' F `  u ) G ( `' F `  v ) ) `  f )  e.  ( ( `' F `  u ) (  Hom  `  X
) ( `' F `  v ) ) )
15130, 31, 32, 137, 134, 136ffthf1o 14109 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( ( `' F `  v ) G ( `' F `  z ) ) : ( ( `' F `  v ) (  Hom  `  X ) ( `' F `  z ) ) -1-1-onto-> ( ( F `  ( `' F `  v ) ) (  Hom  `  Y
) ( F `  ( `' F `  z ) ) ) )
152 f1ocnvfv2 6008 . . . . . . . . . . . . . . . . 17  |-  ( ( F : R -1-1-onto-> S  /\  z  e.  S )  ->  ( F `  ( `' F `  z ) )  =  z )
153139, 135, 152syl2anc 643 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( F `  ( `' F `  z ) )  =  z )
154141, 153oveq12d 6092 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( ( F `
 ( `' F `  v ) ) (  Hom  `  Y )
( F `  ( `' F `  z ) ) )  =  ( v (  Hom  `  Y
) z ) )
155 f1oeq3 5660 . . . . . . . . . . . . . . 15  |-  ( ( ( F `  ( `' F `  v ) ) (  Hom  `  Y
) ( F `  ( `' F `  z ) ) )  =  ( v (  Hom  `  Y
) z )  -> 
( ( ( `' F `  v ) G ( `' F `  z ) ) : ( ( `' F `  v ) (  Hom  `  X ) ( `' F `  z ) ) -1-1-onto-> ( ( F `  ( `' F `  v ) ) (  Hom  `  Y
) ( F `  ( `' F `  z ) ) )  <->  ( ( `' F `  v ) G ( `' F `  z ) ) : ( ( `' F `  v ) (  Hom  `  X ) ( `' F `  z ) ) -1-1-onto-> ( v (  Hom  `  Y ) z ) ) )
156154, 155syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( ( ( `' F `  v ) G ( `' F `  z ) ) : ( ( `' F `  v ) (  Hom  `  X ) ( `' F `  z ) ) -1-1-onto-> ( ( F `  ( `' F `  v ) ) (  Hom  `  Y
) ( F `  ( `' F `  z ) ) )  <->  ( ( `' F `  v ) G ( `' F `  z ) ) : ( ( `' F `  v ) (  Hom  `  X ) ( `' F `  z ) ) -1-1-onto-> ( v (  Hom  `  Y ) z ) ) )
157151, 156mpbid 202 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( ( `' F `  v ) G ( `' F `  z ) ) : ( ( `' F `  v ) (  Hom  `  X ) ( `' F `  z ) ) -1-1-onto-> ( v (  Hom  `  Y ) z ) )
158 f1ocnv 5680 . . . . . . . . . . . . 13  |-  ( ( ( `' F `  v ) G ( `' F `  z ) ) : ( ( `' F `  v ) (  Hom  `  X
) ( `' F `  z ) ) -1-1-onto-> ( v (  Hom  `  Y
) z )  ->  `' ( ( `' F `  v ) G ( `' F `  z ) ) : ( v (  Hom  `  Y ) z ) -1-1-onto-> ( ( `' F `  v ) (  Hom  `  X ) ( `' F `  z ) ) )
159 f1of 5667 . . . . . . . . . . . . 13  |-  ( `' ( ( `' F `  v ) G ( `' F `  z ) ) : ( v (  Hom  `  Y
) z ) -1-1-onto-> ( ( `' F `  v ) (  Hom  `  X
) ( `' F `  z ) )  ->  `' ( ( `' F `  v ) G ( `' F `  z ) ) : ( v (  Hom  `  Y ) z ) --> ( ( `' F `  v ) (  Hom  `  X ) ( `' F `  z ) ) )
160157, 158, 1593syl 19 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  `' ( ( `' F `  v ) G ( `' F `  z ) ) : ( v (  Hom  `  Y ) z ) --> ( ( `' F `  v ) (  Hom  `  X ) ( `' F `  z ) ) )
161 simp3r 986 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  g  e.  ( v (  Hom  `  Y
) z ) )
162160, 161ffvelrnd 5864 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( `' ( ( `' F `  v ) G ( `' F `  z ) ) `  g )  e.  ( ( `' F `  v ) (  Hom  `  X
) ( `' F `  z ) ) )
16330, 31, 56, 55, 129, 132, 134, 136, 150, 162funcco 14061 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( ( ( `' F `  u ) G ( `' F `  z ) ) `  ( ( `' ( ( `' F `  v ) G ( `' F `  z ) ) `  g ) ( <. ( `' F `  u ) ,  ( `' F `  v )
>. (comp `  X )
( `' F `  z ) ) ( `' ( ( `' F `  u ) G ( `' F `  v ) ) `  f ) ) )  =  ( ( ( ( `' F `  v ) G ( `' F `  z ) ) `  ( `' ( ( `' F `  v ) G ( `' F `  z ) ) `  g ) ) ( <. ( F `  ( `' F `  u )
) ,  ( F `
 ( `' F `  v ) ) >.
(comp `  Y )
( F `  ( `' F `  z ) ) ) ( ( ( `' F `  u ) G ( `' F `  v ) ) `  ( `' ( ( `' F `  u ) G ( `' F `  v ) ) `  f ) ) ) )
164140, 141opeq12d 3985 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  <. ( F `  ( `' F `  u ) ) ,  ( F `
 ( `' F `  v ) ) >.  =  <. u ,  v
>. )
165164, 153oveq12d 6092 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( <. ( F `  ( `' F `  u )
) ,  ( F `
 ( `' F `  v ) ) >.
(comp `  Y )
( F `  ( `' F `  z ) ) )  =  (
<. u ,  v >.
(comp `  Y )
z ) )
166 f1ocnvfv2 6008 . . . . . . . . . . . 12  |-  ( ( ( ( `' F `  v ) G ( `' F `  z ) ) : ( ( `' F `  v ) (  Hom  `  X
) ( `' F `  z ) ) -1-1-onto-> ( v (  Hom  `  Y
) z )  /\  g  e.  ( v
(  Hom  `  Y ) z ) )  -> 
( ( ( `' F `  v ) G ( `' F `  z ) ) `  ( `' ( ( `' F `  v ) G ( `' F `  z ) ) `  g ) )  =  g )
167157, 161, 166syl2anc 643 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( ( ( `' F `  v ) G ( `' F `  z ) ) `  ( `' ( ( `' F `  v ) G ( `' F `  z ) ) `  g ) )  =  g )
168 f1ocnvfv2 6008 . . . . . . . . . . . 12  |-  ( ( ( ( `' F `  u ) G ( `' F `  v ) ) : ( ( `' F `  u ) (  Hom  `  X
) ( `' F `  v ) ) -1-1-onto-> ( u (  Hom  `  Y
) v )  /\  f  e.  ( u
(  Hom  `  Y ) v ) )  -> 
( ( ( `' F `  u ) G ( `' F `  v ) ) `  ( `' ( ( `' F `  u ) G ( `' F `  v ) ) `  f ) )  =  f )
169145, 149, 168syl2anc 643 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( ( ( `' F `  u ) G ( `' F `  v ) ) `  ( `' ( ( `' F `  u ) G ( `' F `  v ) ) `  f ) )  =  f )
170165, 167, 169oveq123d 6095 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( ( ( ( `' F `  v ) G ( `' F `  z ) ) `  ( `' ( ( `' F `  v ) G ( `' F `  z ) ) `  g ) ) ( <. ( F `  ( `' F `  u )
) ,  ( F `
 ( `' F `  v ) ) >.
(comp `  Y )
( F `  ( `' F `  z ) ) ) ( ( ( `' F `  u ) G ( `' F `  v ) ) `  ( `' ( ( `' F `  u ) G ( `' F `  v ) ) `  f ) ) )  =  ( g ( <. u ,  v >. (comp `  Y ) z ) f ) )
171163, 170eqtrd 2468 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( ( ( `' F `  u ) G ( `' F `  z ) ) `  ( ( `' ( ( `' F `  v ) G ( `' F `  z ) ) `  g ) ( <. ( `' F `  u ) ,  ( `' F `  v )
>. (comp `  X )
( `' F `  z ) ) ( `' ( ( `' F `  u ) G ( `' F `  v ) ) `  f ) ) )  =  ( g (
<. u ,  v >.
(comp `  Y )
z ) f ) )
17230, 31, 32, 137, 132, 136ffthf1o 14109 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( ( `' F `  u ) G ( `' F `  z ) ) : ( ( `' F `  u ) (  Hom  `  X ) ( `' F `  z ) ) -1-1-onto-> ( ( F `  ( `' F `  u ) ) (  Hom  `  Y
) ( F `  ( `' F `  z ) ) ) )
173140, 153oveq12d 6092 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( ( F `
 ( `' F `  u ) ) (  Hom  `  Y )
( F `  ( `' F `  z ) ) )  =  ( u (  Hom  `  Y
) z ) )
174 f1oeq3 5660 . . . . . . . . . . . 12  |-  ( ( ( F `  ( `' F `  u ) ) (  Hom  `  Y
) ( F `  ( `' F `  z ) ) )  =  ( u (  Hom  `  Y
) z )  -> 
( ( ( `' F `  u ) G ( `' F `  z ) ) : ( ( `' F `  u ) (  Hom  `  X ) ( `' F `  z ) ) -1-1-onto-> ( ( F `  ( `' F `  u ) ) (  Hom  `  Y
) ( F `  ( `' F `  z ) ) )  <->  ( ( `' F `  u ) G ( `' F `  z ) ) : ( ( `' F `  u ) (  Hom  `  X ) ( `' F `  z ) ) -1-1-onto-> ( u (  Hom  `  Y ) z ) ) )
175173, 174syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( ( ( `' F `  u ) G ( `' F `  z ) ) : ( ( `' F `  u ) (  Hom  `  X ) ( `' F `  z ) ) -1-1-onto-> ( ( F `  ( `' F `  u ) ) (  Hom  `  Y
) ( F `  ( `' F `  z ) ) )  <->  ( ( `' F `  u ) G ( `' F `  z ) ) : ( ( `' F `  u ) (  Hom  `  X ) ( `' F `  z ) ) -1-1-onto-> ( u (  Hom  `  Y ) z ) ) )
176172, 175mpbid 202 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( ( `' F `  u ) G ( `' F `  z ) ) : ( ( `' F `  u ) (  Hom  `  X ) ( `' F `  z ) ) -1-1-onto-> ( u (  Hom  `  Y ) z ) )
177663ad2ant1 978 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  X  e.  Cat )
17830, 31, 56, 177, 132, 134, 136, 150, 162catcocl 13903 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( ( `' ( ( `' F `  v ) G ( `' F `  z ) ) `  g ) ( <. ( `' F `  u ) ,  ( `' F `  v )
>. (comp `  X )
( `' F `  z ) ) ( `' ( ( `' F `  u ) G ( `' F `  v ) ) `  f ) )  e.  ( ( `' F `  u ) (  Hom  `  X ) ( `' F `  z ) ) )
179 f1ocnvfv 6009 . . . . . . . . . 10  |-  ( ( ( ( `' F `  u ) G ( `' F `  z ) ) : ( ( `' F `  u ) (  Hom  `  X
) ( `' F `  z ) ) -1-1-onto-> ( u (  Hom  `  Y
) z )  /\  ( ( `' ( ( `' F `  v ) G ( `' F `  z ) ) `  g ) ( <. ( `' F `  u ) ,  ( `' F `  v )
>. (comp `  X )
( `' F `  z ) ) ( `' ( ( `' F `  u ) G ( `' F `  v ) ) `  f ) )  e.  ( ( `' F `  u ) (  Hom  `  X ) ( `' F `  z ) ) )  ->  (
( ( ( `' F `  u ) G ( `' F `  z ) ) `  ( ( `' ( ( `' F `  v ) G ( `' F `  z ) ) `  g ) ( <. ( `' F `  u ) ,  ( `' F `  v )
>. (comp `  X )
( `' F `  z ) ) ( `' ( ( `' F `  u ) G ( `' F `  v ) ) `  f ) ) )  =  ( g (
<. u ,  v >.
(comp `  Y )
z ) f )  ->  ( `' ( ( `' F `  u ) G ( `' F `  z ) ) `  ( g ( <. u ,  v
>. (comp `  Y )
z ) f ) )  =  ( ( `' ( ( `' F `  v ) G ( `' F `  z ) ) `  g ) ( <.
( `' F `  u ) ,  ( `' F `  v )
>. (comp `  X )
( `' F `  z ) ) ( `' ( ( `' F `  u ) G ( `' F `  v ) ) `  f ) ) ) )
180176, 178, 179syl2anc 643 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( ( ( ( `' F `  u ) G ( `' F `  z ) ) `  ( ( `' ( ( `' F `  v ) G ( `' F `  z ) ) `  g ) ( <.
( `' F `  u ) ,  ( `' F `  v )
>. (comp `  X )
( `' F `  z ) ) ( `' ( ( `' F `  u ) G ( `' F `  v ) ) `  f ) ) )  =  ( g (
<. u ,  v >.
(comp `  Y )
z ) f )  ->  ( `' ( ( `' F `  u ) G ( `' F `  z ) ) `  ( g ( <. u ,  v
>. (comp `  Y )
z ) f ) )  =  ( ( `' ( ( `' F `  v ) G ( `' F `  z ) ) `  g ) ( <.
( `' F `  u ) ,  ( `' F `  v )
>. (comp `  X )
( `' F `  z ) ) ( `' ( ( `' F `  u ) G ( `' F `  v ) ) `  f ) ) ) )
181171, 180mpd 15 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( `' ( ( `' F `  u ) G ( `' F `  z ) ) `  ( g ( <. u ,  v
>. (comp `  Y )
z ) f ) )  =  ( ( `' ( ( `' F `  v ) G ( `' F `  z ) ) `  g ) ( <.
( `' F `  u ) ,  ( `' F `  v )
>. (comp `  X )
( `' F `  z ) ) ( `' ( ( `' F `  u ) G ( `' F `  v ) ) `  f ) ) )
182 simpl 444 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  z )  ->  x  =  u )
183182fveq2d 5725 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  z )  ->  ( `' F `  x )  =  ( `' F `  u ) )
184 simpr 448 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  z )  ->  y  =  z )
185184fveq2d 5725 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  z )  ->  ( `' F `  y )  =  ( `' F `  z ) )
186183, 185oveq12d 6092 . . . . . . . . . . . 12  |-  ( ( x  =  u  /\  y  =  z )  ->  ( ( `' F `  x ) G ( `' F `  y ) )  =  ( ( `' F `  u ) G ( `' F `  z ) ) )
187186cnveqd 5041 . . . . . . . . . . 11  |-  ( ( x  =  u  /\  y  =  z )  ->  `' ( ( `' F `  x ) G ( `' F `  y ) )  =  `' ( ( `' F `  u ) G ( `' F `  z ) ) )
188 ovex 6099 . . . . . . . . . . . 12  |-  ( ( `' F `  u ) G ( `' F `  z ) )  e. 
_V
189188cnvex 5399 . . . . . . . . . . 11  |-  `' ( ( `' F `  u ) G ( `' F `  z ) )  e.  _V
190187, 17, 189ovmpt2a 6197 . . . . . . . . . 10  |-  ( ( u  e.  S  /\  z  e.  S )  ->  ( u H z )  =  `' ( ( `' F `  u ) G ( `' F `  z ) ) )
191131, 135, 190syl2anc 643 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( u H z )  =  `' ( ( `' F `  u ) G ( `' F `  z ) ) )
192191fveq1d 5723 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( ( u H z ) `  ( g ( <.
u ,  v >.
(comp `  Y )
z ) f ) )  =  ( `' ( ( `' F `  u ) G ( `' F `  z ) ) `  ( g ( <. u ,  v
>. (comp `  Y )
z ) f ) ) )
193 simpl 444 . . . . . . . . . . . . . . 15  |-  ( ( x  =  v  /\  y  =  z )  ->  x  =  v )
194193fveq2d 5725 . . . . . . . . . . . . . 14  |-  ( ( x  =  v  /\  y  =  z )  ->  ( `' F `  x )  =  ( `' F `  v ) )
195 simpr 448 . . . . . . . . . . . . . . 15  |-  ( ( x  =  v  /\  y  =  z )  ->  y  =  z )
196195fveq2d 5725 . . . . . . . . . . . . . 14  |-  ( ( x  =  v  /\  y  =  z )  ->  ( `' F `  y )  =  ( `' F `  z ) )
197194, 196oveq12d 6092 . . . . . . . . . . . . 13  |-  ( ( x  =  v  /\  y  =  z )  ->  ( ( `' F `  x ) G ( `' F `  y ) )  =  ( ( `' F `  v ) G ( `' F `  z ) ) )
198197cnveqd 5041 . . . . . . . . . . . 12  |-  ( ( x  =  v  /\  y  =  z )  ->  `' ( ( `' F `  x ) G ( `' F `  y ) )  =  `' ( ( `' F `  v ) G ( `' F `  z ) ) )
199 ovex 6099 . . . . . . . . . . . . 13  |-  ( ( `' F `  v ) G ( `' F `  z ) )  e. 
_V
200199cnvex 5399 . . . . . . . . . . . 12  |-  `' ( ( `' F `  v ) G ( `' F `  z ) )  e.  _V
201198, 17, 200ovmpt2a 6197 . . . . . . . . . . 11  |-  ( ( v  e.  S  /\  z  e.  S )  ->  ( v H z )  =  `' ( ( `' F `  v ) G ( `' F `  z ) ) )
202133, 135, 201syl2anc 643 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( v H z )  =  `' ( ( `' F `  v ) G ( `' F `  z ) ) )
203202fveq1d 5723 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( ( v H z ) `  g )  =  ( `' ( ( `' F `  v ) G ( `' F `  z ) ) `  g ) )
204131, 133, 91syl2anc 643 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( u H v )  =  `' ( ( `' F `  u ) G ( `' F `  v ) ) )
205204fveq1d 5723 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( ( u H v ) `  f )  =  ( `' ( ( `' F `  u ) G ( `' F `  v ) ) `  f ) )
206203, 205oveq12d 6092 . . . . . . . 8  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( ( ( v H z ) `
 g ) (
<. ( `' F `  u ) ,  ( `' F `  v )
>. (comp `  X )
( `' F `  z ) ) ( ( u H v ) `  f ) )  =  ( ( `' ( ( `' F `  v ) G ( `' F `  z ) ) `  g ) ( <.
( `' F `  u ) ,  ( `' F `  v )
>. (comp `  X )
( `' F `  z ) ) ( `' ( ( `' F `  u ) G ( `' F `  v ) ) `  f ) ) )
207181, 192, 2063eqtr4d 2478 . . . . . . 7  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S  /\  z  e.  S )  /\  (
f  e.  ( u (  Hom  `  Y
) v )  /\  g  e.  ( v
(  Hom  `  Y ) z ) ) )  ->  ( ( u H z ) `  ( g ( <.
u ,  v >.
(comp `  Y )
z ) f ) )  =  ( ( ( v H z ) `  g ) ( <. ( `' F `  u ) ,  ( `' F `  v )
>. (comp `  X )
( `' F `  z ) ) ( ( u H v ) `  f ) ) )
20852, 30, 32, 31, 53, 54, 55, 56, 64, 66, 69, 73, 103, 128, 207isfuncd 14055 . . . . . 6  |-  ( ph  ->  `' F ( Y  Func  X ) H )
20930, 51, 208cofuval2 14077 . . . . 5  |-  ( ph  ->  ( <. `' F ,  H >.  o.func 
<. F ,  G >. )  =  <. ( `' F  o.  F ) ,  ( u  e.  R , 
v  e.  R  |->  ( ( ( F `  u ) H ( F `  v ) )  o.  ( u G v ) ) ) >. )
210 eqid 2436 . . . . . 6  |-  (idfunc `  X
)  =  (idfunc `  X
)
211210, 30, 66, 31idfuval 14066 . . . . 5  |-  ( ph  ->  (idfunc `  X )  =  <. (  _I  |`  R ) ,  ( z  e.  ( R  X.  R
)  |->  (  _I  |`  (
(  Hom  `  X ) `
 z ) ) ) >. )
21246, 209, 2113eqtr4d 2478 . . . 4  |-  ( ph  ->  ( <. `' F ,  H >.  o.func 
<. F ,  G >. )  =  (idfunc `  X ) )
213 eqid 2436 . . . . 5  |-  (comp `  C )  =  (comp `  C )
214 df-br 4206 . . . . . 6  |-  ( F ( X  Func  Y
) G  <->  <. F ,  G >.  e.  ( X 
Func  Y ) )
21551, 214sylib 189 . . . . 5  |-  ( ph  -> 
<. F ,  G >.  e.  ( X  Func  Y
) )
216 df-br 4206 . . . . . 6  |-  ( `' F ( Y  Func  X ) H  <->  <. `' F ,  H >.  e.  ( Y  Func  X ) )
217208, 216sylib 189 . . . . 5  |-  ( ph  -> 
<. `' F ,  H >.  e.  ( Y  Func  X
) )
21857, 58, 59, 213, 65, 63, 65, 215, 217catcco 14249 . . . 4  |-  ( ph  ->  ( <. `' F ,  H >. ( <. X ,  Y >. (comp `  C
) X ) <. F ,  G >. )  =  ( <. `' F ,  H >.  o.func 
<. F ,  G >. ) )
219 eqid 2436 . . . . 5  |-  ( Id
`  C )  =  ( Id `  C
)
22057, 58, 219, 210, 59, 65catcid 14251 . . . 4  |-  ( ph  ->  ( ( Id `  C ) `  X
)  =  (idfunc `  X
) )
221212, 218, 2203eqtr4d 2478 . . 3  |-  ( ph  ->  ( <. `' F ,  H >. ( <. X ,  Y >. (comp `  C
) X ) <. F ,  G >. )  =  ( ( Id
`  C ) `  X ) )
222 eqid 2436 . . . 4  |-  (  Hom  `  C )  =  (  Hom  `  C )
223 eqid 2436 . . . 4  |-  (Sect `  C )  =  (Sect `  C )
22457catccat 14252 . . . . 5  |-  ( U  e.  V  ->  C  e.  Cat )
22559, 224syl 16 . . . 4  |-  ( ph  ->  C  e.  Cat )
22657, 58, 59, 222, 65, 63catchom 14247 . . . . 5  |-  ( ph  ->  ( X (  Hom  `  C ) Y )  =  ( X  Func  Y ) )
227215, 226eleqtrrd 2513 . . . 4  |-  ( ph  -> 
<. F ,  G >.  e.  ( X (  Hom  `  C ) Y ) )
22857, 58, 59, 222, 63, 65catchom 14247 . . . . 5  |-  ( ph  ->  ( Y (  Hom  `  C ) X )  =  ( Y  Func  X ) )
229217, 228eleqtrrd 2513 . . . 4  |-  ( ph  -> 
<. `' F ,  H >.  e.  ( Y (  Hom  `  C ) X ) )
23058, 222, 213, 219, 223, 225, 65, 63, 227, 229issect2 13973 . . 3  |-  ( ph  ->  ( <. F ,  G >. ( X (Sect `  C ) Y )
<. `' F ,  H >.  <->  ( <. `' F ,  H >. (
<. X ,  Y >. (comp `  C ) X )
<. F ,  G >. )  =  ( ( Id
`  C ) `  X ) ) )
231221, 230mpbird 224 . 2  |-  ( ph  -> 
<. F ,  G >. ( X (Sect `  C
) Y ) <. `' F ,  H >. )
232 f1ococnv2 5695 . . . . . . 7  |-  ( F : R -1-1-onto-> S  ->  ( F  o.  `' F )  =  (  _I  |`  S )
)
2331, 232syl 16 . . . . . 6  |-  ( ph  ->  ( F  o.  `' F )  =  (  _I  |`  S )
)
234913adant1 975 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  ( u H v )  =  `' ( ( `' F `  u ) G ( `' F `  v ) ) )
235234coeq2d 5028 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  ( (
( `' F `  u ) G ( `' F `  v ) )  o.  ( u H v ) )  =  ( ( ( `' F `  u ) G ( `' F `  v ) )  o.  `' ( ( `' F `  u ) G ( `' F `  v ) ) ) )
236333ad2ant1 978 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  F (
( X Full  Y )  i^i  ( X Faith  Y ) ) G )
237753adant3 977 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  ( `' F `  u )  e.  R )
238773adant2 976 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  ( `' F `  v )  e.  R )
23930, 31, 32, 236, 237, 238ffthf1o 14109 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  ( ( `' F `  u ) G ( `' F `  v ) ) : ( ( `' F `  u ) (  Hom  `  X ) ( `' F `  v ) ) -1-1-onto-> ( ( F `  ( `' F `  u ) ) (  Hom  `  Y
) ( F `  ( `' F `  v ) ) ) )
2401003impb 1149 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  ( ( F `  ( `' F `  u )
) (  Hom  `  Y
) ( F `  ( `' F `  v ) ) )  =  ( u (  Hom  `  Y
) v ) )
241240, 143syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  ( (
( `' F `  u ) G ( `' F `  v ) ) : ( ( `' F `  u ) (  Hom  `  X
) ( `' F `  v ) ) -1-1-onto-> ( ( F `  ( `' F `  u ) ) (  Hom  `  Y
) ( F `  ( `' F `  v ) ) )  <->  ( ( `' F `  u ) G ( `' F `  v ) ) : ( ( `' F `  u ) (  Hom  `  X ) ( `' F `  v ) ) -1-1-onto-> ( u (  Hom  `  Y ) v ) ) )
242239, 241mpbid 202 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  ( ( `' F `  u ) G ( `' F `  v ) ) : ( ( `' F `  u ) (  Hom  `  X ) ( `' F `  v ) ) -1-1-onto-> ( u (  Hom  `  Y ) v ) )
243 f1ococnv2 5695 . . . . . . . . . 10  |-  ( ( ( `' F `  u ) G ( `' F `  v ) ) : ( ( `' F `  u ) (  Hom  `  X
) ( `' F `  v ) ) -1-1-onto-> ( u (  Hom  `  Y
) v )  -> 
( ( ( `' F `  u ) G ( `' F `  v ) )  o.  `' ( ( `' F `  u ) G ( `' F `  v ) ) )  =  (  _I  |`  (
u (  Hom  `  Y
) v ) ) )
244242, 243syl 16 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  ( (
( `' F `  u ) G ( `' F `  v ) )  o.  `' ( ( `' F `  u ) G ( `' F `  v ) ) )  =  (  _I  |`  ( u
(  Hom  `  Y ) v ) ) )
245235, 244eqtrd 2468 . . . . . . . 8  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  ( (
( `' F `  u ) G ( `' F `  v ) )  o.  ( u H v ) )  =  (  _I  |`  (
u (  Hom  `  Y
) v ) ) )
246245mpt2eq3dva 6131 . . . . . . 7  |-  ( ph  ->  ( u  e.  S ,  v  e.  S  |->  ( ( ( `' F `  u ) G ( `' F `  v ) )  o.  ( u H v ) ) )  =  ( u  e.  S ,  v  e.  S  |->  (  _I  |`  (
u (  Hom  `  Y
) v ) ) ) )
247 fveq2 5721 . . . . . . . . . 10  |-  ( z  =  <. u ,  v
>.  ->  ( (  Hom  `  Y ) `  z
)  =  ( (  Hom  `  Y ) `  <. u ,  v
>. ) )
248 df-ov 6077 . . . . . . . . . 10  |-  ( u (  Hom  `  Y
) v )  =  ( (  Hom  `  Y
) `  <. u ,  v >. )
249247, 248syl6eqr 2486 . . . . . . . . 9  |-  ( z  =  <. u ,  v
>.  ->  ( (  Hom  `  Y ) `  z
)  =  ( u (  Hom  `  Y
) v ) )
250249reseq2d 5139 . . . . . . . 8  |-  ( z  =  <. u ,  v
>.  ->  (  _I  |`  (
(  Hom  `  Y ) `
 z ) )  =  (  _I  |`  (
u (  Hom  `  Y
) v ) ) )
251250mpt2mpt 6158 . . . . . . 7  |-  ( z  e.  ( S  X.  S )  |->  (  _I  |`  ( (  Hom  `  Y
) `  z )
) )  =  ( u  e.  S , 
v  e.  S  |->  (  _I  |`  ( u
(  Hom  `  Y ) v ) ) )
252246, 251syl6eqr 2486 . . . . . 6  |-  ( ph  ->  ( u  e.  S ,  v  e.  S  |->  ( ( ( `' F `  u ) G ( `' F `  v ) )  o.  ( u H v ) ) )  =  ( z  e.  ( S  X.  S ) 
|->  (  _I  |`  (
(  Hom  `  Y ) `
 z ) ) ) )
253233, 252opeq12d 3985 . . . . 5  |-  ( ph  -> 
<. ( F  o.  `' F ) ,  ( u  e.  S , 
v  e.  S  |->  ( ( ( `' F `  u ) G ( `' F `  v ) )  o.  ( u H v ) ) ) >.  =  <. (  _I  |`  S ) ,  ( z  e.  ( S  X.  S
)  |->  (  _I  |`  (
(  Hom  `  Y ) `
 z ) ) ) >. )
25452, 208, 51cofuval2 14077 . . . . 5  |-  ( ph  ->  ( <. F ,  G >.  o.func 
<. `' F ,  H >. )  =  <. ( F  o.  `' F ) ,  ( u  e.  S , 
v  e.  S  |->  ( ( ( `' F `  u ) G ( `' F `  v ) )  o.  ( u H v ) ) ) >. )
255 eqid 2436 . . . . . 6  |-  (idfunc `  Y
)  =  (idfunc `  Y
)
256255, 52, 64, 32idfuval 14066 . . . . 5  |-  ( ph  ->  (idfunc `  Y )  =  <. (  _I  |`  S ) ,  ( z  e.  ( S  X.  S
)  |->  (  _I  |`  (
(  Hom  `  Y ) `
 z ) ) ) >. )
257253, 254, 2563eqtr4d 2478 . . . 4  |-  ( ph  ->  ( <. F ,  G >.  o.func 
<. `' F ,  H >. )  =  (idfunc `  Y ) )
25857, 58, 59, 213, 63, 65, 63, 217, 215catcco 14249 . . . 4  |-  ( ph  ->  ( <. F ,  G >. ( <. Y ,  X >. (comp `  C ) Y ) <. `' F ,  H >. )  =  (
<. F ,  G >.  o.func  <. `' F ,  H >. ) )
25957, 58, 219, 255, 59, 63catcid 14251 . . . 4  |-  ( ph  ->  ( ( Id `  C ) `  Y
)  =  (idfunc `  Y
) )
260257, 258, 2593eqtr4d 2478 . . 3  |-  ( ph  ->  ( <. F ,  G >. ( <. Y ,  X >. (comp `  C ) Y ) <. `' F ,  H >. )  =  ( ( Id `  C
) `  Y )
)
26158, 222, 213, 219, 223, 225, 63, 65, 229, 227issect2 13973 . . 3  |-  ( ph  ->  ( <. `' F ,  H >. ( Y (Sect `  C ) X )
<. F ,  G >.  <->  ( <. F ,  G >. (
<. Y ,  X >. (comp `  C ) Y )
<. `' F ,  H >. )  =  ( ( Id
`  C ) `  Y ) ) )
262260, 261mpbird 224 . 2  |-  ( ph  -> 
<. `' F ,  H >. ( Y (Sect `  C
) X ) <. F ,  G >. )
263 catcisolem.i . . 3  |-  I  =  (Inv `  C )
26458, 263, 225, 65, 63, 223isinv 13978 . 2  |-  ( ph  ->  ( <. F ,  G >. ( X I Y ) <. `' F ,  H >. 
<->  ( <. F ,  G >. ( X (Sect `  C ) Y )
<. `' F ,  H >.  /\ 
<. `' F ,  H >. ( Y (Sect `  C
) X ) <. F ,  G >. ) ) )
265231, 262, 264mpbir2and 889 1  |-  ( ph  -> 
<. F ,  G >. ( X I Y )
<. `' F ,  H >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    /\ w3a 936    = wceq 1652    e. wcel 1725    i^i cin 3312   <.cop 3810   class class class wbr 4205    e. cmpt 4259    _I cid 4486    X. cxp 4869   `'ccnv 4870    |` cres 4873    o. ccom 4875    Fn wfn 5442   -->wf 5443   -1-1-onto->wf1o 5446   ` cfv 5447  (class class class)co 6074    e. cmpt2 6076   Basecbs 13462    Hom chom 13533  compcco 13534   Catccat 13882   Idccid 13883  Sectcsect 13963  Invcinv 13964    Func cfunc 14044  idfunccidfu 14045    o.func ccofu 14046   Full cful 14092   Faith cfth 14093  CatCatccatc 14242
This theorem is referenced by:  catciso  14255
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-rep 4313  ax-sep 4323  ax-nul 4331  ax-pow 4370  ax-pr 4396  ax-un 4694  ax-cnex 9039  ax-resscn 9040  ax-1cn 9041  ax-icn 9042  ax-addcl 9043  ax-addrcl 9044  ax-mulcl 9045  ax-mulrcl 9046  ax-mulcom 9047  ax-addass 9048  ax-mulass 9049  ax-distr 9050  ax-i2m1 9051  ax-1ne0 9052  ax-1rid 9053  ax-rnegex 9054  ax-rrecex 9055  ax-cnre 9056  ax-pre-lttri 9057  ax-pre-lttrn 9058  ax-pre-ltadd 9059  ax-pre-mulgt0 9060
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-nel 2602  df-ral 2703  df-rex 2704  df-reu 2705  df-rmo 2706  df-rab 2707  df-v 2951  df-sbc 3155  df-csb 3245  df-dif 3316  df-un 3318  df-in 3320  df-ss 3327  df-pss 3329  df-nul 3622  df-if 3733  df-pw 3794  df-sn 3813  df-pr 3814  df-tp 3815  df-op 3816  df-uni 4009  df-int 4044  df-iun 4088  df-br 4206  df-opab 4260  df-mpt 4261  df-tr 4296  df-eprel 4487  df-id 4491  df-po 4496  df-so 4497  df-fr 4534  df-we 4536  df-ord 4577  df-on 4578  df-lim 4579  df-suc 4580  df-om 4839  df-xp 4877  df-rel 4878  df-cnv 4879  df-co 4880  df-dm 4881  df-rn 4882  df-res 4883  df-ima 4884  df-iota 5411  df-fun 5449  df-fn 5450  df-f 5451  df-f1 5452  df-fo 5453  df-f1o 5454  df-fv 5455  df-ov 6077  df-oprab 6078  df-mpt2 6079  df-1st 6342  df-2nd 6343  df-riota 6542  df-recs 6626  df-rdg 6661  df-1o 6717  df-oadd 6721  df-er 6898  df-map 7013  df-ixp 7057  df-en 7103  df-dom 7104  df-sdom 7105  df-fin 7106  df-pnf 9115  df-mnf 9116  df-xr 9117  df-ltxr 9118  df-le 9119  df-sub 9286  df-neg 9287  df-nn 9994  df-2 10051  df-3 10052  df-4 10053  df-5 10054  df-6 10055  df-7 10056  df-8 10057  df-9 10058  df-10 10059  df-n0 10215  df-z 10276  df-dec 10376  df-uz 10482  df-fz 11037  df-struct 13464  df-ndx 13465  df-slot 13466  df-base 13467  df-hom 13546  df-cco 13547  df-cat 13886  df-cid 13887  df-sect 13966  df-inv 13967  df-func 14048  df-idfu 14049  df-cofu 14050  df-full 14094  df-fth 14095  df-catc 14243
  Copyright terms: Public domain W3C validator