Definition df-f1o 6362

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6620, dff1o3 6621, dff1o4 6623, and dff1o5 6624. 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 17351. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7077, 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 8518. (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 6354	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6352	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6353	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 398	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 208	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is referenced by:  f1oeq1  6604  f1oeq2  6605  f1oeq3  6606  nff1o  6613  f1of1  6614  dff1o2  6620  dff1o5  6624  f1oco  6637  fo00  6650  dff1o6  7032  nvof1o  7037  fcof1od  7050  nf1oconst  7060  soisoi  7081  f1oweALT  7673  tposf1o2  7918  smoiso2  8006  f1finf1o  8745  unfilem2  8783  fofinf1o  8799  alephiso  9524  cnref1o  12385  wwlktovf1o  14323  1arith  16263  xpsff1o  16840  isffth2  17186  ffthf1o  17189  orbsta  18443  symgsubmefmnd  18526  symgextf1o  18551  symgfixf1o  18568  odf1o1  18697  znf1o  20698  cygznlem3  20716  scmatf1o  21141  m2cpmf1o  21365  pm2mpf1o  21423  reeff1o  25035  recosf1o  25119  efif1olem4  25129  dvdsmulf1o  25771  wlkswwlksf1o  27657  wwlksnextbij0  27679  clwlkclwwlkf1o  27789  clwwlkf1o  27830  eucrctshift  28022  frgrncvvdeqlem10  28087  numclwwlk1lem2f1o  28138  unopf1o  29693  poimirlem26  34933  poimirlem27  34934  wessf1ornlem  41465  projf1o  41479  sumnnodd  41931  dvnprodlem1  42251  fourierdlem54  42465  imasetpreimafvbij  43586  sprsymrelf1o  43680  prproropf1o  43689  isomuspgrlem2e  44017  uspgrsprf1o  44044  rrx2xpref1o  44725