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

Definition df-fo 5241
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 5233 . 2 wff 𝐹:𝐴onto𝐵
53, 1wfn 5230 . . 3 wff 𝐹 Fn 𝐴
63crn 4645 . . . 4 class ran 𝐹
76, 2wceq 1364 . . 3 wff ran 𝐹 = 𝐵
85, 7wa 104 . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)
94, 8wb 105 1 wff (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
Colors of variables: wff set class
This definition is referenced by:  foeq1  5453  foeq2  5454  foeq3  5455  nffo  5456  fof  5457  forn  5460  dffo2  5461  dffn4  5463  fores  5466  dff1o2  5485  dff1o3  5486  foimacnv  5498  foun  5499  fconstfvm  5754  dff1o6  5797  fo1st  6181  fo2nd  6182  tposfo2  6291  ctssdc  7141  exmidfodomrlemim  7229  reeff1o  14646
  Copyright terms: Public domain W3C validator