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 5194 | . 2 wff 𝐹:𝐴–onto→𝐵 |
5 | 3, 1 | wfn 5191 | . . 3 wff 𝐹 Fn 𝐴 |
6 | 3 | crn 4610 | . . . 4 class ran 𝐹 |
7 | 6, 2 | wceq 1348 | . . 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 5414 foeq2 5415 foeq3 5416 nffo 5417 fof 5418 forn 5421 dffo2 5422 dffn4 5424 fores 5427 dff1o2 5445 dff1o3 5446 foimacnv 5458 foun 5459 fconstfvm 5711 dff1o6 5752 fo1st 6133 fo2nd 6134 tposfo2 6243 ctssdc 7086 exmidfodomrlemim 7165 reeff1o 13447 |
Copyright terms: Public domain | W3C validator |