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

Metamath Proof Explorer

Theorem subcid

Description: The identity in a subcategory is the same as the original category. (Contributed by Mario Carneiro, 4-Jan-2017)

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

Proof

Step Hyp Ref Expression
1 subccat.1 
 |-  D = ( C |`cat J )
2 subccat.j 
 |-  ( ph -> J e. ( Subcat ` C ) )
3 subccatid.1 
 |-  ( ph -> J Fn ( S X. S ) )
4 subccatid.2 
 |-  .1. = ( Id ` C )
5 subcid.x 
 |-  ( ph -> X e. S )
6 1 2 3 4 subccatid 
 |-  ( ph -> ( D e. Cat /\ ( Id ` D ) = ( x e. S |-> ( .1. ` x ) ) ) )
7 6 simprd 
 |-  ( ph -> ( Id ` D ) = ( x e. S |-> ( .1. ` x ) ) )
8 simpr 
 |-  ( ( ph /\ x = X ) -> x = X )
9 8 fveq2d 
 |-  ( ( ph /\ x = X ) -> ( .1. ` x ) = ( .1. ` X ) )
10 fvexd 
 |-  ( ph -> ( .1. ` X ) e. _V )
11 7 9 5 10 fvmptd 
 |-  ( ph -> ( ( Id ` D ) ` X ) = ( .1. ` X ) )
12 11 eqcomd 
 |-  ( ph -> ( .1. ` X ) = ( ( Id ` D ) ` X ) )