Metamath Proof Explorer

Theorem fucidcl

Description: The identity natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses fucidcl.q 
|- Q = ( C FuncCat D )
fucidcl.n 
|- N = ( C Nat D )
fucidcl.x 
|- .1. = ( Id ` D )
fucidcl.f 
|- ( ph -> F e. ( C Func D ) )
Assertion fucidcl 
|- ( ph -> ( .1. o. ( 1st ` F ) ) e. ( F N F ) )

Proof

Step Hyp Ref Expression
1 fucidcl.q 
 |-  Q = ( C FuncCat D )
2 fucidcl.n 
 |-  N = ( C Nat D )
3 fucidcl.x 
 |-  .1. = ( Id ` D )
4 fucidcl.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 simprd 
 |-  ( ph -> D e. Cat )
8 eqid 
 |-  ( Base ` D ) = ( Base ` D )
9 8 3 cidfn 
 |-  ( D e. Cat -> .1. Fn ( Base ` D ) )
10 7 9 syl 
 |-  ( ph -> .1. Fn ( Base ` D ) )
11 dffn2 
 |-  ( .1. Fn ( Base ` D ) <-> .1. : ( Base ` D ) --> _V )
12 10 11 sylib 
 |-  ( ph -> .1. : ( Base ` D ) --> _V )
13 eqid 
 |-  ( Base ` C ) = ( Base ` C )
14 relfunc 
 |-  Rel ( C Func D )
15 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
16 14 4 15 sylancr 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
17 13 8 16 funcf1 
 |-  ( ph -> ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) )
18 fcompt 
 |-  ( ( .1. : ( Base ` D ) --> _V /\ ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) ) -> ( .1. o. ( 1st ` F ) ) = ( x e. ( Base ` C ) |-> ( .1. ` ( ( 1st ` F ) ` x ) ) ) )
19 12 17 18 syl2anc 
 |-  ( ph -> ( .1. o. ( 1st ` F ) ) = ( x e. ( Base ` C ) |-> ( .1. ` ( ( 1st ` F ) ` x ) ) ) )
20 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
21 7 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> D e. Cat )
22 17 ffvelrnda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` F ) ` x ) e. ( Base ` D ) )
23 8 20 3 21 22 catidcl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( .1. ` ( ( 1st ` F ) ` x ) ) e. ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` x ) ) )
24 23 ralrimiva 
 |-  ( ph -> A. x e. ( Base ` C ) ( .1. ` ( ( 1st ` F ) ` x ) ) e. ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` x ) ) )
25 fvex 
 |-  ( Base ` C ) e. _V
26 mptelixpg 
 |-  ( ( Base ` C ) e. _V -> ( ( x e. ( Base ` C ) |-> ( .1. ` ( ( 1st ` F ) ` x ) ) ) e. X_ x e. ( Base ` C ) ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` x ) ) <-> A. x e. ( Base ` C ) ( .1. ` ( ( 1st ` F ) ` x ) ) e. ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` x ) ) ) )
27 25 26 ax-mp 
 |-  ( ( x e. ( Base ` C ) |-> ( .1. ` ( ( 1st ` F ) ` x ) ) ) e. X_ x e. ( Base ` C ) ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` x ) ) <-> A. x e. ( Base ` C ) ( .1. ` ( ( 1st ` F ) ` x ) ) e. ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` x ) ) )
28 24 27 sylibr 
 |-  ( ph -> ( x e. ( Base ` C ) |-> ( .1. ` ( ( 1st ` F ) ` x ) ) ) e. X_ x e. ( Base ` C ) ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` x ) ) )
29 19 28 eqeltrd 
 |-  ( ph -> ( .1. o. ( 1st ` F ) ) e. X_ x e. ( Base ` C ) ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` x ) ) )
30 7 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> D e. Cat )
31 simpr1 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> x e. ( Base ` C ) )
32 31 22 syldan 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( 1st ` F ) ` x ) e. ( Base ` D ) )
33 eqid 
 |-  ( comp ` D ) = ( comp ` D )
34 17 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) )
35 simpr2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> y e. ( Base ` C ) )
36 34 35 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( 1st ` F ) ` y ) e. ( Base ` D ) )
37 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
38 16 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
39 13 37 20 38 31 35 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( x ( 2nd ` F ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) )
40 simpr3 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> f e. ( x ( Hom ` C ) y ) )
41 39 40 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( x ( 2nd ` F ) y ) ` f ) e. ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) )
42 8 20 3 30 32 33 36 41 catlid 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( .1. ` ( ( 1st ` F ) ` y ) ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` F ) ` y ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) = ( ( x ( 2nd ` F ) y ) ` f ) )
43 8 20 3 30 32 33 36 41 catrid 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( ( x ( 2nd ` F ) y ) ` f ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` x ) >. ( comp ` D ) ( ( 1st ` F ) ` y ) ) ( .1. ` ( ( 1st ` F ) ` x ) ) ) = ( ( x ( 2nd ` F ) y ) ` f ) )
44 42 43 eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( .1. ` ( ( 1st ` F ) ` y ) ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` F ) ` y ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) = ( ( ( x ( 2nd ` F ) y ) ` f ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` x ) >. ( comp ` D ) ( ( 1st ` F ) ` y ) ) ( .1. ` ( ( 1st ` F ) ` x ) ) ) )
45 fvco3 
 |-  ( ( ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) /\ y e. ( Base ` C ) ) -> ( ( .1. o. ( 1st ` F ) ) ` y ) = ( .1. ` ( ( 1st ` F ) ` y ) ) )
46 34 35 45 syl2anc 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( .1. o. ( 1st ` F ) ) ` y ) = ( .1. ` ( ( 1st ` F ) ` y ) ) )
47 46 oveq1d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( ( .1. o. ( 1st ` F ) ) ` y ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` F ) ` y ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) = ( ( .1. ` ( ( 1st ` F ) ` y ) ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` F ) ` y ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) )
48 fvco3 
 |-  ( ( ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) /\ x e. ( Base ` C ) ) -> ( ( .1. o. ( 1st ` F ) ) ` x ) = ( .1. ` ( ( 1st ` F ) ` x ) ) )
49 34 31 48 syl2anc 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( .1. o. ( 1st ` F ) ) ` x ) = ( .1. ` ( ( 1st ` F ) ` x ) ) )
50 49 oveq2d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( ( x ( 2nd ` F ) y ) ` f ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` x ) >. ( comp ` D ) ( ( 1st ` F ) ` y ) ) ( ( .1. o. ( 1st ` F ) ) ` x ) ) = ( ( ( x ( 2nd ` F ) y ) ` f ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` x ) >. ( comp ` D ) ( ( 1st ` F ) ` y ) ) ( .1. ` ( ( 1st ` F ) ` x ) ) ) )
51 44 47 50 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( ( .1. o. ( 1st ` F ) ) ` y ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` F ) ` y ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) = ( ( ( x ( 2nd ` F ) y ) ` f ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` x ) >. ( comp ` D ) ( ( 1st ` F ) ` y ) ) ( ( .1. o. ( 1st ` F ) ) ` x ) ) )
52 51 ralrimivvva 
 |-  ( ph -> A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) ( ( ( .1. o. ( 1st ` F ) ) ` y ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` F ) ` y ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) = ( ( ( x ( 2nd ` F ) y ) ` f ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` x ) >. ( comp ` D ) ( ( 1st ` F ) ` y ) ) ( ( .1. o. ( 1st ` F ) ) ` x ) ) )
53 2 13 37 20 33 4 4 isnat2 
 |-  ( ph -> ( ( .1. o. ( 1st ` F ) ) e. ( F N F ) <-> ( ( .1. o. ( 1st ` F ) ) e. X_ x e. ( Base ` C ) ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` x ) ) /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) ( ( ( .1. o. ( 1st ` F ) ) ` y ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` F ) ` y ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) = ( ( ( x ( 2nd ` F ) y ) ` f ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` x ) >. ( comp ` D ) ( ( 1st ` F ) ` y ) ) ( ( .1. o. ( 1st ` F ) ) ` x ) ) ) ) )
54 29 52 53 mpbir2and 
 |-  ( ph -> ( .1. o. ( 1st ` F ) ) e. ( F N F ) )