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

Theorem catcisolem 14957
Description: Lemma for catciso 14958. (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 5657 . . . . . . 7  |-  ( F : R -1-1-onto-> S  ->  ( `' F  o.  F )  =  (  _I  |`  R ) )
31, 2syl 16 . . . . . 6  |-  ( ph  ->  ( `' F  o.  F )  =  (  _I  |`  R )
)
413ad2ant1 1002 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  F : R
-1-1-onto-> S )
5 f1of 5629 . . . . . . . . . . . . . 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 982 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  u  e.  R )
86, 7ffvelrnd 5832 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( F `  u )  e.  S
)
9 simp3 983 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  v  e.  R )
106, 9ffvelrnd 5832 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( F `  v )  e.  S
)
11 simpl 454 . . . . . . . . . . . . . . . 16  |-  ( ( x  =  ( F `
 u )  /\  y  =  ( F `  v ) )  ->  x  =  ( F `  u ) )
1211fveq2d 5683 . . . . . . . . . . . . . . 15  |-  ( ( x  =  ( F `
 u )  /\  y  =  ( F `  v ) )  -> 
( `' F `  x )  =  ( `' F `  ( F `
 u ) ) )
13 simpr 458 . . . . . . . . . . . . . . . 16  |-  ( ( x  =  ( F `
 u )  /\  y  =  ( F `  v ) )  -> 
y  =  ( F `
 v ) )
1413fveq2d 5683 . . . . . . . . . . . . . . 15  |-  ( ( x  =  ( F `
 u )  /\  y  =  ( F `  v ) )  -> 
( `' F `  y )  =  ( `' F `  ( F `
 v ) ) )
1512, 14oveq12d 6098 . . . . . . . . . . . . . 14  |-  ( ( x  =  ( F `
 u )  /\  y  =  ( F `  v ) )  -> 
( ( `' F `  x ) G ( `' F `  y ) )  =  ( ( `' F `  ( F `
 u ) ) G ( `' F `  ( F `  v
) ) ) )
1615cnveqd 5002 . . . . . . . . . . . . 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 6105 . . . . . . . . . . . . . 14  |-  ( ( `' F `  ( F `
 u ) ) G ( `' F `  ( F `  v
) ) )  e. 
_V
1918cnvex 6514 . . . . . . . . . . . . 13  |-  `' ( ( `' F `  ( F `  u ) ) G ( `' F `  ( F `
 v ) ) )  e.  _V
2016, 17, 19ovmpt2a 6210 . . . . . . . . . . . 12  |-  ( ( ( F `  u
)  e.  S  /\  ( F `  v )  e.  S )  -> 
( ( F `  u ) H ( F `  v ) )  =  `' ( ( `' F `  ( F `  u ) ) G ( `' F `  ( F `
 v ) ) ) )
218, 10, 20syl2anc 654 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( ( F `  u ) H ( F `  v ) )  =  `' ( ( `' F `  ( F `
 u ) ) G ( `' F `  ( F `  v
) ) ) )
22 f1ocnvfv1 5970 . . . . . . . . . . . . . 14  |-  ( ( F : R -1-1-onto-> S  /\  u  e.  R )  ->  ( `' F `  ( F `  u ) )  =  u )
234, 7, 22syl2anc 654 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( `' F `  ( F `  u ) )  =  u )
24 f1ocnvfv1 5970 . . . . . . . . . . . . . 14  |-  ( ( F : R -1-1-onto-> S  /\  v  e.  R )  ->  ( `' F `  ( F `  v ) )  =  v )
254, 9, 24syl2anc 654 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( `' F `  ( F `  v ) )  =  v )
2623, 25oveq12d 6098 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( ( `' F `  ( F `
 u ) ) G ( `' F `  ( F `  v
) ) )  =  ( u G v ) )
2726cnveqd 5002 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  `' (
( `' F `  ( F `  u ) ) G ( `' F `  ( F `
 v ) ) )  =  `' ( u G v ) )
2821, 27eqtrd 2465 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( ( F `  u ) H ( F `  v ) )  =  `' ( u G v ) )
2928coeq1d 4988 . . . . . . . . 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 2433 . . . . . . . . . . 11  |-  ( Hom  `  X )  =  ( Hom  `  X )
32 eqid 2433 . . . . . . . . . . 11  |-  ( Hom  `  Y )  =  ( Hom  `  Y )
33 catcisolem.1 . . . . . . . . . . . 12  |-  ( ph  ->  F ( ( X Full 
Y )  i^i  ( X Faith  Y ) ) G )
34333ad2ant1 1002 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  F (
( X Full  Y )  i^i  ( X Faith  Y ) ) G )
3530, 31, 32, 34, 7, 9ffthf1o 14812 . . . . . . . . . 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 5657 . . . . . . . . . 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 2465 . . . . . . . 8  |-  ( (
ph  /\  u  e.  R  /\  v  e.  R
)  ->  ( (
( F `  u
) H ( F `
 v ) )  o.  ( u G v ) )  =  (  _I  |`  (
u ( Hom  `  X
) v ) ) )
3938mpt2eq3dva 6139 . . . . . . 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 5679 . . . . . . . . . 10  |-  ( z  =  <. u ,  v
>.  ->  ( ( Hom  `  X ) `  z
)  =  ( ( Hom  `  X ) `  <. u ,  v
>. ) )
41 df-ov 6083 . . . . . . . . . 10  |-  ( u ( Hom  `  X
) v )  =  ( ( Hom  `  X
) `  <. u ,  v >. )
4240, 41syl6eqr 2483 . . . . . . . . 9  |-  ( z  =  <. u ,  v
>.  ->  ( ( Hom  `  X ) `  z
)  =  ( u ( Hom  `  X
) v ) )
4342reseq2d 5097 . . . . . . . 8  |-  ( z  =  <. u ,  v
>.  ->  (  _I  |`  (
( Hom  `  X ) `
 z ) )  =  (  _I  |`  (
u ( Hom  `  X
) v ) ) )
4443mpt2mpt 6171 . . . . . . 7  |-  ( z  e.  ( R  X.  R )  |->  (  _I  |`  ( ( Hom  `  X
) `  z )
) )  =  ( u  e.  R , 
v  e.  R  |->  (  _I  |`  ( u
( Hom  `  X ) v ) ) )
4539, 44syl6eqr 2483 . . . . . 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 4055 . . . . 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 3558 . . . . . . . . 9  |-  ( ( X Full  Y )  i^i  ( X Faith  Y ) )  C_  ( X Full  Y )
48 fullfunc 14799 . . . . . . . . 9  |-  ( X Full 
Y )  C_  ( X  Func  Y )
4947, 48sstri 3353 . . . . . . . 8  |-  ( ( X Full  Y )  i^i  ( X Faith  Y ) )  C_  ( X  Func  Y )
5049ssbri 4322 . . . . . . 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 2433 . . . . . . 7  |-  ( Id
`  Y )  =  ( Id `  Y
)
54 eqid 2433 . . . . . . 7  |-  ( Id
`  X )  =  ( Id `  X
)
55 eqid 2433 . . . . . . 7  |-  (comp `  Y )  =  (comp `  Y )
56 eqid 2433 . . . . . . 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 14948 . . . . . . . . 9  |-  ( ph  ->  B  =  ( U  i^i  Cat ) )
61 inss2 3559 . . . . . . . . 9  |-  ( U  i^i  Cat )  C_  Cat
6260, 61syl6eqss 3394 . . . . . . . 8  |-  ( ph  ->  B  C_  Cat )
63 catciso.y . . . . . . . 8  |-  ( ph  ->  Y  e.  B )
6462, 63sseldd 3345 . . . . . . 7  |-  ( ph  ->  Y  e.  Cat )
65 catciso.x . . . . . . . 8  |-  ( ph  ->  X  e.  B )
6662, 65sseldd 3345 . . . . . . 7  |-  ( ph  ->  X  e.  Cat )
67 f1ocnv 5641 . . . . . . . 8  |-  ( F : R -1-1-onto-> S  ->  `' F : S -1-1-onto-> R )
68 f1of 5629 . . . . . . . 8  |-  ( `' F : S -1-1-onto-> R  ->  `' F : S --> R )
691, 67, 683syl 20 . . . . . . 7  |-  ( ph  ->  `' F : S --> R )
70 ovex 6105 . . . . . . . . . 10  |-  ( ( `' F `  x ) G ( `' F `  y ) )  e. 
_V
7170cnvex 6514 . . . . . . . . 9  |-  `' ( ( `' F `  x ) G ( `' F `  y ) )  e.  _V
7217, 71fnmpt2i 6632 . . . . . . . 8  |-  H  Fn  ( S  X.  S
)
7372a1i 11 . . . . . . 7  |-  ( ph  ->  H  Fn  ( S  X.  S ) )
7433adantr 462 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  ->  F ( ( X Full 
Y )  i^i  ( X Faith  Y ) ) G )
7569ffvelrnda 5831 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  S )  ->  ( `' F `  u )  e.  R )
7675adantrr 709 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( `' F `  u )  e.  R
)
7769ffvelrnda 5831 . . . . . . . . . . 11  |-  ( (
ph  /\  v  e.  S )  ->  ( `' F `  v )  e.  R )
7877adantrl 708 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( `' F `  v )  e.  R
)
7930, 31, 32, 74, 76, 78ffthf1o 14812 . . . . . . . . 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 5641 . . . . . . . . 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 5629 . . . . . . . . 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 454 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  v )  ->  x  =  u )
8483fveq2d 5683 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  v )  ->  ( `' F `  x )  =  ( `' F `  u ) )
85 simpr 458 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  v )  ->  y  =  v )
8685fveq2d 5683 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  v )  ->  ( `' F `  y )  =  ( `' F `  v ) )
8784, 86oveq12d 6098 . . . . . . . . . . . 12  |-  ( ( x  =  u  /\  y  =  v )  ->  ( ( `' F `  x ) G ( `' F `  y ) )  =  ( ( `' F `  u ) G ( `' F `  v ) ) )
8887cnveqd 5002 . . . . . . . . . . 11  |-  ( ( x  =  u  /\  y  =  v )  ->  `' ( ( `' F `  x ) G ( `' F `  y ) )  =  `' ( ( `' F `  u ) G ( `' F `  v ) ) )
89 ovex 6105 . . . . . . . . . . . 12  |-  ( ( `' F `  u ) G ( `' F `  v ) )  e. 
_V
9089cnvex 6514 . . . . . . . . . . 11  |-  `' ( ( `' F `  u ) G ( `' F `  v ) )  e.  _V
9188, 17, 90ovmpt2a 6210 . . . . . . . . . 10  |-  ( ( u  e.  S  /\  v  e.  S )  ->  ( u H v )  =  `' ( ( `' F `  u ) G ( `' F `  v ) ) )
9291adantl 463 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( u H v )  =  `' ( ( `' F `  u ) G ( `' F `  v ) ) )
931adantr 462 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  ->  F : R -1-1-onto-> S )
94 simprl 748 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  ->  u  e.  S )
95 f1ocnvfv2 5971 . . . . . . . . . . . 12  |-  ( ( F : R -1-1-onto-> S  /\  u  e.  S )  ->  ( F `  ( `' F `  u ) )  =  u )
9693, 94, 95syl2anc 654 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( F `  ( `' F `  u ) )  =  u )
97 simprr 749 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
v  e.  S )
98 f1ocnvfv2 5971 . . . . . . . . . . . 12  |-  ( ( F : R -1-1-onto-> S  /\  v  e.  S )  ->  ( F `  ( `' F `  v ) )  =  v )
9993, 97, 98syl2anc 654 . . . . . . . . . . 11  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( F `  ( `' F `  v ) )  =  v )
10096, 99oveq12d 6098 . . . . . . . . . 10  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( ( F `  ( `' F `  u ) ) ( Hom  `  Y
) ( F `  ( `' F `  v ) ) )  =  ( u ( Hom  `  Y
) v ) )
101100eqcomd 2438 . . . . . . . . 9  |-  ( (
ph  /\  ( u  e.  S  /\  v  e.  S ) )  -> 
( u ( Hom  `  Y ) v )  =  ( ( F `
 ( `' F `  u ) ) ( Hom  `  Y )
( F `  ( `' F `  v ) ) ) )
10292, 101feq12d 5536 . . . . . . . 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 458 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  S )  ->  u  e.  S )
105 simpl 454 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  u )  ->  x  =  u )
106105fveq2d 5683 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  u )  ->  ( `' F `  x )  =  ( `' F `  u ) )
107 simpr 458 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  u )  ->  y  =  u )
108107fveq2d 5683 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  u )  ->  ( `' F `  y )  =  ( `' F `  u ) )
109106, 108oveq12d 6098 . . . . . . . . . . . 12  |-  ( ( x  =  u  /\  y  =  u )  ->  ( ( `' F `  x ) G ( `' F `  y ) )  =  ( ( `' F `  u ) G ( `' F `  u ) ) )
110109cnveqd 5002 . . . . . . . . . . 11  |-  ( ( x  =  u  /\  y  =  u )  ->  `' ( ( `' F `  x ) G ( `' F `  y ) )  =  `' ( ( `' F `  u ) G ( `' F `  u ) ) )
111 ovex 6105 . . . . . . . . . . . 12  |-  ( ( `' F `  u ) G ( `' F `  u ) )  e. 
_V
112111cnvex 6514 . . . . . . . . . . 11  |-  `' ( ( `' F `  u ) G ( `' F `  u ) )  e.  _V
113110, 17, 112ovmpt2a 6210 . . . . . . . . . 10  |-  ( ( u  e.  S  /\  u  e.  S )  ->  ( u H u )  =  `' ( ( `' F `  u ) G ( `' F `  u ) ) )
114104, 104, 113syl2anc 654 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  S )  ->  (
u H u )  =  `' ( ( `' F `  u ) G ( `' F `  u ) ) )
115114fveq1d 5681 . . . . . . . 8  |-  ( (
ph  /\  u  e.  S )  ->  (
( u H u ) `  ( ( Id `  Y ) `
 u ) )  =  ( `' ( ( `' F `  u ) G ( `' F `  u ) ) `  ( ( Id `  Y ) `
 u ) ) )
11651adantr 462 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  S )  ->  F
( X  Func  Y
) G )
11730, 54, 53, 116, 75funcid 14763 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  S )  ->  (
( ( `' F `  u ) G ( `' F `  u ) ) `  ( ( Id `  X ) `
 ( `' F `  u ) ) )  =  ( ( Id
`  Y ) `  ( F `  ( `' F `  u ) ) ) )
1181, 95sylan 468 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  S )  ->  ( F `  ( `' F `  u )
)  =  u )
119118fveq2d 5683 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  S )  ->  (
( Id `  Y
) `  ( F `  ( `' F `  u ) ) )  =  ( ( Id
`  Y ) `  u ) )
120117, 119eqtrd 2465 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  S )  ->  (
( ( `' F `  u ) G ( `' F `  u ) ) `  ( ( Id `  X ) `
 ( `' F `  u ) ) )  =  ( ( Id
`  Y ) `  u ) )
12133adantr 462 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  S )  ->  F
( ( X Full  Y
)  i^i  ( X Faith  Y ) ) G )
12230, 31, 32, 121, 75, 75ffthf1o 14812 . . . . . . . . . 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 462 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  S )  ->  X  e.  Cat )
12430, 31, 54, 123, 75catidcl 14603 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  S )  ->  (
( Id `  X
) `  ( `' F `  u )
)  e.  ( ( `' F `  u ) ( Hom  `  X
) ( `' F `  u ) ) )
125 f1ocnvfv 5972 . . . . . . . . . 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 654 . . . . . . . . 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 2465 . . . . . . 7  |-  ( (
ph  /\  u  e.  S )  ->  (
( u H u ) `  ( ( Id `  Y ) `
 u ) )  =  ( ( Id
`  X ) `  ( `' F `  u ) ) )
129513ad2ant1 1002 . . . . . . . . . . 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 1002 . . . . . . . . . . . 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 1014 . . . . . . . . . . . 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 5832 . . . . . . . . . . 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 1015 . . . . . . . . . . . 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 5832 . . . . . . . . . . 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 1016 . . . . . . . . . . . 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 5832 . . . . . . . . . . 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 1002 . . . . . . . . . . . . . . 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 14812 . . . . . . . . . . . . . 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 1002 . . . . . . . . . . . . . . . . 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 654 . . . . . . . . . . . . . . . 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 654 . . . . . . . . . . . . . . . 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 6098 . . . . . . . . . . . . . . 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 5622 . . . . . . . . . . . . . . 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 5641 . . . . . . . . . . . . 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 5629 . . . . . . . . . . . . 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 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  e.  ( u ( Hom  `  Y
) v ) )
150148, 149ffvelrnd 5832 . . . . . . . . . . 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 14812 . . . . . . . . . . . . . 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 5971 . . . . . . . . . . . . . . . . 17  |-  ( ( F : R -1-1-onto-> S  /\  z  e.  S )  ->  ( F `  ( `' F `  z ) )  =  z )
153139, 135, 152syl2anc 654 . . . . . . . . . . . . . . . 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 6098 . . . . . . . . . . . . . . 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 5622 . . . . . . . . . . . . . . 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 5641 . . . . . . . . . . . . 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 5629 . . . . . . . . . . . . 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 1010 . . . . . . . . . . . 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 5832 . . . . . . . . . . 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 14764 . . . . . . . . . 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 4055 . . . . . . . . . . . 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 6098 . . . . . . . . . . 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 5971 . . . . . . . . . . . 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 654 . . . . . . . . . . 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 5971 . . . . . . . . . . . 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 654 . . . . . . . . . . 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 6101 . . . . . . . . . 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 2465 . . . . . . . . 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 14812 . . . . . . . . . . 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 6098 . . . . . . . . . . . 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 5622 . . . . . . . . . . . 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 1002 . . . . . . . . . . 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 14606 . . . . . . . . . 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 5972 . . . . . . . . . 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 654 . . . . . . . . 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 454 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  z )  ->  x  =  u )
183182fveq2d 5683 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  z )  ->  ( `' F `  x )  =  ( `' F `  u ) )
184 simpr 458 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  z )  ->  y  =  z )
185184fveq2d 5683 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  z )  ->  ( `' F `  y )  =  ( `' F `  z ) )
186183, 185oveq12d 6098 . . . . . . . . . . . 12  |-  ( ( x  =  u  /\  y  =  z )  ->  ( ( `' F `  x ) G ( `' F `  y ) )  =  ( ( `' F `  u ) G ( `' F `  z ) ) )
187186cnveqd 5002 . . . . . . . . . . 11  |-  ( ( x  =  u  /\  y  =  z )  ->  `' ( ( `' F `  x ) G ( `' F `  y ) )  =  `' ( ( `' F `  u ) G ( `' F `  z ) ) )
188 ovex 6105 . . . . . . . . . . . 12  |-  ( ( `' F `  u ) G ( `' F `  z ) )  e. 
_V
189188cnvex 6514 . . . . . . . . . . 11  |-  `' ( ( `' F `  u ) G ( `' F `  z ) )  e.  _V
190187, 17, 189ovmpt2a 6210 . . . . . . . . . 10  |-  ( ( u  e.  S  /\  z  e.  S )  ->  ( u H z )  =  `' ( ( `' F `  u ) G ( `' F `  z ) ) )
191131, 135, 190syl2anc 654 . . . . . . . . 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 5681 . . . . . . . 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 454 . . . . . . . . . . . . . . 15  |-  ( ( x  =  v  /\  y  =  z )  ->  x  =  v )
194193fveq2d 5683 . . . . . . . . . . . . . 14  |-  ( ( x  =  v  /\  y  =  z )  ->  ( `' F `  x )  =  ( `' F `  v ) )
195 simpr 458 . . . . . . . . . . . . . . 15  |-  ( ( x  =  v  /\  y  =  z )  ->  y  =  z )
196195fveq2d 5683 . . . . . . . . . . . . . 14  |-  ( ( x  =  v  /\  y  =  z )  ->  ( `' F `  y )  =  ( `' F `  z ) )
197194, 196oveq12d 6098 . . . . . . . . . . . . 13  |-  ( ( x  =  v  /\  y  =  z )  ->  ( ( `' F `  x ) G ( `' F `  y ) )  =  ( ( `' F `  v ) G ( `' F `  z ) ) )
198197cnveqd 5002 . . . . . . . . . . . 12  |-  ( ( x  =  v  /\  y  =  z )  ->  `' ( ( `' F `  x ) G ( `' F `  y ) )  =  `' ( ( `' F `  v ) G ( `' F `  z ) ) )
199 ovex 6105 . . . . . . . . . . . . 13  |-  ( ( `' F `  v ) G ( `' F `  z ) )  e. 
_V
200199cnvex 6514 . . . . . . . . . . . 12  |-  `' ( ( `' F `  v ) G ( `' F `  z ) )  e.  _V
201198, 17, 200ovmpt2a 6210 . . . . . . . . . . 11  |-  ( ( v  e.  S  /\  z  e.  S )  ->  ( v H z )  =  `' ( ( `' F `  v ) G ( `' F `  z ) ) )
202133, 135, 201syl2anc 654 . . . . . . . . . 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 5681 . . . . . . . . 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 654 . . . . . . . . . 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 5681 . . . . . . . . 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 6098 . . . . . . . 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 2475 . . . . . . 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 14758 . . . . . 6  |-  ( ph  ->  `' F ( Y  Func  X ) H )
20930, 51, 208cofuval2 14780 . . . . 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 2433 . . . . . 6  |-  (idfunc `  X
)  =  (idfunc `  X
)
211210, 30, 66, 31idfuval 14769 . . . . 5  |-  ( ph  ->  (idfunc `  X )  =  <. (  _I  |`  R ) ,  ( z  e.  ( R  X.  R
)  |->  (  _I  |`  (
( Hom  `  X ) `
 z ) ) ) >. )
21246, 209, 2113eqtr4d 2475 . . . 4  |-  ( ph  ->  ( <. `' F ,  H >.  o.func 
<. F ,  G >. )  =  (idfunc `  X ) )
213 eqid 2433 . . . . 5  |-  (comp `  C )  =  (comp `  C )
214 df-br 4281 . . . . . 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 4281 . . . . . 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 14952 . . . 4  |-  ( ph  ->  ( <. `' F ,  H >. ( <. X ,  Y >. (comp `  C
) X ) <. F ,  G >. )  =  ( <. `' F ,  H >.  o.func 
<. F ,  G >. ) )
219 eqid 2433 . . . . 5  |-  ( Id
`  C )  =  ( Id `  C
)
22057, 58, 219, 210, 59, 65catcid 14954 . . . 4  |-  ( ph  ->  ( ( Id `  C ) `  X
)  =  (idfunc `  X
) )
221212, 218, 2203eqtr4d 2475 . . 3  |-  ( ph  ->  ( <. `' F ,  H >. ( <. X ,  Y >. (comp `  C
) X ) <. F ,  G >. )  =  ( ( Id
`  C ) `  X ) )
222 eqid 2433 . . . 4  |-  ( Hom  `  C )  =  ( Hom  `  C )
223 eqid 2433 . . . 4  |-  (Sect `  C )  =  (Sect `  C )
22457catccat 14955 . . . . 5  |-  ( U  e.  V  ->  C  e.  Cat )
22559, 224syl 16 . . . 4  |-  ( ph  ->  C  e.  Cat )
22657, 58, 59, 222, 65, 63catchom 14950 . . . . 5  |-  ( ph  ->  ( X ( Hom  `  C ) Y )  =  ( X  Func  Y ) )
227215, 226eleqtrrd 2510 . . . 4  |-  ( ph  -> 
<. F ,  G >.  e.  ( X ( Hom  `  C ) Y ) )
22857, 58, 59, 222, 63, 65catchom 14950 . . . . 5  |-  ( ph  ->  ( Y ( Hom  `  C ) X )  =  ( Y  Func  X ) )
229217, 228eleqtrrd 2510 . . . 4  |-  ( ph  -> 
<. `' F ,  H >.  e.  ( Y ( Hom  `  C ) X ) )
23058, 222, 213, 219, 223, 225, 65, 63, 227, 229issect2 14676 . . 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 5655 . . . . . . 7  |-  ( F : R -1-1-onto-> S  ->  ( F  o.  `' F )  =  (  _I  |`  S )
)
2331, 232syl 16 . . . . . 6  |-  ( ph  ->  ( F  o.  `' F )  =  (  _I  |`  S )
)
234913adant1 999 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  ( u H v )  =  `' ( ( `' F `  u ) G ( `' F `  v ) ) )
235234coeq2d 4989 . . . . . . . . 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 1002 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  F (
( X Full  Y )  i^i  ( X Faith  Y ) ) G )
237753adant3 1001 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  ( `' F `  u )  e.  R )
238773adant2 1000 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  ( `' F `  v )  e.  R )
23930, 31, 32, 236, 237, 238ffthf1o 14812 . . . . . . . . . . 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 1176 . . . . . . . . . . . 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 5655 . . . . . . . . . 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 2465 . . . . . . . 8  |-  ( (
ph  /\  u  e.  S  /\  v  e.  S
)  ->  ( (
( `' F `  u ) G ( `' F `  v ) )  o.  ( u H v ) )  =  (  _I  |`  (
u ( Hom  `  Y
) v ) ) )
246245mpt2eq3dva 6139 . . . . . . 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 5679 . . . . . . . . . 10  |-  ( z  =  <. u ,  v
>.  ->  ( ( Hom  `  Y ) `  z
)  =  ( ( Hom  `  Y ) `  <. u ,  v
>. ) )
248 df-ov 6083 . . . . . . . . . 10  |-  ( u ( Hom  `  Y
) v )  =  ( ( Hom  `  Y
) `  <. u ,  v >. )
249247, 248syl6eqr 2483 . . . . . . . . 9  |-  ( z  =  <. u ,  v
>.  ->  ( ( Hom  `  Y ) `  z
)  =  ( u ( Hom  `  Y
) v ) )
250249reseq2d 5097 . . . . . . . 8  |-  ( z  =  <. u ,  v
>.  ->  (  _I  |`  (
( Hom  `  Y ) `
 z ) )  =  (  _I  |`  (
u ( Hom  `  Y
) v ) ) )
251250mpt2mpt 6171 . . . . . . 7  |-  ( z  e.  ( S  X.  S )  |->  (  _I  |`  ( ( Hom  `  Y
) `  z )
) )  =  ( u  e.  S , 
v  e.  S  |->  (  _I  |`  ( u
( Hom  `  Y ) v ) ) )
252246, 251syl6eqr 2483 . . . . . 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 4055 . . . . 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 14780 . . . . 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 2433 . . . . . 6  |-  (idfunc `  Y
)  =  (idfunc `  Y
)
256255, 52, 64, 32idfuval 14769 . . . . 5  |-  ( ph  ->  (idfunc `  Y )  =  <. (  _I  |`  S ) ,  ( z  e.  ( S  X.  S
)  |->  (  _I  |`  (
( Hom  `  Y ) `
 z ) ) ) >. )
257253, 254, 2563eqtr4d 2475 . . . 4  |-  ( ph  ->  ( <. F ,  G >.  o.func 
<. `' F ,  H >. )  =  (idfunc `  Y ) )
25857, 58, 59, 213, 63, 65, 63, 217, 215catcco 14952 . . . 4  |-  ( ph  ->  ( <. F ,  G >. ( <. Y ,  X >. (comp `  C ) Y ) <. `' F ,  H >. )  =  (
<. F ,  G >.  o.func  <. `' F ,  H >. ) )
25957, 58, 219, 255, 59, 63catcid 14954 . . . 4  |-  ( ph  ->  ( ( Id `  C ) `  Y
)  =  (idfunc `  Y
) )
260257, 258, 2593eqtr4d 2475 . . 3  |-  ( ph  ->  ( <. F ,  G >. ( <. Y ,  X >. (comp `  C ) Y ) <. `' F ,  H >. )  =  ( ( Id `  C
) `  Y )
)
26158, 222, 213, 219, 223, 225, 63, 65, 229, 227issect2 14676 . . 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 14681 . 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 906 1  |-  ( ph  -> 
<. F ,  G >. ( X I Y )
<. `' F ,  H >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 958    = wceq 1362    e. wcel 1755    i^i cin 3315   <.cop 3871   class class class wbr 4280    e. cmpt 4338    _I cid 4618    X. cxp 4825   `'ccnv 4826    |` cres 4829    o. ccom 4831    Fn wfn 5401   -->wf 5402   -1-1-onto->wf1o 5405   ` cfv 5406  (class class class)co 6080    e. cmpt2 6082   Basecbs 14157   Hom chom 14232  compcco 14233   Catccat 14585   Idccid 14586  Sectcsect 14666  Invcinv 14667    Func cfunc 14747  idfunccidfu 14748    o.func ccofu 14749   Full cful 14795   Faith cfth 14796  CatCatccatc 14945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-rep 4391  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-cnex 9326  ax-resscn 9327  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-mulcom 9334  ax-addass 9335  ax-mulass 9336  ax-distr 9337  ax-i2m1 9338  ax-1ne0 9339  ax-1rid 9340  ax-rnegex 9341  ax-rrecex 9342  ax-cnre 9343  ax-pre-lttri 9344  ax-pre-lttrn 9345  ax-pre-ltadd 9346  ax-pre-mulgt0 9347
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-int 4117  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-riota 6039  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-om 6466  df-1st 6566  df-2nd 6567  df-recs 6818  df-rdg 6852  df-1o 6908  df-oadd 6912  df-er 7089  df-map 7204  df-ixp 7252  df-en 7299  df-dom 7300  df-sdom 7301  df-fin 7302  df-pnf 9408  df-mnf 9409  df-xr 9410  df-ltxr 9411  df-le 9412  df-sub 9585  df-neg 9586  df-nn 10311  df-2 10368  df-3 10369  df-4 10370  df-5 10371  df-6 10372  df-7 10373  df-8 10374  df-9 10375  df-10 10376  df-n0 10568  df-z 10635  df-dec 10744  df-uz 10850  df-fz 11425  df-struct 14159  df-ndx 14160  df-slot 14161  df-base 14162  df-hom 14245  df-cco 14246  df-cat 14589  df-cid 14590  df-sect 14669  df-inv 14670  df-func 14751  df-idfu 14752  df-cofu 14753  df-full 14797  df-fth 14798  df-catc 14946
This theorem is referenced by:  catciso  14958
  Copyright terms: Public domain W3C validator