Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 , dff1o3 , dff1o4 , and dff1o5 . Compare Definition 6.15(6) of TakeutiZaring p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow).
A one-to-one onto function is also called a "bijection" or a "bijective function", F : A -1-1-onto-> B can be read as " F is a bijection between A and B ". Bijections are precisely the isomorphisms in the category SetCat of sets and set functions, see setciso . Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb , two sets are isomorphic iff there is an isomorphism Isom regarding the identity relation. In this case, the two sets are also "equinumerous", see bren . (Contributed by NM, 1-Aug-1994)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-f1o | ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cF | ⊢ 𝐹 | |
| 1 | cA | ⊢ 𝐴 | |
| 2 | cB | ⊢ 𝐵 | |
| 3 | 1 2 0 | wf1o | ⊢ 𝐹 : 𝐴 –1-1-onto→ 𝐵 |
| 4 | 1 2 0 | wf1 | ⊢ 𝐹 : 𝐴 –1-1→ 𝐵 |
| 5 | 1 2 0 | wfo | ⊢ 𝐹 : 𝐴 –onto→ 𝐵 |
| 6 | 4 5 | wa | ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) |
| 7 | 3 6 | wb | ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ) |