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 6614, dff1o3 6615, dff1o4 6617, and dff1o5 6618. 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 17341. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7066, 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 8507. (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 6348 | . 2 wff 𝐹:𝐴–1-1-onto→𝐵 |
5 | 1, 2, 3 | wf1 6346 | . . 3 wff 𝐹:𝐴–1-1→𝐵 |
6 | 1, 2, 3 | wfo 6347 | . . 3 wff 𝐹:𝐴–onto→𝐵 |
7 | 5, 6 | wa 396 | . 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) |
8 | 4, 7 | wb 207 | 1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: f1oeq1 6598 f1oeq2 6599 f1oeq3 6600 nff1o 6607 f1of1 6608 dff1o2 6614 dff1o5 6618 f1oco 6631 fo00 6644 dff1o6 7023 nvof1o 7028 fcof1od 7041 soisoi 7070 f1oweALT 7664 tposf1o2 7909 smoiso2 7997 f1finf1o 8734 unfilem2 8772 fofinf1o 8788 alephiso 9513 cnref1o 12374 wwlktovf1o 14313 1arith 16253 xpsff1o 16830 isffth2 17176 ffthf1o 17179 orbsta 18383 symgextf1o 18482 symgfixf1o 18499 odf1o1 18628 znf1o 20628 cygznlem3 20646 scmatf1o 21071 m2cpmf1o 21295 pm2mpf1o 21353 reeff1o 24964 recosf1o 25046 efif1olem4 25056 dvdsmulf1o 25699 wlkswwlksf1o 27585 wwlksnextbij0 27607 clwlkclwwlkf1o 27717 clwwlkf1o 27758 eucrctshift 27950 frgrncvvdeqlem10 28015 numclwwlk1lem2f1o 28066 unopf1o 29621 poimirlem26 34800 poimirlem27 34801 wessf1ornlem 41325 projf1o 41339 sumnnodd 41791 dvnprodlem1 42111 fourierdlem54 42326 sprsymrelf1o 43507 prproropf1o 43516 isomuspgrlem2e 43844 uspgrsprf1o 43871 symgsubmefmnd 43965 rrx2xpref1o 44603 |
Copyright terms: Public domain | W3C validator |