![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-fo | GIF version |
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.) |
Ref | Expression |
---|---|
df-fo | ⊢ (𝐹:A–onto→B ↔ (𝐹 Fn A ∧ ran 𝐹 = B)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class A | |
2 | cB | . . 3 class B | |
3 | cF | . . 3 class 𝐹 | |
4 | 1, 2, 3 | wfo 4843 | . 2 wff 𝐹:A–onto→B |
5 | 3, 1 | wfn 4840 | . . 3 wff 𝐹 Fn A |
6 | 3 | crn 4289 | . . . 4 class ran 𝐹 |
7 | 6, 2 | wceq 1242 | . . 3 wff ran 𝐹 = B |
8 | 5, 7 | wa 97 | . 2 wff (𝐹 Fn A ∧ ran 𝐹 = B) |
9 | 4, 8 | wb 98 | 1 wff (𝐹:A–onto→B ↔ (𝐹 Fn A ∧ ran 𝐹 = B)) |
Colors of variables: wff set class |
This definition is referenced by: foeq1 5045 foeq2 5046 foeq3 5047 nffo 5048 fof 5049 forn 5052 dffo2 5053 dffn4 5055 fores 5058 dff1o2 5074 dff1o3 5075 foimacnv 5087 foun 5088 fconstfvm 5322 dff1o6 5359 fo1st 5726 fo2nd 5727 tposfo2 5823 |
Copyright terms: Public domain | W3C validator |