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 bitrid ⊢ 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 bitrid ⊢ 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 bitrid ⊢ 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 bitrid ⊢ 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 biimtrrid ⊢ φ ∧ 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 biimtrrid ⊢ φ ∧ 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 biimtrrid ⊢ φ ∧ 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