Definition df-f1o 6425

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6705, dff1o3 6706, dff1o4 6708, and dff1o5 6709. 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", 𝐹:𝐴–1-1-onto→𝐵 can be read as "𝐹 is a bijection between 𝐴 and 𝐵". Bijections are precisely the isomorphisms in the category SetCat of sets and set functions, see setciso 17722. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7175, 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 8701. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-f1o	⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

Detailed syntax breakdown of Definition df-f1o

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cF	. . 3 class 𝐹
4	1, 2, 3	wf1o 6417	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6415	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6416	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 395	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 205	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is referenced by:  f1oeq1  6688  f1oeq2  6689  f1oeq3  6690  nff1o  6698  f1of1  6699  dff1o2  6705  dff1o5  6709  f1oco  6722  fo00  6735  dff1o6  7128  nvof1o  7133  fcof1od  7146  nf1oconst  7157  soisoi  7179  f1oweALT  7788  tposf1o2  8039  smoiso2  8171  f1finf1o  8975  unfilem2  9009  fofinf1o  9024  alephiso  9785  cnref1o  12654  wwlktovf1o  14602  1arith  16556  xpsff1o  17195  isffth2  17548  ffthf1o  17551  orbsta  18834  symgsubmefmnd  18921  symgextf1o  18946  symgfixf1o  18963  odf1o1  19092  znf1o  20671  cygznlem3  20689  scmatf1o  21589  m2cpmf1o  21814  pm2mpf1o  21872  reeff1o  25511  recosf1o  25596  efif1olem4  25606  dvdsmulf1o  26248  wlkswwlksf1o  28145  wwlksnextbij0  28167  clwlkclwwlkf1o  28276  clwwlkf1o  28316  eucrctshift  28508  frgrncvvdeqlem10  28573  numclwwlk1lem2f1o  28624  unopf1o  30179  2ndresdjuf1o  30888  poimirlem26  35730  poimirlem27  35731  sticksstones4  40033  wessf1ornlem  42611  projf1o  42625  sumnnodd  43061  dvnprodlem1  43377  fourierdlem54  43591  fsetsnf1o  44435  cfsetsnfsetf1o  44442  fcoresf1ob  44454  f1ocof1ob  44460  imasetpreimafvbij  44746  sprsymrelf1o  44838  prproropf1o  44847  isomuspgrlem2e  45172  uspgrsprf1o  45199  1arymaptf1o  45878  2arymaptf1o  45889  rrx2xpref1o  45952