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

Definition df-fo 4886
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 4878 . 2  wff  F : A -onto-> B
53, 1wfn 4875 . . 3  wff  F  Fn  A
63crn 4324 . . . 4  class  ran  F
76, 2wceq 1243 . . 3  wff  ran  F  =  B
85, 7wa 97 . 2  wff  ( F  Fn  A  /\  ran  F  =  B )
94, 8wb 98 1  wff  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
Colors of variables: wff set class
This definition is referenced by:  foeq1  5080  foeq2  5081  foeq3  5082  nffo  5083  fof  5084  forn  5087  dffo2  5088  dffn4  5090  fores  5093  dff1o2  5109  dff1o3  5110  foimacnv  5122  foun  5123  fconstfvm  5357  dff1o6  5394  fo1st  5762  fo2nd  5763  tposfo2  5860
  Copyright terms: Public domain W3C validator