This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem subcss2

Description: The morphisms of a subcategory are a subset of the morphisms of the original. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses subcss1.1 
|- ( ph -> J e. ( Subcat ` C ) )
subcss1.2 
|- ( ph -> J Fn ( S X. S ) )
subcss2.h 
|- H = ( Hom ` C )
subcss2.x 
|- ( ph -> X e. S )
subcss2.y 
|- ( ph -> Y e. S )
Assertion subcss2 
|- ( ph -> ( X J Y ) C_ ( X H Y ) )

Proof

Step Hyp Ref Expression
1 subcss1.1 
 |-  ( ph -> J e. ( Subcat ` C ) )
2 subcss1.2 
 |-  ( ph -> J Fn ( S X. S ) )
3 subcss2.h 
 |-  H = ( Hom ` C )
4 subcss2.x 
 |-  ( ph -> X e. S )
5 subcss2.y 
 |-  ( ph -> Y e. S )
6 eqid 
 |-  ( Homf ` C ) = ( Homf ` C )
7 1 6 subcssc 
 |-  ( ph -> J C_cat ( Homf ` C ) )
8 2 7 4 5 ssc2 
 |-  ( ph -> ( X J Y ) C_ ( X ( Homf ` C ) Y ) )
9 eqid 
 |-  ( Base ` C ) = ( Base ` C )
10 1 2 9 subcss1 
 |-  ( ph -> S C_ ( Base ` C ) )
11 10 4 sseldd 
 |-  ( ph -> X e. ( Base ` C ) )
12 10 5 sseldd 
 |-  ( ph -> Y e. ( Base ` C ) )
13 6 9 3 11 12 homfval 
 |-  ( ph -> ( X ( Homf ` C ) Y ) = ( X H Y ) )
14 8 13 sseqtrd 
 |-  ( ph -> ( X J Y ) C_ ( X H Y ) )