Metamath Proof Explorer

Theorem invfun

Description: The inverse relation is a function, which is to say that every morphism has at most one inverse. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses invfval.b ⊢ B = Base C
invfval.n ⊢ N = Inv ⁡ C
invfval.c ⊢ φ → C ∈ Cat
invss.x ⊢ φ → X ∈ B
invss.y ⊢ φ → Y ∈ B
Assertion invfun ⊢ φ → Fun ⁡ X N Y

Proof

Step Hyp Ref Expression
1 invfval.b ⊢ B = Base C
2 invfval.n ⊢ N = Inv ⁡ C
3 invfval.c ⊢ φ → C ∈ Cat
4 invss.x ⊢ φ → X ∈ B
5 invss.y ⊢ φ → Y ∈ B
6 eqid ⊢ Hom ⁡ C = Hom ⁡ C
7 1 2 3 4 5 6 invss ⊢ φ → X N Y ⊆ X Hom ⁡ C Y × Y Hom ⁡ C X
8 relxp ⊢ Rel ⁡ X Hom ⁡ C Y × Y Hom ⁡ C X
9 relss ⊢ X N Y ⊆ X Hom ⁡ C Y × Y Hom ⁡ C X → Rel ⁡ X Hom ⁡ C Y × Y Hom ⁡ C X → Rel ⁡ X N Y
10 7 8 9 mpisyl ⊢ φ → Rel ⁡ X N Y
11 eqid ⊢ Sect ⁡ C = Sect ⁡ C
12 3 adantr ⊢ φ ∧ f X N Y g ∧ f X N Y h → C ∈ Cat
13 5 adantr ⊢ φ ∧ f X N Y g ∧ f X N Y h → Y ∈ B
14 4 adantr ⊢ φ ∧ f X N Y g ∧ f X N Y h → X ∈ B
15 1 2 3 4 5 11 isinv ⊢ φ → f X N Y g ↔ f X Sect ⁡ C Y g ∧ g Y Sect ⁡ C X f
16 15 simplbda ⊢ φ ∧ f X N Y g → g Y Sect ⁡ C X f
17 16 adantrr ⊢ φ ∧ f X N Y g ∧ f X N Y h → g Y Sect ⁡ C X f
18 1 2 3 4 5 11 isinv ⊢ φ → f X N Y h ↔ f X Sect ⁡ C Y h ∧ h Y Sect ⁡ C X f
19 18 simprbda ⊢ φ ∧ f X N Y h → f X Sect ⁡ C Y h
20 19 adantrl ⊢ φ ∧ f X N Y g ∧ f X N Y h → f X Sect ⁡ C Y h
21 1 11 12 13 14 17 20 sectcan ⊢ φ ∧ f X N Y g ∧ f X N Y h → g = h
22 21 ex ⊢ φ → f X N Y g ∧ f X N Y h → g = h
23 22 alrimiv ⊢ φ → ∀ h f X N Y g ∧ f X N Y h → g = h
24 23 alrimivv ⊢ φ → ∀ f ∀ g ∀ h f X N Y g ∧ f X N Y h → g = h
25 dffun2 ⊢ Fun ⁡ X N Y ↔ Rel ⁡ X N Y ∧ ∀ f ∀ g ∀ h f X N Y g ∧ f X N Y h → g = h
26 10 24 25 sylanbrc ⊢ φ → Fun ⁡ X N Y