Definition df-f1o 6556

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6843, dff1o3 6844, dff1o4 6846, and dff1o5 6847. 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 18083. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7331, 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 8974. (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 6548	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6546	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6547	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 394	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 205	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is referenced by:  f1oeq1  6826  f1oeq2  6827  f1oeq3  6828  nff1o  6836  f1of1  6837  dff1o2  6843  dff1o5  6847  f1oco  6861  fo00  6874  dff1o6  7284  nvof1o  7289  fcof1od  7303  nf1oconst  7313  soisoi  7335  f1oweALT  7977  tposf1o2  8258  smoiso2  8390  f1finf1o  9296  f1finf1oOLD  9297  unfilem2  9336  fofinf1o  9353  alephiso  10123  cnref1o  13002  wwlktovf1o  14946  1arith  16899  xpsff1o  17552  isffth2  17908  ffthf1o  17911  orbsta  19276  symgsubmefmnd  19365  symgextf1o  19390  symgfixf1o  19407  odf1o1  19539  rngqiprngim  21211  znf1o  21502  cygznlem3  21520  scmatf1o  22478  m2cpmf1o  22703  pm2mpf1o  22761  reeff1o  26429  recosf1o  26514  efif1olem4  26524  mpodvdsmulf1o  27171  dvdsmulf1o  27173  negsf1o  28012  om2noseqf1o  28224  wlkswwlksf1o  29762  wwlksnextbij0  29784  clwlkclwwlkf1o  29893  clwwlkf1o  29933  eucrctshift  30125  frgrncvvdeqlem10  30190  numclwwlk1lem2f1o  30241  unopf1o  31798  2ndresdjuf1o  32517  zringfrac  33369  poimirlem26  37250  poimirlem27  37251  sticksstones4  41752  wessf1ornlem  44697  projf1o  44709  sumnnodd  45156  dvnprodlem1  45472  fourierdlem54  45686  fsetsnf1o  46574  cfsetsnfsetf1o  46581  fcoresf1ob  46593  f1ocof1ob  46599  imasetpreimafvbij  46883  sprsymrelf1o  46975  prproropf1o  46984  uspgrsprf1o  47397  1arymaptf1o  47903  2arymaptf1o  47914  rrx2xpref1o  47977