Description: A monomorphism is a morphism. (Contributed by Mario Carneiro, 2-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ismon.b | |
|
ismon.h | |
||
ismon.o | |
||
ismon.s | |
||
ismon.c | |
||
ismon.x | |
||
ismon.y | |
||
Assertion | monhom | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ismon.b | |
|
2 | ismon.h | |
|
3 | ismon.o | |
|
4 | ismon.s | |
|
5 | ismon.c | |
|
6 | ismon.x | |
|
7 | ismon.y | |
|
8 | 1 2 3 4 5 6 7 | ismon | |
9 | simpl | |
|
10 | 8 9 | syl6bi | |
11 | 10 | ssrdv | |