Metamath Proof Explorer


Definition df-f1o

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 , dff1o3 , dff1o4 , and dff1o5 . Compare Definition 6.15(6) of TakeutiZaring p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow).

A one-to-one onto function is also called a "bijection" or a "bijective function", F : A -1-1-onto-> B can be read as " F is a bijection between A and B ". Bijections are precisely the isomorphisms in the category SetCat of sets and set functions, see setciso . Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb , two sets are isomorphic iff there is an isomorphism Isom regarding the identity relation. In this case, the two sets are also "equinumerous", see bren . (Contributed by NM, 1-Aug-1994)

Ref Expression
Assertion df-f1o
|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cF
 |-  F
1 cA
 |-  A
2 cB
 |-  B
3 1 2 0 wf1o
 |-  F : A -1-1-onto-> B
4 1 2 0 wf1
 |-  F : A -1-1-> B
5 1 2 0 wfo
 |-  F : A -onto-> B
6 4 5 wa
 |-  ( F : A -1-1-> B /\ F : A -onto-> B )
7 3 6 wb
 |-  ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )