Metamath Proof Explorer

Theorem fuclid

Description: Left identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses fuclid.q 
|- Q = ( C FuncCat D )
fuclid.n 
|- N = ( C Nat D )
fuclid.x 
|- .xb = ( comp ` Q )
fuclid.1 
|- .1. = ( Id ` D )
fuclid.r 
|- ( ph -> R e. ( F N G ) )
Assertion fuclid 
|- ( ph -> ( ( .1. o. ( 1st ` G ) ) ( <. F , G >. .xb G ) R ) = R )

Proof

Step Hyp Ref Expression
1 fuclid.q 
 |-  Q = ( C FuncCat D )
2 fuclid.n 
 |-  N = ( C Nat D )
3 fuclid.x 
 |-  .xb = ( comp ` Q )
4 fuclid.1 
 |-  .1. = ( Id ` D )
5 fuclid.r 
 |-  ( ph -> R e. ( F N G ) )
6 eqid 
 |-  ( Base ` C ) = ( Base ` C )
7 eqid 
 |-  ( Base ` D ) = ( Base ` D )
8 relfunc 
 |-  Rel ( C Func D )
9 2 natrcl 
 |-  ( R e. ( F N G ) -> ( F e. ( C Func D ) /\ G e. ( C Func D ) ) )
10 5 9 syl 
 |-  ( ph -> ( F e. ( C Func D ) /\ G e. ( C Func D ) ) )
11 10 simprd 
 |-  ( ph -> G e. ( C Func D ) )
12 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ G e. ( C Func D ) ) -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
13 8 11 12 sylancr 
 |-  ( ph -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
14 6 7 13 funcf1 
 |-  ( ph -> ( 1st ` G ) : ( Base ` C ) --> ( Base ` D ) )
15 fvco3 
 |-  ( ( ( 1st ` G ) : ( Base ` C ) --> ( Base ` D ) /\ x e. ( Base ` C ) ) -> ( ( .1. o. ( 1st ` G ) ) ` x ) = ( .1. ` ( ( 1st ` G ) ` x ) ) )
16 14 15 sylan 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( .1. o. ( 1st ` G ) ) ` x ) = ( .1. ` ( ( 1st ` G ) ` x ) ) )
17 16 oveq1d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( .1. o. ( 1st ` G ) ) ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` G ) ` x ) ) ( R ` x ) ) = ( ( .1. ` ( ( 1st ` G ) ` x ) ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` G ) ` x ) ) ( R ` x ) ) )
18 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
19 10 simpld 
 |-  ( ph -> F e. ( C Func D ) )
20 funcrcl 
 |-  ( F e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
21 19 20 syl 
 |-  ( ph -> ( C e. Cat /\ D e. Cat ) )
22 21 simprd 
 |-  ( ph -> D e. Cat )
23 22 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> D e. Cat )
24 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
25 8 19 24 sylancr 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
26 6 7 25 funcf1 
 |-  ( ph -> ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) )
27 26 ffvelrnda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` F ) ` x ) e. ( Base ` D ) )
28 eqid 
 |-  ( comp ` D ) = ( comp ` D )
29 14 ffvelrnda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` G ) ` x ) e. ( Base ` D ) )
30 2 5 nat1st2nd 
 |-  ( ph -> R e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` G ) , ( 2nd ` G ) >. ) )
31 30 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> R e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` G ) , ( 2nd ` G ) >. ) )
32 simpr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
33 2 31 6 18 32 natcl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( R ` x ) e. ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` G ) ` x ) ) )
34 7 18 4 23 27 28 29 33 catlid 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( .1. ` ( ( 1st ` G ) ` x ) ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` G ) ` x ) ) ( R ` x ) ) = ( R ` x ) )
35 17 34 eqtrd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( .1. o. ( 1st ` G ) ) ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` G ) ` x ) ) ( R ` x ) ) = ( R ` x ) )
36 35 mpteq2dva 
 |-  ( ph -> ( x e. ( Base ` C ) |-> ( ( ( .1. o. ( 1st ` G ) ) ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` G ) ` x ) ) ( R ` x ) ) ) = ( x e. ( Base ` C ) |-> ( R ` x ) ) )
37 1 2 4 11 fucidcl 
 |-  ( ph -> ( .1. o. ( 1st ` G ) ) e. ( G N G ) )
38 1 2 6 28 3 5 37 fucco 
 |-  ( ph -> ( ( .1. o. ( 1st ` G ) ) ( <. F , G >. .xb G ) R ) = ( x e. ( Base ` C ) |-> ( ( ( .1. o. ( 1st ` G ) ) ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` G ) ` x ) ) ( R ` x ) ) ) )
39 2 30 6 natfn 
 |-  ( ph -> R Fn ( Base ` C ) )
40 dffn5 
 |-  ( R Fn ( Base ` C ) <-> R = ( x e. ( Base ` C ) |-> ( R ` x ) ) )
41 39 40 sylib 
 |-  ( ph -> R = ( x e. ( Base ` C ) |-> ( R ` x ) ) )
42 36 38 41 3eqtr4d 
 |-  ( ph -> ( ( .1. o. ( 1st ` G ) ) ( <. F , G >. .xb G ) R ) = R )