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

Definition df-fo 5202
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 5194 . 2 wff 𝐹:𝐴onto𝐵
53, 1wfn 5191 . . 3 wff 𝐹 Fn 𝐴
63crn 4610 . . . 4 class ran 𝐹
76, 2wceq 1348 . . 3 wff ran 𝐹 = 𝐵
85, 7wa 103 . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
94, 8wb 104 1 wff (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
Colors of variables: wff set class
This definition is referenced by:  foeq1  5414  foeq2  5415  foeq3  5416  nffo  5417  fof  5418  forn  5421  dffo2  5422  dffn4  5424  fores  5427  dff1o2  5445  dff1o3  5446  foimacnv  5458  foun  5459  fconstfvm  5711  dff1o6  5752  fo1st  6133  fo2nd  6134  tposfo2  6243  ctssdc  7086  exmidfodomrlemim  7165  reeff1o  13447
  Copyright terms: Public domain W3C validator