Definition df-f1o 5796

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6039, dff1o3 6040, dff1o4 6042, and dff1o5 6043. 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 16512. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 6451, 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 7827. (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 5788	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 5786	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 5787	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 382	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 194	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is referenced by:  f1oeq1  6024  f1oeq2  6025  f1oeq3  6026  nff1o  6032  f1of1  6033  dff1o2  6039  dff1o5  6043  f1oco  6056  fo00  6068  dff1o6  6408  nvof1o  6413  fcof1od  6426  soisoi  6455  f1oweALT  7020  tposf1o2  7242  smoiso2  7330  f1finf1o  8049  unfilem2  8087  fofinf1o  8103  alephiso  8781  cnref1o  11661  wwlktovf1o  13498  1arith  15417  xpsff1o  15999  isffth2  16347  ffthf1o  16350  orbsta  17517  symgextf1o  17614  symgfixf1o  17631  odf1o1  17758  znf1o  19666  cygznlem3  19684  scmatf1o  20104  m2cpmf1o  20328  pm2mpf1o  20386  reeff1o  23949  recosf1o  24029  efif1olem4  24039  dvdsmulf1o  24664  wlknwwlknbij  26034  wlkiswwlkbij  26041  wwlkextbij0  26053  clwwlkf1o  26119  clwlkf1oclwwlk  26171  eupatrl  26288  frgrancvvdeqlem8  26360  numclwlk1lem2f1o  26416  unopf1o  27952  poimirlem26  32388  poimirlem27  32389  wessf1ornlem  38149  projf1o  38164  sumnnodd  38480  dvnprodlem1  38619  fourierdlem54  38836  1wlkpwwlkf1ouspgr  41057  wlknwwlksnbij  41069  wlkwwlkbij  41076  wwlksnextbij0  41088  clwwlksf1o  41207  clwlksf1oclwwlk  41258  eucrctshift  41392  frgrncvvdeqlem8  41460  av-numclwlk1lem2f1o  41507