Metamath Proof Explorer


Theorem dff1o2

Description: Alternate definition of one-to-one onto function. (Contributed by NM, 10-Feb-1997) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Assertion dff1o2 F:A1-1 ontoBFFnAFunF-1ranF=B

Proof

Step Hyp Ref Expression
1 df-f1o F:A1-1 ontoBF:A1-1BF:AontoB
2 df-f1 F:A1-1BF:ABFunF-1
3 df-fo F:AontoBFFnAranF=B
4 2 3 anbi12i F:A1-1BF:AontoBF:ABFunF-1FFnAranF=B
5 anass F:ABFunF-1FFnAranF=BF:ABFunF-1FFnAranF=B
6 3anan12 FFnAFunF-1ranF=BFunF-1FFnAranF=B
7 6 anbi1i FFnAFunF-1ranF=BF:ABFunF-1FFnAranF=BF:AB
8 eqimss ranF=BranFB
9 df-f F:ABFFnAranFB
10 9 biimpri FFnAranFBF:AB
11 8 10 sylan2 FFnAranF=BF:AB
12 11 3adant2 FFnAFunF-1ranF=BF:AB
13 12 pm4.71i FFnAFunF-1ranF=BFFnAFunF-1ranF=BF:AB
14 ancom F:ABFunF-1FFnAranF=BFunF-1FFnAranF=BF:AB
15 7 13 14 3bitr4ri F:ABFunF-1FFnAranF=BFFnAFunF-1ranF=B
16 5 15 bitri F:ABFunF-1FFnAranF=BFFnAFunF-1ranF=B
17 4 16 bitri F:A1-1BF:AontoBFFnAFunF-1ranF=B
18 1 17 bitri F:A1-1 ontoBFFnAFunF-1ranF=B