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

Metamath Proof Explorer

Theorem fucid

Description: The identity morphism in the functor category. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses fucid.q 
|- Q = ( C FuncCat D )
fucid.i 
|- I = ( Id ` Q )
fucid.1 
|- .1. = ( Id ` D )
fucid.f 
|- ( ph -> F e. ( C Func D ) )
Assertion fucid 
|- ( ph -> ( I ` F ) = ( .1. o. ( 1st ` F ) ) )

Proof

Step Hyp Ref Expression
1 fucid.q 
 |-  Q = ( C FuncCat D )
2 fucid.i 
 |-  I = ( Id ` Q )
3 fucid.1 
 |-  .1. = ( Id ` D )
4 fucid.f 
 |-  ( ph -> F e. ( C Func D ) )
5 funcrcl 
 |-  ( F e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
6 4 5 syl 
 |-  ( ph -> ( C e. Cat /\ D e. Cat ) )
7 6 simpld 
 |-  ( ph -> C e. Cat )
8 6 simprd 
 |-  ( ph -> D e. Cat )
9 1 7 8 3 fuccatid 
 |-  ( ph -> ( Q e. Cat /\ ( Id ` Q ) = ( f e. ( C Func D ) |-> ( .1. o. ( 1st ` f ) ) ) ) )
10 9 simprd 
 |-  ( ph -> ( Id ` Q ) = ( f e. ( C Func D ) |-> ( .1. o. ( 1st ` f ) ) ) )
11 2 10 eqtrid 
 |-  ( ph -> I = ( f e. ( C Func D ) |-> ( .1. o. ( 1st ` f ) ) ) )
12 simpr 
 |-  ( ( ph /\ f = F ) -> f = F )
13 12 fveq2d 
 |-  ( ( ph /\ f = F ) -> ( 1st ` f ) = ( 1st ` F ) )
14 13 coeq2d 
 |-  ( ( ph /\ f = F ) -> ( .1. o. ( 1st ` f ) ) = ( .1. o. ( 1st ` F ) ) )
15 3 fvexi 
 |-  .1. e. _V
16 fvex 
 |-  ( 1st ` F ) e. _V
17 15 16 coex 
 |-  ( .1. o. ( 1st ` F ) ) e. _V
18 17 a1i 
 |-  ( ph -> ( .1. o. ( 1st ` F ) ) e. _V )
19 11 14 4 18 fvmptd 
 |-  ( ph -> ( I ` F ) = ( .1. o. ( 1st ` F ) ) )