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

Theorem catcisolem 15092
Description: Lemma for catciso 15093. (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 5776 . . . . . . 7  |-  ( F : R -1-1-onto-> S  ->  ( `' F  o.  F )  =  (  _I  |`  R ) )
31, 2syl 16 . . . . . 6  |-  ( ph  ->  ( `' F  o.  F )  =  (  _I  |`  R )
)
413ad2ant1 1009 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  F : R
-1-1-onto-> S )
5 f1of 5748 . . . . . . . . . . . . . 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 989 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  u  e.  R )
86, 7ffvelrnd 5952 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( F `  u )  e.  S
)
9 simp3 990 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  v  e.  R )
106, 9ffvelrnd 5952 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( F `  v )  e.  S
)
11 simpl 457 . . . . . . . . . . . . . . . 16  |-  ( ( x  =  ( F `
 u )  /\  y  =  ( F `  v ) )  ->  x  =  ( F `  u ) )
1211fveq2d 5802 . . . . . . . . . . . . . . 15  |-  ( ( x  =  ( F `
 u )  /\  y  =  ( F `  v ) )  -> 
( `' F `  x )  =  ( `' F `  ( F `
 u ) ) )
13 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( ( x  =  ( F `
 u )  /\  y  =  ( F `  v ) )  -> 
y  =  ( F `
 v ) )
1413fveq2d 5802 . . . . . . . . . . . . . . 15  |-  ( ( x  =  ( F `
 u )  /\  y  =  ( F `  v ) )  -> 
( `' F `  y )  =  ( `' F `  ( F `
 v ) ) )
1512, 14oveq12d 6217 . . . . . . . . . . . . . 14  |-  ( ( x  =  ( F `
 u )  /\  y  =  ( F `  v ) )  -> 
( ( `' F `  x ) G ( `' F `  y ) )  =  ( ( `' F `  ( F `
 u ) ) G ( `' F `  ( F `  v
) ) ) )
1615cnveqd 5122 . . . . . . . . . . . . 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 6224 . . . . . . . . . . . . . 14  |-  ( ( `' F `  ( F `
 u ) ) G ( `' F `  ( F `  v
) ) )  e. 
_V
1918cnvex 6634 . . . . . . . . . . . . 13  |-  `' ( ( `' F `  ( F `  u ) ) G ( `' F `  ( F `
 v ) ) )  e.  _V
2016, 17, 19ovmpt2a 6330 . . . . . . . . . . . 12  |-  ( ( ( F `  u
)  e.  S  /\  ( F `  v )  e.  S )  -> 
( ( F `  u ) H ( F `  v ) )  =  `' ( ( `' F `  ( F `  u ) ) G ( `' F `  ( F `
 v ) ) ) )
218, 10, 20syl2anc 661 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( ( F `  u ) H ( F `  v ) )  =  `' ( ( `' F `  ( F `
 u ) ) G ( `' F `  ( F `  v
) ) ) )
22 f1ocnvfv1 6091 . . . . . . . . . . . . . 14  |-  ( ( F : R -1-1-onto-> S  /\  u  e.  R )  ->  ( `' F `  ( F `  u ) )  =  u )
234, 7, 22syl2anc 661 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( `' F `  ( F `  u ) )  =  u )
24 f1ocnvfv1 6091 . . . . . . . . . . . . . 14  |-  ( ( F : R -1-1-onto-> S  /\  v  e.  R )  ->  ( `' F `  ( F `  v ) )  =  v )
254, 9, 24syl2anc 661 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( `' F `  ( F `  v ) )  =  v )
2623, 25oveq12d 6217 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( ( `' F `  ( F `
 u ) ) G ( `' F `  ( F `  v
) ) )  =  ( u G v ) )
2726cnveqd 5122 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  `' (
( `' F `  ( F `  u ) ) G ( `' F `  ( F `
 v ) ) )  =  `' ( u G v ) )
2821, 27eqtrd 2495 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( ( F `  u ) H ( F `  v ) )  =  `' ( u G v ) )
2928coeq1d 5108 . . . . . . . . 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 2454 . . . . . . . . . . 11  |-  ( Hom  `  X )  =  ( Hom  `  X )
32 eqid 2454 . . . . . . . . . . 11  |-  ( Hom  `  Y )  =  ( Hom  `  Y )
33 catcisolem.1 . . . . . . . . . . . 12  |-  ( ph  ->  F ( ( X Full 
Y )  i^i  ( X Faith  Y ) ) G )
34333ad2ant1 1009 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  F (
( X Full  Y )  i^i  ( X Faith  Y ) ) G )
3530, 31, 32, 34, 7, 9ffthf1o 14947 . . . . . . . . . 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 5776 . . . . . . . . . 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 2495 . . . . . . . 8  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( (
( F `  u
) H ( F `
 v ) )  o.  ( u G v ) )  =  (  _I  |`  (
u ( Hom  `  X
) v ) ) )
3938mpt2eq3dva 6258 . . . . . . 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 5798 . . . . . . . . . 10  |-  ( z  =  <. u ,  v
>.  ->  ( ( Hom  `  X ) `  z
)  =  ( ( Hom  `  X ) `  <. u ,  v
>. ) )
41 df-ov 6202 . . . . . . . . . 10  |-  ( u ( Hom  `  X
) v )  =  ( ( Hom  `  X
) `  <. u ,  v >. )
4240, 41syl6eqr 2513 . . . . . . . . 9  |-  ( z  =  <. u ,  v
>.  ->  ( ( Hom  `  X ) `  z
)  =  ( u ( Hom  `  X
) v ) )
4342reseq2d 5217 . . . . . . . 8  |-  ( z  =  <. u ,  v
>.  ->  (  _I  |`  (
( Hom  `  X ) `
 z ) )  =  (  _I  |`  (
u ( Hom  `  X
) v ) ) )
4443mpt2mpt 6291 . . . . . . 7  |-  ( z  e.  ( R  X.  R )  |->  (  _I  |`  ( ( Hom  `  X
) `  z )
) )  =  ( u  e.  R , 
v  e.  R  |->  (  _I  |`  ( u
( Hom  `  X ) v ) ) )
4539, 44syl6eqr 2513 . . . . . 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 4174 . . . . 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 3677 . . . . . . . . 9  |-  ( ( X Full  Y )  i^i  ( X Faith  Y ) )  C_  ( X Full  Y )
48 fullfunc 14934 . . . . . . . . 9  |-  ( X Full 
Y )  C_  ( X  Func  Y )
4947, 48sstri 3472 . . . . . . . 8  |-  ( ( X Full  Y )  i^i  ( X Faith  Y ) )  C_  ( X  Func  Y )
5049ssbri 4441 . . . . . . 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 2454 . . . . . . 7  |-  ( Id
`  Y )  =  ( Id `  Y
)
54 eqid 2454 . . . . . . 7  |-  ( Id
`  X )  =  ( Id `  X
)
55 eqid 2454 . . . . . . 7  |-  (comp `  Y )  =  (comp `  Y )
56 eqid 2454 . . . . . . 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 15083 . . . . . . . . 9  |-  ( ph  ->  B  =  ( U  i^i  Cat ) )
61 inss2 3678 . . . . . . . . 9  |-  ( U  i^i  Cat )  C_  Cat
6260, 61syl6eqss 3513 . . . . . . . 8  |-  ( ph  ->  B  C_  Cat )
63 catciso.y . . . . . . . 8  |-  ( ph  ->  Y  e.  B )
6462, 63sseldd 3464 . . . . . . 7  |-  ( ph  ->  Y  e.  Cat )
65 catciso.x . . . . . . . 8  |-  ( ph  ->  X  e.  B )
6662, 65sseldd 3464 . . . . . . 7  |-  ( ph  ->  X  e.  Cat )
67 f1ocnv 5760 . . . . . . . 8  |-  ( F : R -1-1-onto-> S  ->  `' F : S -1-1-onto-> R )
68 f1of 5748 . . . . . . . 8  |-  ( `' F : S -1-1-onto-> R  ->  `' F : S --> R )
691, 67, 683syl 20 . . . . . . 7  |-  ( ph  ->  `' F : S --> R )
70 ovex 6224 . . . . . . . . . 10  |-  ( ( `' F `  x ) G ( `' F `  y ) )  e. 
_V
7170cnvex 6634 . . . . . . . . 9  |-  `' ( ( `' F `  x ) G ( `' F `  y ) )  e.  _V
7217, 71fnmpt2i 6752 . . . . . . . 8  |-  H  Fn  ( S  X.  S
)
7372a1i 11 . . . . . . 7  |-  ( ph  ->  H  Fn  ( S  X.  S ) )
7433adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  ->  F ( ( X Full 
Y )  i^i  ( X Faith  Y ) ) G )
7569ffvelrnda 5951 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  S )  ->  ( `' F `  u )  e.  R )
7675adantrr 716 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( `' F `  u )  e.  R
)
7769ffvelrnda 5951 . . . . . . . . . . 11  |-  ( (
ph  /\  v  e.  S )  ->  ( `' F `  v )  e.  R )
7877adantrl 715 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( `' F `  v )  e.  R
)
7930, 31, 32, 74, 76, 78ffthf1o 14947 . . . . . . . . 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 5760 . . . . . . . . 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 5748 . . . . . . . . 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 20 . . . . . . . 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 457 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  v )  ->  x  =  u )
8483fveq2d 5802 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  v )  ->  ( `' F `  x )  =  ( `' F `  u ) )
85 simpr 461 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  v )  ->  y  =  v )
8685fveq2d 5802 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  v )  ->  ( `' F `  y )  =  ( `' F `  v ) )
8784, 86oveq12d 6217 . . . . . . . . . . . 12  |-  ( ( x  =  u  /\  y  =  v )  ->  ( ( `' F `  x ) G ( `' F `  y ) )  =  ( ( `' F `  u ) G ( `' F `  v ) ) )
8887cnveqd 5122 . . . . . . . . . . 11  |-  ( ( x  =  u  /\  y  =  v )  ->  `' ( ( `' F `  x ) G ( `' F `  y ) )  =  `' ( ( `' F `  u ) G ( `' F `  v ) ) )
89 ovex 6224 . . . . . . . . . . . 12  |-  ( ( `' F `  u ) G ( `' F `  v ) )  e. 
_V
9089cnvex 6634 . . . . . . . . . . 11  |-  `' ( ( `' F `  u ) G ( `' F `  v ) )  e.  _V
9188, 17, 90ovmpt2a 6330 . . . . . . . . . 10  |-  ( ( u  e.  S  /\  v  e.  S )  ->  ( u H v )  =  `' ( ( `' F `  u ) G ( `' F `  v ) ) )
9291adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( u H v )  =  `' ( ( `' F `  u ) G ( `' F `  v ) ) )
931adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  ->  F : R -1-1-onto-> S )
94 simprl 755 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  ->  u  e.  S )
95 f1ocnvfv2 6092 . . . . . . . . . . . 12  |-  ( ( F : R -1-1-onto-> S  /\  u  e.  S )  ->  ( F `  ( `' F `  u ) )  =  u )
9693, 94, 95syl2anc 661 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( F `  ( `' F `  u ) )  =  u )
97 simprr 756 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
v  e.  S )
98 f1ocnvfv2 6092 . . . . . . . . . . . 12  |-  ( ( F : R -1-1-onto-> S  /\  v  e.  S )  ->  ( F `  ( `' F `  v ) )  =  v )
9993, 97, 98syl2anc 661 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( F `  ( `' F `  v ) )  =  v )
10096, 99oveq12d 6217 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( ( F `  ( `' F `  u ) ) ( Hom  `  Y
) ( F `  ( `' F `  v ) ) )  =  ( u ( Hom  `  Y
) v ) )
101100eqcomd 2462 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( u ( Hom  `  Y ) v )  =  ( ( F `
 ( `' F `  u ) ) ( Hom  `  Y )
( F `  ( `' F `  v ) ) ) )
10292, 101feq12d 5655 . . . . . . . 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 232 . . . . . . 7  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( u H v ) : ( u ( Hom  `  Y
) v ) --> ( ( `' F `  u ) ( Hom  `  X ) ( `' F `  v ) ) )
104 simpr 461 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  S )  ->  u  e.  S )
105 simpl 457 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  u )  ->  x  =  u )
106105fveq2d 5802 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  u )  ->  ( `' F `  x )  =  ( `' F `  u ) )
107 simpr 461 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  u )  ->  y  =  u )
108107fveq2d 5802 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  u )  ->  ( `' F `  y )  =  ( `' F `  u ) )
109106, 108oveq12d 6217 . . . . . . . . . . . 12  |-  ( ( x  =  u  /\  y  =  u )  ->  ( ( `' F `  x ) G ( `' F `  y ) )  =  ( ( `' F `  u ) G ( `' F `  u ) ) )
110109cnveqd 5122 . . . . . . . . . . 11  |-  ( ( x  =  u  /\  y  =  u )  ->  `' ( ( `' F `  x ) G ( `' F `  y ) )  =  `' ( ( `' F `  u ) G ( `' F `  u ) ) )
111 ovex 6224 . . . . . . . . . . . 12  |-  ( ( `' F `  u ) G ( `' F `  u ) )  e. 
_V
112111cnvex 6634 . . . . . . . . . . 11  |-  `' ( ( `' F `  u ) G ( `' F `  u ) )  e.  _V
113110, 17, 112ovmpt2a 6330 . . . . . . . . . 10  |-  ( ( u  e.  S  /\  u  e.  S )  ->  ( u H u )  =  `' ( ( `' F `  u ) G ( `' F `  u ) ) )
114104, 104, 113syl2anc 661 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  S )  ->  (
u H u )  =  `' ( ( `' F `  u ) G ( `' F `  u ) ) )
115114fveq1d 5800 . . . . . . . 8  |-  ( (
ph  /\  u  e.  S )  ->  (
( u H u ) `  ( ( Id `  Y ) `
 u ) )  =  ( `' ( ( `' F `  u ) G ( `' F `  u ) ) `  ( ( Id `  Y ) `
 u ) ) )
11651adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  S )  ->  F
( X  Func  Y
) G )
11730, 54, 53, 116, 75funcid 14898 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  S )  ->  (
( ( `' F `  u ) G ( `' F `  u ) ) `  ( ( Id `  X ) `
 ( `' F `  u ) ) )  =  ( ( Id
`  Y ) `  ( F `  ( `' F `  u ) ) ) )
1181, 95sylan 471 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  S )  ->  ( F `  ( `' F `  u )
)  =  u )
119118fveq2d 5802 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  S )  ->  (
( Id `  Y
) `  ( F `  ( `' F `  u ) ) )  =  ( ( Id
`  Y ) `  u ) )
120117, 119eqtrd 2495 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  S )  ->  (
( ( `' F `  u ) G ( `' F `  u ) ) `  ( ( Id `  X ) `
 ( `' F `  u ) ) )  =  ( ( Id
`  Y ) `  u ) )
12133adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  S )  ->  F
( ( X Full  Y
)  i^i  ( X Faith  Y ) ) G )
12230, 31, 32, 121, 75, 75ffthf1o 14947 . . . . . . . . . 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 465 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  S )  ->  X  e.  Cat )
12430, 31, 54, 123, 75catidcl 14738 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  S )  ->  (
( Id `  X
) `  ( `' F `  u )
)  e.  ( ( `' F `  u ) ( Hom  `  X
) ( `' F `  u ) ) )
125 f1ocnvfv 6093 . . . . . . . . . 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 661 . . . . . . . . 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 2495 . . . . . . 7  |-  ( (
ph  /\  u  e.  S )  ->  (
( u H u ) `  ( ( Id `  Y ) `
 u ) )  =  ( ( Id
`  X ) `  ( `' F `  u ) ) )
129513ad2ant1 1009 . . . . . . . . . . 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 1009 . . . . . . . . . . . 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 1021 . . . . . . . . . . . 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 5952 . . . . . . . . . . 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 1022 . . . . . . . . . . . 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 5952 . . . . . . . . . . 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 1023 . . . . . . . . . . . 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 5952 . . . . . . . . . . 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 1009 . . . . . . . . . . . . . . 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 14947 . . . . . . . . . . . . . 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 1009 . . . . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . . . . 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 6217 . . . . . . . . . . . . . . 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 5741 . . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . 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 5760 . . . . . . . . . . . . 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 5748 . . . . . . . . . . . . 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 20 . . . . . . . . . . . 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 1016 . . . . . . . . . . . 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 5952 . . . . . . . . . . 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 14947 . . . . . . . . . . . . . 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 6092 . . . . . . . . . . . . . . . . 17  |-  ( ( F : R -1-1-onto-> S  /\  z  e.  S )  ->  ( F `  ( `' F `  z ) )  =  z )
153139, 135, 152syl2anc 661 . . . . . . . . . . . . . . . 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 6217 . . . . . . . . . . . . . . 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 5741 . . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . 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 5760 . . . . . . . . . . . . 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 5748 . . . . . . . . . . . . 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 20 . . . . . . . . . . . 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 1017 . . . . . . . . . . . 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 5952 . . . . . . . . . . 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 14899 . . . . . . . . . 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 4174 . . . . . . . . . . . 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 6217 . . . . . . . . . . 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 6092 . . . . . . . . . . . 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 661 . . . . . . . . . . 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 6092 . . . . . . . . . . . 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 661 . . . . . . . . . . 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 6220 . . . . . . . . . 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 2495 . . . . . . . . 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 14947 . . . . . . . . . . 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 6217 . . . . . . . . . . . 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 5741 . . . . . . . . . . . 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 210 . . . . . . . . . 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 1009 . . . . . . . . . . 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 14741 . . . . . . . . . 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 6093 . . . . . . . . . 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 661 . . . . . . . . 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 457 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  z )  ->  x  =  u )
183182fveq2d 5802 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  z )  ->  ( `' F `  x )  =  ( `' F `  u ) )
184 simpr 461 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  z )  ->  y  =  z )
185184fveq2d 5802 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  z )  ->  ( `' F `  y )  =  ( `' F `  z ) )
186183, 185oveq12d 6217 . . . . . . . . . . . 12  |-  ( ( x  =  u  /\  y  =  z )  ->  ( ( `' F `  x ) G ( `' F `  y ) )  =  ( ( `' F `  u ) G ( `' F `  z ) ) )
187186cnveqd 5122 . . . . . . . . . . 11  |-  ( ( x  =  u  /\  y  =  z )  ->  `' ( ( `' F `  x ) G ( `' F `  y ) )  =  `' ( ( `' F `  u ) G ( `' F `  z ) ) )
188 ovex 6224 . . . . . . . . . . . 12  |-  ( ( `' F `  u ) G ( `' F `  z ) )  e. 
_V
189188cnvex 6634 . . . . . . . . . . 11  |-  `' ( ( `' F `  u ) G ( `' F `  z ) )  e.  _V
190187, 17, 189ovmpt2a 6330 . . . . . . . . . 10  |-  ( ( u  e.  S  /\  z  e.  S )  ->  ( u H z )  =  `' ( ( `' F `  u ) G ( `' F `  z ) ) )
191131, 135, 190syl2anc 661 . . . . . . . . 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 5800 . . . . . . . 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 457 . . . . . . . . . . . . . . 15  |-  ( ( x  =  v  /\  y  =  z )  ->  x  =  v )
194193fveq2d 5802 . . . . . . . . . . . . . 14  |-  ( ( x  =  v  /\  y  =  z )  ->  ( `' F `  x )  =  ( `' F `  v ) )
195 simpr 461 . . . . . . . . . . . . . . 15  |-  ( ( x  =  v  /\  y  =  z )  ->  y  =  z )
196195fveq2d 5802 . . . . . . . . . . . . . 14  |-  ( ( x  =  v  /\  y  =  z )  ->  ( `' F `  y )  =  ( `' F `  z ) )
197194, 196oveq12d 6217 . . . . . . . . . . . . 13  |-  ( ( x  =  v  /\  y  =  z )  ->  ( ( `' F `  x ) G ( `' F `  y ) )  =  ( ( `' F `  v ) G ( `' F `  z ) ) )
198197cnveqd 5122 . . . . . . . . . . . 12  |-  ( ( x  =  v  /\  y  =  z )  ->  `' ( ( `' F `  x ) G ( `' F `  y ) )  =  `' ( ( `' F `  v ) G ( `' F `  z ) ) )
199 ovex 6224 . . . . . . . . . . . . 13  |-  ( ( `' F `  v ) G ( `' F `  z ) )  e. 
_V
200199cnvex 6634 . . . . . . . . . . . 12  |-  `' ( ( `' F `  v ) G ( `' F `  z ) )  e.  _V
201198, 17, 200ovmpt2a 6330 . . . . . . . . . . 11  |-  ( ( v  e.  S  /\  z  e.  S )  ->  ( v H z )  =  `' ( ( `' F `  v ) G ( `' F `  z ) ) )
202133, 135, 201syl2anc 661 . . . . . . . . . 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 5800 . . . . . . . . 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 661 . . . . . . . . . 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 5800 . . . . . . . . 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 6217 . . . . . . . 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 2505 . . . . . . 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 14893 . . . . . 6  |-  ( ph  ->  `' F ( Y  Func  X ) H )
20930, 51, 208cofuval2 14915 . . . . 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 2454 . . . . . 6  |-  (idfunc `  X
)  =  (idfunc `  X
)
211210, 30, 66, 31idfuval 14904 . . . . 5  |-  ( ph  ->  (idfunc `  X )  =  <. (  _I  |`  R ) ,  ( z  e.  ( R  X.  R
)  |->  (  _I  |`  (
( Hom  `  X ) `
 z ) ) ) >. )
21246, 209, 2113eqtr4d 2505 . . . 4  |-  ( ph  ->  ( <. `' F ,  H >.  o.func 
<. F ,  G >. )  =  (idfunc `  X ) )
213 eqid 2454 . . . . 5  |-  (comp `  C )  =  (comp `  C )
214 df-br 4400 . . . . . 6  |-  ( F ( X  Func  Y
) G  <->  <. F ,  G >.  e.  ( X 
Func  Y ) )
21551, 214sylib 196 . . . . 5  |-  ( ph  -> 
<. F ,  G >.  e.  ( X  Func  Y
) )
216 df-br 4400 . . . . . 6  |-  ( `' F ( Y  Func  X ) H  <->  <. `' F ,  H >.  e.  ( Y  Func  X ) )
217208, 216sylib 196 . . . . 5  |-  ( ph  -> 
<. `' F ,  H >.  e.  ( Y  Func  X
) )
21857, 58, 59, 213, 65, 63, 65, 215, 217catcco 15087 . . . 4  |-  ( ph  ->  ( <. `' F ,  H >. ( <. X ,  Y >. (comp `  C
) X ) <. F ,  G >. )  =  ( <. `' F ,  H >.  o.func 
<. F ,  G >. ) )
219 eqid 2454 . . . . 5  |-  ( Id
`  C )  =  ( Id `  C
)
22057, 58, 219, 210, 59, 65catcid 15089 . . . 4  |-  ( ph  ->  ( ( Id `  C ) `  X
)  =  (idfunc `  X
) )
221212, 218, 2203eqtr4d 2505 . . 3  |-  ( ph  ->  ( <. `' F ,  H >. ( <. X ,  Y >. (comp `  C
) X ) <. F ,  G >. )  =  ( ( Id
`  C ) `  X ) )
222 eqid 2454 . . . 4  |-  ( Hom  `  C )  =  ( Hom  `  C )
223 eqid 2454 . . . 4  |-  (Sect `  C )  =  (Sect `  C )
22457catccat 15090 . . . . 5  |-  ( U  e.  V  ->  C  e.  Cat )
22559, 224syl 16 . . . 4  |-  ( ph  ->  C  e.  Cat )
22657, 58, 59, 222, 65, 63catchom 15085 . . . . 5  |-  ( ph  ->  ( X ( Hom  `  C ) Y )  =  ( X  Func  Y ) )
227215, 226eleqtrrd 2545 . . . 4  |-  ( ph  -> 
<. F ,  G >.  e.  ( X ( Hom  `  C ) Y ) )
22857, 58, 59, 222, 63, 65catchom 15085 . . . . 5  |-  ( ph  ->  ( Y ( Hom  `  C ) X )  =  ( Y  Func  X ) )
229217, 228eleqtrrd 2545 . . . 4  |-  ( ph  -> 
<. `' F ,  H >.  e.  ( Y ( Hom  `  C ) X ) )
23058, 222, 213, 219, 223, 225, 65, 63, 227, 229issect2 14811 . . 3  |-  ( ph  ->  ( <. F ,  G >. ( X (Sect `  C ) Y )
<. `' F ,  H >.  <->  ( <. `' F ,  H >. (
<. X ,  Y >. (comp `  C ) X )
<. F ,  G >. )  =  ( ( Id
`  C ) `  X ) ) )
231221, 230mpbird 232 . 2  |-  ( ph  -> 
<. F ,  G >. ( X (Sect `  C
) Y ) <. `' F ,  H >. )
232 f1ococnv2 5774 . . . . . . 7  |-  ( F : R -1-1-onto-> S  ->  ( F  o.  `' F )  =  (  _I  |`  S )
)
2331, 232syl 16 . . . . . 6  |-  ( ph  ->  ( F  o.  `' F )  =  (  _I  |`  S )
)
234913adant1 1006 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  ( u H v )  =  `' ( ( `' F `  u ) G ( `' F `  v ) ) )
235234coeq2d 5109 . . . . . . . . 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 1009 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  F (
( X Full  Y )  i^i  ( X Faith  Y ) ) G )
237753adant3 1008 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  ( `' F `  u )  e.  R )
238773adant2 1007 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  ( `' F `  v )  e.  R )
23930, 31, 32, 236, 237, 238ffthf1o 14947 . . . . . . . . . . 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 1184 . . . . . . . . . . . 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 210 . . . . . . . . . 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 5774 . . . . . . . . . 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 2495 . . . . . . . 8  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  ( (
( `' F `  u ) G ( `' F `  v ) )  o.  ( u H v ) )  =  (  _I  |`  (
u ( Hom  `  Y
) v ) ) )
246245mpt2eq3dva 6258 . . . . . . 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 5798 . . . . . . . . . 10  |-  ( z  =  <. u ,  v
>.  ->  ( ( Hom  `  Y ) `  z
)  =  ( ( Hom  `  Y ) `  <. u ,  v
>. ) )
248 df-ov 6202 . . . . . . . . . 10  |-  ( u ( Hom  `  Y
) v )  =  ( ( Hom  `  Y
) `  <. u ,  v >. )
249247, 248syl6eqr 2513 . . . . . . . . 9  |-  ( z  =  <. u ,  v
>.  ->  ( ( Hom  `  Y ) `  z
)  =  ( u ( Hom  `  Y
) v ) )
250249reseq2d 5217 . . . . . . . 8  |-  ( z  =  <. u ,  v
>.  ->  (  _I  |`  (
( Hom  `  Y ) `
 z ) )  =  (  _I  |`  (
u ( Hom  `  Y
) v ) ) )
251250mpt2mpt 6291 . . . . . . 7  |-  ( z  e.  ( S  X.  S )  |->  (  _I  |`  ( ( Hom  `  Y
) `  z )
) )  =  ( u  e.  S , 
v  e.  S  |->  (  _I  |`  ( u
( Hom  `  Y ) v ) ) )
252246, 251syl6eqr 2513 . . . . . 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 4174 . . . . 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 14915 . . . . 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 2454 . . . . . 6  |-  (idfunc `  Y
)  =  (idfunc `  Y
)
256255, 52, 64, 32idfuval 14904 . . . . 5  |-  ( ph  ->  (idfunc `  Y )  =  <. (  _I  |`  S ) ,  ( z  e.  ( S  X.  S
)  |->  (  _I  |`  (
( Hom  `  Y ) `
 z ) ) ) >. )
257253, 254, 2563eqtr4d 2505 . . . 4  |-  ( ph  ->  ( <. F ,  G >.  o.func 
<. `' F ,  H >. )  =  (idfunc `  Y ) )
25857, 58, 59, 213, 63, 65, 63, 217, 215catcco 15087 . . . 4  |-  ( ph  ->  ( <. F ,  G >. ( <. Y ,  X >. (comp `  C ) Y ) <. `' F ,  H >. )  =  (
<. F ,  G >.  o.func  <. `' F ,  H >. ) )
25957, 58, 219, 255, 59, 63catcid 15089 . . . 4  |-  ( ph  ->  ( ( Id `  C ) `  Y
)  =  (idfunc `  Y
) )
260257, 258, 2593eqtr4d 2505 . . 3  |-  ( ph  ->  ( <. F ,  G >. ( <. Y ,  X >. (comp `  C ) Y ) <. `' F ,  H >. )  =  ( ( Id `  C
) `  Y )
)
26158, 222, 213, 219, 223, 225, 63, 65, 229, 227issect2 14811 . . 3  |-  ( ph  ->  ( <. `' F ,  H >. ( Y (Sect `  C ) X )
<. F ,  G >.  <->  ( <. F ,  G >. (
<. Y ,  X >. (comp `  C ) Y )
<. `' F ,  H >. )  =  ( ( Id
`  C ) `  Y ) ) )
262260, 261mpbird 232 . 2  |-  ( ph  -> 
<. `' F ,  H >. ( Y (Sect `  C
) X ) <. F ,  G >. )
263 catcisolem.i . . 3  |-  I  =  (Inv `  C )
26458, 263, 225, 65, 63, 223isinv 14816 . 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 913 1  |-  ( ph  -> 
<. F ,  G >. ( X I Y )
<. `' F ,  H >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1370    e. wcel 1758    i^i cin 3434   <.cop 3990   class class class wbr 4399    |-> cmpt 4457    _I cid 4738    X. cxp 4945   `'ccnv 4946    |` cres 4949    o. ccom 4951    Fn wfn 5520   -->wf 5521   -1-1-onto->wf1o 5524   ` cfv 5525  (class class class)co 6199    |-> cmpt2 6201   Basecbs 14291   Hom chom 14367  compcco 14368   Catccat 14720   Idccid 14721  Sectcsect 14801  Invcinv 14802    Func cfunc 14882  idfunccidfu 14883    o.func ccofu 14884   Full cful 14930   Faith cfth 14931  CatCatccatc 15080
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4510  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481  ax-cnex 9448  ax-resscn 9449  ax-1cn 9450  ax-icn 9451  ax-addcl 9452  ax-addrcl 9453  ax-mulcl 9454  ax-mulrcl 9455  ax-mulcom 9456  ax-addass 9457  ax-mulass 9458  ax-distr 9459  ax-i2m1 9460  ax-1ne0 9461  ax-1rid 9462  ax-rnegex 9463  ax-rrecex 9464  ax-cnre 9465  ax-pre-lttri 9466  ax-pre-lttrn 9467  ax-pre-ltadd 9468  ax-pre-mulgt0 9469
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-nel 2650  df-ral 2803  df-rex 2804  df-reu 2805  df-rmo 2806  df-rab 2807  df-v 3078  df-sbc 3293  df-csb 3395  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-pss 3451  df-nul 3745  df-if 3899  df-pw 3969  df-sn 3985  df-pr 3987  df-tp 3989  df-op 3991  df-uni 4199  df-int 4236  df-iun 4280  df-br 4400  df-opab 4458  df-mpt 4459  df-tr 4493  df-eprel 4739  df-id 4743  df-po 4748  df-so 4749  df-fr 4786  df-we 4788  df-ord 4829  df-on 4830  df-lim 4831  df-suc 4832  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-riota 6160  df-ov 6202  df-oprab 6203  df-mpt2 6204  df-om 6586  df-1st 6686  df-2nd 6687  df-recs 6941  df-rdg 6975  df-1o 7029  df-oadd 7033  df-er 7210  df-map 7325  df-ixp 7373  df-en 7420  df-dom 7421  df-sdom 7422  df-fin 7423  df-pnf 9530  df-mnf 9531  df-xr 9532  df-ltxr 9533  df-le 9534  df-sub 9707  df-neg 9708  df-nn 10433  df-2 10490  df-3 10491  df-4 10492  df-5 10493  df-6 10494  df-7 10495  df-8 10496  df-9 10497  df-10 10498  df-n0 10690  df-z 10757  df-dec 10866  df-uz 10972  df-fz 11554  df-struct 14293  df-ndx 14294  df-slot 14295  df-base 14296  df-hom 14380  df-cco 14381  df-cat 14724  df-cid 14725  df-sect 14804  df-inv 14805  df-func 14886  df-idfu 14887  df-cofu 14888  df-full 14932  df-fth 14933  df-catc 15081
This theorem is referenced by:  catciso  15093
  Copyright terms: Public domain W3C validator