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

Definition df-fo 4989
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 4981 . 2 wff 𝐹:𝐴onto𝐵
53, 1wfn 4978 . . 3 wff 𝐹 Fn 𝐴
63crn 4414 . . . 4 class ran 𝐹
76, 2wceq 1287 . . 3 wff ran 𝐹 = 𝐵
85, 7wa 102 . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
94, 8wb 103 1 wff (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
Colors of variables: wff set class
This definition is referenced by:  foeq1  5194  foeq2  5195  foeq3  5196  nffo  5197  fof  5198  forn  5201  dffo2  5202  dffn4  5204  fores  5207  dff1o2  5223  dff1o3  5224  foimacnv  5236  foun  5237  fconstfvm  5478  dff1o6  5518  fo1st  5887  fo2nd  5888  tposfo2  5988  exmidfodomrlemim  6774
  Copyright terms: Public domain W3C validator