![]() |
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 5129 | . 2 wff 𝐹:𝐴–onto→𝐵 |
5 | 3, 1 | wfn 5126 | . . 3 wff 𝐹 Fn 𝐴 |
6 | 3 | crn 4548 | . . . 4 class ran 𝐹 |
7 | 6, 2 | wceq 1332 | . . 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 5349 foeq2 5350 foeq3 5351 nffo 5352 fof 5353 forn 5356 dffo2 5357 dffn4 5359 fores 5362 dff1o2 5380 dff1o3 5381 foimacnv 5393 foun 5394 fconstfvm 5646 dff1o6 5685 fo1st 6063 fo2nd 6064 tposfo2 6172 ctssdc 7006 exmidfodomrlemim 7074 reeff1o 12902 |
Copyright terms: Public domain | W3C validator |