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∈BHom⁡CA∧F∈AHom⁡CB→FAInv⁡CBG

Proof

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