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

Definition df-fo 4987
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 4979 . 2  wff  F : A -onto-> B
53, 1wfn 4976 . . 3  wff  F  Fn  A
63crn 4412 . . . 4  class  ran  F
76, 2wceq 1287 . . 3  wff  ran  F  =  B
85, 7wa 102 . 2  wff  ( F  Fn  A  /\  ran  F  =  B )
94, 8wb 103 1  wff  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
Colors of variables: wff set class
This definition is referenced by:  foeq1  5192  foeq2  5193  foeq3  5194  nffo  5195  fof  5196  forn  5199  dffo2  5200  dffn4  5202  fores  5205  dff1o2  5221  dff1o3  5222  foimacnv  5234  foun  5235  fconstfvm  5476  dff1o6  5516  fo1st  5885  fo2nd  5886  tposfo2  5986  exmidfodomrlemim  6771
  Copyright terms: Public domain W3C validator