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 φ F C Func D
Assertion fucidcl φ 1 ˙ 1 st F 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 φ F C Func D
5 funcrcl F C Func D C Cat D Cat
6 4 5 syl φ C Cat D Cat
7 6 simprd φ D Cat
8 eqid Base D = Base D
9 8 3 cidfn D Cat 1 ˙ Fn Base D
10 7 9 syl φ 1 ˙ Fn Base D
11 dffn2 1 ˙ Fn Base D 1 ˙ : Base D V
12 10 11 sylib φ 1 ˙ : Base D V
13 eqid Base C = Base C
14 relfunc Rel C Func D
15 1st2ndbr Rel C Func D F C Func D 1 st F C Func D 2 nd F
16 14 4 15 sylancr φ 1 st F C Func D 2 nd F
17 13 8 16 funcf1 φ 1 st F : Base C Base D
18 fcompt 1 ˙ : Base D V 1 st F : Base C Base D 1 ˙ 1 st F = x Base C 1 ˙ 1 st F x
19 12 17 18 syl2anc φ 1 ˙ 1 st F = x Base C 1 ˙ 1 st F x
20 eqid Hom D = Hom D
21 7 adantr φ x Base C D Cat
22 17 ffvelrnda φ x Base C 1 st F x Base D
23 8 20 3 21 22 catidcl φ x Base C 1 ˙ 1 st F x 1 st F x Hom D 1 st F x
24 23 ralrimiva φ x Base C 1 ˙ 1 st F x 1 st F x Hom D 1 st F x
25 fvex Base C V
26 mptelixpg Base C V x Base C 1 ˙ 1 st F x x Base C 1 st F x Hom D 1 st F x x Base C 1 ˙ 1 st F x 1 st F x Hom D 1 st F x
27 25 26 ax-mp x Base C 1 ˙ 1 st F x x Base C 1 st F x Hom D 1 st F x x Base C 1 ˙ 1 st F x 1 st F x Hom D 1 st F x
28 24 27 sylibr φ x Base C 1 ˙ 1 st F x x Base C 1 st F x Hom D 1 st F x
29 19 28 eqeltrd φ 1 ˙ 1 st F x Base C 1 st F x Hom D 1 st F x
30 7 adantr φ x Base C y Base C f x Hom C y D Cat
31 simpr1 φ x Base C y Base C f x Hom C y x Base C
32 31 22 syldan φ x Base C y Base C f x Hom C y 1 st F x Base D
33 eqid comp D = comp D
34 17 adantr φ x Base C y Base C f x Hom C y 1 st F : Base C Base D
35 simpr2 φ x Base C y Base C f x Hom C y y Base C
36 34 35 ffvelrnd φ x Base C y Base C f x Hom C y 1 st F y Base D
37 eqid Hom C = Hom C
38 16 adantr φ x Base C y Base C f x Hom C y 1 st F C Func D 2 nd F
39 13 37 20 38 31 35 funcf2 φ x Base C y Base C f x Hom C y x 2 nd F y : x Hom C y 1 st F x Hom D 1 st F y
40 simpr3 φ x Base C y Base C f x Hom C y f x Hom C y
41 39 40 ffvelrnd φ x Base C y Base C f x Hom C y x 2 nd F y f 1 st F x Hom D 1 st F y
42 8 20 3 30 32 33 36 41 catlid φ x Base C y Base C f x Hom C y 1 ˙ 1 st F y 1 st F x 1 st F y comp D 1 st F y x 2 nd F y f = x 2 nd F y f
43 8 20 3 30 32 33 36 41 catrid φ x Base C y Base C f x Hom C y x 2 nd F y f 1 st F x 1 st F x comp D 1 st F y 1 ˙ 1 st F x = x 2 nd F y f
44 42 43 eqtr4d φ x Base C y Base C f x Hom C y 1 ˙ 1 st F y 1 st F x 1 st F y comp D 1 st F y x 2 nd F y f = x 2 nd F y f 1 st F x 1 st F x comp D 1 st F y 1 ˙ 1 st F x
45 fvco3 1 st F : Base C Base D y Base C 1 ˙ 1 st F y = 1 ˙ 1 st F y
46 34 35 45 syl2anc φ x Base C y Base C f x Hom C y 1 ˙ 1 st F y = 1 ˙ 1 st F y
47 46 oveq1d φ x Base C y Base C f x Hom C y 1 ˙ 1 st F y 1 st F x 1 st F y comp D 1 st F y x 2 nd F y f = 1 ˙ 1 st F y 1 st F x 1 st F y comp D 1 st F y x 2 nd F y f
48 fvco3 1 st F : Base C Base D x Base C 1 ˙ 1 st F x = 1 ˙ 1 st F x
49 34 31 48 syl2anc φ x Base C y Base C f x Hom C y 1 ˙ 1 st F x = 1 ˙ 1 st F x
50 49 oveq2d φ x Base C y Base C f x Hom C y x 2 nd F y f 1 st F x 1 st F x comp D 1 st F y 1 ˙ 1 st F x = x 2 nd F y f 1 st F x 1 st F x comp D 1 st F y 1 ˙ 1 st F x
51 44 47 50 3eqtr4d φ x Base C y Base C f x Hom C y 1 ˙ 1 st F y 1 st F x 1 st F y comp D 1 st F y x 2 nd F y f = x 2 nd F y f 1 st F x 1 st F x comp D 1 st F y 1 ˙ 1 st F x
52 51 ralrimivvva φ x Base C y Base C f x Hom C y 1 ˙ 1 st F y 1 st F x 1 st F y comp D 1 st F y x 2 nd F y f = x 2 nd F y f 1 st F x 1 st F x comp D 1 st F y 1 ˙ 1 st F x
53 2 13 37 20 33 4 4 isnat2 φ 1 ˙ 1 st F F N F 1 ˙ 1 st F x Base C 1 st F x Hom D 1 st F x x Base C y Base C f x Hom C y 1 ˙ 1 st F y 1 st F x 1 st F y comp D 1 st F y x 2 nd F y f = x 2 nd F y f 1 st F x 1 st F x comp D 1 st F y 1 ˙ 1 st F x
54 29 52 53 mpbir2and φ 1 ˙ 1 st F F N F