Step |
Hyp |
Ref |
Expression |
1 |
|
ismon.b |
โข ๐ต = ( Base โ ๐ถ ) |
2 |
|
ismon.h |
โข ๐ป = ( Hom โ ๐ถ ) |
3 |
|
ismon.o |
โข ยท = ( comp โ ๐ถ ) |
4 |
|
ismon.s |
โข ๐ = ( Mono โ ๐ถ ) |
5 |
|
ismon.c |
โข ( ๐ โ ๐ถ โ Cat ) |
6 |
|
ismon.x |
โข ( ๐ โ ๐ โ ๐ต ) |
7 |
|
ismon.y |
โข ( ๐ โ ๐ โ ๐ต ) |
8 |
1 2 3 4 5 6 7
|
ismon |
โข ( ๐ โ ( ๐ โ ( ๐ ๐ ๐ ) โ ( ๐ โ ( ๐ ๐ป ๐ ) โง โ ๐ง โ ๐ต Fun โก ( ๐ โ ( ๐ง ๐ป ๐ ) โฆ ( ๐ ( โจ ๐ง , ๐ โฉ ยท ๐ ) ๐ ) ) ) ) ) |
9 |
|
simpl |
โข ( ( ๐ โ ( ๐ ๐ป ๐ ) โง โ ๐ง โ ๐ต Fun โก ( ๐ โ ( ๐ง ๐ป ๐ ) โฆ ( ๐ ( โจ ๐ง , ๐ โฉ ยท ๐ ) ๐ ) ) ) โ ๐ โ ( ๐ ๐ป ๐ ) ) |
10 |
8 9
|
biimtrdi |
โข ( ๐ โ ( ๐ โ ( ๐ ๐ ๐ ) โ ๐ โ ( ๐ ๐ป ๐ ) ) ) |
11 |
10
|
ssrdv |
โข ( ๐ โ ( ๐ ๐ ๐ ) โ ( ๐ ๐ป ๐ ) ) |