Definition df-f1o 5933

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6180, dff1o3 6181, dff1o4 6183, and dff1o5 6184. 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 16788. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 6614, 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 8006. (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 5925	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 5923	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 5924	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 383	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 196	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is referenced by:  f1oeq1  6165  f1oeq2  6166  f1oeq3  6167  nff1o  6173  f1of1  6174  dff1o2  6180  dff1o5  6184  f1oco  6197  fo00  6210  dff1o6  6571  nvof1o  6576  fcof1od  6589  soisoi  6618  f1oweALT  7194  tposf1o2  7423  smoiso2  7511  f1finf1o  8228  unfilem2  8266  fofinf1o  8282  alephiso  8959  cnref1o  11865  wwlktovf1o  13748  1arith  15678  xpsff1o  16275  isffth2  16623  ffthf1o  16626  orbsta  17792  symgextf1o  17889  symgfixf1o  17906  odf1o1  18033  znf1o  19948  cygznlem3  19966  scmatf1o  20386  m2cpmf1o  20610  pm2mpf1o  20668  reeff1o  24246  recosf1o  24326  efif1olem4  24336  dvdsmulf1o  24965  wlkpwwlkf1ouspgr  26833  wlknwwlksnbij  26845  wlkwwlkbij  26852  wwlksnextbij0  26864  clwwlkf1o  27014  clwlksf1oclwwlk  27057  eucrctshift  27221  frgrncvvdeqlem10  27288  numclwlk1lem2f1o  27349  unopf1o  28903  poimirlem26  33565  poimirlem27  33566  wessf1ornlem  39685  projf1o  39700  sumnnodd  40180  dvnprodlem1  40479  fourierdlem54  40695  sprsymrelf1o  42073  uspgrsprf1o  42082