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

Definition df-fo 4935
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 4927 . 2  wff  F : A -onto-> B
53, 1wfn 4924 . . 3  wff  F  Fn  A
63crn 4373 . . . 4  class  ran  F
76, 2wceq 1259 . . 3  wff  ran  F  =  B
85, 7wa 101 . 2  wff  ( F  Fn  A  /\  ran  F  =  B )
94, 8wb 102 1  wff  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
Colors of variables: wff set class
This definition is referenced by:  foeq1  5129  foeq2  5130  foeq3  5131  nffo  5132  fof  5133  forn  5136  dffo2  5137  dffn4  5139  fores  5142  dff1o2  5158  dff1o3  5159  foimacnv  5171  foun  5172  fconstfvm  5406  dff1o6  5443  fo1st  5811  fo2nd  5812  tposfo2  5912
  Copyright terms: Public domain W3C validator