Description: The mapping of binary (endo)functions is a one-to-one function onto the set of binary operations. (Contributed by AV, 23-May-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | 2arymaptf.h | ⊢ 𝐻 = ( ℎ ∈ ( 2 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( ℎ ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) ) | |
| Assertion | 2arymaptf1o | ⊢ ( 𝑋 ∈ 𝑉 → 𝐻 : ( 2 -aryF 𝑋 ) ⟶1-1onto ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 2arymaptf.h | ⊢ 𝐻 = ( ℎ ∈ ( 2 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( ℎ ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) ) | |
| 2 | 1 | 2arymaptf1 | ⊢ ( 𝑋 ∈ 𝑉 → 𝐻 : ( 2 -aryF 𝑋 ) ⟶1-1 ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ) |
| 3 | 1 | 2arymaptfo | ⊢ ( 𝑋 ∈ 𝑉 → 𝐻 : ( 2 -aryF 𝑋 ) ⟶onto ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ) |
| 4 | df-f1o | ⊢ ( 𝐻 : ( 2 -aryF 𝑋 ) ⟶1-1onto ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ↔ ( 𝐻 : ( 2 -aryF 𝑋 ) ⟶1-1 ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ∧ 𝐻 : ( 2 -aryF 𝑋 ) ⟶onto ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ) ) | |
| 5 | 2 3 4 | sylanbrc | ⊢ ( 𝑋 ∈ 𝑉 → 𝐻 : ( 2 -aryF 𝑋 ) ⟶1-1onto ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ) |