Metamath Proof Explorer


Theorem catpropd

Description: Two structures with the same base, hom-sets and composition operation are either both categories or neither. (Contributed by Mario Carneiro, 5-Jan-2017)

Ref Expression
Hypotheses catpropd.1 φ Hom 𝑓 C = Hom 𝑓 D
catpropd.2 φ comp 𝑓 C = comp 𝑓 D
catpropd.3 φ C V
catpropd.4 φ D W
Assertion catpropd φ C Cat D Cat

Proof

Step Hyp Ref Expression
1 catpropd.1 φ Hom 𝑓 C = Hom 𝑓 D
2 catpropd.2 φ comp 𝑓 C = comp 𝑓 D
3 catpropd.3 φ C V
4 catpropd.4 φ D W
5 simpl g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f g x y comp C z f x Hom C z
6 5 2ralimi f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f f x Hom C y g y Hom C z g x y comp C z f x Hom C z
7 6 2ralimi y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z
8 7 adantl g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z
9 8 ralimi x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z
10 9 a1i φ x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z
11 simpl g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f g x y comp C z f x Hom C z
12 11 2ralimi f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f f x Hom C y g y Hom C z g x y comp C z f x Hom C z
13 12 2ralimi y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z
14 13 adantl g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z
15 14 ralimi x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z
16 15 a1i φ x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z
17 nfra1 y y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z
18 nfv x z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w
19 nfra1 z z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z
20 nfv y w Base C g x Hom C z h z Hom C w h x z comp C w g x Hom C w
21 nfra1 g g y Hom C z g x y comp C z f x Hom C z
22 nfv f h y Hom C z h x y comp C z g x Hom C z
23 oveq1 g = h g x y comp C z f = h x y comp C z f
24 23 eleq1d g = h g x y comp C z f x Hom C z h x y comp C z f x Hom C z
25 24 cbvralvw g y Hom C z g x y comp C z f x Hom C z h y Hom C z h x y comp C z f x Hom C z
26 oveq2 f = g h x y comp C z f = h x y comp C z g
27 26 eleq1d f = g h x y comp C z f x Hom C z h x y comp C z g x Hom C z
28 27 ralbidv f = g h y Hom C z h x y comp C z f x Hom C z h y Hom C z h x y comp C z g x Hom C z
29 25 28 syl5bb f = g g y Hom C z g x y comp C z f x Hom C z h y Hom C z h x y comp C z g x Hom C z
30 21 22 29 cbvralw f x Hom C y g y Hom C z g x y comp C z f x Hom C z g x Hom C y h y Hom C z h x y comp C z g x Hom C z
31 oveq2 z = w y Hom C z = y Hom C w
32 oveq2 z = w x y comp C z = x y comp C w
33 32 oveqd z = w h x y comp C z g = h x y comp C w g
34 oveq2 z = w x Hom C z = x Hom C w
35 33 34 eleq12d z = w h x y comp C z g x Hom C z h x y comp C w g x Hom C w
36 31 35 raleqbidv z = w h y Hom C z h x y comp C z g x Hom C z h y Hom C w h x y comp C w g x Hom C w
37 36 ralbidv z = w g x Hom C y h y Hom C z h x y comp C z g x Hom C z g x Hom C y h y Hom C w h x y comp C w g x Hom C w
38 30 37 syl5bb z = w f x Hom C y g y Hom C z g x y comp C z f x Hom C z g x Hom C y h y Hom C w h x y comp C w g x Hom C w
39 38 cbvralvw z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C g x Hom C y h y Hom C w h x y comp C w g x Hom C w
40 oveq2 y = z x Hom C y = x Hom C z
41 oveq1 y = z y Hom C w = z Hom C w
42 opeq2 y = z x y = x z
43 42 oveq1d y = z x y comp C w = x z comp C w
44 43 oveqd y = z h x y comp C w g = h x z comp C w g
45 44 eleq1d y = z h x y comp C w g x Hom C w h x z comp C w g x Hom C w
46 41 45 raleqbidv y = z h y Hom C w h x y comp C w g x Hom C w h z Hom C w h x z comp C w g x Hom C w
47 40 46 raleqbidv y = z g x Hom C y h y Hom C w h x y comp C w g x Hom C w g x Hom C z h z Hom C w h x z comp C w g x Hom C w
48 47 ralbidv y = z w Base C g x Hom C y h y Hom C w h x y comp C w g x Hom C w w Base C g x Hom C z h z Hom C w h x z comp C w g x Hom C w
49 39 48 syl5bb y = z z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C g x Hom C z h z Hom C w h x z comp C w g x Hom C w
50 19 20 49 cbvralw y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z z Base C w Base C g x Hom C z h z Hom C w h x z comp C w g x Hom C w
51 oveq1 x = y x Hom C z = y Hom C z
52 opeq1 x = y x z = y z
53 52 oveq1d x = y x z comp C w = y z comp C w
54 53 oveqd x = y h x z comp C w g = h y z comp C w g
55 oveq1 x = y x Hom C w = y Hom C w
56 54 55 eleq12d x = y h x z comp C w g x Hom C w h y z comp C w g y Hom C w
57 56 ralbidv x = y h z Hom C w h x z comp C w g x Hom C w h z Hom C w h y z comp C w g y Hom C w
58 51 57 raleqbidv x = y g x Hom C z h z Hom C w h x z comp C w g x Hom C w g y Hom C z h z Hom C w h y z comp C w g y Hom C w
59 58 ralbidv x = y w Base C g x Hom C z h z Hom C w h x z comp C w g x Hom C w w Base C g y Hom C z h z Hom C w h y z comp C w g y Hom C w
60 ralcom w Base C g y Hom C z h z Hom C w h y z comp C w g y Hom C w g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w
61 59 60 bitrdi x = y w Base C g x Hom C z h z Hom C w h x z comp C w g x Hom C w g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w
62 61 ralbidv x = y z Base C w Base C g x Hom C z h z Hom C w h x z comp C w g x Hom C w z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w
63 50 62 syl5bb x = y y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w
64 17 18 63 cbvralw x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z y Base C z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w
65 64 biimpi x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z y Base C z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w
66 65 ancri x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z y Base C z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z
67 r19.26 y Base C z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z y Base C z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z
68 r19.26 z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w f x Hom C y g y Hom C z g x y comp C z f x Hom C z z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z
69 r19.26 g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w g x y comp C z f x Hom C z g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w g y Hom C z g x y comp C z f x Hom C z
70 eqid Base C = Base C
71 eqid Hom C = Hom C
72 eqid comp C = comp C
73 eqid comp D = comp D
74 1 adantr φ x Base C Hom 𝑓 C = Hom 𝑓 D
75 74 ad4antr φ x Base C y Base C z Base C f x Hom C y g y Hom C z Hom 𝑓 C = Hom 𝑓 D
76 75 ad4antr φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w Hom 𝑓 C = Hom 𝑓 D
77 2 ad5antr φ x Base C y Base C z Base C f x Hom C y g y Hom C z comp 𝑓 C = comp 𝑓 D
78 77 ad4antr φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w comp 𝑓 C = comp 𝑓 D
79 simpllr φ x Base C y Base C z Base C x Base C
80 79 ad2antrr φ x Base C y Base C z Base C f x Hom C y g y Hom C z x Base C
81 80 ad4antr φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w x Base C
82 simp-4r φ x Base C y Base C z Base C f x Hom C y g y Hom C z y Base C
83 82 ad4antr φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w y Base C
84 simpllr φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w w Base C
85 simplr φ x Base C y Base C z Base C f x Hom C y g y Hom C z f x Hom C y
86 85 ad4antr φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w f x Hom C y
87 simpr φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w h y z comp C w g y Hom C w
88 70 71 72 73 76 78 81 83 84 86 87 comfeqval φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w h y z comp C w g x y comp C w f = h y z comp C w g x y comp D w f
89 simpllr φ x Base C y Base C z Base C f x Hom C y g y Hom C z z Base C
90 89 ad4antr φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w z Base C
91 simp-4r φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w g x y comp C z f x Hom C z
92 simplr φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w h z Hom C w
93 70 71 72 73 76 78 81 90 84 91 92 comfeqval φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w h x z comp C w g x y comp C z f = h x z comp D w g x y comp C z f
94 88 93 eqeq12d φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
95 94 ex φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
96 95 ralimdva φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
97 ralbi h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
98 96 97 syl6 φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
99 98 ralimdva φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
100 99 impancom φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
101 100 impr φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
102 ralbi w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
103 101 102 syl φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
104 103 anbi2d φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w g x y comp C z f x Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
105 104 ex φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w g x y comp C z f x Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
106 105 ralimdva φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w g x y comp C z f x Hom C z g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
107 69 106 syl5bir φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w g y Hom C z g x y comp C z f x Hom C z g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
108 107 expdimp φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w g y Hom C z g x y comp C z f x Hom C z g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
109 ralbi g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
110 108 109 syl6 φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w g y Hom C z g x y comp C z f x Hom C z g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
111 110 an32s φ x Base C y Base C z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w f x Hom C y g y Hom C z g x y comp C z f x Hom C z g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
112 111 ralimdva φ x Base C y Base C z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w f x Hom C y g y Hom C z g x y comp C z f x Hom C z f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
113 ralbi f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
114 112 113 syl6 φ x Base C y Base C z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w f x Hom C y g y Hom C z g x y comp C z f x Hom C z f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
115 114 expimpd φ x Base C y Base C z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w f x Hom C y g y Hom C z g x y comp C z f x Hom C z f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
116 115 ralimdva φ x Base C y Base C z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w f x Hom C y g y Hom C z g x y comp C z f x Hom C z z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
117 ralbi z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
118 116 117 syl6 φ x Base C y Base C z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w f x Hom C y g y Hom C z g x y comp C z f x Hom C z z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
119 68 118 syl5bir φ x Base C y Base C z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
120 119 ralimdva φ x Base C y Base C z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
121 ralbi y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
122 120 121 syl6 φ x Base C y Base C z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
123 67 122 syl5bir φ x Base C y Base C z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
124 123 imp φ x Base C y Base C z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
125 124 an4s φ y Base C z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
126 125 anbi2d φ y Base C z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
127 126 expr φ y Base C z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
128 127 ralimdva φ y Base C z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
129 128 expimpd φ y Base C z Base C g y Hom C z w Base C h z Hom C w h y z comp C w g y Hom C w x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
130 ralbi x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
131 66 129 130 syl56 φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
132 10 16 131 pm5.21ndd φ x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f
133 1 homfeqbas φ Base C = Base D
134 eqid Hom D = Hom D
135 simpr φ x Base C x Base C
136 70 71 134 74 135 135 homfeqval φ x Base C x Hom C x = x Hom D x
137 133 ad2antrr φ x Base C g x Hom C x Base C = Base D
138 74 ad2antrr φ x Base C g x Hom C x y Base C Hom 𝑓 C = Hom 𝑓 D
139 simpr φ x Base C g x Hom C x y Base C y Base C
140 simpllr φ x Base C g x Hom C x y Base C x Base C
141 70 71 134 138 139 140 homfeqval φ x Base C g x Hom C x y Base C y Hom C x = y Hom D x
142 1 ad4antr φ x Base C g x Hom C x y Base C f y Hom C x Hom 𝑓 C = Hom 𝑓 D
143 2 ad4antr φ x Base C g x Hom C x y Base C f y Hom C x comp 𝑓 C = comp 𝑓 D
144 simplr φ x Base C g x Hom C x y Base C f y Hom C x y Base C
145 simp-4r φ x Base C g x Hom C x y Base C f y Hom C x x Base C
146 simpr φ x Base C g x Hom C x y Base C f y Hom C x f y Hom C x
147 simpllr φ x Base C g x Hom C x y Base C f y Hom C x g x Hom C x
148 70 71 72 73 142 143 144 145 145 146 147 comfeqval φ x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = g y x comp D x f
149 148 eqeq1d φ x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f g y x comp D x f = f
150 141 149 raleqbidva φ x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f y Hom D x g y x comp D x f = f
151 70 71 134 138 140 139 homfeqval φ x Base C g x Hom C x y Base C x Hom C y = x Hom D y
152 1 ad4antr φ x Base C g x Hom C x y Base C f x Hom C y Hom 𝑓 C = Hom 𝑓 D
153 2 ad4antr φ x Base C g x Hom C x y Base C f x Hom C y comp 𝑓 C = comp 𝑓 D
154 simp-4r φ x Base C g x Hom C x y Base C f x Hom C y x Base C
155 simplr φ x Base C g x Hom C x y Base C f x Hom C y y Base C
156 simpllr φ x Base C g x Hom C x y Base C f x Hom C y g x Hom C x
157 simpr φ x Base C g x Hom C x y Base C f x Hom C y f x Hom C y
158 70 71 72 73 152 153 154 154 155 156 157 comfeqval φ x Base C g x Hom C x y Base C f x Hom C y f x x comp C y g = f x x comp D y g
159 158 eqeq1d φ x Base C g x Hom C x y Base C f x Hom C y f x x comp C y g = f f x x comp D y g = f
160 151 159 raleqbidva φ x Base C g x Hom C x y Base C f x Hom C y f x x comp C y g = f f x Hom D y f x x comp D y g = f
161 150 160 anbi12d φ x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f f y Hom D x g y x comp D x f = f f x Hom D y f x x comp D y g = f
162 137 161 raleqbidva φ x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base D f y Hom D x g y x comp D x f = f f x Hom D y f x x comp D y g = f
163 136 162 rexeqbidva φ x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f g x Hom D x y Base D f y Hom D x g y x comp D x f = f f x Hom D y f x x comp D y g = f
164 133 adantr φ x Base C Base C = Base D
165 164 adantr φ x Base C y Base C Base C = Base D
166 74 ad2antrr φ x Base C y Base C z Base C Hom 𝑓 C = Hom 𝑓 D
167 simplr φ x Base C y Base C z Base C y Base C
168 70 71 134 166 79 167 homfeqval φ x Base C y Base C z Base C x Hom C y = x Hom D y
169 simpr φ x Base C y Base C z Base C z Base C
170 70 71 134 166 167 169 homfeqval φ x Base C y Base C z Base C y Hom C z = y Hom D z
171 170 adantr φ x Base C y Base C z Base C f x Hom C y y Hom C z = y Hom D z
172 simpr φ x Base C y Base C z Base C f x Hom C y g y Hom C z g y Hom C z
173 70 71 72 73 75 77 80 82 89 85 172 comfeqval φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f = g x y comp D z f
174 70 71 134 166 79 169 homfeqval φ x Base C y Base C z Base C x Hom C z = x Hom D z
175 174 ad2antrr φ x Base C y Base C z Base C f x Hom C y g y Hom C z x Hom C z = x Hom D z
176 173 175 eleq12d φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z g x y comp D z f x Hom D z
177 164 ad4antr φ x Base C y Base C z Base C f x Hom C y g y Hom C z Base C = Base D
178 75 adantr φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C Hom 𝑓 C = Hom 𝑓 D
179 simp-4r φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C z Base C
180 simpr φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C w Base C
181 70 71 134 178 179 180 homfeqval φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C z Hom C w = z Hom D w
182 166 ad4antr φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w Hom 𝑓 C = Hom 𝑓 D
183 2 ad7antr φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w comp 𝑓 C = comp 𝑓 D
184 167 ad4antr φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w y Base C
185 169 ad4antr φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w z Base C
186 simplr φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w w Base C
187 simpllr φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w g y Hom C z
188 simpr φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w h z Hom C w
189 70 71 72 73 182 183 184 185 186 187 188 comfeqval φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w h y z comp C w g = h y z comp D w g
190 189 oveq1d φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h y z comp D w g x y comp D w f
191 79 ad4antr φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w x Base C
192 simp-4r φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w f x Hom C y
193 70 71 72 73 182 183 191 184 185 192 187 comfeqval φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w g x y comp C z f = g x y comp D z f
194 193 oveq2d φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w h x z comp D w g x y comp C z f = h x z comp D w g x y comp D z f
195 190 194 eqeq12d φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f h y z comp D w g x y comp D w f = h x z comp D w g x y comp D z f
196 181 195 raleqbidva φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f h z Hom D w h y z comp D w g x y comp D w f = h x z comp D w g x y comp D z f
197 177 196 raleqbidva φ x Base C y Base C z Base C f x Hom C y g y Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f w Base D h z Hom D w h y z comp D w g x y comp D w f = h x z comp D w g x y comp D z f
198 176 197 anbi12d φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f g x y comp D z f x Hom D z w Base D h z Hom D w h y z comp D w g x y comp D w f = h x z comp D w g x y comp D z f
199 171 198 raleqbidva φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f g y Hom D z g x y comp D z f x Hom D z w Base D h z Hom D w h y z comp D w g x y comp D w f = h x z comp D w g x y comp D z f
200 168 199 raleqbidva φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f f x Hom D y g y Hom D z g x y comp D z f x Hom D z w Base D h z Hom D w h y z comp D w g x y comp D w f = h x z comp D w g x y comp D z f
201 165 200 raleqbidva φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f z Base D f x Hom D y g y Hom D z g x y comp D z f x Hom D z w Base D h z Hom D w h y z comp D w g x y comp D w f = h x z comp D w g x y comp D z f
202 164 201 raleqbidva φ x Base C y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f y Base D z Base D f x Hom D y g y Hom D z g x y comp D z f x Hom D z w Base D h z Hom D w h y z comp D w g x y comp D w f = h x z comp D w g x y comp D z f
203 163 202 anbi12d φ x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f g x Hom D x y Base D f y Hom D x g y x comp D x f = f f x Hom D y f x x comp D y g = f y Base D z Base D f x Hom D y g y Hom D z g x y comp D z f x Hom D z w Base D h z Hom D w h y z comp D w g x y comp D w f = h x z comp D w g x y comp D z f
204 133 203 raleqbidva φ x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp D w f = h x z comp D w g x y comp C z f x Base D g x Hom D x y Base D f y Hom D x g y x comp D x f = f f x Hom D y f x x comp D y g = f y Base D z Base D f x Hom D y g y Hom D z g x y comp D z f x Hom D z w Base D h z Hom D w h y z comp D w g x y comp D w f = h x z comp D w g x y comp D z f
205 132 204 bitrd φ x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f x Base D g x Hom D x y Base D f y Hom D x g y x comp D x f = f f x Hom D y f x x comp D y g = f y Base D z Base D f x Hom D y g y Hom D z g x y comp D z f x Hom D z w Base D h z Hom D w h y z comp D w g x y comp D w f = h x z comp D w g x y comp D z f
206 70 71 72 iscat C V C Cat x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f
207 3 206 syl φ C Cat x Base C g x Hom C x y Base C f y Hom C x g y x comp C x f = f f x Hom C y f x x comp C y g = f y Base C z Base C f x Hom C y g y Hom C z g x y comp C z f x Hom C z w Base C h z Hom C w h y z comp C w g x y comp C w f = h x z comp C w g x y comp C z f
208 eqid Base D = Base D
209 208 134 73 iscat D W D Cat x Base D g x Hom D x y Base D f y Hom D x g y x comp D x f = f f x Hom D y f x x comp D y g = f y Base D z Base D f x Hom D y g y Hom D z g x y comp D z f x Hom D z w Base D h z Hom D w h y z comp D w g x y comp D w f = h x z comp D w g x y comp D z f
210 4 209 syl φ D Cat x Base D g x Hom D x y Base D f y Hom D x g y x comp D x f = f f x Hom D y f x x comp D y g = f y Base D z Base D f x Hom D y g y Hom D z g x y comp D z f x Hom D z w Base D h z Hom D w h y z comp D w g x y comp D w f = h x z comp D w g x y comp D z f
211 205 207 210 3bitr4d φ C Cat D Cat