ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-fo Unicode version

Definition df-fo 5099
Description: Define an onto function. Definition 6.15(4) of [TakeutiZaring] p. 27. We use their notation ("onto" under the arrow). (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-fo  |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )

Detailed syntax breakdown of Definition df-fo
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cF . . 3  class  F
41, 2, 3wfo 5091 . 2  wff  F : A -onto-> B
53, 1wfn 5088 . . 3  wff  F  Fn  A
63crn 4510 . . . 4  class  ran  F
76, 2wceq 1316 . . 3  wff  ran  F  =  B
85, 7wa 103 . 2  wff  ( F  Fn  A  /\  ran  F  =  B )
94, 8wb 104 1  wff  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
Colors of variables: wff set class
This definition is referenced by:  foeq1  5311  foeq2  5312  foeq3  5313  nffo  5314  fof  5315  forn  5318  dffo2  5319  dffn4  5321  fores  5324  dff1o2  5340  dff1o3  5341  foimacnv  5353  foun  5354  fconstfvm  5606  dff1o6  5645  fo1st  6023  fo2nd  6024  tposfo2  6132  ctssdc  6966  exmidfodomrlemim  7025
  Copyright terms: Public domain W3C validator