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

Definition df-fo 4975
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 4967 . 2  wff  F : A -onto-> B
53, 1wfn 4964 . . 3  wff  F  Fn  A
63crn 4402 . . . 4  class  ran  F
76, 2wceq 1285 . . 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  5177  foeq2  5178  foeq3  5179  nffo  5180  fof  5181  forn  5184  dffo2  5185  dffn4  5187  fores  5190  dff1o2  5206  dff1o3  5207  foimacnv  5219  foun  5220  fconstfvm  5455  dff1o6  5495  fo1st  5863  fo2nd  5864  tposfo2  5964  exmidfodomrlemim  6730
  Copyright terms: Public domain W3C validator