This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem smndex2dbas

Description: The doubling function D is an endofunction on NN0 . (Contributed by AV, 18-Feb-2024)

Ref Expression
Hypotheses smndex2dbas.m ⊢ M = EndoFMnd ⁡ ℕ 0
smndex2dbas.b ⊢ B = Base M
smndex2dbas.0 ⊢ 0 ˙ = 0 M
smndex2dbas.d ⊢ D = x ∈ ℕ 0 ⟼ 2 ⁢ x
Assertion smndex2dbas ⊢ D ∈ B

Proof

Step Hyp Ref Expression
1 smndex2dbas.m ⊢ M = EndoFMnd ⁡ ℕ 0
2 smndex2dbas.b ⊢ B = Base M
3 smndex2dbas.0 ⊢ 0 ˙ = 0 M
4 smndex2dbas.d ⊢ D = x ∈ ℕ 0 ⟼ 2 ⁢ x
5 2nn0 ⊢ 2 ∈ ℕ 0
6 5 a1i ⊢ x ∈ ℕ 0 → 2 ∈ ℕ 0
7 id ⊢ x ∈ ℕ 0 → x ∈ ℕ 0
8 6 7 nn0mulcld ⊢ x ∈ ℕ 0 → 2 ⁢ x ∈ ℕ 0
9 4 8 fmpti ⊢ D : ℕ 0 ⟶ ℕ 0
10 nn0ex ⊢ ℕ 0 ∈ V
11 10 mptex ⊢ x ∈ ℕ 0 ⟼ 2 ⁢ x ∈ V
12 4 11 eqeltri ⊢ D ∈ V
13 1 2 elefmndbas2 ⊢ D ∈ V → D ∈ B ↔ D : ℕ 0 ⟶ ℕ 0
14 12 13 ax-mp ⊢ D ∈ B ↔ D : ℕ 0 ⟶ ℕ 0
15 9 14 mpbir ⊢ D ∈ B