Definition df-f1o 5895

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6142, dff1o3 6143, dff1o4 6145, and dff1o5 6146. 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 16741. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 6574, 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 7964. (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 5887	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 5885	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 5886	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 384	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 196	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is referenced by:  f1oeq1  6127  f1oeq2  6128  f1oeq3  6129  nff1o  6135  f1of1  6136  dff1o2  6142  dff1o5  6146  f1oco  6159  fo00  6172  dff1o6  6531  nvof1o  6536  fcof1od  6549  soisoi  6578  f1oweALT  7152  tposf1o2  7378  smoiso2  7466  f1finf1o  8187  unfilem2  8225  fofinf1o  8241  alephiso  8921  cnref1o  11827  wwlktovf1o  13702  1arith  15631  xpsff1o  16228  isffth2  16576  ffthf1o  16579  orbsta  17746  symgextf1o  17843  symgfixf1o  17860  odf1o1  17987  znf1o  19900  cygznlem3  19918  scmatf1o  20338  m2cpmf1o  20562  pm2mpf1o  20620  reeff1o  24201  recosf1o  24281  efif1olem4  24291  dvdsmulf1o  24920  wlkpwwlkf1ouspgr  26765  wlknwwlksnbij  26777  wlkwwlkbij  26784  wwlksnextbij0  26796  clwwlksf1o  26919  clwlksf1oclwwlk  26970  eucrctshift  27103  frgrncvvdeqlem10  27172  numclwlk1lem2f1o  27229  unopf1o  28775  poimirlem26  33435  poimirlem27  33436  wessf1ornlem  39371  projf1o  39386  sumnnodd  39862  dvnprodlem1  40161  fourierdlem54  40377  sprsymrelf1o  41748  uspgrsprf1o  41757