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 5182 | . 2 wff 𝐹:𝐴–1-1-onto→𝐵 |
5 | 1, 2, 3 | wf1 5180 | . . 3 wff 𝐹:𝐴–1-1→𝐵 |
6 | 1, 2, 3 | wfo 5181 | . . 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 5416 f1oeq2 5417 f1oeq3 5418 nff1o 5425 f1of1 5426 dff1o2 5432 dff1o5 5436 f1oco 5450 fo00 5463 dff1o6 5739 fcof1o 5752 tposf1o2 6230 cnref1o 9580 1arith 12286 reeff1o 13261 ioocosf1o 13342 |
Copyright terms: Public domain | W3C validator |