Metamath Proof Explorer

Theorem catcisolem

Description: Lemma for catciso . (Contributed by Mario Carneiro, 29-Jan-2017)

Ref Expression
Hypotheses 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 catcisolem 
|- ( ph -> <. F , G >. ( X I Y ) <. `' F , H >. )

Proof

Step Hyp Ref Expression
1 catciso.c 
 |-  C = ( CatCat ` U )
2 catciso.b 
 |-  B = ( Base ` C )
3 catciso.r 
 |-  R = ( Base ` X )
4 catciso.s 
 |-  S = ( Base ` Y )
5 catciso.u 
 |-  ( ph -> U e. V )
6 catciso.x 
 |-  ( ph -> X e. B )
7 catciso.y 
 |-  ( ph -> Y e. B )
8 catcisolem.i 
 |-  I = ( Inv ` C )
9 catcisolem.g 
 |-  H = ( x e. S , y e. S |-> `' ( ( `' F ` x ) G ( `' F ` y ) ) )
10 catcisolem.1 
 |-  ( ph -> F ( ( X Full Y ) i^i ( X Faith Y ) ) G )
11 catcisolem.2 
 |-  ( ph -> F : R -1-1-onto-> S )
12 f1ococnv1 
 |-  ( F : R -1-1-onto-> S -> ( `' F o. F ) = ( _I |` R ) )
13 11 12 syl 
 |-  ( ph -> ( `' F o. F ) = ( _I |` R ) )
14 11 3ad2ant1 
 |-  ( ( ph /\ u e. R /\ v e. R ) -> F : R -1-1-onto-> S )
15 f1of 
 |-  ( F : R -1-1-onto-> S -> F : R --> S )
16 14 15 syl 
 |-  ( ( ph /\ u e. R /\ v e. R ) -> F : R --> S )
17 simp2 
 |-  ( ( ph /\ u e. R /\ v e. R ) -> u e. R )
18 16 17 ffvelrnd 
 |-  ( ( ph /\ u e. R /\ v e. R ) -> ( F ` u ) e. S )
19 simp3 
 |-  ( ( ph /\ u e. R /\ v e. R ) -> v e. R )
20 16 19 ffvelrnd 
 |-  ( ( ph /\ u e. R /\ v e. R ) -> ( F ` v ) e. S )
21 simpl 
 |-  ( ( x = ( F ` u ) /\ y = ( F ` v ) ) -> x = ( F ` u ) )
22 21 fveq2d 
 |-  ( ( x = ( F ` u ) /\ y = ( F ` v ) ) -> ( `' F ` x ) = ( `' F ` ( F ` u ) ) )
23 simpr 
 |-  ( ( x = ( F ` u ) /\ y = ( F ` v ) ) -> y = ( F ` v ) )
24 23 fveq2d 
 |-  ( ( x = ( F ` u ) /\ y = ( F ` v ) ) -> ( `' F ` y ) = ( `' F ` ( F ` v ) ) )
25 22 24 oveq12d 
 |-  ( ( x = ( F ` u ) /\ y = ( F ` v ) ) -> ( ( `' F ` x ) G ( `' F ` y ) ) = ( ( `' F ` ( F ` u ) ) G ( `' F ` ( F ` v ) ) ) )
26 25 cnveqd 
 |-  ( ( x = ( F ` u ) /\ y = ( F ` v ) ) -> `' ( ( `' F ` x ) G ( `' F ` y ) ) = `' ( ( `' F ` ( F ` u ) ) G ( `' F ` ( F ` v ) ) ) )
27 ovex 
 |-  ( ( `' F ` ( F ` u ) ) G ( `' F ` ( F ` v ) ) ) e. _V
28 27 cnvex 
 |-  `' ( ( `' F ` ( F ` u ) ) G ( `' F ` ( F ` v ) ) ) e. _V
29 26 9 28 ovmpoa 
 |-  ( ( ( F ` u ) e. S /\ ( F ` v ) e. S ) -> ( ( F ` u ) H ( F ` v ) ) = `' ( ( `' F ` ( F ` u ) ) G ( `' F ` ( F ` v ) ) ) )
30 18 20 29 syl2anc 
 |-  ( ( ph /\ u e. R /\ v e. R ) -> ( ( F ` u ) H ( F ` v ) ) = `' ( ( `' F ` ( F ` u ) ) G ( `' F ` ( F ` v ) ) ) )
31 f1ocnvfv1 
 |-  ( ( F : R -1-1-onto-> S /\ u e. R ) -> ( `' F ` ( F ` u ) ) = u )
32 14 17 31 syl2anc 
 |-  ( ( ph /\ u e. R /\ v e. R ) -> ( `' F ` ( F ` u ) ) = u )
33 f1ocnvfv1 
 |-  ( ( F : R -1-1-onto-> S /\ v e. R ) -> ( `' F ` ( F ` v ) ) = v )
34 14 19 33 syl2anc 
 |-  ( ( ph /\ u e. R /\ v e. R ) -> ( `' F ` ( F ` v ) ) = v )
35 32 34 oveq12d 
 |-  ( ( ph /\ u e. R /\ v e. R ) -> ( ( `' F ` ( F ` u ) ) G ( `' F ` ( F ` v ) ) ) = ( u G v ) )
36 35 cnveqd 
 |-  ( ( ph /\ u e. R /\ v e. R ) -> `' ( ( `' F ` ( F ` u ) ) G ( `' F ` ( F ` v ) ) ) = `' ( u G v ) )
37 30 36 eqtrd 
 |-  ( ( ph /\ u e. R /\ v e. R ) -> ( ( F ` u ) H ( F ` v ) ) = `' ( u G v ) )
38 37 coeq1d 
 |-  ( ( ph /\ u e. R /\ v e. R ) -> ( ( ( F ` u ) H ( F ` v ) ) o. ( u G v ) ) = ( `' ( u G v ) o. ( u G v ) ) )
39 eqid 
 |-  ( Hom ` X ) = ( Hom ` X )
40 eqid 
 |-  ( Hom ` Y ) = ( Hom ` Y )
41 10 3ad2ant1 
 |-  ( ( ph /\ u e. R /\ v e. R ) -> F ( ( X Full Y ) i^i ( X Faith Y ) ) G )
42 3 39 40 41 17 19 ffthf1o 
 |-  ( ( ph /\ u e. R /\ v e. R ) -> ( u G v ) : ( u ( Hom ` X ) v ) -1-1-onto-> ( ( F ` u ) ( Hom ` Y ) ( F ` v ) ) )
43 f1ococnv1 
 |-  ( ( 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 ) ) )
44 42 43 syl 
 |-  ( ( ph /\ u e. R /\ v e. R ) -> ( `' ( u G v ) o. ( u G v ) ) = ( _I |` ( u ( Hom ` X ) v ) ) )
45 38 44 eqtrd 
 |-  ( ( ph /\ u e. R /\ v e. R ) -> ( ( ( F ` u ) H ( F ` v ) ) o. ( u G v ) ) = ( _I |` ( u ( Hom ` X ) v ) ) )
46 45 mpoeq3dva 
 |-  ( 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 ) ) ) )
47 fveq2 
 |-  ( z = <. u , v >. -> ( ( Hom ` X ) ` z ) = ( ( Hom ` X ) ` <. u , v >. ) )
48 df-ov 
 |-  ( u ( Hom ` X ) v ) = ( ( Hom ` X ) ` <. u , v >. )
49 47 48 eqtr4di 
 |-  ( z = <. u , v >. -> ( ( Hom ` X ) ` z ) = ( u ( Hom ` X ) v ) )
50 49 reseq2d 
 |-  ( z = <. u , v >. -> ( _I |` ( ( Hom ` X ) ` z ) ) = ( _I |` ( u ( Hom ` X ) v ) ) )
51 50 mpompt 
 |-  ( z e. ( R X. R ) |-> ( _I |` ( ( Hom ` X ) ` z ) ) ) = ( u e. R , v e. R |-> ( _I |` ( u ( Hom ` X ) v ) ) )
52 46 51 eqtr4di 
 |-  ( 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 ) ) ) )
53 13 52 opeq12d 
 |-  ( 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 ) ) ) >. )
54 inss1 
 |-  ( ( X Full Y ) i^i ( X Faith Y ) ) C_ ( X Full Y )
55 fullfunc 
 |-  ( X Full Y ) C_ ( X Func Y )
56 54 55 sstri 
 |-  ( ( X Full Y ) i^i ( X Faith Y ) ) C_ ( X Func Y )
57 56 ssbri 
 |-  ( F ( ( X Full Y ) i^i ( X Faith Y ) ) G -> F ( X Func Y ) G )
58 10 57 syl 
 |-  ( ph -> F ( X Func Y ) G )
59 eqid 
 |-  ( Id ` Y ) = ( Id ` Y )
60 eqid 
 |-  ( Id ` X ) = ( Id ` X )
61 eqid 
 |-  ( comp ` Y ) = ( comp ` Y )
62 eqid 
 |-  ( comp ` X ) = ( comp ` X )
63 1 2 5 catcbas 
 |-  ( ph -> B = ( U i^i Cat ) )
64 inss2 
 |-  ( U i^i Cat ) C_ Cat
65 63 64 eqsstrdi 
 |-  ( ph -> B C_ Cat )
66 65 7 sseldd 
 |-  ( ph -> Y e. Cat )
67 65 6 sseldd 
 |-  ( ph -> X e. Cat )
68 f1ocnv 
 |-  ( F : R -1-1-onto-> S -> `' F : S -1-1-onto-> R )
69 f1of 
 |-  ( `' F : S -1-1-onto-> R -> `' F : S --> R )
70 11 68 69 3syl 
 |-  ( ph -> `' F : S --> R )
71 ovex 
 |-  ( ( `' F ` x ) G ( `' F ` y ) ) e. _V
72 71 cnvex 
 |-  `' ( ( `' F ` x ) G ( `' F ` y ) ) e. _V
73 9 72 fnmpoi 
 |-  H Fn ( S X. S )
74 73 a1i 
 |-  ( ph -> H Fn ( S X. S ) )
75 10 adantr 
 |-  ( ( ph /\ ( u e. S /\ v e. S ) ) -> F ( ( X Full Y ) i^i ( X Faith Y ) ) G )
76 70 ffvelrnda 
 |-  ( ( ph /\ u e. S ) -> ( `' F ` u ) e. R )
77 76 adantrr 
 |-  ( ( ph /\ ( u e. S /\ v e. S ) ) -> ( `' F ` u ) e. R )
78 70 ffvelrnda 
 |-  ( ( ph /\ v e. S ) -> ( `' F ` v ) e. R )
79 78 adantrl 
 |-  ( ( ph /\ ( u e. S /\ v e. S ) ) -> ( `' F ` v ) e. R )
80 3 39 40 75 77 79 ffthf1o 
 |-  ( ( 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 ) ) ) )
81 f1ocnv 
 |-  ( ( ( `' 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 ) ) )
82 f1of 
 |-  ( `' ( ( `' 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 ) ) )
83 80 81 82 3syl 
 |-  ( ( 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 ) ) )
84 simpl 
 |-  ( ( x = u /\ y = v ) -> x = u )
85 84 fveq2d 
 |-  ( ( x = u /\ y = v ) -> ( `' F ` x ) = ( `' F ` u ) )
86 simpr 
 |-  ( ( x = u /\ y = v ) -> y = v )
87 86 fveq2d 
 |-  ( ( x = u /\ y = v ) -> ( `' F ` y ) = ( `' F ` v ) )
88 85 87 oveq12d 
 |-  ( ( x = u /\ y = v ) -> ( ( `' F ` x ) G ( `' F ` y ) ) = ( ( `' F ` u ) G ( `' F ` v ) ) )
89 88 cnveqd 
 |-  ( ( x = u /\ y = v ) -> `' ( ( `' F ` x ) G ( `' F ` y ) ) = `' ( ( `' F ` u ) G ( `' F ` v ) ) )
90 ovex 
 |-  ( ( `' F ` u ) G ( `' F ` v ) ) e. _V
91 90 cnvex 
 |-  `' ( ( `' F ` u ) G ( `' F ` v ) ) e. _V
92 89 9 91 ovmpoa 
 |-  ( ( u e. S /\ v e. S ) -> ( u H v ) = `' ( ( `' F ` u ) G ( `' F ` v ) ) )
93 92 adantl 
 |-  ( ( ph /\ ( u e. S /\ v e. S ) ) -> ( u H v ) = `' ( ( `' F ` u ) G ( `' F ` v ) ) )
94 11 adantr 
 |-  ( ( ph /\ ( u e. S /\ v e. S ) ) -> F : R -1-1-onto-> S )
95 simprl 
 |-  ( ( ph /\ ( u e. S /\ v e. S ) ) -> u e. S )
96 f1ocnvfv2 
 |-  ( ( F : R -1-1-onto-> S /\ u e. S ) -> ( F ` ( `' F ` u ) ) = u )
97 94 95 96 syl2anc 
 |-  ( ( ph /\ ( u e. S /\ v e. S ) ) -> ( F ` ( `' F ` u ) ) = u )
98 simprr 
 |-  ( ( ph /\ ( u e. S /\ v e. S ) ) -> v e. S )
99 f1ocnvfv2 
 |-  ( ( F : R -1-1-onto-> S /\ v e. S ) -> ( F ` ( `' F ` v ) ) = v )
100 94 98 99 syl2anc 
 |-  ( ( ph /\ ( u e. S /\ v e. S ) ) -> ( F ` ( `' F ` v ) ) = v )
101 97 100 oveq12d 
 |-  ( ( ph /\ ( u e. S /\ v e. S ) ) -> ( ( F ` ( `' F ` u ) ) ( Hom ` Y ) ( F ` ( `' F ` v ) ) ) = ( u ( Hom ` Y ) v ) )
102 101 eqcomd 
 |-  ( ( ph /\ ( u e. S /\ v e. S ) ) -> ( u ( Hom ` Y ) v ) = ( ( F ` ( `' F ` u ) ) ( Hom ` Y ) ( F ` ( `' F ` v ) ) ) )
103 93 102 feq12d 
 |-  ( ( 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 ) ) ) )
104 83 103 mpbird 
 |-  ( ( ph /\ ( u e. S /\ v e. S ) ) -> ( u H v ) : ( u ( Hom ` Y ) v ) --> ( ( `' F ` u ) ( Hom ` X ) ( `' F ` v ) ) )
105 simpr 
 |-  ( ( ph /\ u e. S ) -> u e. S )
106 simpl 
 |-  ( ( x = u /\ y = u ) -> x = u )
107 106 fveq2d 
 |-  ( ( x = u /\ y = u ) -> ( `' F ` x ) = ( `' F ` u ) )
108 simpr 
 |-  ( ( x = u /\ y = u ) -> y = u )
109 108 fveq2d 
 |-  ( ( x = u /\ y = u ) -> ( `' F ` y ) = ( `' F ` u ) )
110 107 109 oveq12d 
 |-  ( ( x = u /\ y = u ) -> ( ( `' F ` x ) G ( `' F ` y ) ) = ( ( `' F ` u ) G ( `' F ` u ) ) )
111 110 cnveqd 
 |-  ( ( x = u /\ y = u ) -> `' ( ( `' F ` x ) G ( `' F ` y ) ) = `' ( ( `' F ` u ) G ( `' F ` u ) ) )
112 ovex 
 |-  ( ( `' F ` u ) G ( `' F ` u ) ) e. _V
113 112 cnvex 
 |-  `' ( ( `' F ` u ) G ( `' F ` u ) ) e. _V
114 111 9 113 ovmpoa 
 |-  ( ( u e. S /\ u e. S ) -> ( u H u ) = `' ( ( `' F ` u ) G ( `' F ` u ) ) )
115 105 105 114 syl2anc 
 |-  ( ( ph /\ u e. S ) -> ( u H u ) = `' ( ( `' F ` u ) G ( `' F ` u ) ) )
116 115 fveq1d 
 |-  ( ( ph /\ u e. S ) -> ( ( u H u ) ` ( ( Id ` Y ) ` u ) ) = ( `' ( ( `' F ` u ) G ( `' F ` u ) ) ` ( ( Id ` Y ) ` u ) ) )
117 58 adantr 
 |-  ( ( ph /\ u e. S ) -> F ( X Func Y ) G )
118 3 60 59 117 76 funcid 
 |-  ( ( ph /\ u e. S ) -> ( ( ( `' F ` u ) G ( `' F ` u ) ) ` ( ( Id ` X ) ` ( `' F ` u ) ) ) = ( ( Id ` Y ) ` ( F ` ( `' F ` u ) ) ) )
119 11 96 sylan 
 |-  ( ( ph /\ u e. S ) -> ( F ` ( `' F ` u ) ) = u )
120 119 fveq2d 
 |-  ( ( ph /\ u e. S ) -> ( ( Id ` Y ) ` ( F ` ( `' F ` u ) ) ) = ( ( Id ` Y ) ` u ) )
121 118 120 eqtrd 
 |-  ( ( ph /\ u e. S ) -> ( ( ( `' F ` u ) G ( `' F ` u ) ) ` ( ( Id ` X ) ` ( `' F ` u ) ) ) = ( ( Id ` Y ) ` u ) )
122 10 adantr 
 |-  ( ( ph /\ u e. S ) -> F ( ( X Full Y ) i^i ( X Faith Y ) ) G )
123 3 39 40 122 76 76 ffthf1o 
 |-  ( ( 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 ) ) ) )
124 67 adantr 
 |-  ( ( ph /\ u e. S ) -> X e. Cat )
125 3 39 60 124 76 catidcl 
 |-  ( ( ph /\ u e. S ) -> ( ( Id ` X ) ` ( `' F ` u ) ) e. ( ( `' F ` u ) ( Hom ` X ) ( `' F ` u ) ) )
126 f1ocnvfv 
 |-  ( ( ( ( `' 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 ) ) ) )
127 123 125 126 syl2anc 
 |-  ( ( 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 ) ) ) )
128 121 127 mpd 
 |-  ( ( ph /\ u e. S ) -> ( `' ( ( `' F ` u ) G ( `' F ` u ) ) ` ( ( Id ` Y ) ` u ) ) = ( ( Id ` X ) ` ( `' F ` u ) ) )
129 116 128 eqtrd 
 |-  ( ( ph /\ u e. S ) -> ( ( u H u ) ` ( ( Id ` Y ) ` u ) ) = ( ( Id ` X ) ` ( `' F ` u ) ) )
130 58 3ad2ant1 
 |-  ( ( 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 )
131 70 3ad2ant1 
 |-  ( ( 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 )
132 simp21 
 |-  ( ( 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 )
133 131 132 ffvelrnd 
 |-  ( ( 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 )
134 simp22 
 |-  ( ( 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 )
135 131 134 ffvelrnd 
 |-  ( ( 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 )
136 simp23 
 |-  ( ( 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 )
137 131 136 ffvelrnd 
 |-  ( ( 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 )
138 10 3ad2ant1 
 |-  ( ( 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 )
139 3 39 40 138 133 135 ffthf1o 
 |-  ( ( 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 ) ) ) )
140 11 3ad2ant1 
 |-  ( ( 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 )
141 140 132 96 syl2anc 
 |-  ( ( 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 )
142 140 134 99 syl2anc 
 |-  ( ( 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 )
143 141 142 oveq12d 
 |-  ( ( 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 ) )
144 143 f1oeq3d 
 |-  ( ( 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 ) ) )
145 139 144 mpbid 
 |-  ( ( 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 
 |-  ( ( ( `' 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 
 |-  ( `' ( ( `' 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 ) ) )
148 145 146 147 3syl 
 |-  ( ( 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 
 |-  ( ( 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 ) )
150 148 149 ffvelrnd 
 |-  ( ( 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 ) ) )
151 3 39 40 138 135 137 ffthf1o 
 |-  ( ( 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 
 |-  ( ( F : R -1-1-onto-> S /\ z e. S ) -> ( F ` ( `' F ` z ) ) = z )
153 140 136 152 syl2anc 
 |-  ( ( 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 )
154 142 153 oveq12d 
 |-  ( ( 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 154 f1oeq3d 
 |-  ( ( 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 ) ) )
156 151 155 mpbid 
 |-  ( ( 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 ) )
157 f1ocnv 
 |-  ( ( ( `' 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 ) ) )
158 f1of 
 |-  ( `' ( ( `' 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 ) ) )
159 156 157 158 3syl 
 |-  ( ( 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 ) ) )
160 simp3r 
 |-  ( ( 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 ) )
161 159 160 ffvelrnd 
 |-  ( ( 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 ) ) )
162 3 39 62 61 130 133 135 137 150 161 funcco 
 |-  ( ( 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 ) ) ) )
163 141 142 opeq12d 
 |-  ( ( 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 >. )
164 163 153 oveq12d 
 |-  ( ( 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 ) )
165 f1ocnvfv2 
 |-  ( ( ( ( `' 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 )
166 156 160 165 syl2anc 
 |-  ( ( 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 )
167 f1ocnvfv2 
 |-  ( ( ( ( `' 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 )
168 145 149 167 syl2anc 
 |-  ( ( 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 )
169 164 166 168 oveq123d 
 |-  ( ( 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 ) )
170 162 169 eqtrd 
 |-  ( ( 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 ) )
171 3 39 40 138 133 137 ffthf1o 
 |-  ( ( 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 ) ) ) )
172 141 153 oveq12d 
 |-  ( ( 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 ) )
173 172 f1oeq3d 
 |-  ( ( 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 ) ) )
174 171 173 mpbid 
 |-  ( ( 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 ) )
175 67 3ad2ant1 
 |-  ( ( 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 )
176 3 39 62 175 133 135 137 150 161 catcocl 
 |-  ( ( 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 ) ) )
177 f1ocnvfv 
 |-  ( ( ( ( `' 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 ) ) ) )
178 174 176 177 syl2anc 
 |-  ( ( 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 ) ) ) )
179 170 178 mpd 
 |-  ( ( 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 ) ) )
180 simpl 
 |-  ( ( x = u /\ y = z ) -> x = u )
181 180 fveq2d 
 |-  ( ( x = u /\ y = z ) -> ( `' F ` x ) = ( `' F ` u ) )
182 simpr 
 |-  ( ( x = u /\ y = z ) -> y = z )
183 182 fveq2d 
 |-  ( ( x = u /\ y = z ) -> ( `' F ` y ) = ( `' F ` z ) )
184 181 183 oveq12d 
 |-  ( ( x = u /\ y = z ) -> ( ( `' F ` x ) G ( `' F ` y ) ) = ( ( `' F ` u ) G ( `' F ` z ) ) )
185 184 cnveqd 
 |-  ( ( x = u /\ y = z ) -> `' ( ( `' F ` x ) G ( `' F ` y ) ) = `' ( ( `' F ` u ) G ( `' F ` z ) ) )
186 ovex 
 |-  ( ( `' F ` u ) G ( `' F ` z ) ) e. _V
187 186 cnvex 
 |-  `' ( ( `' F ` u ) G ( `' F ` z ) ) e. _V
188 185 9 187 ovmpoa 
 |-  ( ( u e. S /\ z e. S ) -> ( u H z ) = `' ( ( `' F ` u ) G ( `' F ` z ) ) )
189 132 136 188 syl2anc 
 |-  ( ( 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 ) ) )
190 189 fveq1d 
 |-  ( ( 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 ) ) )
191 simpl 
 |-  ( ( x = v /\ y = z ) -> x = v )
192 191 fveq2d 
 |-  ( ( x = v /\ y = z ) -> ( `' F ` x ) = ( `' F ` v ) )
193 simpr 
 |-  ( ( x = v /\ y = z ) -> y = z )
194 193 fveq2d 
 |-  ( ( x = v /\ y = z ) -> ( `' F ` y ) = ( `' F ` z ) )
195 192 194 oveq12d 
 |-  ( ( x = v /\ y = z ) -> ( ( `' F ` x ) G ( `' F ` y ) ) = ( ( `' F ` v ) G ( `' F ` z ) ) )
196 195 cnveqd 
 |-  ( ( x = v /\ y = z ) -> `' ( ( `' F ` x ) G ( `' F ` y ) ) = `' ( ( `' F ` v ) G ( `' F ` z ) ) )
197 ovex 
 |-  ( ( `' F ` v ) G ( `' F ` z ) ) e. _V
198 197 cnvex 
 |-  `' ( ( `' F ` v ) G ( `' F ` z ) ) e. _V
199 196 9 198 ovmpoa 
 |-  ( ( v e. S /\ z e. S ) -> ( v H z ) = `' ( ( `' F ` v ) G ( `' F ` z ) ) )
200 134 136 199 syl2anc 
 |-  ( ( 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 ) ) )
201 200 fveq1d 
 |-  ( ( 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 ) )
202 132 134 92 syl2anc 
 |-  ( ( 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 ) ) )
203 202 fveq1d 
 |-  ( ( 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 ) )
204 201 203 oveq12d 
 |-  ( ( 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 ) ) )
205 179 190 204 3eqtr4d 
 |-  ( ( 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 ) ) )
206 4 3 40 39 59 60 61 62 66 67 70 74 104 129 205 isfuncd 
 |-  ( ph -> `' F ( Y Func X ) H )
207 3 58 206 cofuval2 
 |-  ( 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 ) ) ) >. )
208 eqid 
 |-  ( idFunc ` X ) = ( idFunc ` X )
209 208 3 67 39 idfuval 
 |-  ( ph -> ( idFunc ` X ) = <. ( _I |` R ) , ( z e. ( R X. R ) |-> ( _I |` ( ( Hom ` X ) ` z ) ) ) >. )
210 53 207 209 3eqtr4d 
 |-  ( ph -> ( <. `' F , H >. o.func <. F , G >. ) = ( idFunc ` X ) )
211 eqid 
 |-  ( comp ` C ) = ( comp ` C )
212 df-br 
 |-  ( F ( X Func Y ) G <-> <. F , G >. e. ( X Func Y ) )
213 58 212 sylib 
 |-  ( ph -> <. F , G >. e. ( X Func Y ) )
214 df-br 
 |-  ( `' F ( Y Func X ) H <-> <. `' F , H >. e. ( Y Func X ) )
215 206 214 sylib 
 |-  ( ph -> <. `' F , H >. e. ( Y Func X ) )
216 1 2 5 211 6 7 6 213 215 catcco 
 |-  ( ph -> ( <. `' F , H >. ( <. X , Y >. ( comp ` C ) X ) <. F , G >. ) = ( <. `' F , H >. o.func <. F , G >. ) )
217 eqid 
 |-  ( Id ` C ) = ( Id ` C )
218 1 2 217 208 5 6 catcid 
 |-  ( ph -> ( ( Id ` C ) ` X ) = ( idFunc ` X ) )
219 210 216 218 3eqtr4d 
 |-  ( ph -> ( <. `' F , H >. ( <. X , Y >. ( comp ` C ) X ) <. F , G >. ) = ( ( Id ` C ) ` X ) )
220 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
221 eqid 
 |-  ( Sect ` C ) = ( Sect ` C )
222 1 catccat 
 |-  ( U e. V -> C e. Cat )
223 5 222 syl 
 |-  ( ph -> C e. Cat )
224 1 2 5 220 6 7 catchom 
 |-  ( ph -> ( X ( Hom ` C ) Y ) = ( X Func Y ) )
225 213 224 eleqtrrd 
 |-  ( ph -> <. F , G >. e. ( X ( Hom ` C ) Y ) )
226 1 2 5 220 7 6 catchom 
 |-  ( ph -> ( Y ( Hom ` C ) X ) = ( Y Func X ) )
227 215 226 eleqtrrd 
 |-  ( ph -> <. `' F , H >. e. ( Y ( Hom ` C ) X ) )
228 2 220 211 217 221 223 6 7 225 227 issect2 
 |-  ( ph -> ( <. F , G >. ( X ( Sect ` C ) Y ) <. `' F , H >. <-> ( <. `' F , H >. ( <. X , Y >. ( comp ` C ) X ) <. F , G >. ) = ( ( Id ` C ) ` X ) ) )
229 219 228 mpbird 
 |-  ( ph -> <. F , G >. ( X ( Sect ` C ) Y ) <. `' F , H >. )
230 f1ococnv2 
 |-  ( F : R -1-1-onto-> S -> ( F o. `' F ) = ( _I |` S ) )
231 11 230 syl 
 |-  ( ph -> ( F o. `' F ) = ( _I |` S ) )
232 92 3adant1 
 |-  ( ( ph /\ u e. S /\ v e. S ) -> ( u H v ) = `' ( ( `' F ` u ) G ( `' F ` v ) ) )
233 232 coeq2d 
 |-  ( ( 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 ) ) ) )
234 10 3ad2ant1 
 |-  ( ( ph /\ u e. S /\ v e. S ) -> F ( ( X Full Y ) i^i ( X Faith Y ) ) G )
235 76 3adant3 
 |-  ( ( ph /\ u e. S /\ v e. S ) -> ( `' F ` u ) e. R )
236 78 3adant2 
 |-  ( ( ph /\ u e. S /\ v e. S ) -> ( `' F ` v ) e. R )
237 3 39 40 234 235 236 ffthf1o 
 |-  ( ( 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 ) ) ) )
238 101 3impb 
 |-  ( ( ph /\ u e. S /\ v e. S ) -> ( ( F ` ( `' F ` u ) ) ( Hom ` Y ) ( F ` ( `' F ` v ) ) ) = ( u ( Hom ` Y ) v ) )
239 238 f1oeq3d 
 |-  ( ( 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 ) ) )
240 237 239 mpbid 
 |-  ( ( 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 ) )
241 f1ococnv2 
 |-  ( ( ( `' 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 ) ) )
242 240 241 syl 
 |-  ( ( ph /\ u e. S /\ v e. S ) -> ( ( ( `' F ` u ) G ( `' F ` v ) ) o. `' ( ( `' F ` u ) G ( `' F ` v ) ) ) = ( _I |` ( u ( Hom ` Y ) v ) ) )
243 233 242 eqtrd 
 |-  ( ( ph /\ u e. S /\ v e. S ) -> ( ( ( `' F ` u ) G ( `' F ` v ) ) o. ( u H v ) ) = ( _I |` ( u ( Hom ` Y ) v ) ) )
244 243 mpoeq3dva 
 |-  ( 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 ) ) ) )
245 fveq2 
 |-  ( z = <. u , v >. -> ( ( Hom ` Y ) ` z ) = ( ( Hom ` Y ) ` <. u , v >. ) )
246 df-ov 
 |-  ( u ( Hom ` Y ) v ) = ( ( Hom ` Y ) ` <. u , v >. )
247 245 246 eqtr4di 
 |-  ( z = <. u , v >. -> ( ( Hom ` Y ) ` z ) = ( u ( Hom ` Y ) v ) )
248 247 reseq2d 
 |-  ( z = <. u , v >. -> ( _I |` ( ( Hom ` Y ) ` z ) ) = ( _I |` ( u ( Hom ` Y ) v ) ) )
249 248 mpompt 
 |-  ( z e. ( S X. S ) |-> ( _I |` ( ( Hom ` Y ) ` z ) ) ) = ( u e. S , v e. S |-> ( _I |` ( u ( Hom ` Y ) v ) ) )
250 244 249 eqtr4di 
 |-  ( 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 ) ) ) )
251 231 250 opeq12d 
 |-  ( 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 ) ) ) >. )
252 4 206 58 cofuval2 
 |-  ( 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 ) ) ) >. )
253 eqid 
 |-  ( idFunc ` Y ) = ( idFunc ` Y )
254 253 4 66 40 idfuval 
 |-  ( ph -> ( idFunc ` Y ) = <. ( _I |` S ) , ( z e. ( S X. S ) |-> ( _I |` ( ( Hom ` Y ) ` z ) ) ) >. )
255 251 252 254 3eqtr4d 
 |-  ( ph -> ( <. F , G >. o.func <. `' F , H >. ) = ( idFunc ` Y ) )
256 1 2 5 211 7 6 7 215 213 catcco 
 |-  ( ph -> ( <. F , G >. ( <. Y , X >. ( comp ` C ) Y ) <. `' F , H >. ) = ( <. F , G >. o.func <. `' F , H >. ) )
257 1 2 217 253 5 7 catcid 
 |-  ( ph -> ( ( Id ` C ) ` Y ) = ( idFunc ` Y ) )
258 255 256 257 3eqtr4d 
 |-  ( ph -> ( <. F , G >. ( <. Y , X >. ( comp ` C ) Y ) <. `' F , H >. ) = ( ( Id ` C ) ` Y ) )
259 2 220 211 217 221 223 7 6 227 225 issect2 
 |-  ( ph -> ( <. `' F , H >. ( Y ( Sect ` C ) X ) <. F , G >. <-> ( <. F , G >. ( <. Y , X >. ( comp ` C ) Y ) <. `' F , H >. ) = ( ( Id ` C ) ` Y ) ) )
260 258 259 mpbird 
 |-  ( ph -> <. `' F , H >. ( Y ( Sect ` C ) X ) <. F , G >. )
261 2 8 223 6 7 221 isinv 
 |-  ( ph -> ( <. F , G >. ( X I Y ) <. `' F , H >. <-> ( <. F , G >. ( X ( Sect ` C ) Y ) <. `' F , H >. /\ <. `' F , H >. ( Y ( Sect ` C ) X ) <. F , G >. ) ) )
262 229 260 261 mpbir2and 
 |-  ( ph -> <. F , G >. ( X I Y ) <. `' F , H >. )