Metamath Proof Explorer


Theorem invfuc

Description: If V ( x ) is an inverse to U ( x ) for each x , and U is a natural transformation, then V is also a natural transformation, and they are inverse in the functor category. (Contributed by Mario Carneiro, 28-Jan-2017)

Ref Expression
Hypotheses fuciso.q Q = C FuncCat D
fuciso.b B = Base C
fuciso.n N = C Nat D
fuciso.f φ F C Func D
fuciso.g φ G C Func D
fucinv.i I = Inv Q
fucinv.j J = Inv D
invfuc.u φ U F N G
invfuc.v φ x B U x 1 st F x J 1 st G x X
Assertion invfuc φ U F I G x B X

Proof

Step Hyp Ref Expression
1 fuciso.q Q = C FuncCat D
2 fuciso.b B = Base C
3 fuciso.n N = C Nat D
4 fuciso.f φ F C Func D
5 fuciso.g φ G C Func D
6 fucinv.i I = Inv Q
7 fucinv.j J = Inv D
8 invfuc.u φ U F N G
9 invfuc.v φ x B U x 1 st F x J 1 st G x X
10 eqid Base D = Base D
11 funcrcl F C Func D C Cat D Cat
12 4 11 syl φ C Cat D Cat
13 12 simprd φ D Cat
14 13 adantr φ x B D Cat
15 relfunc Rel C Func D
16 1st2ndbr Rel C Func D F C Func D 1 st F C Func D 2 nd F
17 15 4 16 sylancr φ 1 st F C Func D 2 nd F
18 2 10 17 funcf1 φ 1 st F : B Base D
19 18 ffvelrnda φ x B 1 st F x Base D
20 1st2ndbr Rel C Func D G C Func D 1 st G C Func D 2 nd G
21 15 5 20 sylancr φ 1 st G C Func D 2 nd G
22 2 10 21 funcf1 φ 1 st G : B Base D
23 22 ffvelrnda φ x B 1 st G x Base D
24 eqid Hom D = Hom D
25 10 7 14 19 23 24 invss φ x B 1 st F x J 1 st G x 1 st F x Hom D 1 st G x × 1 st G x Hom D 1 st F x
26 25 ssbrd φ x B U x 1 st F x J 1 st G x X U x 1 st F x Hom D 1 st G x × 1 st G x Hom D 1 st F x X
27 9 26 mpd φ x B U x 1 st F x Hom D 1 st G x × 1 st G x Hom D 1 st F x X
28 brxp U x 1 st F x Hom D 1 st G x × 1 st G x Hom D 1 st F x X U x 1 st F x Hom D 1 st G x X 1 st G x Hom D 1 st F x
29 28 simprbi U x 1 st F x Hom D 1 st G x × 1 st G x Hom D 1 st F x X X 1 st G x Hom D 1 st F x
30 27 29 syl φ x B X 1 st G x Hom D 1 st F x
31 30 ralrimiva φ x B X 1 st G x Hom D 1 st F x
32 2 fvexi B V
33 mptelixpg B V x B X x B 1 st G x Hom D 1 st F x x B X 1 st G x Hom D 1 st F x
34 32 33 ax-mp x B X x B 1 st G x Hom D 1 st F x x B X 1 st G x Hom D 1 st F x
35 31 34 sylibr φ x B X x B 1 st G x Hom D 1 st F x
36 fveq2 x = y 1 st G x = 1 st G y
37 fveq2 x = y 1 st F x = 1 st F y
38 36 37 oveq12d x = y 1 st G x Hom D 1 st F x = 1 st G y Hom D 1 st F y
39 38 cbvixpv x B 1 st G x Hom D 1 st F x = y B 1 st G y Hom D 1 st F y
40 35 39 eleqtrdi φ x B X y B 1 st G y Hom D 1 st F y
41 simpr2 φ y B z B f y Hom C z z B
42 simpr φ x B x B
43 eqid x B X = x B X
44 43 fvmpt2 x B X 1 st G x Hom D 1 st F x x B X x = X
45 42 30 44 syl2anc φ x B x B X x = X
46 9 45 breqtrrd φ x B U x 1 st F x J 1 st G x x B X x
47 46 ralrimiva φ x B U x 1 st F x J 1 st G x x B X x
48 47 adantr φ y B z B f y Hom C z x B U x 1 st F x J 1 st G x x B X x
49 nfcv _ x U z
50 nfcv _ x 1 st F z J 1 st G z
51 nffvmpt1 _ x x B X z
52 49 50 51 nfbr x U z 1 st F z J 1 st G z x B X z
53 fveq2 x = z U x = U z
54 fveq2 x = z 1 st F x = 1 st F z
55 fveq2 x = z 1 st G x = 1 st G z
56 54 55 oveq12d x = z 1 st F x J 1 st G x = 1 st F z J 1 st G z
57 fveq2 x = z x B X x = x B X z
58 53 56 57 breq123d x = z U x 1 st F x J 1 st G x x B X x U z 1 st F z J 1 st G z x B X z
59 52 58 rspc z B x B U x 1 st F x J 1 st G x x B X x U z 1 st F z J 1 st G z x B X z
60 41 48 59 sylc φ y B z B f y Hom C z U z 1 st F z J 1 st G z x B X z
61 13 adantr φ y B z B f y Hom C z D Cat
62 18 adantr φ y B z B f y Hom C z 1 st F : B Base D
63 62 41 ffvelrnd φ y B z B f y Hom C z 1 st F z Base D
64 22 adantr φ y B z B f y Hom C z 1 st G : B Base D
65 64 41 ffvelrnd φ y B z B f y Hom C z 1 st G z Base D
66 eqid Sect D = Sect D
67 10 7 61 63 65 66 isinv φ y B z B f y Hom C z U z 1 st F z J 1 st G z x B X z U z 1 st F z Sect D 1 st G z x B X z x B X z 1 st G z Sect D 1 st F z U z
68 60 67 mpbid φ y B z B f y Hom C z U z 1 st F z Sect D 1 st G z x B X z x B X z 1 st G z Sect D 1 st F z U z
69 68 simpld φ y B z B f y Hom C z U z 1 st F z Sect D 1 st G z x B X z
70 eqid comp D = comp D
71 eqid Id D = Id D
72 10 24 70 71 66 61 63 65 issect φ y B z B f y Hom C z U z 1 st F z Sect D 1 st G z x B X z U z 1 st F z Hom D 1 st G z x B X z 1 st G z Hom D 1 st F z x B X z 1 st F z 1 st G z comp D 1 st F z U z = Id D 1 st F z
73 69 72 mpbid φ y B z B f y Hom C z U z 1 st F z Hom D 1 st G z x B X z 1 st G z Hom D 1 st F z x B X z 1 st F z 1 st G z comp D 1 st F z U z = Id D 1 st F z
74 73 simp3d φ y B z B f y Hom C z x B X z 1 st F z 1 st G z comp D 1 st F z U z = Id D 1 st F z
75 74 oveq1d φ y B z B f y Hom C z x B X z 1 st F z 1 st G z comp D 1 st F z U z 1 st F y 1 st F z comp D 1 st F z y 2 nd F z f = Id D 1 st F z 1 st F y 1 st F z comp D 1 st F z y 2 nd F z f
76 simpr1 φ y B z B f y Hom C z y B
77 62 76 ffvelrnd φ y B z B f y Hom C z 1 st F y Base D
78 eqid Hom C = Hom C
79 17 adantr φ y B z B f y Hom C z 1 st F C Func D 2 nd F
80 2 78 24 79 76 41 funcf2 φ y B z B f y Hom C z y 2 nd F z : y Hom C z 1 st F y Hom D 1 st F z
81 simpr3 φ y B z B f y Hom C z f y Hom C z
82 80 81 ffvelrnd φ y B z B f y Hom C z y 2 nd F z f 1 st F y Hom D 1 st F z
83 10 24 71 61 77 70 63 82 catlid φ y B z B f y Hom C z Id D 1 st F z 1 st F y 1 st F z comp D 1 st F z y 2 nd F z f = y 2 nd F z f
84 75 83 eqtr2d φ y B z B f y Hom C z y 2 nd F z f = x B X z 1 st F z 1 st G z comp D 1 st F z U z 1 st F y 1 st F z comp D 1 st F z y 2 nd F z f
85 8 adantr φ y B z B f y Hom C z U F N G
86 3 85 nat1st2nd φ y B z B f y Hom C z U 1 st F 2 nd F N 1 st G 2 nd G
87 3 86 2 24 41 natcl φ y B z B f y Hom C z U z 1 st F z Hom D 1 st G z
88 73 simp2d φ y B z B f y Hom C z x B X z 1 st G z Hom D 1 st F z
89 10 24 70 61 77 63 65 82 87 63 88 catass φ y B z B f y Hom C z x B X z 1 st F z 1 st G z comp D 1 st F z U z 1 st F y 1 st F z comp D 1 st F z y 2 nd F z f = x B X z 1 st F y 1 st G z comp D 1 st F z U z 1 st F y 1 st F z comp D 1 st G z y 2 nd F z f
90 3 86 2 78 70 76 41 81 nati φ y B z B f y Hom C z U z 1 st F y 1 st F z comp D 1 st G z y 2 nd F z f = y 2 nd G z f 1 st F y 1 st G y comp D 1 st G z U y
91 90 oveq2d φ y B z B f y Hom C z x B X z 1 st F y 1 st G z comp D 1 st F z U z 1 st F y 1 st F z comp D 1 st G z y 2 nd F z f = x B X z 1 st F y 1 st G z comp D 1 st F z y 2 nd G z f 1 st F y 1 st G y comp D 1 st G z U y
92 84 89 91 3eqtrd φ y B z B f y Hom C z y 2 nd F z f = x B X z 1 st F y 1 st G z comp D 1 st F z y 2 nd G z f 1 st F y 1 st G y comp D 1 st G z U y
93 92 oveq1d φ y B z B f y Hom C z y 2 nd F z f 1 st G y 1 st F y comp D 1 st F z x B X y = x B X z 1 st F y 1 st G z comp D 1 st F z y 2 nd G z f 1 st F y 1 st G y comp D 1 st G z U y 1 st G y 1 st F y comp D 1 st F z x B X y
94 64 76 ffvelrnd φ y B z B f y Hom C z 1 st G y Base D
95 nfcv _ x U y
96 nfcv _ x 1 st F y J 1 st G y
97 nffvmpt1 _ x x B X y
98 95 96 97 nfbr x U y 1 st F y J 1 st G y x B X y
99 fveq2 x = y U x = U y
100 37 36 oveq12d x = y 1 st F x J 1 st G x = 1 st F y J 1 st G y
101 fveq2 x = y x B X x = x B X y
102 99 100 101 breq123d x = y U x 1 st F x J 1 st G x x B X x U y 1 st F y J 1 st G y x B X y
103 98 102 rspc y B x B U x 1 st F x J 1 st G x x B X x U y 1 st F y J 1 st G y x B X y
104 76 48 103 sylc φ y B z B f y Hom C z U y 1 st F y J 1 st G y x B X y
105 10 7 61 77 94 66 isinv φ y B z B f y Hom C z U y 1 st F y J 1 st G y x B X y U y 1 st F y Sect D 1 st G y x B X y x B X y 1 st G y Sect D 1 st F y U y
106 104 105 mpbid φ y B z B f y Hom C z U y 1 st F y Sect D 1 st G y x B X y x B X y 1 st G y Sect D 1 st F y U y
107 106 simprd φ y B z B f y Hom C z x B X y 1 st G y Sect D 1 st F y U y
108 10 24 70 71 66 61 94 77 issect φ y B z B f y Hom C z x B X y 1 st G y Sect D 1 st F y U y x B X y 1 st G y Hom D 1 st F y U y 1 st F y Hom D 1 st G y U y 1 st G y 1 st F y comp D 1 st G y x B X y = Id D 1 st G y
109 107 108 mpbid φ y B z B f y Hom C z x B X y 1 st G y Hom D 1 st F y U y 1 st F y Hom D 1 st G y U y 1 st G y 1 st F y comp D 1 st G y x B X y = Id D 1 st G y
110 109 simp1d φ y B z B f y Hom C z x B X y 1 st G y Hom D 1 st F y
111 109 simp2d φ y B z B f y Hom C z U y 1 st F y Hom D 1 st G y
112 21 adantr φ y B z B f y Hom C z 1 st G C Func D 2 nd G
113 2 78 24 112 76 41 funcf2 φ y B z B f y Hom C z y 2 nd G z : y Hom C z 1 st G y Hom D 1 st G z
114 113 81 ffvelrnd φ y B z B f y Hom C z y 2 nd G z f 1 st G y Hom D 1 st G z
115 10 24 70 61 77 94 65 111 114 catcocl φ y B z B f y Hom C z y 2 nd G z f 1 st F y 1 st G y comp D 1 st G z U y 1 st F y Hom D 1 st G z
116 10 24 70 61 94 77 65 110 115 63 88 catass φ y B z B f y Hom C z x B X z 1 st F y 1 st G z comp D 1 st F z y 2 nd G z f 1 st F y 1 st G y comp D 1 st G z U y 1 st G y 1 st F y comp D 1 st F z x B X y = x B X z 1 st G y 1 st G z comp D 1 st F z y 2 nd G z f 1 st F y 1 st G y comp D 1 st G z U y 1 st G y 1 st F y comp D 1 st G z x B X y
117 3 86 2 24 76 natcl φ y B z B f y Hom C z U y 1 st F y Hom D 1 st G y
118 10 24 70 61 94 77 94 110 117 65 114 catass φ y B z B f y Hom C z y 2 nd G z f 1 st F y 1 st G y comp D 1 st G z U y 1 st G y 1 st F y comp D 1 st G z x B X y = y 2 nd G z f 1 st G y 1 st G y comp D 1 st G z U y 1 st G y 1 st F y comp D 1 st G y x B X y
119 109 simp3d φ y B z B f y Hom C z U y 1 st G y 1 st F y comp D 1 st G y x B X y = Id D 1 st G y
120 119 oveq2d φ y B z B f y Hom C z y 2 nd G z f 1 st G y 1 st G y comp D 1 st G z U y 1 st G y 1 st F y comp D 1 st G y x B X y = y 2 nd G z f 1 st G y 1 st G y comp D 1 st G z Id D 1 st G y
121 10 24 71 61 94 70 65 114 catrid φ y B z B f y Hom C z y 2 nd G z f 1 st G y 1 st G y comp D 1 st G z Id D 1 st G y = y 2 nd G z f
122 118 120 121 3eqtrd φ y B z B f y Hom C z y 2 nd G z f 1 st F y 1 st G y comp D 1 st G z U y 1 st G y 1 st F y comp D 1 st G z x B X y = y 2 nd G z f
123 122 oveq2d φ y B z B f y Hom C z x B X z 1 st G y 1 st G z comp D 1 st F z y 2 nd G z f 1 st F y 1 st G y comp D 1 st G z U y 1 st G y 1 st F y comp D 1 st G z x B X y = x B X z 1 st G y 1 st G z comp D 1 st F z y 2 nd G z f
124 93 116 123 3eqtrrd φ y B z B f y Hom C z x B X z 1 st G y 1 st G z comp D 1 st F z y 2 nd G z f = y 2 nd F z f 1 st G y 1 st F y comp D 1 st F z x B X y
125 124 ralrimivvva φ y B z B f y Hom C z x B X z 1 st G y 1 st G z comp D 1 st F z y 2 nd G z f = y 2 nd F z f 1 st G y 1 st F y comp D 1 st F z x B X y
126 3 2 78 24 70 5 4 isnat2 φ x B X G N F x B X y B 1 st G y Hom D 1 st F y y B z B f y Hom C z x B X z 1 st G y 1 st G z comp D 1 st F z y 2 nd G z f = y 2 nd F z f 1 st G y 1 st F y comp D 1 st F z x B X y
127 40 125 126 mpbir2and φ x B X G N F
128 nfv y U x 1 st F x J 1 st G x x B X x
129 128 98 102 cbvralw x B U x 1 st F x J 1 st G x x B X x y B U y 1 st F y J 1 st G y x B X y
130 47 129 sylib φ y B U y 1 st F y J 1 st G y x B X y
131 1 2 3 4 5 6 7 fucinv φ U F I G x B X U F N G x B X G N F y B U y 1 st F y J 1 st G y x B X y
132 8 127 130 131 mpbir3and φ U F I G x B X