![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-f1o | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-f1o | ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)) |
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→𝐵)) |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |