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

Definition df-fo 4908
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 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))

Detailed syntax breakdown of Definition df-fo
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cF . . 3 class 𝐹
41, 2, 3wfo 4900 . 2 wff 𝐹:𝐴onto𝐵
53, 1wfn 4897 . . 3 wff 𝐹 Fn 𝐴
63crn 4346 . . . 4 class ran 𝐹
76, 2wceq 1243 . . 3 wff ran 𝐹 = 𝐵
85, 7wa 97 . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
94, 8wb 98 1 wff (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
Colors of variables: wff set class
This definition is referenced by:  foeq1  5102  foeq2  5103  foeq3  5104  nffo  5105  fof  5106  forn  5109  dffo2  5110  dffn4  5112  fores  5115  dff1o2  5131  dff1o3  5132  foimacnv  5144  foun  5145  fconstfvm  5379  dff1o6  5416  fo1st  5784  fo2nd  5785  tposfo2  5882
  Copyright terms: Public domain W3C validator