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

Definition df-fo 5234
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 5226 . 2  wff  F : A -onto-> B
53, 1wfn 5223 . . 3  wff  F  Fn  A
63crn 4639 . . . 4  class  ran  F
76, 2wceq 1363 . . 3  wff  ran  F  =  B
85, 7wa 104 . 2  wff  ( F  Fn  A  /\  ran  F  =  B )
94, 8wb 105 1  wff  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
Colors of variables: wff set class
This definition is referenced by:  foeq1  5446  foeq2  5447  foeq3  5448  nffo  5449  fof  5450  forn  5453  dffo2  5454  dffn4  5456  fores  5459  dff1o2  5478  dff1o3  5479  foimacnv  5491  foun  5492  fconstfvm  5747  dff1o6  5790  fo1st  6171  fo2nd  6172  tposfo2  6281  ctssdc  7125  exmidfodomrlemim  7213  reeff1o  14465
  Copyright terms: Public domain W3C validator