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 ) )