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 ⊢gxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf→gxycomp⁡Czf∈xHom⁡Cz
6 5 2ralimi ⊢∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf→∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz
7 6 2ralimi ⊢∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf→∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz
8 7 adantl ⊢∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf→∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz
9 8 ralimi ⊢∀x∈BaseC∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf→∀x∈BaseC∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz
10 9 a1i ⊢φ→∀x∈BaseC∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf→∀x∈BaseC∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz
11 simpl ⊢gxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf→gxycomp⁡Czf∈xHom⁡Cz
12 11 2ralimi ⊢∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf→∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz
13 12 2ralimi ⊢∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf→∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz
14 13 adantl ⊢∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf→∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz
15 14 ralimi ⊢∀x∈BaseC∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf→∀x∈BaseC∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz
16 15 a1i ⊢φ→∀x∈BaseC∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf→∀x∈BaseC∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz
17 nfra1 ⊢Ⅎy∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz
18 nfv ⊢Ⅎx∀z∈BaseC∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw
19 nfra1 ⊢Ⅎz∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz
20 nfv ⊢Ⅎy∀w∈BaseC∀g∈xHom⁡Cz∀h∈zHom⁡Cwhxzcomp⁡Cwg∈xHom⁡Cw
21 nfra1 ⊢Ⅎg∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz
22 nfv ⊢Ⅎf∀h∈yHom⁡Czhxycomp⁡Czg∈xHom⁡Cz
23 oveq1 ⊢g=h→gxycomp⁡Czf=hxycomp⁡Czf
24 23 eleq1d ⊢g=h→gxycomp⁡Czf∈xHom⁡Cz↔hxycomp⁡Czf∈xHom⁡Cz
25 24 cbvralvw ⊢∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz↔∀h∈yHom⁡Czhxycomp⁡Czf∈xHom⁡Cz
26 oveq2 ⊢f=g→hxycomp⁡Czf=hxycomp⁡Czg
27 26 eleq1d ⊢f=g→hxycomp⁡Czf∈xHom⁡Cz↔hxycomp⁡Czg∈xHom⁡Cz
28 27 ralbidv ⊢f=g→∀h∈yHom⁡Czhxycomp⁡Czf∈xHom⁡Cz↔∀h∈yHom⁡Czhxycomp⁡Czg∈xHom⁡Cz
29 25 28 bitrid ⊢f=g→∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz↔∀h∈yHom⁡Czhxycomp⁡Czg∈xHom⁡Cz
30 21 22 29 cbvralw ⊢∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz↔∀g∈xHom⁡Cy∀h∈yHom⁡Czhxycomp⁡Czg∈xHom⁡Cz
31 oveq2 ⊢z=w→yHom⁡Cz=yHom⁡Cw
32 oveq2 ⊢z=w→xycomp⁡Cz=xycomp⁡Cw
33 32 oveqd ⊢z=w→hxycomp⁡Czg=hxycomp⁡Cwg
34 oveq2 ⊢z=w→xHom⁡Cz=xHom⁡Cw
35 33 34 eleq12d ⊢z=w→hxycomp⁡Czg∈xHom⁡Cz↔hxycomp⁡Cwg∈xHom⁡Cw
36 31 35 raleqbidv ⊢z=w→∀h∈yHom⁡Czhxycomp⁡Czg∈xHom⁡Cz↔∀h∈yHom⁡Cwhxycomp⁡Cwg∈xHom⁡Cw
37 36 ralbidv ⊢z=w→∀g∈xHom⁡Cy∀h∈yHom⁡Czhxycomp⁡Czg∈xHom⁡Cz↔∀g∈xHom⁡Cy∀h∈yHom⁡Cwhxycomp⁡Cwg∈xHom⁡Cw
38 30 37 bitrid ⊢z=w→∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz↔∀g∈xHom⁡Cy∀h∈yHom⁡Cwhxycomp⁡Cwg∈xHom⁡Cw
39 38 cbvralvw ⊢∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz↔∀w∈BaseC∀g∈xHom⁡Cy∀h∈yHom⁡Cwhxycomp⁡Cwg∈xHom⁡Cw
40 oveq2 ⊢y=z→xHom⁡Cy=xHom⁡Cz
41 oveq1 ⊢y=z→yHom⁡Cw=zHom⁡Cw
42 opeq2 ⊢y=z→xy=xz
43 42 oveq1d ⊢y=z→xycomp⁡Cw=xzcomp⁡Cw
44 43 oveqd ⊢y=z→hxycomp⁡Cwg=hxzcomp⁡Cwg
45 44 eleq1d ⊢y=z→hxycomp⁡Cwg∈xHom⁡Cw↔hxzcomp⁡Cwg∈xHom⁡Cw
46 41 45 raleqbidv ⊢y=z→∀h∈yHom⁡Cwhxycomp⁡Cwg∈xHom⁡Cw↔∀h∈zHom⁡Cwhxzcomp⁡Cwg∈xHom⁡Cw
47 40 46 raleqbidv ⊢y=z→∀g∈xHom⁡Cy∀h∈yHom⁡Cwhxycomp⁡Cwg∈xHom⁡Cw↔∀g∈xHom⁡Cz∀h∈zHom⁡Cwhxzcomp⁡Cwg∈xHom⁡Cw
48 47 ralbidv ⊢y=z→∀w∈BaseC∀g∈xHom⁡Cy∀h∈yHom⁡Cwhxycomp⁡Cwg∈xHom⁡Cw↔∀w∈BaseC∀g∈xHom⁡Cz∀h∈zHom⁡Cwhxzcomp⁡Cwg∈xHom⁡Cw
49 39 48 bitrid ⊢y=z→∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz↔∀w∈BaseC∀g∈xHom⁡Cz∀h∈zHom⁡Cwhxzcomp⁡Cwg∈xHom⁡Cw
50 19 20 49 cbvralw ⊢∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz↔∀z∈BaseC∀w∈BaseC∀g∈xHom⁡Cz∀h∈zHom⁡Cwhxzcomp⁡Cwg∈xHom⁡Cw
51 oveq1 ⊢x=y→xHom⁡Cz=yHom⁡Cz
52 opeq1 ⊢x=y→xz=yz
53 52 oveq1d ⊢x=y→xzcomp⁡Cw=yzcomp⁡Cw
54 53 oveqd ⊢x=y→hxzcomp⁡Cwg=hyzcomp⁡Cwg
55 oveq1 ⊢x=y→xHom⁡Cw=yHom⁡Cw
56 54 55 eleq12d ⊢x=y→hxzcomp⁡Cwg∈xHom⁡Cw↔hyzcomp⁡Cwg∈yHom⁡Cw
57 56 ralbidv ⊢x=y→∀h∈zHom⁡Cwhxzcomp⁡Cwg∈xHom⁡Cw↔∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw
58 51 57 raleqbidv ⊢x=y→∀g∈xHom⁡Cz∀h∈zHom⁡Cwhxzcomp⁡Cwg∈xHom⁡Cw↔∀g∈yHom⁡Cz∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw
59 58 ralbidv ⊢x=y→∀w∈BaseC∀g∈xHom⁡Cz∀h∈zHom⁡Cwhxzcomp⁡Cwg∈xHom⁡Cw↔∀w∈BaseC∀g∈yHom⁡Cz∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw
60 ralcom ⊢∀w∈BaseC∀g∈yHom⁡Cz∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw↔∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw
61 59 60 bitrdi ⊢x=y→∀w∈BaseC∀g∈xHom⁡Cz∀h∈zHom⁡Cwhxzcomp⁡Cwg∈xHom⁡Cw↔∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw
62 61 ralbidv ⊢x=y→∀z∈BaseC∀w∈BaseC∀g∈xHom⁡Cz∀h∈zHom⁡Cwhxzcomp⁡Cwg∈xHom⁡Cw↔∀z∈BaseC∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw
63 50 62 bitrid ⊢x=y→∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz↔∀z∈BaseC∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw
64 17 18 63 cbvralw ⊢∀x∈BaseC∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz↔∀y∈BaseC∀z∈BaseC∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw
65 64 biimpi ⊢∀x∈BaseC∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz→∀y∈BaseC∀z∈BaseC∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw
66 65 ancri ⊢∀x∈BaseC∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz→∀y∈BaseC∀z∈BaseC∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧∀x∈BaseC∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz
67 r19.26 ⊢∀y∈BaseC∀z∈BaseC∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz↔∀y∈BaseC∀z∈BaseC∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz
68 r19.26 ⊢∀z∈BaseC∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz↔∀z∈BaseC∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz
69 r19.26 ⊢∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧gxycomp⁡Czf∈xHom⁡Cz↔∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz
70 eqid ⊢BaseC=BaseC
71 eqid ⊢Hom⁡C=Hom⁡C
72 eqid ⊢comp⁡C=comp⁡C
73 eqid ⊢comp⁡D=comp⁡D
74 1 adantr ⊢φ∧x∈BaseC→Hom𝑓⁡C=Hom𝑓⁡D
75 74 ad4antr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→Hom𝑓⁡C=Hom𝑓⁡D
76 75 ad4antr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧gxycomp⁡Czf∈xHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw∧hyzcomp⁡Cwg∈yHom⁡Cw→Hom𝑓⁡C=Hom𝑓⁡D
77 2 ad5antr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→comp𝑓⁡C=comp𝑓⁡D
78 77 ad4antr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧gxycomp⁡Czf∈xHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw∧hyzcomp⁡Cwg∈yHom⁡Cw→comp𝑓⁡C=comp𝑓⁡D
79 simpllr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC→x∈BaseC
80 79 ad2antrr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→x∈BaseC
81 80 ad4antr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧gxycomp⁡Czf∈xHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw∧hyzcomp⁡Cwg∈yHom⁡Cw→x∈BaseC
82 simp-4r ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→y∈BaseC
83 82 ad4antr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧gxycomp⁡Czf∈xHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw∧hyzcomp⁡Cwg∈yHom⁡Cw→y∈BaseC
84 simpllr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧gxycomp⁡Czf∈xHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw∧hyzcomp⁡Cwg∈yHom⁡Cw→w∈BaseC
85 simplr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→f∈xHom⁡Cy
86 85 ad4antr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧gxycomp⁡Czf∈xHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw∧hyzcomp⁡Cwg∈yHom⁡Cw→f∈xHom⁡Cy
87 simpr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧gxycomp⁡Czf∈xHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw∧hyzcomp⁡Cwg∈yHom⁡Cw→hyzcomp⁡Cwg∈yHom⁡Cw
88 70 71 72 73 76 78 81 83 84 86 87 comfeqval ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧gxycomp⁡Czf∈xHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw∧hyzcomp⁡Cwg∈yHom⁡Cw→hyzcomp⁡Cwgxycomp⁡Cwf=hyzcomp⁡Cwgxycomp⁡Dwf
89 simpllr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→z∈BaseC
90 89 ad4antr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧gxycomp⁡Czf∈xHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw∧hyzcomp⁡Cwg∈yHom⁡Cw→z∈BaseC
91 simp-4r ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧gxycomp⁡Czf∈xHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw∧hyzcomp⁡Cwg∈yHom⁡Cw→gxycomp⁡Czf∈xHom⁡Cz
92 simplr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧gxycomp⁡Czf∈xHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw∧hyzcomp⁡Cwg∈yHom⁡Cw→h∈zHom⁡Cw
93 70 71 72 73 76 78 81 90 84 91 92 comfeqval ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧gxycomp⁡Czf∈xHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw∧hyzcomp⁡Cwg∈yHom⁡Cw→hxzcomp⁡Cwgxycomp⁡Czf=hxzcomp⁡Dwgxycomp⁡Czf
94 88 93 eqeq12d ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧gxycomp⁡Czf∈xHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw∧hyzcomp⁡Cwg∈yHom⁡Cw→hyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔hyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
95 94 ex ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧gxycomp⁡Czf∈xHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw→hyzcomp⁡Cwg∈yHom⁡Cw→hyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔hyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
96 95 ralimdva ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧gxycomp⁡Czf∈xHom⁡Cz∧w∈BaseC→∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw→∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔hyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
97 ralbi ⊢∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔hyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf→∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
98 96 97 syl6 ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧gxycomp⁡Czf∈xHom⁡Cz∧w∈BaseC→∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw→∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
99 98 ralimdva ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧gxycomp⁡Czf∈xHom⁡Cz→∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw→∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
100 99 impancom ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw→gxycomp⁡Czf∈xHom⁡Cz→∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
101 100 impr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧gxycomp⁡Czf∈xHom⁡Cz→∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
102 ralbi ⊢∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf→∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
103 101 102 syl ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧gxycomp⁡Czf∈xHom⁡Cz→∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
104 103 anbi2d ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧gxycomp⁡Czf∈xHom⁡Cz→gxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔gxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
105 104 ex ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧gxycomp⁡Czf∈xHom⁡Cz→gxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔gxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
106 105 ralimdva ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy→∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧gxycomp⁡Czf∈xHom⁡Cz→∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔gxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
107 69 106 biimtrrid ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy→∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz→∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔gxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
108 107 expdimp ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw→∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz→∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔gxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
109 ralbi ⊢∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔gxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf→∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
110 108 109 syl6 ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw→∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz→∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
111 110 an32s ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧f∈xHom⁡Cy→∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz→∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
112 111 ralimdva ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw→∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz→∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
113 ralbi ⊢∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf→∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
114 112 113 syl6 ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw→∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz→∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
115 114 expimpd ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC→∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz→∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
116 115 ralimdva ⊢φ∧x∈BaseC∧y∈BaseC→∀z∈BaseC∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz→∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
117 ralbi ⊢∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf→∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
118 116 117 syl6 ⊢φ∧x∈BaseC∧y∈BaseC→∀z∈BaseC∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz→∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
119 68 118 biimtrrid ⊢φ∧x∈BaseC∧y∈BaseC→∀z∈BaseC∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz→∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
120 119 ralimdva ⊢φ∧x∈BaseC→∀y∈BaseC∀z∈BaseC∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz→∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
121 ralbi ⊢∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf→∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
122 120 121 syl6 ⊢φ∧x∈BaseC→∀y∈BaseC∀z∈BaseC∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz→∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
123 67 122 biimtrrid ⊢φ∧x∈BaseC→∀y∈BaseC∀z∈BaseC∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz→∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
124 123 imp ⊢φ∧x∈BaseC∧∀y∈BaseC∀z∈BaseC∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz→∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
125 124 an4s ⊢φ∧∀y∈BaseC∀z∈BaseC∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧x∈BaseC∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz→∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
126 125 anbi2d ⊢φ∧∀y∈BaseC∀z∈BaseC∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧x∈BaseC∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz→∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
127 126 expr ⊢φ∧∀y∈BaseC∀z∈BaseC∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧x∈BaseC→∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz→∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
128 127 ralimdva ⊢φ∧∀y∈BaseC∀z∈BaseC∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw→∀x∈BaseC∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz→∀x∈BaseC∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
129 128 expimpd ⊢φ→∀y∈BaseC∀z∈BaseC∀g∈yHom⁡Cz∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwg∈yHom⁡Cw∧∀x∈BaseC∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz→∀x∈BaseC∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
130 ralbi ⊢∀x∈BaseC∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf→∀x∈BaseC∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀x∈BaseC∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
131 66 129 130 syl56 ⊢φ→∀x∈BaseC∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz→∀x∈BaseC∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀x∈BaseC∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
132 10 16 131 pm5.21ndd ⊢φ→∀x∈BaseC∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀x∈BaseC∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf
133 1 homfeqbas ⊢φ→BaseC=BaseD
134 eqid ⊢Hom⁡D=Hom⁡D
135 simpr ⊢φ∧x∈BaseC→x∈BaseC
136 70 71 134 74 135 135 homfeqval ⊢φ∧x∈BaseC→xHom⁡Cx=xHom⁡Dx
137 133 ad2antrr ⊢φ∧x∈BaseC∧g∈xHom⁡Cx→BaseC=BaseD
138 74 ad2antrr ⊢φ∧x∈BaseC∧g∈xHom⁡Cx∧y∈BaseC→Hom𝑓⁡C=Hom𝑓⁡D
139 simpr ⊢φ∧x∈BaseC∧g∈xHom⁡Cx∧y∈BaseC→y∈BaseC
140 simpllr ⊢φ∧x∈BaseC∧g∈xHom⁡Cx∧y∈BaseC→x∈BaseC
141 70 71 134 138 139 140 homfeqval ⊢φ∧x∈BaseC∧g∈xHom⁡Cx∧y∈BaseC→yHom⁡Cx=yHom⁡Dx
142 1 ad4antr ⊢φ∧x∈BaseC∧g∈xHom⁡Cx∧y∈BaseC∧f∈yHom⁡Cx→Hom𝑓⁡C=Hom𝑓⁡D
143 2 ad4antr ⊢φ∧x∈BaseC∧g∈xHom⁡Cx∧y∈BaseC∧f∈yHom⁡Cx→comp𝑓⁡C=comp𝑓⁡D
144 simplr ⊢φ∧x∈BaseC∧g∈xHom⁡Cx∧y∈BaseC∧f∈yHom⁡Cx→y∈BaseC
145 simp-4r ⊢φ∧x∈BaseC∧g∈xHom⁡Cx∧y∈BaseC∧f∈yHom⁡Cx→x∈BaseC
146 simpr ⊢φ∧x∈BaseC∧g∈xHom⁡Cx∧y∈BaseC∧f∈yHom⁡Cx→f∈yHom⁡Cx
147 simpllr ⊢φ∧x∈BaseC∧g∈xHom⁡Cx∧y∈BaseC∧f∈yHom⁡Cx→g∈xHom⁡Cx
148 70 71 72 73 142 143 144 145 145 146 147 comfeqval ⊢φ∧x∈BaseC∧g∈xHom⁡Cx∧y∈BaseC∧f∈yHom⁡Cx→gyxcomp⁡Cxf=gyxcomp⁡Dxf
149 148 eqeq1d ⊢φ∧x∈BaseC∧g∈xHom⁡Cx∧y∈BaseC∧f∈yHom⁡Cx→gyxcomp⁡Cxf=f↔gyxcomp⁡Dxf=f
150 141 149 raleqbidva ⊢φ∧x∈BaseC∧g∈xHom⁡Cx∧y∈BaseC→∀f∈yHom⁡Cxgyxcomp⁡Cxf=f↔∀f∈yHom⁡Dxgyxcomp⁡Dxf=f
151 70 71 134 138 140 139 homfeqval ⊢φ∧x∈BaseC∧g∈xHom⁡Cx∧y∈BaseC→xHom⁡Cy=xHom⁡Dy
152 1 ad4antr ⊢φ∧x∈BaseC∧g∈xHom⁡Cx∧y∈BaseC∧f∈xHom⁡Cy→Hom𝑓⁡C=Hom𝑓⁡D
153 2 ad4antr ⊢φ∧x∈BaseC∧g∈xHom⁡Cx∧y∈BaseC∧f∈xHom⁡Cy→comp𝑓⁡C=comp𝑓⁡D
154 simp-4r ⊢φ∧x∈BaseC∧g∈xHom⁡Cx∧y∈BaseC∧f∈xHom⁡Cy→x∈BaseC
155 simplr ⊢φ∧x∈BaseC∧g∈xHom⁡Cx∧y∈BaseC∧f∈xHom⁡Cy→y∈BaseC
156 simpllr ⊢φ∧x∈BaseC∧g∈xHom⁡Cx∧y∈BaseC∧f∈xHom⁡Cy→g∈xHom⁡Cx
157 simpr ⊢φ∧x∈BaseC∧g∈xHom⁡Cx∧y∈BaseC∧f∈xHom⁡Cy→f∈xHom⁡Cy
158 70 71 72 73 152 153 154 154 155 156 157 comfeqval ⊢φ∧x∈BaseC∧g∈xHom⁡Cx∧y∈BaseC∧f∈xHom⁡Cy→fxxcomp⁡Cyg=fxxcomp⁡Dyg
159 158 eqeq1d ⊢φ∧x∈BaseC∧g∈xHom⁡Cx∧y∈BaseC∧f∈xHom⁡Cy→fxxcomp⁡Cyg=f↔fxxcomp⁡Dyg=f
160 151 159 raleqbidva ⊢φ∧x∈BaseC∧g∈xHom⁡Cx∧y∈BaseC→∀f∈xHom⁡Cyfxxcomp⁡Cyg=f↔∀f∈xHom⁡Dyfxxcomp⁡Dyg=f
161 150 160 anbi12d ⊢φ∧x∈BaseC∧g∈xHom⁡Cx∧y∈BaseC→∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f↔∀f∈yHom⁡Dxgyxcomp⁡Dxf=f∧∀f∈xHom⁡Dyfxxcomp⁡Dyg=f
162 137 161 raleqbidva ⊢φ∧x∈BaseC∧g∈xHom⁡Cx→∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f↔∀y∈BaseD∀f∈yHom⁡Dxgyxcomp⁡Dxf=f∧∀f∈xHom⁡Dyfxxcomp⁡Dyg=f
163 136 162 rexeqbidva ⊢φ∧x∈BaseC→∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f↔∃g∈xHom⁡Dx∀y∈BaseD∀f∈yHom⁡Dxgyxcomp⁡Dxf=f∧∀f∈xHom⁡Dyfxxcomp⁡Dyg=f
164 133 adantr ⊢φ∧x∈BaseC→BaseC=BaseD
165 164 adantr ⊢φ∧x∈BaseC∧y∈BaseC→BaseC=BaseD
166 74 ad2antrr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC→Hom𝑓⁡C=Hom𝑓⁡D
167 simplr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC→y∈BaseC
168 70 71 134 166 79 167 homfeqval ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC→xHom⁡Cy=xHom⁡Dy
169 simpr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC→z∈BaseC
170 70 71 134 166 167 169 homfeqval ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC→yHom⁡Cz=yHom⁡Dz
171 170 adantr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy→yHom⁡Cz=yHom⁡Dz
172 simpr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→g∈yHom⁡Cz
173 70 71 72 73 75 77 80 82 89 85 172 comfeqval ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→gxycomp⁡Czf=gxycomp⁡Dzf
174 70 71 134 166 79 169 homfeqval ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC→xHom⁡Cz=xHom⁡Dz
175 174 ad2antrr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→xHom⁡Cz=xHom⁡Dz
176 173 175 eleq12d ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→gxycomp⁡Czf∈xHom⁡Cz↔gxycomp⁡Dzf∈xHom⁡Dz
177 164 ad4antr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→BaseC=BaseD
178 75 adantr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧w∈BaseC→Hom𝑓⁡C=Hom𝑓⁡D
179 simp-4r ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧w∈BaseC→z∈BaseC
180 simpr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧w∈BaseC→w∈BaseC
181 70 71 134 178 179 180 homfeqval ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧w∈BaseC→zHom⁡Cw=zHom⁡Dw
182 166 ad4antr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw→Hom𝑓⁡C=Hom𝑓⁡D
183 2 ad7antr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw→comp𝑓⁡C=comp𝑓⁡D
184 167 ad4antr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw→y∈BaseC
185 169 ad4antr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw→z∈BaseC
186 simplr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw→w∈BaseC
187 simpllr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw→g∈yHom⁡Cz
188 simpr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw→h∈zHom⁡Cw
189 70 71 72 73 182 183 184 185 186 187 188 comfeqval ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw→hyzcomp⁡Cwg=hyzcomp⁡Dwg
190 189 oveq1d ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw→hyzcomp⁡Cwgxycomp⁡Dwf=hyzcomp⁡Dwgxycomp⁡Dwf
191 79 ad4antr ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw→x∈BaseC
192 simp-4r ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw→f∈xHom⁡Cy
193 70 71 72 73 182 183 191 184 185 192 187 comfeqval ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw→gxycomp⁡Czf=gxycomp⁡Dzf
194 193 oveq2d ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw→hxzcomp⁡Dwgxycomp⁡Czf=hxzcomp⁡Dwgxycomp⁡Dzf
195 190 194 eqeq12d ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧w∈BaseC∧h∈zHom⁡Cw→hyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf↔hyzcomp⁡Dwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Dzf
196 181 195 raleqbidva ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz∧w∈BaseC→∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf↔∀h∈zHom⁡Dwhyzcomp⁡Dwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Dzf
197 177 196 raleqbidva ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf↔∀w∈BaseD∀h∈zHom⁡Dwhyzcomp⁡Dwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Dzf
198 176 197 anbi12d ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→gxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf↔gxycomp⁡Dzf∈xHom⁡Dz∧∀w∈BaseD∀h∈zHom⁡Dwhyzcomp⁡Dwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Dzf
199 171 198 raleqbidva ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy→∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf↔∀g∈yHom⁡Dzgxycomp⁡Dzf∈xHom⁡Dz∧∀w∈BaseD∀h∈zHom⁡Dwhyzcomp⁡Dwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Dzf
200 168 199 raleqbidva ⊢φ∧x∈BaseC∧y∈BaseC∧z∈BaseC→∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf↔∀f∈xHom⁡Dy∀g∈yHom⁡Dzgxycomp⁡Dzf∈xHom⁡Dz∧∀w∈BaseD∀h∈zHom⁡Dwhyzcomp⁡Dwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Dzf
201 165 200 raleqbidva ⊢φ∧x∈BaseC∧y∈BaseC→∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf↔∀z∈BaseD∀f∈xHom⁡Dy∀g∈yHom⁡Dzgxycomp⁡Dzf∈xHom⁡Dz∧∀w∈BaseD∀h∈zHom⁡Dwhyzcomp⁡Dwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Dzf
202 164 201 raleqbidva ⊢φ∧x∈BaseC→∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf↔∀y∈BaseD∀z∈BaseD∀f∈xHom⁡Dy∀g∈yHom⁡Dzgxycomp⁡Dzf∈xHom⁡Dz∧∀w∈BaseD∀h∈zHom⁡Dwhyzcomp⁡Dwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Dzf
203 163 202 anbi12d ⊢φ∧x∈BaseC→∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf↔∃g∈xHom⁡Dx∀y∈BaseD∀f∈yHom⁡Dxgyxcomp⁡Dxf=f∧∀f∈xHom⁡Dyfxxcomp⁡Dyg=f∧∀y∈BaseD∀z∈BaseD∀f∈xHom⁡Dy∀g∈yHom⁡Dzgxycomp⁡Dzf∈xHom⁡Dz∧∀w∈BaseD∀h∈zHom⁡Dwhyzcomp⁡Dwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Dzf
204 133 203 raleqbidva ⊢φ→∀x∈BaseC∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Czf↔∀x∈BaseD∃g∈xHom⁡Dx∀y∈BaseD∀f∈yHom⁡Dxgyxcomp⁡Dxf=f∧∀f∈xHom⁡Dyfxxcomp⁡Dyg=f∧∀y∈BaseD∀z∈BaseD∀f∈xHom⁡Dy∀g∈yHom⁡Dzgxycomp⁡Dzf∈xHom⁡Dz∧∀w∈BaseD∀h∈zHom⁡Dwhyzcomp⁡Dwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Dzf
205 132 204 bitrd ⊢φ→∀x∈BaseC∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf↔∀x∈BaseD∃g∈xHom⁡Dx∀y∈BaseD∀f∈yHom⁡Dxgyxcomp⁡Dxf=f∧∀f∈xHom⁡Dyfxxcomp⁡Dyg=f∧∀y∈BaseD∀z∈BaseD∀f∈xHom⁡Dy∀g∈yHom⁡Dzgxycomp⁡Dzf∈xHom⁡Dz∧∀w∈BaseD∀h∈zHom⁡Dwhyzcomp⁡Dwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Dzf
206 70 71 72 iscat ⊢C∈V→C∈Cat↔∀x∈BaseC∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf
207 3 206 syl ⊢φ→C∈Cat↔∀x∈BaseC∃g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czgxycomp⁡Czf∈xHom⁡Cz∧∀w∈BaseC∀h∈zHom⁡Cwhyzcomp⁡Cwgxycomp⁡Cwf=hxzcomp⁡Cwgxycomp⁡Czf
208 eqid ⊢BaseD=BaseD
209 208 134 73 iscat ⊢D∈W→D∈Cat↔∀x∈BaseD∃g∈xHom⁡Dx∀y∈BaseD∀f∈yHom⁡Dxgyxcomp⁡Dxf=f∧∀f∈xHom⁡Dyfxxcomp⁡Dyg=f∧∀y∈BaseD∀z∈BaseD∀f∈xHom⁡Dy∀g∈yHom⁡Dzgxycomp⁡Dzf∈xHom⁡Dz∧∀w∈BaseD∀h∈zHom⁡Dwhyzcomp⁡Dwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Dzf
210 4 209 syl ⊢φ→D∈Cat↔∀x∈BaseD∃g∈xHom⁡Dx∀y∈BaseD∀f∈yHom⁡Dxgyxcomp⁡Dxf=f∧∀f∈xHom⁡Dyfxxcomp⁡Dyg=f∧∀y∈BaseD∀z∈BaseD∀f∈xHom⁡Dy∀g∈yHom⁡Dzgxycomp⁡Dzf∈xHom⁡Dz∧∀w∈BaseD∀h∈zHom⁡Dwhyzcomp⁡Dwgxycomp⁡Dwf=hxzcomp⁡Dwgxycomp⁡Dzf
211 205 207 210 3bitr4d ⊢φ→C∈Cat↔D∈Cat