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 ` NN0 )
	smndex2dbas.b	|- B = ( Base ` M )
	smndex2dbas.0	|- .0. = ( 0g ` M )
	smndex2dbas.d	|- D = ( x e. NN0 |-> ( 2 x. x ) )
Assertion	smndex2dbas	|- D e. B

Proof

Step	Hyp	Ref	Expression
1		smndex2dbas.m	|- M = ( EndoFMnd ` NN0 )
2		smndex2dbas.b	|- B = ( Base ` M )
3		smndex2dbas.0	|- .0. = ( 0g ` M )
4		smndex2dbas.d	|- D = ( x e. NN0 |-> ( 2 x. x ) )
5		2nn0	|- 2 e. NN0
6	5	a1i	|- ( x e. NN0 -> 2 e. NN0 )
7		id	|- ( x e. NN0 -> x e. NN0 )
8	6 7	nn0mulcld	|- ( x e. NN0 -> ( 2 x. x ) e. NN0 )
9	4 8	fmpti	|- D : NN0 --> NN0
10		nn0ex	|- NN0 e. _V
11	10	mptex	|- ( x e. NN0 |-> ( 2 x. x ) ) e. _V
12	4 11	eqeltri	|- D e. _V
13	1 2	elefmndbas2	|- ( D e. _V -> ( D e. B <-> D : NN0 --> NN0 ) )
14	12 13	ax-mp	|- ( D e. B <-> D : NN0 --> NN0 )
15	9 14	mpbir	|- D e. B