Metamath Proof Explorer


Theorem 2fvidf1od

Description: A function is bijective if it has an inverse function. (Contributed by AV, 15-Dec-2019)

Ref Expression
Hypotheses 2fvcoidd.f φF:AB
2fvcoidd.g φG:BA
2fvcoidd.i φaAGFa=a
2fvidf1od.i φbBFGb=b
Assertion 2fvidf1od φF:A1-1 ontoB

Proof

Step Hyp Ref Expression
1 2fvcoidd.f φF:AB
2 2fvcoidd.g φG:BA
3 2fvcoidd.i φaAGFa=a
4 2fvidf1od.i φbBFGb=b
5 1 2 3 2fvcoidd φGF=IA
6 2 1 4 2fvcoidd φFG=IB
7 1 2 5 6 fcof1od φF:A1-1 ontoB