Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . 6
โข (๐ถ โ Cat โ ๐ถ โ Cat) |
2 | | eqid 2726 |
. . . . . 6
โข
(Baseโ๐ถ) =
(Baseโ๐ถ) |
3 | | eqid 2726 |
. . . . . 6
โข (Hom
โ๐ถ) = (Hom
โ๐ถ) |
4 | 1, 2, 3 | zerooval 17954 |
. . . . 5
โข (๐ถ โ Cat โ
(ZeroOโ๐ถ) =
((InitOโ๐ถ) โฉ
(TermOโ๐ถ))) |
5 | 4 | eleq2d 2813 |
. . . 4
โข (๐ถ โ Cat โ (๐ โ (ZeroOโ๐ถ) โ ๐ โ ((InitOโ๐ถ) โฉ (TermOโ๐ถ)))) |
6 | | elin 3959 |
. . . . 5
โข (๐ โ ((InitOโ๐ถ) โฉ (TermOโ๐ถ)) โ (๐ โ (InitOโ๐ถ) โง ๐ โ (TermOโ๐ถ))) |
7 | | initoo 17966 |
. . . . . 6
โข (๐ถ โ Cat โ (๐ โ (InitOโ๐ถ) โ ๐ โ (Baseโ๐ถ))) |
8 | 7 | adantrd 491 |
. . . . 5
โข (๐ถ โ Cat โ ((๐ โ (InitOโ๐ถ) โง ๐ โ (TermOโ๐ถ)) โ ๐ โ (Baseโ๐ถ))) |
9 | 6, 8 | biimtrid 241 |
. . . 4
โข (๐ถ โ Cat โ (๐ โ ((InitOโ๐ถ) โฉ (TermOโ๐ถ)) โ ๐ โ (Baseโ๐ถ))) |
10 | 5, 9 | sylbid 239 |
. . 3
โข (๐ถ โ Cat โ (๐ โ (ZeroOโ๐ถ) โ ๐ โ (Baseโ๐ถ))) |
11 | 10 | imp 406 |
. 2
โข ((๐ถ โ Cat โง ๐ โ (ZeroOโ๐ถ)) โ ๐ โ (Baseโ๐ถ)) |
12 | | simpl 482 |
. . . . 5
โข ((๐ถ โ Cat โง ๐ โ (Baseโ๐ถ)) โ ๐ถ โ Cat) |
13 | | simpr 484 |
. . . . 5
โข ((๐ถ โ Cat โง ๐ โ (Baseโ๐ถ)) โ ๐ โ (Baseโ๐ถ)) |
14 | 2, 3, 12, 13 | iszeroo 17957 |
. . . 4
โข ((๐ถ โ Cat โง ๐ โ (Baseโ๐ถ)) โ (๐ โ (ZeroOโ๐ถ) โ (๐ โ (InitOโ๐ถ) โง ๐ โ (TermOโ๐ถ)))) |
15 | 14 | biimpd 228 |
. . 3
โข ((๐ถ โ Cat โง ๐ โ (Baseโ๐ถ)) โ (๐ โ (ZeroOโ๐ถ) โ (๐ โ (InitOโ๐ถ) โง ๐ โ (TermOโ๐ถ)))) |
16 | 15 | impancom 451 |
. 2
โข ((๐ถ โ Cat โง ๐ โ (ZeroOโ๐ถ)) โ (๐ โ (Baseโ๐ถ) โ (๐ โ (InitOโ๐ถ) โง ๐ โ (TermOโ๐ถ)))) |
17 | 11, 16 | jcai 516 |
1
โข ((๐ถ โ Cat โง ๐ โ (ZeroOโ๐ถ)) โ (๐ โ (Baseโ๐ถ) โง (๐ โ (InitOโ๐ถ) โง ๐ โ (TermOโ๐ถ)))) |