Metamath Proof Explorer

Theorem inveq

Description: If there are two inverses of a morphism, these inverses are equal. Corollary 3.11 of Adamek p. 28. (Contributed by AV, 10-Apr-2020) (Revised by AV, 3-Jul-2022)

Ref Expression
Hypotheses inveq.b ⊢ B = Base C
inveq.n ⊢ N = Inv ⁡ C
inveq.c ⊢ φ → C ∈ Cat
inveq.x ⊢ φ → X ∈ B
inveq.y ⊢ φ → Y ∈ B
Assertion inveq ⊢ φ → F X N Y G ∧ F X N Y K → G = K

Proof

Step Hyp Ref Expression
1 inveq.b ⊢ B = Base C
2 inveq.n ⊢ N = Inv ⁡ C
3 inveq.c ⊢ φ → C ∈ Cat
4 inveq.x ⊢ φ → X ∈ B
5 inveq.y ⊢ φ → Y ∈ B
6 eqid ⊢ Sect ⁡ C = Sect ⁡ C
7 3 adantr ⊢ φ ∧ F X N Y G ∧ F X N Y K → C ∈ Cat
8 5 adantr ⊢ φ ∧ F X N Y G ∧ F X N Y K → Y ∈ B
9 4 adantr ⊢ φ ∧ F X N Y G ∧ F X N Y K → X ∈ B
10 1 2 3 4 5 6 isinv ⊢ φ → F X N Y G ↔ F X Sect ⁡ C Y G ∧ G Y Sect ⁡ C X F
11 simpr ⊢ F X Sect ⁡ C Y G ∧ G Y Sect ⁡ C X F → G Y Sect ⁡ C X F
12 10 11 syl6bi ⊢ φ → F X N Y G → G Y Sect ⁡ C X F
13 12 com12 ⊢ F X N Y G → φ → G Y Sect ⁡ C X F
14 13 adantr ⊢ F X N Y G ∧ F X N Y K → φ → G Y Sect ⁡ C X F
15 14 impcom ⊢ φ ∧ F X N Y G ∧ F X N Y K → G Y Sect ⁡ C X F
16 1 2 3 4 5 6 isinv ⊢ φ → F X N Y K ↔ F X Sect ⁡ C Y K ∧ K Y Sect ⁡ C X F
17 simpl ⊢ F X Sect ⁡ C Y K ∧ K Y Sect ⁡ C X F → F X Sect ⁡ C Y K
18 16 17 syl6bi ⊢ φ → F X N Y K → F X Sect ⁡ C Y K
19 18 adantld ⊢ φ → F X N Y G ∧ F X N Y K → F X Sect ⁡ C Y K
20 19 imp ⊢ φ ∧ F X N Y G ∧ F X N Y K → F X Sect ⁡ C Y K
21 1 6 7 8 9 15 20 sectcan ⊢ φ ∧ F X N Y G ∧ F X N Y K → G = K
22 21 ex ⊢ φ → F X N Y G ∧ F X N Y K → G = K