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

Definition df-fo 4851
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 : -onto->  F  Fn  ran  F

Detailed syntax breakdown of Definition df-fo
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 cF . . 3  F
41, 2, 3wfo 4843 . 2  F : -onto->
53, 1wfn 4840 . . 3  F  Fn
63crn 4289 . . . 4  ran  F
76, 2wceq 1242 . . 3  ran  F
85, 7wa 97 . 2  F  Fn  ran  F
94, 8wb 98 1  F : -onto->  F  Fn  ran  F
Colors of variables: wff set class
This definition is referenced by:  foeq1  5045  foeq2  5046  foeq3  5047  nffo  5048  fof  5049  forn  5052  dffo2  5053  dffn4  5055  fores  5058  dff1o2  5074  dff1o3  5075  foimacnv  5087  foun  5088  fconstfvm  5322  dff1o6  5359  fo1st  5726  fo2nd  5727  tposfo2  5823
  Copyright terms: Public domain W3C validator