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

Definition df-fo 5055
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 5047 . 2 wff 𝐹:𝐴onto𝐵
53, 1wfn 5044 . . 3 wff 𝐹 Fn 𝐴
63crn 4468 . . . 4 class ran 𝐹
76, 2wceq 1296 . . 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  5264  foeq2  5265  foeq3  5266  nffo  5267  fof  5268  forn  5271  dffo2  5272  dffn4  5274  fores  5277  dff1o2  5293  dff1o3  5294  foimacnv  5306  foun  5307  fconstfvm  5554  dff1o6  5593  fo1st  5966  fo2nd  5967  tposfo2  6070  exmidfodomrlemim  6924
  Copyright terms: Public domain W3C validator