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=BaseC
invfval.n N=InvC
invfval.c φCCat
invfval.x φXB
invfval.y φYB
Assertion invfun φFunXNY

Proof

Step Hyp Ref Expression
1 invfval.b B=BaseC
2 invfval.n N=InvC
3 invfval.c φCCat
4 invfval.x φXB
5 invfval.y φYB
6 eqid HomC=HomC
7 1 2 3 4 5 6 invss φXNYXHomCY×YHomCX
8 relxp RelXHomCY×YHomCX
9 relss XNYXHomCY×YHomCXRelXHomCY×YHomCXRelXNY
10 7 8 9 mpisyl φRelXNY
11 eqid SectC=SectC
12 3 adantr φfXNYgfXNYhCCat
13 5 adantr φfXNYgfXNYhYB
14 4 adantr φfXNYgfXNYhXB
15 1 2 3 4 5 11 isinv φfXNYgfXSectCYggYSectCXf
16 15 simplbda φfXNYggYSectCXf
17 16 adantrr φfXNYgfXNYhgYSectCXf
18 1 2 3 4 5 11 isinv φfXNYhfXSectCYhhYSectCXf
19 18 simprbda φfXNYhfXSectCYh
20 19 adantrl φfXNYgfXNYhfXSectCYh
21 1 11 12 13 14 17 20 sectcan φfXNYgfXNYhg=h
22 21 ex φfXNYgfXNYhg=h
23 22 alrimiv φhfXNYgfXNYhg=h
24 23 alrimivv φfghfXNYgfXNYhg=h
25 dffun2 FunXNYRelXNYfghfXNYgfXNYhg=h
26 10 24 25 sylanbrc φFunXNY