MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fo Structured version   Visualization version   GIF version

Definition df-fo 6047
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 6272, dffo3 6529, dffo4 6530, and dffo5 6531.

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 16931. (Contributed by NM, 1-Aug-1994.)

Assertion
Ref Expression
df-fo (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

Detailed syntax breakdown of Definition df-fo
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cF . . 3 class 𝐹
41, 2, 3wfo 6039 . 2 wff 𝐹:𝐴onto𝐵
53, 1wfn 6036 . . 3 wff 𝐹 Fn 𝐴
63crn 5259 . . . 4 class ran 𝐹
76, 2wceq 1624 . . 3 wff ran 𝐹 = 𝐵
85, 7wa 383 . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
94, 8wb 196 1 wff (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  foeq1  6264  foeq2  6265  foeq3  6266  nffo  6267  fof  6268  forn  6271  dffo2  6272  dffn4  6274  fores  6277  dff1o2  6295  dff1o3  6296  foimacnv  6307  foun  6308  fconst5  6627  dff1o6  6686  nvof1o  6691  f1oweALT  7309  fo1st  7345  fo2nd  7346  tposfo2  7536  fodomr  8268  f1finf1o  8344  unfilem2  8382  brwdom2  8635  harwdom  8652  infpwfien  9067  alephiso  9103  brdom3  9534  brdom5  9535  brdom4  9536  iunfo  9545  qnnen  15133  isfull2  16764  odf1o2  18180  cygctb  18485  qtopss  21712  qtopomap  21715  qtopcmap  21716  reeff1o  24392  efifo  24484  pjfoi  28863  bdayfo  32126  fobigcup  32305  fargshiftfo  41880
  Copyright terms: Public domain W3C validator