Definition df-f1

Description: Define a one-to-one function. For equivalent definitions see dff12 and dff13 . Compare Definition 6.15(5) of TakeutiZaring p. 27. We use their notation ("1-1" above the arrow).

A one-to-one function is also called an "injection" or an "injective function", F : A -1-1-> B can be read as " F is an injection from A into B ". Injections are precisely the monomorphisms in the category SetCat of sets and set functions, see setcmon . (Contributed by NM, 1-Aug-1994)

	Ref	Expression
Assertion	df-f1	$$⊢F:A\underset{1-1}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \mathrm{Fun}{F}^{-1}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	$$classF$$
1		cA	$$classA$$
2		cB	$$classB$$
3	1 2 0	wf1	$$wffF:A\underset{1-1}{⟶}B$$
4	1 2 0	wf	$$wffF:A⟶B$$
5	0	ccnv	$$class{F}^{-1}$$
6	5	wfun	$$wff\mathrm{Fun}{F}^{-1}$$
7	4 6	wa	$$wff\left(F:A⟶B\wedge \mathrm{Fun}{F}^{-1}\right)$$
8	3 7	wb	$$wff\left(F:A\underset{1-1}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \mathrm{Fun}{F}^{-1}\right)\right)$$