Metamath Proof Explorer

Theorem fthinv

Description: A faithful functor reflects inverses. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses fthsect.b ⊢ B = Base C
fthsect.h ⊢ H = Hom ⁡ C
fthsect.f ⊢ φ → F C Faith D G
fthsect.x ⊢ φ → X ∈ B
fthsect.y ⊢ φ → Y ∈ B
fthsect.m ⊢ φ → M ∈ X H Y
fthsect.n ⊢ φ → N ∈ Y H X
fthinv.s ⊢ I = Inv ⁡ C
fthinv.t ⊢ J = Inv ⁡ D
Assertion fthinv ⊢ φ → M X I Y N ↔ X G Y ⁡ M F ⁡ X J F ⁡ Y Y G X ⁡ N

Proof

Step Hyp Ref Expression
1 fthsect.b ⊢ B = Base C
2 fthsect.h ⊢ H = Hom ⁡ C
3 fthsect.f ⊢ φ → F C Faith D G
4 fthsect.x ⊢ φ → X ∈ B
5 fthsect.y ⊢ φ → Y ∈ B
6 fthsect.m ⊢ φ → M ∈ X H Y
7 fthsect.n ⊢ φ → N ∈ Y H X
8 fthinv.s ⊢ I = Inv ⁡ C
9 fthinv.t ⊢ J = Inv ⁡ D
10 eqid ⊢ Sect ⁡ C = Sect ⁡ C
11 eqid ⊢ Sect ⁡ D = Sect ⁡ D
12 1 2 3 4 5 6 7 10 11 fthsect ⊢ φ → M X Sect ⁡ C Y N ↔ X G Y ⁡ M F ⁡ X Sect ⁡ D F ⁡ Y Y G X ⁡ N
13 1 2 3 5 4 7 6 10 11 fthsect ⊢ φ → N Y Sect ⁡ C X M ↔ Y G X ⁡ N F ⁡ Y Sect ⁡ D F ⁡ X X G Y ⁡ M
14 12 13 anbi12d ⊢ φ → M X Sect ⁡ C Y N ∧ N Y Sect ⁡ C X M ↔ X G Y ⁡ M F ⁡ X Sect ⁡ D F ⁡ Y Y G X ⁡ N ∧ Y G X ⁡ N F ⁡ Y Sect ⁡ D F ⁡ X X G Y ⁡ M
15 fthfunc ⊢ C Faith D ⊆ C Func D
16 15 ssbri ⊢ F C Faith D G → F C Func D G
17 3 16 syl ⊢ φ → F C Func D G
18 df-br ⊢ F C Func D G ↔ F G ∈ C Func D
19 17 18 sylib ⊢ φ → F G ∈ C Func D
20 funcrcl ⊢ F G ∈ C Func D → C ∈ Cat ∧ D ∈ Cat
21 19 20 syl ⊢ φ → C ∈ Cat ∧ D ∈ Cat
22 21 simpld ⊢ φ → C ∈ Cat
23 1 8 22 4 5 10 isinv ⊢ φ → M X I Y N ↔ M X Sect ⁡ C Y N ∧ N Y Sect ⁡ C X M
24 eqid ⊢ Base D = Base D
25 21 simprd ⊢ φ → D ∈ Cat
26 1 24 17 funcf1 ⊢ φ → F : B ⟶ Base D
27 26 4 ffvelrnd ⊢ φ → F ⁡ X ∈ Base D
28 26 5 ffvelrnd ⊢ φ → F ⁡ Y ∈ Base D
29 24 9 25 27 28 11 isinv ⊢ φ → X G Y ⁡ M F ⁡ X J F ⁡ Y Y G X ⁡ N ↔ X G Y ⁡ M F ⁡ X Sect ⁡ D F ⁡ Y Y G X ⁡ N ∧ Y G X ⁡ N F ⁡ Y Sect ⁡ D F ⁡ X X G Y ⁡ M
30 14 23 29 3bitr4d ⊢ φ → M X I Y N ↔ X G Y ⁡ M F ⁡ X J F ⁡ Y Y G X ⁡ N