| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-fo | Structured version Visualization version GIF version | ||
| Description: Define an onto function.
Definition 6.15(4) of [TakeutiZaring] p.
27.
We use their notation ("onto" under the arrow). For alternate
definitions, see dffo2 6824, dffo3 7122, dffo4 7123, and dffo5 7124.
An onto function is also called a "surjection" or a "surjective function", 𝐹:𝐴–onto→𝐵 can be read as "𝐹 is a surjection from 𝐴 onto 𝐵". Surjections are precisely the epimorphisms in the category SetCat of sets and set functions, see setcepi 18133. (Contributed by NM, 1-Aug-1994.) |
| Ref | Expression |
|---|---|
| df-fo | ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA | . . 3 class 𝐴 | |
| 2 | cB | . . 3 class 𝐵 | |
| 3 | cF | . . 3 class 𝐹 | |
| 4 | 1, 2, 3 | wfo 6559 | . 2 wff 𝐹:𝐴–onto→𝐵 |
| 5 | 3, 1 | wfn 6556 | . . 3 wff 𝐹 Fn 𝐴 |
| 6 | 3 | crn 5686 | . . . 4 class ran 𝐹 |
| 7 | 6, 2 | wceq 1540 | . . 3 wff ran 𝐹 = 𝐵 |
| 8 | 5, 7 | wa 395 | . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) |
| 9 | 4, 8 | wb 206 | 1 wff (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) |
| Colors of variables: wff setvar class |
| This definition is referenced by: foeq1 6816 foeq2 6817 foeq3 6818 nffo 6819 fof 6820 forn 6823 dffo2 6824 dffn4 6826 fores 6830 dff1o2 6853 dff1o3 6854 foimacnv 6865 foun 6866 rescnvimafod 7093 fconst5 7226 dff1o6 7295 nvof1o 7300 f1oweALT 7997 fo1st 8034 fo2nd 8035 tposfo2 8274 fodomr 9168 f1finf1o 9305 f1finf1oOLD 9306 unfilem2 9344 fodomfir 9368 brwdom2 9613 harwdom 9631 infpwfien 10102 alephiso 10138 brdom3 10568 brdom5 10569 brdom4 10570 iunfo 10579 qnnen 16249 isfull2 17958 smndex2dnrinv 18928 odf1o2 19591 cygctb 19910 qtopss 23723 qtopomap 23726 qtopcmap 23727 reeff1o 26491 efifo 26589 bdayfo 27722 om2noseqfo 28304 pjfoi 31722 lvecendof1f1o 33684 fobigcup 35901 tfsconcatfo 43356 modelaxreplem1 44995 fundcmpsurinjlem2 47386 fargshiftfo 47429 |
| Copyright terms: Public domain | W3C validator |