Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-f1o | Structured version Visualization version Unicode version |
Description: Define a one-to-one onto
function. For equivalent definitions see
dff1o2 6142, dff1o3 6143, dff1o4 6145, and dff1o5 6146. 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", can be read as " is a bijection between and ". Bijections are precisely the isomorphisms in the category of sets and set functions, see setciso 16741. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 6574, two sets are isomorphic iff there is an isomorphism regarding the identity relation. In this case, the two sets are also "equinumerous", see bren 7964. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-f1o |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | cF | . . 3 | |
4 | 1, 2, 3 | wf1o 5887 | . 2 |
5 | 1, 2, 3 | wf1 5885 | . . 3 |
6 | 1, 2, 3 | wfo 5886 | . . 3 |
7 | 5, 6 | wa 384 | . 2 |
8 | 4, 7 | wb 196 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: f1oeq1 6127 f1oeq2 6128 f1oeq3 6129 nff1o 6135 f1of1 6136 dff1o2 6142 dff1o5 6146 f1oco 6159 fo00 6172 dff1o6 6531 nvof1o 6536 fcof1od 6549 soisoi 6578 f1oweALT 7152 tposf1o2 7378 smoiso2 7466 f1finf1o 8187 unfilem2 8225 fofinf1o 8241 alephiso 8921 cnref1o 11827 wwlktovf1o 13702 1arith 15631 xpsff1o 16228 isffth2 16576 ffthf1o 16579 orbsta 17746 symgextf1o 17843 symgfixf1o 17860 odf1o1 17987 znf1o 19900 cygznlem3 19918 scmatf1o 20338 m2cpmf1o 20562 pm2mpf1o 20620 reeff1o 24201 recosf1o 24281 efif1olem4 24291 dvdsmulf1o 24920 wlkpwwlkf1ouspgr 26765 wlknwwlksnbij 26777 wlkwwlkbij 26784 wwlksnextbij0 26796 clwwlksf1o 26919 clwlksf1oclwwlk 26970 eucrctshift 27103 frgrncvvdeqlem10 27172 numclwlk1lem2f1o 27229 unopf1o 28775 poimirlem26 33435 poimirlem27 33436 wessf1ornlem 39371 projf1o 39386 sumnnodd 39862 dvnprodlem1 40161 fourierdlem54 40377 sprsymrelf1o 41748 uspgrsprf1o 41757 |
Copyright terms: Public domain | W3C validator |