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\underset{1-1\; onto}{⟶}B\leftrightarrow \left(F:A\underset{1-1}{⟶}B\wedge F:A\underset{onto}{⟶}B\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	$$classF$$
1		cA	$$classA$$
2		cB	$$classB$$
3	1 2 0	wf1o	$$wffF:A\underset{1-1\; onto}{⟶}B$$
4	1 2 0	wf1	$$wffF:A\underset{1-1}{⟶}B$$
5	1 2 0	wfo	$$wffF:A\underset{onto}{⟶}B$$
6	4 5	wa	$$wff\left(F:A\underset{1-1}{⟶}B\wedge F:A\underset{onto}{⟶}B\right)$$
7	3 6	wb	$$wff\left(F:A\underset{1-1\; onto}{⟶}B\leftrightarrow \left(F:A\underset{1-1}{⟶}B\wedge F:A\underset{onto}{⟶}B\right)\right)$$