Description: A function is bijective if it has an inverse function. (Contributed by AV, 15-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 2fvcoidd.f | |
|
2fvcoidd.g | |
||
2fvcoidd.i | |
||
2fvidf1od.i | |
||
Assertion | 2fvidf1od | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2fvcoidd.f | |
|
2 | 2fvcoidd.g | |
|
3 | 2fvcoidd.i | |
|
4 | 2fvidf1od.i | |
|
5 | 1 2 3 | 2fvcoidd | |
6 | 2 1 4 | 2fvcoidd | |
7 | 1 2 5 6 | fcof1od | |