Metamath Proof Explorer

Theorem funcinv

Description: The image of an inverse under a functor is an inverse. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses funcinv.b ⊢ B = Base D
funcinv.s ⊢ I = Inv ⁡ D
funcinv.t ⊢ J = Inv ⁡ E
funcinv.f ⊢ φ → F D Func E G
funcinv.x ⊢ φ → X ∈ B
funcinv.y ⊢ φ → Y ∈ B
funcinv.m ⊢ φ → M X I Y N
Assertion funcinv ⊢ φ → X G Y ⁡ M F ⁡ X J F ⁡ Y Y G X ⁡ N

Proof

Step Hyp Ref Expression
1 funcinv.b ⊢ B = Base D
2 funcinv.s ⊢ I = Inv ⁡ D
3 funcinv.t ⊢ J = Inv ⁡ E
4 funcinv.f ⊢ φ → F D Func E G
5 funcinv.x ⊢ φ → X ∈ B
6 funcinv.y ⊢ φ → Y ∈ B
7 funcinv.m ⊢ φ → M X I Y N
8 eqid ⊢ Sect ⁡ D = Sect ⁡ D
9 eqid ⊢ Sect ⁡ E = Sect ⁡ E
10 df-br ⊢ F D Func E G ↔ F G ∈ D Func E
11 4 10 sylib ⊢ φ → F G ∈ D Func E
12 funcrcl ⊢ F G ∈ D Func E → D ∈ Cat ∧ E ∈ Cat
13 11 12 syl ⊢ φ → D ∈ Cat ∧ E ∈ Cat
14 13 simpld ⊢ φ → D ∈ Cat
15 1 2 14 5 6 8 isinv ⊢ φ → M X I Y N ↔ M X Sect ⁡ D Y N ∧ N Y Sect ⁡ D X M
16 7 15 mpbid ⊢ φ → M X Sect ⁡ D Y N ∧ N Y Sect ⁡ D X M
17 16 simpld ⊢ φ → M X Sect ⁡ D Y N
18 1 8 9 4 5 6 17 funcsect ⊢ φ → X G Y ⁡ M F ⁡ X Sect ⁡ E F ⁡ Y Y G X ⁡ N
19 16 simprd ⊢ φ → N Y Sect ⁡ D X M
20 1 8 9 4 6 5 19 funcsect ⊢ φ → Y G X ⁡ N F ⁡ Y Sect ⁡ E F ⁡ X X G Y ⁡ M
21 eqid ⊢ Base E = Base E
22 13 simprd ⊢ φ → E ∈ Cat
23 1 21 4 funcf1 ⊢ φ → F : B ⟶ Base E
24 23 5 ffvelrnd ⊢ φ → F ⁡ X ∈ Base E
25 23 6 ffvelrnd ⊢ φ → F ⁡ Y ∈ Base E
26 21 3 22 24 25 9 isinv ⊢ φ → X G Y ⁡ M F ⁡ X J F ⁡ Y Y G X ⁡ N ↔ X G Y ⁡ M F ⁡ X Sect ⁡ E F ⁡ Y Y G X ⁡ N ∧ Y G X ⁡ N F ⁡ Y Sect ⁡ E F ⁡ X X G Y ⁡ M
27 18 20 26 mpbir2and ⊢ φ → X G Y ⁡ M F ⁡ X J F ⁡ Y Y G X ⁡ N