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 6637, dffo3 6921, dffo4 6922, and dffo5 6923.
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 17594. (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 6378 | . 2 wff 𝐹:𝐴–onto→𝐵 |
5 | 3, 1 | wfn 6375 | . . 3 wff 𝐹 Fn 𝐴 |
6 | 3 | crn 5552 | . . . 4 class ran 𝐹 |
7 | 6, 2 | wceq 1543 | . . 3 wff ran 𝐹 = 𝐵 |
8 | 5, 7 | wa 399 | . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) |
9 | 4, 8 | wb 209 | 1 wff (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: foeq1 6629 foeq2 6630 foeq3 6631 nffo 6632 fof 6633 forn 6636 dffo2 6637 dffn4 6639 fores 6643 dff1o2 6666 dff1o3 6667 foimacnv 6678 foun 6679 rescnvimafod 6894 fconst5 7021 dff1o6 7086 nvof1o 7091 f1oweALT 7745 fo1st 7781 fo2nd 7782 tposfo2 7991 fodomr 8797 f1finf1o 8902 unfilem2 8936 brwdom2 9189 harwdom 9207 infpwfien 9676 alephiso 9712 brdom3 10142 brdom5 10143 brdom4 10144 iunfo 10153 qnnen 15774 isfull2 17418 smndex2dnrinv 18342 odf1o2 18962 cygctb 19277 qtopss 22612 qtopomap 22615 qtopcmap 22616 reeff1o 25339 efifo 25436 pjfoi 29784 bdayfo 33617 fobigcup 33939 fundcmpsurinjlem2 44524 fargshiftfo 44567 |
Copyright terms: Public domain | W3C validator |