Theorem 2aryenef

Description: The set of binary (endo)functions and the set of binary operations are equinumerous. (Contributed by AV, 19-May-2024)

	Ref	Expression
Assertion	2aryenef	⊢ ( 2 -aryF 𝑋 ) ≈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		ovex	⊢ ( 2 -aryF 𝑋 ) ∈ V
2	1	mptex	⊢ ( 𝑓 ∈ ( 2 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) ) ∈ V
3	2	a1i	⊢ ( 𝑋 ∈ V → ( 𝑓 ∈ ( 2 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) ) ∈ V )
4		eqid	⊢ ( 𝑓 ∈ ( 2 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) ) = ( 𝑓 ∈ ( 2 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) )
5	4	2arymaptf1o	⊢ ( 𝑋 ∈ V → ( 𝑓 ∈ ( 2 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) ) : ( 2 -aryF 𝑋 ) –1-1-onto→ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) )
6		f1oeq1	⊢ ( ℎ = ( 𝑓 ∈ ( 2 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) ) → ( ℎ : ( 2 -aryF 𝑋 ) –1-1-onto→ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ↔ ( 𝑓 ∈ ( 2 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑦 ⟩ } ) ) ) : ( 2 -aryF 𝑋 ) –1-1-onto→ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ) )
7	3 5 6	spcedv	⊢ ( 𝑋 ∈ V → ∃ ℎ ℎ : ( 2 -aryF 𝑋 ) –1-1-onto→ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) )
8		bren	⊢ ( ( 2 -aryF 𝑋 ) ≈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) ↔ ∃ ℎ ℎ : ( 2 -aryF 𝑋 ) –1-1-onto→ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) )
9	7 8	sylibr	⊢ ( 𝑋 ∈ V → ( 2 -aryF 𝑋 ) ≈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) )
10		0ex	⊢ ∅ ∈ V
11	10	enref	⊢ ∅ ≈ ∅
12	11	a1i	⊢ ( ¬ 𝑋 ∈ V → ∅ ≈ ∅ )
13		df-naryf	⊢ -aryF = ( 𝑛 ∈ ℕ0 , 𝑥 ∈ V ↦ ( 𝑥 ↑m ( 𝑥 ↑m ( 0 ..^ 𝑛 ) ) ) )
14	13	reldmmpo	⊢ Rel dom -aryF
15	14	ovprc2	⊢ ( ¬ 𝑋 ∈ V → ( 2 -aryF 𝑋 ) = ∅ )
16		reldmmap	⊢ Rel dom ↑m
17	16	ovprc1	⊢ ( ¬ 𝑋 ∈ V → ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) = ∅ )
18	12 15 17	3brtr4d	⊢ ( ¬ 𝑋 ∈ V → ( 2 -aryF 𝑋 ) ≈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) ) )
19	9 18	pm2.61i	⊢ ( 2 -aryF 𝑋 ) ≈ ( 𝑋 ↑m ( 𝑋 × 𝑋 ) )