Metamath Proof Explorer

Theorem 2initoinv

Description: Morphisms between two initial objects are inverses. (Contributed by AV, 14-Apr-2020)

Ref Expression
Hypotheses initoeu1.c ⊢ φ → C ∈ Cat
initoeu1.a ⊢ φ → A ∈ InitO ⁡ C
initoeu1.b ⊢ φ → B ∈ InitO ⁡ C
Assertion 2initoinv ⊢ φ ∧ G ∈ B Hom ⁡ C A ∧ F ∈ A Hom ⁡ C B → F A Inv ⁡ C B G

Proof

Step Hyp Ref Expression
1 initoeu1.c ⊢ φ → C ∈ Cat
2 initoeu1.a ⊢ φ → A ∈ InitO ⁡ C
3 initoeu1.b ⊢ φ → B ∈ InitO ⁡ C
4 eqid ⊢ Base C = Base C
5 eqid ⊢ Hom ⁡ C = Hom ⁡ C
6 eqid ⊢ comp ⁡ C = comp ⁡ C
7 1 3ad2ant1 ⊢ φ ∧ G ∈ B Hom ⁡ C A ∧ F ∈ A Hom ⁡ C B → C ∈ Cat
8 initoo ⊢ C ∈ Cat → A ∈ InitO ⁡ C → A ∈ Base C
9 1 2 8 sylc ⊢ φ → A ∈ Base C
10 9 3ad2ant1 ⊢ φ ∧ G ∈ B Hom ⁡ C A ∧ F ∈ A Hom ⁡ C B → A ∈ Base C
11 initoo ⊢ C ∈ Cat → B ∈ InitO ⁡ C → B ∈ Base C
12 1 3 11 sylc ⊢ φ → B ∈ Base C
13 12 3ad2ant1 ⊢ φ ∧ G ∈ B Hom ⁡ C A ∧ F ∈ A Hom ⁡ C B → B ∈ Base C
14 simp3 ⊢ φ ∧ G ∈ B Hom ⁡ C A ∧ F ∈ A Hom ⁡ C B → F ∈ A Hom ⁡ C B
15 simp2 ⊢ φ ∧ G ∈ B Hom ⁡ C A ∧ F ∈ A Hom ⁡ C B → G ∈ B Hom ⁡ C A
16 4 5 6 7 10 13 10 14 15 catcocl ⊢ φ ∧ G ∈ B Hom ⁡ C A ∧ F ∈ A Hom ⁡ C B → G A B comp ⁡ C A F ∈ A Hom ⁡ C A
17 4 5 1 initoid ⊢ φ ∧ A ∈ InitO ⁡ C → A Hom ⁡ C A = Id ⁡ C ⁡ A
18 2 17 mpdan ⊢ φ → A Hom ⁡ C A = Id ⁡ C ⁡ A
19 18 3ad2ant1 ⊢ φ ∧ G ∈ B Hom ⁡ C A ∧ F ∈ A Hom ⁡ C B → A Hom ⁡ C A = Id ⁡ C ⁡ A
20 19 eleq2d ⊢ φ ∧ G ∈ B Hom ⁡ C A ∧ F ∈ A Hom ⁡ C B → G A B comp ⁡ C A F ∈ A Hom ⁡ C A ↔ G A B comp ⁡ C A F ∈ Id ⁡ C ⁡ A
21 elsni ⊢ G A B comp ⁡ C A F ∈ Id ⁡ C ⁡ A → G A B comp ⁡ C A F = Id ⁡ C ⁡ A
22 20 21 syl6bi ⊢ φ ∧ G ∈ B Hom ⁡ C A ∧ F ∈ A Hom ⁡ C B → G A B comp ⁡ C A F ∈ A Hom ⁡ C A → G A B comp ⁡ C A F = Id ⁡ C ⁡ A
23 16 22 mpd ⊢ φ ∧ G ∈ B Hom ⁡ C A ∧ F ∈ A Hom ⁡ C B → G A B comp ⁡ C A F = Id ⁡ C ⁡ A
24 eqid ⊢ Id ⁡ C = Id ⁡ C
25 eqid ⊢ Sect ⁡ C = Sect ⁡ C
26 4 5 6 24 25 7 10 13 14 15 issect2 ⊢ φ ∧ G ∈ B Hom ⁡ C A ∧ F ∈ A Hom ⁡ C B → F A Sect ⁡ C B G ↔ G A B comp ⁡ C A F = Id ⁡ C ⁡ A
27 23 26 mpbird ⊢ φ ∧ G ∈ B Hom ⁡ C A ∧ F ∈ A Hom ⁡ C B → F A Sect ⁡ C B G
28 4 5 6 7 13 10 13 15 14 catcocl ⊢ φ ∧ G ∈ B Hom ⁡ C A ∧ F ∈ A Hom ⁡ C B → F B A comp ⁡ C B G ∈ B Hom ⁡ C B
29 4 5 1 initoid ⊢ φ ∧ B ∈ InitO ⁡ C → B Hom ⁡ C B = Id ⁡ C ⁡ B
30 3 29 mpdan ⊢ φ → B Hom ⁡ C B = Id ⁡ C ⁡ B
31 30 3ad2ant1 ⊢ φ ∧ G ∈ B Hom ⁡ C A ∧ F ∈ A Hom ⁡ C B → B Hom ⁡ C B = Id ⁡ C ⁡ B
32 31 eleq2d ⊢ φ ∧ G ∈ B Hom ⁡ C A ∧ F ∈ A Hom ⁡ C B → F B A comp ⁡ C B G ∈ B Hom ⁡ C B ↔ F B A comp ⁡ C B G ∈ Id ⁡ C ⁡ B
33 elsni ⊢ F B A comp ⁡ C B G ∈ Id ⁡ C ⁡ B → F B A comp ⁡ C B G = Id ⁡ C ⁡ B
34 32 33 syl6bi ⊢ φ ∧ G ∈ B Hom ⁡ C A ∧ F ∈ A Hom ⁡ C B → F B A comp ⁡ C B G ∈ B Hom ⁡ C B → F B A comp ⁡ C B G = Id ⁡ C ⁡ B
35 28 34 mpd ⊢ φ ∧ G ∈ B Hom ⁡ C A ∧ F ∈ A Hom ⁡ C B → F B A comp ⁡ C B G = Id ⁡ C ⁡ B
36 4 5 6 24 25 7 13 10 15 14 issect2 ⊢ φ ∧ G ∈ B Hom ⁡ C A ∧ F ∈ A Hom ⁡ C B → G B Sect ⁡ C A F ↔ F B A comp ⁡ C B G = Id ⁡ C ⁡ B
37 35 36 mpbird ⊢ φ ∧ G ∈ B Hom ⁡ C A ∧ F ∈ A Hom ⁡ C B → G B Sect ⁡ C A F
38 eqid ⊢ Inv ⁡ C = Inv ⁡ C
39 4 38 1 9 12 25 isinv ⊢ φ → F A Inv ⁡ C B G ↔ F A Sect ⁡ C B G ∧ G B Sect ⁡ C A F
40 39 3ad2ant1 ⊢ φ ∧ G ∈ B Hom ⁡ C A ∧ F ∈ A Hom ⁡ C B → F A Inv ⁡ C B G ↔ F A Sect ⁡ C B G ∧ G B Sect ⁡ C A F
41 27 37 40 mpbir2and ⊢ φ ∧ G ∈ B Hom ⁡ C A ∧ F ∈ A Hom ⁡ C B → F A Inv ⁡ C B G