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

Metamath Proof Explorer

Theorem subcidcl

Description: The identity of the original category is contained in each subcategory. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses subcidcl.j 
|- ( ph -> J e. ( Subcat ` C ) )
subcidcl.2 
|- ( ph -> J Fn ( S X. S ) )
subcidcl.x 
|- ( ph -> X e. S )
subcidcl.1 
|- .1. = ( Id ` C )
Assertion subcidcl 
|- ( ph -> ( .1. ` X ) e. ( X J X ) )

Proof

Step Hyp Ref Expression
1 subcidcl.j 
 |-  ( ph -> J e. ( Subcat ` C ) )
2 subcidcl.2 
 |-  ( ph -> J Fn ( S X. S ) )
3 subcidcl.x 
 |-  ( ph -> X e. S )
4 subcidcl.1 
 |-  .1. = ( Id ` C )
5 fveq2 
 |-  ( x = X -> ( .1. ` x ) = ( .1. ` X ) )
6 id 
 |-  ( x = X -> x = X )
7 6 6 oveq12d 
 |-  ( x = X -> ( x J x ) = ( X J X ) )
8 5 7 eleq12d 
 |-  ( x = X -> ( ( .1. ` x ) e. ( x J x ) <-> ( .1. ` X ) e. ( X J X ) ) )
9 eqid 
 |-  ( Homf ` C ) = ( Homf ` C )
10 eqid 
 |-  ( comp ` C ) = ( comp ` C )
11 subcrcl 
 |-  ( J e. ( Subcat ` C ) -> C e. Cat )
12 1 11 syl 
 |-  ( ph -> C e. Cat )
13 9 4 10 12 2 issubc2 
 |-  ( ph -> ( J e. ( Subcat ` C ) <-> ( J C_cat ( Homf ` C ) /\ A. x e. S ( ( .1. ` x ) e. ( x J x ) /\ A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) ) ) )
14 1 13 mpbid 
 |-  ( ph -> ( J C_cat ( Homf ` C ) /\ A. x e. S ( ( .1. ` x ) e. ( x J x ) /\ A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) ) )
15 simpl 
 |-  ( ( ( .1. ` x ) e. ( x J x ) /\ A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) -> ( .1. ` x ) e. ( x J x ) )
16 15 ralimi 
 |-  ( A. x e. S ( ( .1. ` x ) e. ( x J x ) /\ A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) -> A. x e. S ( .1. ` x ) e. ( x J x ) )
17 14 16 simpl2im 
 |-  ( ph -> A. x e. S ( .1. ` x ) e. ( x J x ) )
18 8 17 3 rspcdva 
 |-  ( ph -> ( .1. ` X ) e. ( X J X ) )