Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-f1o | GIF version |
Description: Define a one-to-one onto function. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow). (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-f1o | ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | cF | . . 3 class 𝐹 | |
4 | 1, 2, 3 | wf1o 5092 | . 2 wff 𝐹:𝐴–1-1-onto→𝐵 |
5 | 1, 2, 3 | wf1 5090 | . . 3 wff 𝐹:𝐴–1-1→𝐵 |
6 | 1, 2, 3 | wfo 5091 | . . 3 wff 𝐹:𝐴–onto→𝐵 |
7 | 5, 6 | wa 103 | . 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) |
8 | 4, 7 | wb 104 | 1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)) |
Colors of variables: wff set class |
This definition is referenced by: f1oeq1 5326 f1oeq2 5327 f1oeq3 5328 nff1o 5333 f1of1 5334 dff1o2 5340 dff1o5 5344 f1oco 5358 fo00 5371 dff1o6 5645 fcof1o 5658 tposf1o2 6135 cnref1o 9396 |
Copyright terms: Public domain | W3C validator |