Metamath Proof Explorer


Theorem monhom

Description: A monomorphism is a morphism. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses ismon.b โŠข ๐ต = ( Base โ€˜ ๐ถ )
ismon.h โŠข ๐ป = ( Hom โ€˜ ๐ถ )
ismon.o โŠข ยท = ( comp โ€˜ ๐ถ )
ismon.s โŠข ๐‘€ = ( Mono โ€˜ ๐ถ )
ismon.c โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ Cat )
ismon.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต )
ismon.y โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ต )
Assertion monhom ( ๐œ‘ โ†’ ( ๐‘‹ ๐‘€ ๐‘Œ ) โІ ( ๐‘‹ ๐ป ๐‘Œ ) )

Proof

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 โŠข ( ๐œ‘ โ†’ ( ๐‘‹ ๐‘€ ๐‘Œ ) โІ ( ๐‘‹ ๐ป ๐‘Œ ) )