Definition df-f1o 6548

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6836, dff1o3 6837, dff1o4 6839, and dff1o5 6840. 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 18038. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7318, 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 8946. (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 6540	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6538	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6539	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 397	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 205	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is referenced by:  f1oeq1  6819  f1oeq2  6820  f1oeq3  6821  nff1o  6829  f1of1  6830  dff1o2  6836  dff1o5  6840  f1oco  6854  fo00  6867  dff1o6  7270  nvof1o  7275  fcof1od  7289  nf1oconst  7300  soisoi  7322  f1oweALT  7956  tposf1o2  8234  smoiso2  8366  f1finf1o  9268  f1finf1oOLD  9269  unfilem2  9308  fofinf1o  9324  alephiso  10090  cnref1o  12966  wwlktovf1o  14907  1arith  16857  xpsff1o  17510  isffth2  17864  ffthf1o  17867  orbsta  19172  symgsubmefmnd  19261  symgextf1o  19286  symgfixf1o  19303  odf1o1  19435  znf1o  21099  cygznlem3  21117  scmatf1o  22026  m2cpmf1o  22251  pm2mpf1o  22309  reeff1o  25951  recosf1o  26036  efif1olem4  26046  dvdsmulf1o  26688  negsf1o  27518  wlkswwlksf1o  29123  wwlksnextbij0  29145  clwlkclwwlkf1o  29254  clwwlkf1o  29294  eucrctshift  29486  frgrncvvdeqlem10  29551  numclwwlk1lem2f1o  29602  unopf1o  31157  2ndresdjuf1o  31863  poimirlem26  36503  poimirlem27  36504  sticksstones4  40954  wessf1ornlem  43868  projf1o  43882  sumnnodd  44333  dvnprodlem1  44649  fourierdlem54  44863  fsetsnf1o  45751  cfsetsnfsetf1o  45758  fcoresf1ob  45770  f1ocof1ob  45776  imasetpreimafvbij  46061  sprsymrelf1o  46153  prproropf1o  46162  isomuspgrlem2e  46487  uspgrsprf1o  46514  rngqiprngim  46770  1arymaptf1o  47284  2arymaptf1o  47295  rrx2xpref1o  47358