Metamath Proof Explorer

Theorem fucinv

Description: Two natural transformations are inverses of each other iff all the components are inverse. (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
Assertion fucinv ⊢ φ → U F I G V ↔ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x J 1 st ⁡ G ⁡ x V ⁡ 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 eqid ⊢ Sect ⁡ Q = Sect ⁡ Q
9 eqid ⊢ Sect ⁡ D = Sect ⁡ D
10 1 2 3 4 5 8 9 fucsect ⊢ φ → U F Sect ⁡ Q G V ↔ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x Sect ⁡ D 1 st ⁡ G ⁡ x V ⁡ x
11 1 2 3 5 4 8 9 fucsect ⊢ φ → V G Sect ⁡ Q F U ↔ V ∈ G N F ∧ U ∈ F N G ∧ ∀ x ∈ B V ⁡ x 1 st ⁡ G ⁡ x Sect ⁡ D 1 st ⁡ F ⁡ x U ⁡ x
12 10 11 anbi12d ⊢ φ → U F Sect ⁡ Q G V ∧ V G Sect ⁡ Q F U ↔ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x Sect ⁡ D 1 st ⁡ G ⁡ x V ⁡ x ∧ V ∈ G N F ∧ U ∈ F N G ∧ ∀ x ∈ B V ⁡ x 1 st ⁡ G ⁡ x Sect ⁡ D 1 st ⁡ F ⁡ x U ⁡ x
13 1 fucbas ⊢ C Func D = Base Q
14 funcrcl ⊢ F ∈ C Func D → C ∈ Cat ∧ D ∈ Cat
15 4 14 syl ⊢ φ → C ∈ Cat ∧ D ∈ Cat
16 15 simpld ⊢ φ → C ∈ Cat
17 15 simprd ⊢ φ → D ∈ Cat
18 1 16 17 fuccat ⊢ φ → Q ∈ Cat
19 13 6 18 4 5 8 isinv ⊢ φ → U F I G V ↔ U F Sect ⁡ Q G V ∧ V G Sect ⁡ Q F U
20 eqid ⊢ Base D = Base D
21 17 adantr ⊢ φ ∧ x ∈ B → D ∈ Cat
22 relfunc ⊢ Rel ⁡ C Func D
23 1st2ndbr ⊢ Rel ⁡ C Func D ∧ F ∈ C Func D → 1 st ⁡ F C Func D 2 nd ⁡ F
24 22 4 23 sylancr ⊢ φ → 1 st ⁡ F C Func D 2 nd ⁡ F
25 2 20 24 funcf1 ⊢ φ → 1 st ⁡ F : B ⟶ Base D
26 25 ffvelrnda ⊢ φ ∧ x ∈ B → 1 st ⁡ F ⁡ x ∈ Base D
27 1st2ndbr ⊢ Rel ⁡ C Func D ∧ G ∈ C Func D → 1 st ⁡ G C Func D 2 nd ⁡ G
28 22 5 27 sylancr ⊢ φ → 1 st ⁡ G C Func D 2 nd ⁡ G
29 2 20 28 funcf1 ⊢ φ → 1 st ⁡ G : B ⟶ Base D
30 29 ffvelrnda ⊢ φ ∧ x ∈ B → 1 st ⁡ G ⁡ x ∈ Base D
31 20 7 21 26 30 9 isinv ⊢ φ ∧ x ∈ B → U ⁡ x 1 st ⁡ F ⁡ x J 1 st ⁡ G ⁡ x V ⁡ x ↔ U ⁡ x 1 st ⁡ F ⁡ x Sect ⁡ D 1 st ⁡ G ⁡ x V ⁡ x ∧ V ⁡ x 1 st ⁡ G ⁡ x Sect ⁡ D 1 st ⁡ F ⁡ x U ⁡ x
32 31 ralbidva ⊢ φ → ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x J 1 st ⁡ G ⁡ x V ⁡ x ↔ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x Sect ⁡ D 1 st ⁡ G ⁡ x V ⁡ x ∧ V ⁡ x 1 st ⁡ G ⁡ x Sect ⁡ D 1 st ⁡ F ⁡ x U ⁡ x
33 r19.26 ⊢ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x Sect ⁡ D 1 st ⁡ G ⁡ x V ⁡ x ∧ V ⁡ x 1 st ⁡ G ⁡ x Sect ⁡ D 1 st ⁡ F ⁡ x U ⁡ x ↔ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x Sect ⁡ D 1 st ⁡ G ⁡ x V ⁡ x ∧ ∀ x ∈ B V ⁡ x 1 st ⁡ G ⁡ x Sect ⁡ D 1 st ⁡ F ⁡ x U ⁡ x
34 32 33 bitrdi ⊢ φ → ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x J 1 st ⁡ G ⁡ x V ⁡ x ↔ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x Sect ⁡ D 1 st ⁡ G ⁡ x V ⁡ x ∧ ∀ x ∈ B V ⁡ x 1 st ⁡ G ⁡ x Sect ⁡ D 1 st ⁡ F ⁡ x U ⁡ x
35 34 anbi2d ⊢ φ → U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x J 1 st ⁡ G ⁡ x V ⁡ x ↔ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x Sect ⁡ D 1 st ⁡ G ⁡ x V ⁡ x ∧ ∀ x ∈ B V ⁡ x 1 st ⁡ G ⁡ x Sect ⁡ D 1 st ⁡ F ⁡ x U ⁡ x
36 df-3an ⊢ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x J 1 st ⁡ G ⁡ x V ⁡ x ↔ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x J 1 st ⁡ G ⁡ x V ⁡ x
37 df-3an ⊢ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x Sect ⁡ D 1 st ⁡ G ⁡ x V ⁡ x ↔ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x Sect ⁡ D 1 st ⁡ G ⁡ x V ⁡ x
38 3ancoma ⊢ V ∈ G N F ∧ U ∈ F N G ∧ ∀ x ∈ B V ⁡ x 1 st ⁡ G ⁡ x Sect ⁡ D 1 st ⁡ F ⁡ x U ⁡ x ↔ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B V ⁡ x 1 st ⁡ G ⁡ x Sect ⁡ D 1 st ⁡ F ⁡ x U ⁡ x
39 df-3an ⊢ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B V ⁡ x 1 st ⁡ G ⁡ x Sect ⁡ D 1 st ⁡ F ⁡ x U ⁡ x ↔ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B V ⁡ x 1 st ⁡ G ⁡ x Sect ⁡ D 1 st ⁡ F ⁡ x U ⁡ x
40 38 39 bitri ⊢ V ∈ G N F ∧ U ∈ F N G ∧ ∀ x ∈ B V ⁡ x 1 st ⁡ G ⁡ x Sect ⁡ D 1 st ⁡ F ⁡ x U ⁡ x ↔ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B V ⁡ x 1 st ⁡ G ⁡ x Sect ⁡ D 1 st ⁡ F ⁡ x U ⁡ x
41 37 40 anbi12i ⊢ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x Sect ⁡ D 1 st ⁡ G ⁡ x V ⁡ x ∧ V ∈ G N F ∧ U ∈ F N G ∧ ∀ x ∈ B V ⁡ x 1 st ⁡ G ⁡ x Sect ⁡ D 1 st ⁡ F ⁡ x U ⁡ x ↔ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x Sect ⁡ D 1 st ⁡ G ⁡ x V ⁡ x ∧ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B V ⁡ x 1 st ⁡ G ⁡ x Sect ⁡ D 1 st ⁡ F ⁡ x U ⁡ x
42 anandi ⊢ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x Sect ⁡ D 1 st ⁡ G ⁡ x V ⁡ x ∧ ∀ x ∈ B V ⁡ x 1 st ⁡ G ⁡ x Sect ⁡ D 1 st ⁡ F ⁡ x U ⁡ x ↔ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x Sect ⁡ D 1 st ⁡ G ⁡ x V ⁡ x ∧ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B V ⁡ x 1 st ⁡ G ⁡ x Sect ⁡ D 1 st ⁡ F ⁡ x U ⁡ x
43 41 42 bitr4i ⊢ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x Sect ⁡ D 1 st ⁡ G ⁡ x V ⁡ x ∧ V ∈ G N F ∧ U ∈ F N G ∧ ∀ x ∈ B V ⁡ x 1 st ⁡ G ⁡ x Sect ⁡ D 1 st ⁡ F ⁡ x U ⁡ x ↔ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x Sect ⁡ D 1 st ⁡ G ⁡ x V ⁡ x ∧ ∀ x ∈ B V ⁡ x 1 st ⁡ G ⁡ x Sect ⁡ D 1 st ⁡ F ⁡ x U ⁡ x
44 35 36 43 3bitr4g ⊢ φ → U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x J 1 st ⁡ G ⁡ x V ⁡ x ↔ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x Sect ⁡ D 1 st ⁡ G ⁡ x V ⁡ x ∧ V ∈ G N F ∧ U ∈ F N G ∧ ∀ x ∈ B V ⁡ x 1 st ⁡ G ⁡ x Sect ⁡ D 1 st ⁡ F ⁡ x U ⁡ x
45 12 19 44 3bitr4d ⊢ φ → U F I G V ↔ U ∈ F N G ∧ V ∈ G N F ∧ ∀ x ∈ B U ⁡ x 1 st ⁡ F ⁡ x J 1 st ⁡ G ⁡ x V ⁡ x