Step |
Hyp |
Ref |
Expression |
1 |
|
catcocl.b |
โข ๐ต = ( Base โ ๐ถ ) |
2 |
|
catcocl.h |
โข ๐ป = ( Hom โ ๐ถ ) |
3 |
|
catcocl.o |
โข ยท = ( comp โ ๐ถ ) |
4 |
|
catcocl.c |
โข ( ๐ โ ๐ถ โ Cat ) |
5 |
|
catcocl.x |
โข ( ๐ โ ๐ โ ๐ต ) |
6 |
|
catcocl.y |
โข ( ๐ โ ๐ โ ๐ต ) |
7 |
|
catcocl.z |
โข ( ๐ โ ๐ โ ๐ต ) |
8 |
|
catcone0.f |
โข ( ๐ โ ( ๐ ๐ป ๐ ) โ โ
) |
9 |
|
catcone0.g |
โข ( ๐ โ ( ๐ ๐ป ๐ ) โ โ
) |
10 |
|
n0 |
โข ( ( ๐ ๐ป ๐ ) โ โ
โ โ ๐ ๐ โ ( ๐ ๐ป ๐ ) ) |
11 |
|
n0 |
โข ( ( ๐ ๐ป ๐ ) โ โ
โ โ ๐ ๐ โ ( ๐ ๐ป ๐ ) ) |
12 |
10 11
|
anbi12i |
โข ( ( ( ๐ ๐ป ๐ ) โ โ
โง ( ๐ ๐ป ๐ ) โ โ
) โ ( โ ๐ ๐ โ ( ๐ ๐ป ๐ ) โง โ ๐ ๐ โ ( ๐ ๐ป ๐ ) ) ) |
13 |
|
exdistrv |
โข ( โ ๐ โ ๐ ( ๐ โ ( ๐ ๐ป ๐ ) โง ๐ โ ( ๐ ๐ป ๐ ) ) โ ( โ ๐ ๐ โ ( ๐ ๐ป ๐ ) โง โ ๐ ๐ โ ( ๐ ๐ป ๐ ) ) ) |
14 |
12 13
|
sylbb2 |
โข ( ( ( ๐ ๐ป ๐ ) โ โ
โง ( ๐ ๐ป ๐ ) โ โ
) โ โ ๐ โ ๐ ( ๐ โ ( ๐ ๐ป ๐ ) โง ๐ โ ( ๐ ๐ป ๐ ) ) ) |
15 |
8 9 14
|
syl2anc |
โข ( ๐ โ โ ๐ โ ๐ ( ๐ โ ( ๐ ๐ป ๐ ) โง ๐ โ ( ๐ ๐ป ๐ ) ) ) |
16 |
15
|
ancli |
โข ( ๐ โ ( ๐ โง โ ๐ โ ๐ ( ๐ โ ( ๐ ๐ป ๐ ) โง ๐ โ ( ๐ ๐ป ๐ ) ) ) ) |
17 |
|
19.42vv |
โข ( โ ๐ โ ๐ ( ๐ โง ( ๐ โ ( ๐ ๐ป ๐ ) โง ๐ โ ( ๐ ๐ป ๐ ) ) ) โ ( ๐ โง โ ๐ โ ๐ ( ๐ โ ( ๐ ๐ป ๐ ) โง ๐ โ ( ๐ ๐ป ๐ ) ) ) ) |
18 |
17
|
biimpri |
โข ( ( ๐ โง โ ๐ โ ๐ ( ๐ โ ( ๐ ๐ป ๐ ) โง ๐ โ ( ๐ ๐ป ๐ ) ) ) โ โ ๐ โ ๐ ( ๐ โง ( ๐ โ ( ๐ ๐ป ๐ ) โง ๐ โ ( ๐ ๐ป ๐ ) ) ) ) |
19 |
4
|
adantr |
โข ( ( ๐ โง ( ๐ โ ( ๐ ๐ป ๐ ) โง ๐ โ ( ๐ ๐ป ๐ ) ) ) โ ๐ถ โ Cat ) |
20 |
5
|
adantr |
โข ( ( ๐ โง ( ๐ โ ( ๐ ๐ป ๐ ) โง ๐ โ ( ๐ ๐ป ๐ ) ) ) โ ๐ โ ๐ต ) |
21 |
6
|
adantr |
โข ( ( ๐ โง ( ๐ โ ( ๐ ๐ป ๐ ) โง ๐ โ ( ๐ ๐ป ๐ ) ) ) โ ๐ โ ๐ต ) |
22 |
7
|
adantr |
โข ( ( ๐ โง ( ๐ โ ( ๐ ๐ป ๐ ) โง ๐ โ ( ๐ ๐ป ๐ ) ) ) โ ๐ โ ๐ต ) |
23 |
|
simprl |
โข ( ( ๐ โง ( ๐ โ ( ๐ ๐ป ๐ ) โง ๐ โ ( ๐ ๐ป ๐ ) ) ) โ ๐ โ ( ๐ ๐ป ๐ ) ) |
24 |
|
simprr |
โข ( ( ๐ โง ( ๐ โ ( ๐ ๐ป ๐ ) โง ๐ โ ( ๐ ๐ป ๐ ) ) ) โ ๐ โ ( ๐ ๐ป ๐ ) ) |
25 |
1 2 3 19 20 21 22 23 24
|
catcocl |
โข ( ( ๐ โง ( ๐ โ ( ๐ ๐ป ๐ ) โง ๐ โ ( ๐ ๐ป ๐ ) ) ) โ ( ๐ ( โจ ๐ , ๐ โฉ ยท ๐ ) ๐ ) โ ( ๐ ๐ป ๐ ) ) |
26 |
25
|
2eximi |
โข ( โ ๐ โ ๐ ( ๐ โง ( ๐ โ ( ๐ ๐ป ๐ ) โง ๐ โ ( ๐ ๐ป ๐ ) ) ) โ โ ๐ โ ๐ ( ๐ ( โจ ๐ , ๐ โฉ ยท ๐ ) ๐ ) โ ( ๐ ๐ป ๐ ) ) |
27 |
16 18 26
|
3syl |
โข ( ๐ โ โ ๐ โ ๐ ( ๐ ( โจ ๐ , ๐ โฉ ยท ๐ ) ๐ ) โ ( ๐ ๐ป ๐ ) ) |
28 |
|
ne0i |
โข ( ( ๐ ( โจ ๐ , ๐ โฉ ยท ๐ ) ๐ ) โ ( ๐ ๐ป ๐ ) โ ( ๐ ๐ป ๐ ) โ โ
) |
29 |
28
|
exlimivv |
โข ( โ ๐ โ ๐ ( ๐ ( โจ ๐ , ๐ โฉ ยท ๐ ) ๐ ) โ ( ๐ ๐ป ๐ ) โ ( ๐ ๐ป ๐ ) โ โ
) |
30 |
27 29
|
syl |
โข ( ๐ โ ( ๐ ๐ป ๐ ) โ โ
) |