Theorem smndex2dbas

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

	Ref	Expression
Hypotheses	smndex2dbas.m	No typesetting found for |- M = ( EndoFMnd ` NN0 ) with typecode |-
	smndex2dbas.b	$$⊢B={\mathrm{Base}}_M$$
	smndex2dbas.0	$$⊢\underset{\dot{}}{0}=0_M$$
	smndex2dbas.d	$$⊢D=\left(x\in {\mathbb{N}}_0⟼2x\right)$$
Assertion	smndex2dbas	$$⊢D\in B$$

Proof

Step	Hyp	Ref	Expression
1		smndex2dbas.m	Could not format M = ( EndoFMnd ` NN0 ) : No typesetting found for |- M = ( EndoFMnd ` NN0 ) with typecode |-
2		smndex2dbas.b	$$⊢B={\mathrm{Base}}_M$$
3		smndex2dbas.0	$$⊢\underset{\dot{}}{0}=0_M$$
4		smndex2dbas.d	$$⊢D=\left(x\in {\mathbb{N}}_0⟼2x\right)$$
5		2nn0	$$⊢2\in {\mathbb{N}}_0$$
6	5	a1i	$$⊢x\in {\mathbb{N}}_0\to 2\in {\mathbb{N}}_0$$
7		id	$$⊢x\in {\mathbb{N}}_0\to x\in {\mathbb{N}}_0$$
8	6 7	nn0mulcld	$$⊢x\in {\mathbb{N}}_0\to 2x\in {\mathbb{N}}_0$$
9	4 8	fmpti	$$⊢D:{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
10		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
11	10	mptex	$$⊢\left(x\in {\mathbb{N}}_0⟼2x\right)\in \mathrm{V}$$
12	4 11	eqeltri	$$⊢D\in \mathrm{V}$$
13	1 2	elefmndbas2	$$⊢D\in \mathrm{V}\to \left(D\in B\leftrightarrow D:{\mathbb{N}}_0⟶{\mathbb{N}}_0\right)$$
14	12 13	ax-mp	$$⊢D\in B\leftrightarrow D:{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
15	9 14	mpbir	$$⊢D\in B$$