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 X ≈ X X

Proof

Step Hyp Ref Expression
1 ovex ⊢ 1 -aryF X ∈ V
2 1 mptex ⊢ f ∈ 1 -aryF X ⟼ x ∈ X ⟼ f ⁡ 0 x ∈ V
3 2 a1i ⊢ X ∈ V → f ∈ 1 -aryF X ⟼ x ∈ X ⟼ f ⁡ 0 x ∈ V
4 eqid ⊢ f ∈ 1 -aryF X ⟼ x ∈ X ⟼ f ⁡ 0 x = f ∈ 1 -aryF X ⟼ x ∈ X ⟼ f ⁡ 0 x
5 4 1arymaptf1o ⊢ X ∈ V → f ∈ 1 -aryF X ⟼ x ∈ X ⟼ f ⁡ 0 x : 1 -aryF X ⟶ 1-1 onto X X
6 f1oeq1 ⊢ h = f ∈ 1 -aryF X ⟼ x ∈ X ⟼ f ⁡ 0 x → h : 1 -aryF X ⟶ 1-1 onto X X ↔ f ∈ 1 -aryF X ⟼ x ∈ X ⟼ f ⁡ 0 x : 1 -aryF X ⟶ 1-1 onto X X
7 3 5 6 spcedv ⊢ X ∈ V → ∃ h h : 1 -aryF X ⟶ 1-1 onto X X
8 bren ⊢ 1 -aryF X ≈ X X ↔ ∃ h h : 1 -aryF X ⟶ 1-1 onto X X
9 7 8 sylibr ⊢ X ∈ V → 1 -aryF X ≈ X X
10 0ex ⊢ ∅ ∈ V
11 10 enref ⊢ ∅ ≈ ∅
12 11 a1i ⊢ ¬ X ∈ V → ∅ ≈ ∅
13 df-naryf ⊢ -aryF = n ∈ ℕ 0 , x ∈ V ⟼ x x 0 ..^ n
14 13 reldmmpo ⊢ Rel ⁡ dom ⁡ -aryF
15 14 ovprc2 ⊢ ¬ X ∈ V → 1 -aryF X = ∅
16 reldmmap ⊢ Rel ⁡ dom ⁡ ↑ 𝑚
17 16 ovprc1 ⊢ ¬ X ∈ V → X X = ∅
18 12 15 17 3brtr4d ⊢ ¬ X ∈ V → 1 -aryF X ≈ X X
19 9 18 pm2.61i ⊢ 1 -aryF X ≈ X X