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 6032, dffo3 6282, dffo4 6283, and dffo5 6284.
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 16561. (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 5802 | . 2 wff 𝐹:𝐴–onto→𝐵 |
5 | 3, 1 | wfn 5799 | . . 3 wff 𝐹 Fn 𝐴 |
6 | 3 | crn 5039 | . . . 4 class ran 𝐹 |
7 | 6, 2 | wceq 1475 | . . 3 wff ran 𝐹 = 𝐵 |
8 | 5, 7 | wa 383 | . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) |
9 | 4, 8 | wb 195 | 1 wff (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: foeq1 6024 foeq2 6025 foeq3 6026 nffo 6027 fof 6028 forn 6031 dffo2 6032 dffn4 6034 fores 6037 dff1o2 6055 dff1o3 6056 foimacnv 6067 foun 6068 fconst5 6376 dff1o6 6431 nvof1o 6436 f1oweALT 7043 fo1st 7079 fo2nd 7080 tposfo2 7262 fodomr 7996 f1finf1o 8072 unfilem2 8110 brwdom2 8361 harwdom 8378 infpwfien 8768 alephiso 8804 brdom3 9231 brdom5 9232 brdom4 9233 iunfo 9240 qnnen 14781 isfull2 16394 odf1o2 17811 cygctb 18116 qtopss 21328 qtopomap 21331 qtopcmap 21332 reeff1o 24005 efifo 24097 fargshiftfo 26166 pjfoi 27946 bdayfo 31074 fobigcup 31177 |
Copyright terms: Public domain | W3C validator |