![]() |
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 5233 | . 2 wff 𝐹:𝐴–onto→𝐵 |
5 | 3, 1 | wfn 5230 | . . 3 wff 𝐹 Fn 𝐴 |
6 | 3 | crn 4645 | . . . 4 class ran 𝐹 |
7 | 6, 2 | wceq 1364 | . . 3 wff ran 𝐹 = 𝐵 |
8 | 5, 7 | wa 104 | . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) |
9 | 4, 8 | wb 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 |