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

Theorem catcisolem 15944
Description: Lemma for catciso 15945. (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 5802 . . . . . . 7  |-  ( F : R -1-1-onto-> S  ->  ( `' F  o.  F )  =  (  _I  |`  R ) )
31, 2syl 17 . . . . . 6  |-  ( ph  ->  ( `' F  o.  F )  =  (  _I  |`  R )
)
413ad2ant1 1026 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  F : R
-1-1-onto-> S )
5 f1of 5774 . . . . . . . . . . . . . 14  |-  ( F : R -1-1-onto-> S  ->  F : R
--> S )
64, 5syl 17 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  F : R
--> S )
7 simp2 1006 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  u  e.  R )
86, 7ffvelrnd 5982 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( F `  u )  e.  S
)
9 simp3 1007 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  v  e.  R )
106, 9ffvelrnd 5982 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( F `  v )  e.  S
)
11 simpl 458 . . . . . . . . . . . . . . . 16  |-  ( ( x  =  ( F `
 u )  /\  y  =  ( F `  v ) )  ->  x  =  ( F `  u ) )
1211fveq2d 5829 . . . . . . . . . . . . . . 15  |-  ( ( x  =  ( F `
 u )  /\  y  =  ( F `  v ) )  -> 
( `' F `  x )  =  ( `' F `  ( F `
 u ) ) )
13 simpr 462 . . . . . . . . . . . . . . . 16  |-  ( ( x  =  ( F `
 u )  /\  y  =  ( F `  v ) )  -> 
y  =  ( F `
 v ) )
1413fveq2d 5829 . . . . . . . . . . . . . . 15  |-  ( ( x  =  ( F `
 u )  /\  y  =  ( F `  v ) )  -> 
( `' F `  y )  =  ( `' F `  ( F `
 v ) ) )
1512, 14oveq12d 6267 . . . . . . . . . . . . . 14  |-  ( ( x  =  ( F `
 u )  /\  y  =  ( F `  v ) )  -> 
( ( `' F `  x ) G ( `' F `  y ) )  =  ( ( `' F `  ( F `
 u ) ) G ( `' F `  ( F `  v
) ) ) )
1615cnveqd 4972 . . . . . . . . . . . . 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 6277 . . . . . . . . . . . . . 14  |-  ( ( `' F `  ( F `
 u ) ) G ( `' F `  ( F `  v
) ) )  e. 
_V
1918cnvex 6698 . . . . . . . . . . . . 13  |-  `' ( ( `' F `  ( F `  u ) ) G ( `' F `  ( F `
 v ) ) )  e.  _V
2016, 17, 19ovmpt2a 6385 . . . . . . . . . . . 12  |-  ( ( ( F `  u
)  e.  S  /\  ( F `  v )  e.  S )  -> 
( ( F `  u ) H ( F `  v ) )  =  `' ( ( `' F `  ( F `  u ) ) G ( `' F `  ( F `
 v ) ) ) )
218, 10, 20syl2anc 665 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( ( F `  u ) H ( F `  v ) )  =  `' ( ( `' F `  ( F `
 u ) ) G ( `' F `  ( F `  v
) ) ) )
22 f1ocnvfv1 6134 . . . . . . . . . . . . . 14  |-  ( ( F : R -1-1-onto-> S  /\  u  e.  R )  ->  ( `' F `  ( F `  u ) )  =  u )
234, 7, 22syl2anc 665 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( `' F `  ( F `  u ) )  =  u )
24 f1ocnvfv1 6134 . . . . . . . . . . . . . 14  |-  ( ( F : R -1-1-onto-> S  /\  v  e.  R )  ->  ( `' F `  ( F `  v ) )  =  v )
254, 9, 24syl2anc 665 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( `' F `  ( F `  v ) )  =  v )
2623, 25oveq12d 6267 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( ( `' F `  ( F `
 u ) ) G ( `' F `  ( F `  v
) ) )  =  ( u G v ) )
2726cnveqd 4972 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  `' (
( `' F `  ( F `  u ) ) G ( `' F `  ( F `
 v ) ) )  =  `' ( u G v ) )
2821, 27eqtrd 2462 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( ( F `  u ) H ( F `  v ) )  =  `' ( u G v ) )
2928coeq1d 4958 . . . . . . . . 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 2428 . . . . . . . . . . 11  |-  ( Hom  `  X )  =  ( Hom  `  X )
32 eqid 2428 . . . . . . . . . . 11  |-  ( Hom  `  Y )  =  ( Hom  `  Y )
33 catcisolem.1 . . . . . . . . . . . 12  |-  ( ph  ->  F ( ( X Full 
Y )  i^i  ( X Faith  Y ) ) G )
34333ad2ant1 1026 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  F (
( X Full  Y )  i^i  ( X Faith  Y ) ) G )
3530, 31, 32, 34, 7, 9ffthf1o 15767 . . . . . . . . . 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 5802 . . . . . . . . . 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 17 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( `' ( u G v )  o.  ( u G v ) )  =  (  _I  |`  (
u ( Hom  `  X
) v ) ) )
3829, 37eqtrd 2462 . . . . . . . 8  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( (
( F `  u
) H ( F `
 v ) )  o.  ( u G v ) )  =  (  _I  |`  (
u ( Hom  `  X
) v ) ) )
3938mpt2eq3dva 6313 . . . . . . 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 5825 . . . . . . . . . 10  |-  ( z  =  <. u ,  v
>.  ->  ( ( Hom  `  X ) `  z
)  =  ( ( Hom  `  X ) `  <. u ,  v
>. ) )
41 df-ov 6252 . . . . . . . . . 10  |-  ( u ( Hom  `  X
) v )  =  ( ( Hom  `  X
) `  <. u ,  v >. )
4240, 41syl6eqr 2480 . . . . . . . . 9  |-  ( z  =  <. u ,  v
>.  ->  ( ( Hom  `  X ) `  z
)  =  ( u ( Hom  `  X
) v ) )
4342reseq2d 5067 . . . . . . . 8  |-  ( z  =  <. u ,  v
>.  ->  (  _I  |`  (
( Hom  `  X ) `
 z ) )  =  (  _I  |`  (
u ( Hom  `  X
) v ) ) )
4443mpt2mpt 6346 . . . . . . 7  |-  ( z  e.  ( R  X.  R )  |->  (  _I  |`  ( ( Hom  `  X
) `  z )
) )  =  ( u  e.  R , 
v  e.  R  |->  (  _I  |`  ( u
( Hom  `  X ) v ) ) )
4539, 44syl6eqr 2480 . . . . . 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 4138 . . . . 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 3625 . . . . . . . . 9  |-  ( ( X Full  Y )  i^i  ( X Faith  Y ) )  C_  ( X Full  Y )
48 fullfunc 15754 . . . . . . . . 9  |-  ( X Full 
Y )  C_  ( X  Func  Y )
4947, 48sstri 3416 . . . . . . . 8  |-  ( ( X Full  Y )  i^i  ( X Faith  Y ) )  C_  ( X  Func  Y )
5049ssbri 4409 . . . . . . 7  |-  ( F ( ( X Full  Y
)  i^i  ( X Faith  Y ) ) G  ->  F ( X  Func  Y ) G )
5133, 50syl 17 . . . . . 6  |-  ( ph  ->  F ( X  Func  Y ) G )
52 catciso.s . . . . . . 7  |-  S  =  ( Base `  Y
)
53 eqid 2428 . . . . . . 7  |-  ( Id
`  Y )  =  ( Id `  Y
)
54 eqid 2428 . . . . . . 7  |-  ( Id
`  X )  =  ( Id `  X
)
55 eqid 2428 . . . . . . 7  |-  (comp `  Y )  =  (comp `  Y )
56 eqid 2428 . . . . . . 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 15935 . . . . . . . . 9  |-  ( ph  ->  B  =  ( U  i^i  Cat ) )
61 inss2 3626 . . . . . . . . 9  |-  ( U  i^i  Cat )  C_  Cat
6260, 61syl6eqss 3457 . . . . . . . 8  |-  ( ph  ->  B  C_  Cat )
63 catciso.y . . . . . . . 8  |-  ( ph  ->  Y  e.  B )
6462, 63sseldd 3408 . . . . . . 7  |-  ( ph  ->  Y  e.  Cat )
65 catciso.x . . . . . . . 8  |-  ( ph  ->  X  e.  B )
6662, 65sseldd 3408 . . . . . . 7  |-  ( ph  ->  X  e.  Cat )
67 f1ocnv 5786 . . . . . . . 8  |-  ( F : R -1-1-onto-> S  ->  `' F : S -1-1-onto-> R )
68 f1of 5774 . . . . . . . 8  |-  ( `' F : S -1-1-onto-> R  ->  `' F : S --> R )
691, 67, 683syl 18 . . . . . . 7  |-  ( ph  ->  `' F : S --> R )
70 ovex 6277 . . . . . . . . . 10  |-  ( ( `' F `  x ) G ( `' F `  y ) )  e. 
_V
7170cnvex 6698 . . . . . . . . 9  |-  `' ( ( `' F `  x ) G ( `' F `  y ) )  e.  _V
7217, 71fnmpt2i 6820 . . . . . . . 8  |-  H  Fn  ( S  X.  S
)
7372a1i 11 . . . . . . 7  |-  ( ph  ->  H  Fn  ( S  X.  S ) )
7433adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  ->  F ( ( X Full 
Y )  i^i  ( X Faith  Y ) ) G )
7569ffvelrnda 5981 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  S )  ->  ( `' F `  u )  e.  R )
7675adantrr 721 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( `' F `  u )  e.  R
)
7769ffvelrnda 5981 . . . . . . . . . . 11  |-  ( (
ph  /\  v  e.  S )  ->  ( `' F `  v )  e.  R )
7877adantrl 720 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( `' F `  v )  e.  R
)
7930, 31, 32, 74, 76, 78ffthf1o 15767 . . . . . . . . 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 5786 . . . . . . . . 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 5774 . . . . . . . . 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 18 . . . . . . . 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 458 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  v )  ->  x  =  u )
8483fveq2d 5829 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  v )  ->  ( `' F `  x )  =  ( `' F `  u ) )
85 simpr 462 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  v )  ->  y  =  v )
8685fveq2d 5829 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  v )  ->  ( `' F `  y )  =  ( `' F `  v ) )
8784, 86oveq12d 6267 . . . . . . . . . . . 12  |-  ( ( x  =  u  /\  y  =  v )  ->  ( ( `' F `  x ) G ( `' F `  y ) )  =  ( ( `' F `  u ) G ( `' F `  v ) ) )
8887cnveqd 4972 . . . . . . . . . . 11  |-  ( ( x  =  u  /\  y  =  v )  ->  `' ( ( `' F `  x ) G ( `' F `  y ) )  =  `' ( ( `' F `  u ) G ( `' F `  v ) ) )
89 ovex 6277 . . . . . . . . . . . 12  |-  ( ( `' F `  u ) G ( `' F `  v ) )  e. 
_V
9089cnvex 6698 . . . . . . . . . . 11  |-  `' ( ( `' F `  u ) G ( `' F `  v ) )  e.  _V
9188, 17, 90ovmpt2a 6385 . . . . . . . . . 10  |-  ( ( u  e.  S  /\  v  e.  S )  ->  ( u H v )  =  `' ( ( `' F `  u ) G ( `' F `  v ) ) )
9291adantl 467 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( u H v )  =  `' ( ( `' F `  u ) G ( `' F `  v ) ) )
931adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  ->  F : R -1-1-onto-> S )
94 simprl 762 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  ->  u  e.  S )
95 f1ocnvfv2 6135 . . . . . . . . . . . 12  |-  ( ( F : R -1-1-onto-> S  /\  u  e.  S )  ->  ( F `  ( `' F `  u ) )  =  u )
9693, 94, 95syl2anc 665 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( F `  ( `' F `  u ) )  =  u )
97 simprr 764 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
v  e.  S )
98 f1ocnvfv2 6135 . . . . . . . . . . . 12  |-  ( ( F : R -1-1-onto-> S  /\  v  e.  S )  ->  ( F `  ( `' F `  v ) )  =  v )
9993, 97, 98syl2anc 665 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( F `  ( `' F `  v ) )  =  v )
10096, 99oveq12d 6267 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( ( F `  ( `' F `  u ) ) ( Hom  `  Y
) ( F `  ( `' F `  v ) ) )  =  ( u ( Hom  `  Y
) v ) )
101100eqcomd 2434 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( u ( Hom  `  Y ) v )  =  ( ( F `
 ( `' F `  u ) ) ( Hom  `  Y )
( F `  ( `' F `  v ) ) ) )
10292, 101feq12d 5678 . . . . . . . 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 235 . . . . . . 7  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( u H v ) : ( u ( Hom  `  Y
) v ) --> ( ( `' F `  u ) ( Hom  `  X ) ( `' F `  v ) ) )
104 simpr 462 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  S )  ->  u  e.  S )
105 simpl 458 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  u )  ->  x  =  u )
106105fveq2d 5829 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  u )  ->  ( `' F `  x )  =  ( `' F `  u ) )
107 simpr 462 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  u )  ->  y  =  u )
108107fveq2d 5829 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  u )  ->  ( `' F `  y )  =  ( `' F `  u ) )
109106, 108oveq12d 6267 . . . . . . . . . . . 12  |-  ( ( x  =  u  /\  y  =  u )  ->  ( ( `' F `  x ) G ( `' F `  y ) )  =  ( ( `' F `  u ) G ( `' F `  u ) ) )
110109cnveqd 4972 . . . . . . . . . . 11  |-  ( ( x  =  u  /\  y  =  u )  ->  `' ( ( `' F `  x ) G ( `' F `  y ) )  =  `' ( ( `' F `  u ) G ( `' F `  u ) ) )
111 ovex 6277 . . . . . . . . . . . 12  |-  ( ( `' F `  u ) G ( `' F `  u ) )  e. 
_V
112111cnvex 6698 . . . . . . . . . . 11  |-  `' ( ( `' F `  u ) G ( `' F `  u ) )  e.  _V
113110, 17, 112ovmpt2a 6385 . . . . . . . . . 10  |-  ( ( u  e.  S  /\  u  e.  S )  ->  ( u H u )  =  `' ( ( `' F `  u ) G ( `' F `  u ) ) )
114104, 104, 113syl2anc 665 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  S )  ->  (
u H u )  =  `' ( ( `' F `  u ) G ( `' F `  u ) ) )
115114fveq1d 5827 . . . . . . . 8  |-  ( (
ph  /\  u  e.  S )  ->  (
( u H u ) `  ( ( Id `  Y ) `
 u ) )  =  ( `' ( ( `' F `  u ) G ( `' F `  u ) ) `  ( ( Id `  Y ) `
 u ) ) )
11651adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  S )  ->  F
( X  Func  Y
) G )
11730, 54, 53, 116, 75funcid 15718 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  S )  ->  (
( ( `' F `  u ) G ( `' F `  u ) ) `  ( ( Id `  X ) `
 ( `' F `  u ) ) )  =  ( ( Id
`  Y ) `  ( F `  ( `' F `  u ) ) ) )
1181, 95sylan 473 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  S )  ->  ( F `  ( `' F `  u )
)  =  u )
119118fveq2d 5829 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  S )  ->  (
( Id `  Y
) `  ( F `  ( `' F `  u ) ) )  =  ( ( Id
`  Y ) `  u ) )
120117, 119eqtrd 2462 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  S )  ->  (
( ( `' F `  u ) G ( `' F `  u ) ) `  ( ( Id `  X ) `
 ( `' F `  u ) ) )  =  ( ( Id
`  Y ) `  u ) )
12133adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  S )  ->  F
( ( X Full  Y
)  i^i  ( X Faith  Y ) ) G )
12230, 31, 32, 121, 75, 75ffthf1o 15767 . . . . . . . . . 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 466 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  S )  ->  X  e.  Cat )
12430, 31, 54, 123, 75catidcl 15531 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  S )  ->  (
( Id `  X
) `  ( `' F `  u )
)  e.  ( ( `' F `  u ) ( Hom  `  X
) ( `' F `  u ) ) )
125 f1ocnvfv 6136 . . . . . . . . . 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 665 . . . . . . . . 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 2462 . . . . . . 7  |-  ( (
ph  /\  u  e.  S )  ->  (
( u H u ) `  ( ( Id `  Y ) `
 u ) )  =  ( ( Id
`  X ) `  ( `' F `  u ) ) )
129513ad2ant1 1026 . . . . . . . . . . 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 1026 . . . . . . . . . . . 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 1038 . . . . . . . . . . . 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 5982 . . . . . . . . . . 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 1039 . . . . . . . . . . . 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 5982 . . . . . . . . . . 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 1040 . . . . . . . . . . . 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 5982 . . . . . . . . . . 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 1026 . . . . . . . . . . . . . . 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 15767 . . . . . . . . . . . . . 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 1026 . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . 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 6267 . . . . . . . . . . . . . . 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 5767 . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . 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 5786 . . . . . . . . . . . . 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 5774 . . . . . . . . . . . . 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 18 . . . . . . . . . . . 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 1033 . . . . . . . . . . . 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 5982 . . . . . . . . . . 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 15767 . . . . . . . . . . . . . 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 6135 . . . . . . . . . . . . . . . . 17  |-  ( ( F : R -1-1-onto-> S  /\  z  e.  S )  ->  ( F `  ( `' F `  z ) )  =  z )
153139, 135, 152syl2anc 665 . . . . . . . . . . . . . . . 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 6267 . . . . . . . . . . . . . . 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 5767 . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . 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 5786 . . . . . . . . . . . . 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 5774 . . . . . . . . . . . . 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 18 . . . . . . . . . . . 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 1034 . . . . . . . . . . . 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 5982 . . . . . . . . . . 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 15719 . . . . . . . . . 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 4138 . . . . . . . . . . . 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 6267 . . . . . . . . . . 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 6135 . . . . . . . . . . . 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 665 . . . . . . . . . . 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 6135 . . . . . . . . . . . 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 665 . . . . . . . . . . 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 6270 . . . . . . . . . 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 2462 . . . . . . . . 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 15767 . . . . . . . . . . 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 6267 . . . . . . . . . . . 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 5767 . . . . . . . . . . . 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 17 . . . . . . . . . . 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 213 . . . . . . . . . 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 1026 . . . . . . . . . . 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 15534 . . . . . . . . . 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 6136 . . . . . . . . . 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 665 . . . . . . . . 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 458 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  z )  ->  x  =  u )
183182fveq2d 5829 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  z )  ->  ( `' F `  x )  =  ( `' F `  u ) )
184 simpr 462 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  z )  ->  y  =  z )
185184fveq2d 5829 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  z )  ->  ( `' F `  y )  =  ( `' F `  z ) )
186183, 185oveq12d 6267 . . . . . . . . . . . 12  |-  ( ( x  =  u  /\  y  =  z )  ->  ( ( `' F `  x ) G ( `' F `  y ) )  =  ( ( `' F `  u ) G ( `' F `  z ) ) )
187186cnveqd 4972 . . . . . . . . . . 11  |-  ( ( x  =  u  /\  y  =  z )  ->  `' ( ( `' F `  x ) G ( `' F `  y ) )  =  `' ( ( `' F `  u ) G ( `' F `  z ) ) )
188 ovex 6277 . . . . . . . . . . . 12  |-  ( ( `' F `  u ) G ( `' F `  z ) )  e. 
_V
189188cnvex 6698 . . . . . . . . . . 11  |-  `' ( ( `' F `  u ) G ( `' F `  z ) )  e.  _V
190187, 17, 189ovmpt2a 6385 . . . . . . . . . 10  |-  ( ( u  e.  S  /\  z  e.  S )  ->  ( u H z )  =  `' ( ( `' F `  u ) G ( `' F `  z ) ) )
191131, 135, 190syl2anc 665 . . . . . . . . 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 5827 . . . . . . . 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 458 . . . . . . . . . . . . . . 15  |-  ( ( x  =  v  /\  y  =  z )  ->  x  =  v )
194193fveq2d 5829 . . . . . . . . . . . . . 14  |-  ( ( x  =  v  /\  y  =  z )  ->  ( `' F `  x )  =  ( `' F `  v ) )
195 simpr 462 . . . . . . . . . . . . . . 15  |-  ( ( x  =  v  /\  y  =  z )  ->  y  =  z )
196195fveq2d 5829 . . . . . . . . . . . . . 14  |-  ( ( x  =  v  /\  y  =  z )  ->  ( `' F `  y )  =  ( `' F `  z ) )
197194, 196oveq12d 6267 . . . . . . . . . . . . 13  |-  ( ( x  =  v  /\  y  =  z )  ->  ( ( `' F `  x ) G ( `' F `  y ) )  =  ( ( `' F `  v ) G ( `' F `  z ) ) )
198197cnveqd 4972 . . . . . . . . . . . 12  |-  ( ( x  =  v  /\  y  =  z )  ->  `' ( ( `' F `  x ) G ( `' F `  y ) )  =  `' ( ( `' F `  v ) G ( `' F `  z ) ) )
199 ovex 6277 . . . . . . . . . . . . 13  |-  ( ( `' F `  v ) G ( `' F `  z ) )  e. 
_V
200199cnvex 6698 . . . . . . . . . . . 12  |-  `' ( ( `' F `  v ) G ( `' F `  z ) )  e.  _V
201198, 17, 200ovmpt2a 6385 . . . . . . . . . . 11  |-  ( ( v  e.  S  /\  z  e.  S )  ->  ( v H z )  =  `' ( ( `' F `  v ) G ( `' F `  z ) ) )
202133, 135, 201syl2anc 665 . . . . . . . . . 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 5827 . . . . . . . . 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 665 . . . . . . . . . 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 5827 . . . . . . . . 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 6267 . . . . . . . 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 2472 . . . . . . 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 15713 . . . . . 6  |-  ( ph  ->  `' F ( Y  Func  X ) H )
20930, 51, 208cofuval2 15735 . . . . 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 2428 . . . . . 6  |-  (idfunc `  X
)  =  (idfunc `  X
)
211210, 30, 66, 31idfuval 15724 . . . . 5  |-  ( ph  ->  (idfunc `  X )  =  <. (  _I  |`  R ) ,  ( z  e.  ( R  X.  R
)  |->  (  _I  |`  (
( Hom  `  X ) `
 z ) ) ) >. )
21246, 209, 2113eqtr4d 2472 . . . 4  |-  ( ph  ->  ( <. `' F ,  H >.  o.func 
<. F ,  G >. )  =  (idfunc `  X ) )
213 eqid 2428 . . . . 5  |-  (comp `  C )  =  (comp `  C )
214 df-br 4367 . . . . . 6  |-  ( F ( X  Func  Y
) G  <->  <. F ,  G >.  e.  ( X 
Func  Y ) )
21551, 214sylib 199 . . . . 5  |-  ( ph  -> 
<. F ,  G >.  e.  ( X  Func  Y
) )
216 df-br 4367 . . . . . 6  |-  ( `' F ( Y  Func  X ) H  <->  <. `' F ,  H >.  e.  ( Y  Func  X ) )
217208, 216sylib 199 . . . . 5  |-  ( ph  -> 
<. `' F ,  H >.  e.  ( Y  Func  X
) )
21857, 58, 59, 213, 65, 63, 65, 215, 217catcco 15939 . . . 4  |-  ( ph  ->  ( <. `' F ,  H >. ( <. X ,  Y >. (comp `  C
) X ) <. F ,  G >. )  =  ( <. `' F ,  H >.  o.func 
<. F ,  G >. ) )
219 eqid 2428 . . . . 5  |-  ( Id
`  C )  =  ( Id `  C
)
22057, 58, 219, 210, 59, 65catcid 15941 . . . 4  |-  ( ph  ->  ( ( Id `  C ) `  X
)  =  (idfunc `  X
) )
221212, 218, 2203eqtr4d 2472 . . 3  |-  ( ph  ->  ( <. `' F ,  H >. ( <. X ,  Y >. (comp `  C
) X ) <. F ,  G >. )  =  ( ( Id
`  C ) `  X ) )
222 eqid 2428 . . . 4  |-  ( Hom  `  C )  =  ( Hom  `  C )
223 eqid 2428 . . . 4  |-  (Sect `  C )  =  (Sect `  C )
22457catccat 15942 . . . . 5  |-  ( U  e.  V  ->  C  e.  Cat )
22559, 224syl 17 . . . 4  |-  ( ph  ->  C  e.  Cat )
22657, 58, 59, 222, 65, 63catchom 15937 . . . . 5  |-  ( ph  ->  ( X ( Hom  `  C ) Y )  =  ( X  Func  Y ) )
227215, 226eleqtrrd 2509 . . . 4  |-  ( ph  -> 
<. F ,  G >.  e.  ( X ( Hom  `  C ) Y ) )
22857, 58, 59, 222, 63, 65catchom 15937 . . . . 5  |-  ( ph  ->  ( Y ( Hom  `  C ) X )  =  ( Y  Func  X ) )
229217, 228eleqtrrd 2509 . . . 4  |-  ( ph  -> 
<. `' F ,  H >.  e.  ( Y ( Hom  `  C ) X ) )
23058, 222, 213, 219, 223, 225, 65, 63, 227, 229issect2 15602 . . 3  |-  ( ph  ->  ( <. F ,  G >. ( X (Sect `  C ) Y )
<. `' F ,  H >.  <->  ( <. `' F ,  H >. (
<. X ,  Y >. (comp `  C ) X )
<. F ,  G >. )  =  ( ( Id
`  C ) `  X ) ) )
231221, 230mpbird 235 . 2  |-  ( ph  -> 
<. F ,  G >. ( X (Sect `  C
) Y ) <. `' F ,  H >. )
232 f1ococnv2 5800 . . . . . . 7  |-  ( F : R -1-1-onto-> S  ->  ( F  o.  `' F )  =  (  _I  |`  S )
)
2331, 232syl 17 . . . . . 6  |-  ( ph  ->  ( F  o.  `' F )  =  (  _I  |`  S )
)
234913adant1 1023 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  ( u H v )  =  `' ( ( `' F `  u ) G ( `' F `  v ) ) )
235234coeq2d 4959 . . . . . . . . 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 1026 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  F (
( X Full  Y )  i^i  ( X Faith  Y ) ) G )
237753adant3 1025 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  ( `' F `  u )  e.  R )
238773adant2 1024 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  ( `' F `  v )  e.  R )
23930, 31, 32, 236, 237, 238ffthf1o 15767 . . . . . . . . . . 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 1201 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  ( ( F `  ( `' F `  u )
) ( Hom  `  Y
) ( F `  ( `' F `  v ) ) )  =  ( u ( Hom  `  Y
) v ) )
241240, 143syl 17 . . . . . . . . . . 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 213 . . . . . . . . . 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 5800 . . . . . . . . . 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 17 . . . . . . . . 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 2462 . . . . . . . 8  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  ( (
( `' F `  u ) G ( `' F `  v ) )  o.  ( u H v ) )  =  (  _I  |`  (
u ( Hom  `  Y
) v ) ) )
246245mpt2eq3dva 6313 . . . . . . 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 5825 . . . . . . . . . 10  |-  ( z  =  <. u ,  v
>.  ->  ( ( Hom  `  Y ) `  z
)  =  ( ( Hom  `  Y ) `  <. u ,  v
>. ) )
248 df-ov 6252 . . . . . . . . . 10  |-  ( u ( Hom  `  Y
) v )  =  ( ( Hom  `  Y
) `  <. u ,  v >. )
249247, 248syl6eqr 2480 . . . . . . . . 9  |-  ( z  =  <. u ,  v
>.  ->  ( ( Hom  `  Y ) `  z
)  =  ( u ( Hom  `  Y
) v ) )
250249reseq2d 5067 . . . . . . . 8  |-  ( z  =  <. u ,  v
>.  ->  (  _I  |`  (
( Hom  `  Y ) `
 z ) )  =  (  _I  |`  (
u ( Hom  `  Y
) v ) ) )
251250mpt2mpt 6346 . . . . . . 7  |-  ( z  e.  ( S  X.  S )  |->  (  _I  |`  ( ( Hom  `  Y
) `  z )
) )  =  ( u  e.  S , 
v  e.  S  |->  (  _I  |`  ( u
( Hom  `  Y ) v ) ) )
252246, 251syl6eqr 2480 . . . . . 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 4138 . . . . 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 15735 . . . . 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 2428 . . . . . 6  |-  (idfunc `  Y
)  =  (idfunc `  Y
)
256255, 52, 64, 32idfuval 15724 . . . . 5  |-  ( ph  ->  (idfunc `  Y )  =  <. (  _I  |`  S ) ,  ( z  e.  ( S  X.  S
)  |->  (  _I  |`  (
( Hom  `  Y ) `
 z ) ) ) >. )
257253, 254, 2563eqtr4d 2472 . . . 4  |-  ( ph  ->  ( <. F ,  G >.  o.func 
<. `' F ,  H >. )  =  (idfunc `  Y ) )
25857, 58, 59, 213, 63, 65, 63, 217, 215catcco 15939 . . . 4  |-  ( ph  ->  ( <. F ,  G >. ( <. Y ,  X >. (comp `  C ) Y ) <. `' F ,  H >. )  =  (
<. F ,  G >.  o.func  <. `' F ,  H >. ) )
25957, 58, 219, 255, 59, 63catcid 15941 . . . 4  |-  ( ph  ->  ( ( Id `  C ) `  Y
)  =  (idfunc `  Y
) )
260257, 258, 2593eqtr4d 2472 . . 3  |-  ( ph  ->  ( <. F ,  G >. ( <. Y ,  X >. (comp `  C ) Y ) <. `' F ,  H >. )  =  ( ( Id `  C
) `  Y )
)
26158, 222, 213, 219, 223, 225, 63, 65, 229, 227issect2 15602 . . 3  |-  ( ph  ->  ( <. `' F ,  H >. ( Y (Sect `  C ) X )
<. F ,  G >.  <->  ( <. F ,  G >. (
<. Y ,  X >. (comp `  C ) Y )
<. `' F ,  H >. )  =  ( ( Id
`  C ) `  Y ) ) )
262260, 261mpbird 235 . 2  |-  ( ph  -> 
<. `' F ,  H >. ( Y (Sect `  C
) X ) <. F ,  G >. )
263 catcisolem.i . . 3  |-  I  =  (Inv `  C )
26458, 263, 225, 65, 63, 223isinv 15608 . 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 930 1  |-  ( ph  -> 
<. F ,  G >. ( X I Y )
<. `' F ,  H >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1872    i^i cin 3378   <.cop 3947   class class class wbr 4366    |-> cmpt 4425    _I cid 4706    X. cxp 4794   `'ccnv 4795    |` cres 4798    o. ccom 4800    Fn wfn 5539   -->wf 5540   -1-1-onto->wf1o 5543   ` cfv 5544  (class class class)co 6249    |-> cmpt2 6251   Basecbs 15064   Hom chom 15144  compcco 15145   Catccat 15513   Idccid 15514  Sectcsect 15592  Invcinv 15593    Func cfunc 15702  idfunccidfu 15703    o.func ccofu 15704   Full cful 15750   Faith cfth 15751  CatCatccatc 15932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-rep 4479  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541  ax-cnex 9546  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566  ax-pre-mulgt0 9567
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-nel 2602  df-ral 2719  df-rex 2720  df-reu 2721  df-rmo 2722  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-pss 3395  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-tp 3946  df-op 3948  df-uni 4163  df-int 4199  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-tr 4462  df-eprel 4707  df-id 4711  df-po 4717  df-so 4718  df-fr 4755  df-we 4757  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-pred 5342  df-ord 5388  df-on 5389  df-lim 5390  df-suc 5391  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-riota 6211  df-ov 6252  df-oprab 6253  df-mpt2 6254  df-om 6651  df-1st 6751  df-2nd 6752  df-wrecs 6983  df-recs 7045  df-rdg 7083  df-1o 7137  df-oadd 7141  df-er 7318  df-map 7429  df-ixp 7478  df-en 7525  df-dom 7526  df-sdom 7527  df-fin 7528  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632  df-sub 9813  df-neg 9814  df-nn 10561  df-2 10619  df-3 10620  df-4 10621  df-5 10622  df-6 10623  df-7 10624  df-8 10625  df-9 10626  df-10 10627  df-n0 10821  df-z 10889  df-dec 11003  df-uz 11111  df-fz 11736  df-struct 15066  df-ndx 15067  df-slot 15068  df-base 15069  df-hom 15157  df-cco 15158  df-cat 15517  df-cid 15518  df-sect 15595  df-inv 15596  df-func 15706  df-idfu 15707  df-cofu 15708  df-full 15752  df-fth 15753  df-catc 15933
This theorem is referenced by:  catciso  15945
  Copyright terms: Public domain W3C validator