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 | |
|
invfval.n | |
||
invfval.c | |
||
invfval.x | |
||
invfval.y | |
||
Assertion | invfun | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | invfval.b | |
|
2 | invfval.n | |
|
3 | invfval.c | |
|
4 | invfval.x | |
|
5 | invfval.y | |
|
6 | eqid | |
|
7 | 1 2 3 4 5 6 | invss | |
8 | relxp | |
|
9 | relss | |
|
10 | 7 8 9 | mpisyl | |
11 | eqid | |
|
12 | 3 | adantr | |
13 | 5 | adantr | |
14 | 4 | adantr | |
15 | 1 2 3 4 5 11 | isinv | |
16 | 15 | simplbda | |
17 | 16 | adantrr | |
18 | 1 2 3 4 5 11 | isinv | |
19 | 18 | simprbda | |
20 | 19 | adantrl | |
21 | 1 11 12 13 14 17 20 | sectcan | |
22 | 21 | ex | |
23 | 22 | alrimiv | |
24 | 23 | alrimivv | |
25 | dffun2 | |
|
26 | 10 24 25 | sylanbrc | |