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

Definition df-fo 4932
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 4924 . 2 wff 𝐹:𝐴onto𝐵
53, 1wfn 4921 . . 3 wff 𝐹 Fn 𝐴
63crn 4366 . . . 4 class ran 𝐹
76, 2wceq 1285 . . 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  5127  foeq2  5128  foeq3  5129  nffo  5130  fof  5131  forn  5134  dffo2  5135  dffn4  5137  fores  5140  dff1o2  5156  dff1o3  5157  foimacnv  5169  foun  5170  fconstfvm  5405  dff1o6  5441  fo1st  5809  fo2nd  5810  tposfo2  5910
  Copyright terms: Public domain W3C validator