Theorem 2arymaptf1o

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-1-onto→ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) )

Proof

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-1-onto→ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ↔ ( 𝐻 : ( 2 -aryF 𝑋 ) –1-1→ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ∧ 𝐻 : ( 2 -aryF 𝑋 ) –onto→ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ) )
5	2 3 4	sylanbrc	⊢ ( 𝑋 ∈ 𝑉 → 𝐻 : ( 2 -aryF 𝑋 ) –1-1-onto→ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) )