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 ⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
smndex2dbas.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
smndex2dbas.0 ⊢ 0 = ( 0g ‘ 𝑀 )
smndex2dbas.d ⊢ 𝐷 = ( 𝑥 ∈ ℕ0 ↦ ( 2 · 𝑥 ) )
Assertion smndex2dbas 𝐷 ∈ 𝐵

Proof

Step Hyp Ref Expression
1 smndex2dbas.m ⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
2 smndex2dbas.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
3 smndex2dbas.0 ⊢ 0 = ( 0g ‘ 𝑀 )
4 smndex2dbas.d ⊢ 𝐷 = ( 𝑥 ∈ ℕ0 ↦ ( 2 · 𝑥 ) )
5 2nn0 ⊢ 2 ∈ ℕ0
6 5 a1i ⊢ ( 𝑥 ∈ ℕ0 → 2 ∈ ℕ0 )
7 id ⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℕ0 )
8 6 7 nn0mulcld ⊢ ( 𝑥 ∈ ℕ0 → ( 2 · 𝑥 ) ∈ ℕ0 )
9 4 8 fmpti ⊢ 𝐷 : ℕ0 ⟶ ℕ0
10 nn0ex ⊢ ℕ0 ∈ V
11 10 mptex ⊢ ( 𝑥 ∈ ℕ0 ↦ ( 2 · 𝑥 ) ) ∈ V
12 4 11 eqeltri ⊢ 𝐷 ∈ V
13 1 2 elefmndbas2 ⊢ ( 𝐷 ∈ V → ( 𝐷 ∈ 𝐵 ↔ 𝐷 : ℕ0 ⟶ ℕ0 ) )
14 12 13 ax-mp ⊢ ( 𝐷 ∈ 𝐵 ↔ 𝐷 : ℕ0 ⟶ ℕ0 )
15 9 14 mpbir ⊢ 𝐷 ∈ 𝐵