Definition df-f1o 5811

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6055, dff1o3 6056, dff1o4 6058, and dff1o5 6059. 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 16564. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 6474, 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 7850. (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 5803	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 5801	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 5802	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 383	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 195	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is referenced by:  f1oeq1  6040  f1oeq2  6041  f1oeq3  6042  nff1o  6048  f1of1  6049  dff1o2  6055  dff1o5  6059  f1oco  6072  fo00  6084  dff1o6  6431  nvof1o  6436  fcof1od  6449  soisoi  6478  f1oweALT  7043  tposf1o2  7265  smoiso2  7353  f1finf1o  8072  unfilem2  8110  fofinf1o  8126  alephiso  8804  cnref1o  11703  wwlktovf1o  13550  1arith  15469  xpsff1o  16051  isffth2  16399  ffthf1o  16402  orbsta  17569  symgextf1o  17666  symgfixf1o  17683  odf1o1  17810  znf1o  19719  cygznlem3  19737  scmatf1o  20157  m2cpmf1o  20381  pm2mpf1o  20439  reeff1o  24005  recosf1o  24085  efif1olem4  24095  dvdsmulf1o  24720  wlknwwlknbij  26241  wlkiswwlkbij  26248  wwlkextbij0  26260  clwwlkf1o  26326  clwlkf1oclwwlk  26378  eupatrl  26495  frgrancvvdeqlem8  26567  numclwlk1lem2f1o  26623  unopf1o  28159  poimirlem26  32605  poimirlem27  32606  wessf1ornlem  38366  projf1o  38381  sumnnodd  38697  dvnprodlem1  38836  fourierdlem54  39053  1wlkpwwlkf1ouspgr  41076  wlknwwlksnbij  41088  wlkwwlkbij  41095  wwlksnextbij0  41107  clwwlksf1o  41226  clwlksf1oclwwlk  41277  eucrctshift  41411  frgrncvvdeqlem8  41479  av-numclwlk1lem2f1o  41526