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

Definition df-fo 5129
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 5121 . 2 wff 𝐹:𝐴onto𝐵
53, 1wfn 5118 . . 3 wff 𝐹 Fn 𝐴
63crn 4540 . . . 4 class ran 𝐹
76, 2wceq 1331 . . 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  5341  foeq2  5342  foeq3  5343  nffo  5344  fof  5345  forn  5348  dffo2  5349  dffn4  5351  fores  5354  dff1o2  5372  dff1o3  5373  foimacnv  5385  foun  5386  fconstfvm  5638  dff1o6  5677  fo1st  6055  fo2nd  6056  tposfo2  6164  ctssdc  6998  exmidfodomrlemim  7057  reeff1o  12872
  Copyright terms: Public domain W3C validator