![]() |
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 | ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | cF | . . 3 class 𝐹 | |
4 | 1, 2, 3 | wfo 5047 | . 2 wff 𝐹:𝐴–onto→𝐵 |
5 | 3, 1 | wfn 5044 | . . 3 wff 𝐹 Fn 𝐴 |
6 | 3 | crn 4468 | . . . 4 class ran 𝐹 |
7 | 6, 2 | wceq 1296 | . . 3 wff ran 𝐹 = 𝐵 |
8 | 5, 7 | wa 103 | . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) |
9 | 4, 8 | wb 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 |