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	⊢ 𝐷 ∈ 𝐵