![]() |
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 6488, dff1o3 6489, dff1o4 6491, and dff1o5 6492. 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 17180. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 6940, 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 8366. (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 6224 | . 2 wff 𝐹:𝐴–1-1-onto→𝐵 |
5 | 1, 2, 3 | wf1 6222 | . . 3 wff 𝐹:𝐴–1-1→𝐵 |
6 | 1, 2, 3 | wfo 6223 | . . 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 6472 f1oeq2 6473 f1oeq3 6474 nff1o 6481 f1of1 6482 dff1o2 6488 dff1o5 6492 f1oco 6505 fo00 6518 dff1o6 6897 nvof1o 6902 fcof1od 6915 soisoi 6944 f1oweALT 7529 tposf1o2 7769 smoiso2 7858 f1finf1o 8591 unfilem2 8629 fofinf1o 8645 alephiso 9370 cnref1o 12234 wwlktovf1o 14157 1arith 16092 xpsff1o 16669 isffth2 17015 ffthf1o 17018 orbsta 18184 symgextf1o 18282 symgfixf1o 18299 odf1o1 18427 znf1o 20380 cygznlem3 20398 scmatf1o 20825 m2cpmf1o 21049 pm2mpf1o 21107 reeff1o 24718 recosf1o 24800 efif1olem4 24810 dvdsmulf1o 25453 wlkswwlksf1o 27344 wwlksnextbij0 27366 clwlkclwwlkf1o 27476 clwwlkf1o 27517 eucrctshift 27710 frgrncvvdeqlem10 27779 numclwwlk1lem2f1o 27830 unopf1o 29384 poimirlem26 34449 poimirlem27 34450 wessf1ornlem 40985 projf1o 40999 sumnnodd 41453 dvnprodlem1 41772 fourierdlem54 41987 sprsymrelf1o 43142 prproropf1o 43151 isomuspgrlem2e 43479 uspgrsprf1o 43506 rrx2xpref1o 44186 |
Copyright terms: Public domain | W3C validator |