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 ` 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