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 6588, dffo3 6861, dffo4 6862, and dffo5 6863.
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 17338. (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 6347 | . 2 wff 𝐹:𝐴–onto→𝐵 |
5 | 3, 1 | wfn 6344 | . . 3 wff 𝐹 Fn 𝐴 |
6 | 3 | crn 5550 | . . . 4 class ran 𝐹 |
7 | 6, 2 | wceq 1528 | . . 3 wff ran 𝐹 = 𝐵 |
8 | 5, 7 | wa 396 | . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) |
9 | 4, 8 | wb 207 | 1 wff (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: foeq1 6580 foeq2 6581 foeq3 6582 nffo 6583 fof 6584 forn 6587 dffo2 6588 dffn4 6590 fores 6594 dff1o2 6614 dff1o3 6615 foimacnv 6626 foun 6627 fconst5 6961 dff1o6 7023 nvof1o 7028 f1oweALT 7664 fo1st 7700 fo2nd 7701 tposfo2 7906 fodomr 8657 f1finf1o 8734 unfilem2 8772 brwdom2 9026 harwdom 9043 infpwfien 9477 alephiso 9513 brdom3 9939 brdom5 9940 brdom4 9941 iunfo 9950 qnnen 15556 isfull2 17171 odf1o2 18629 cygctb 18943 qtopss 22253 qtopomap 22256 qtopcmap 22257 reeff1o 24964 efifo 25058 pjfoi 29408 bdayfo 33080 fobigcup 33259 fargshiftfo 43449 smndex2dnrinv 43985 |
Copyright terms: Public domain | W3C validator |