Metamath Proof Explorer


Theorem 1aryenef

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

Ref Expression
Assertion 1aryenef ( 1 -aryF 𝑋 ) ≈ ( 𝑋m 𝑋 )

Proof

Step Hyp Ref Expression
1 ovex ( 1 -aryF 𝑋 ) ∈ V
2 1 mptex ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ↦ ( 𝑥𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) ) ∈ V
3 2 a1i ( 𝑋 ∈ V → ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ↦ ( 𝑥𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) ) ∈ V )
4 eqid ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ↦ ( 𝑥𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) ) = ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ↦ ( 𝑥𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) )
5 4 1arymaptf1o ( 𝑋 ∈ V → ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ↦ ( 𝑥𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) ) : ( 1 -aryF 𝑋 ) –1-1-onto→ ( 𝑋m 𝑋 ) )
6 f1oeq1 ( = ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ↦ ( 𝑥𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) ) → ( : ( 1 -aryF 𝑋 ) –1-1-onto→ ( 𝑋m 𝑋 ) ↔ ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ↦ ( 𝑥𝑋 ↦ ( 𝑓 ‘ { ⟨ 0 , 𝑥 ⟩ } ) ) ) : ( 1 -aryF 𝑋 ) –1-1-onto→ ( 𝑋m 𝑋 ) ) )
7 3 5 6 spcedv ( 𝑋 ∈ V → ∃ : ( 1 -aryF 𝑋 ) –1-1-onto→ ( 𝑋m 𝑋 ) )
8 bren ( ( 1 -aryF 𝑋 ) ≈ ( 𝑋m 𝑋 ) ↔ ∃ : ( 1 -aryF 𝑋 ) –1-1-onto→ ( 𝑋m 𝑋 ) )
9 7 8 sylibr ( 𝑋 ∈ V → ( 1 -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 → ( 1 -aryF 𝑋 ) = ∅ )
16 reldmmap Rel dom ↑m
17 16 ovprc1 ( ¬ 𝑋 ∈ V → ( 𝑋m 𝑋 ) = ∅ )
18 12 15 17 3brtr4d ( ¬ 𝑋 ∈ V → ( 1 -aryF 𝑋 ) ≈ ( 𝑋m 𝑋 ) )
19 9 18 pm2.61i ( 1 -aryF 𝑋 ) ≈ ( 𝑋m 𝑋 )