This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem smndex2hbas

Description: The halving functions H are endofunctions 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 ) )
smndex2hbas.n 
|- N e. NN0
smndex2hbas.h 
|- H = ( x e. NN0 |-> if ( 2 || x , ( x / 2 ) , N ) )
Assertion smndex2hbas 
|- H 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 smndex2hbas.n 
 |-  N e. NN0
6 smndex2hbas.h 
 |-  H = ( x e. NN0 |-> if ( 2 || x , ( x / 2 ) , N ) )
7 nn0ehalf 
 |-  ( ( x e. NN0 /\ 2 || x ) -> ( x / 2 ) e. NN0 )
8 5 a1i 
 |-  ( ( x e. NN0 /\ -. 2 || x ) -> N e. NN0 )
9 7 8 ifclda 
 |-  ( x e. NN0 -> if ( 2 || x , ( x / 2 ) , N ) e. NN0 )
10 6 9 fmpti 
 |-  H : NN0 --> NN0
11 nn0ex 
 |-  NN0 e. _V
12 11 mptex 
 |-  ( x e. NN0 |-> if ( 2 || x , ( x / 2 ) , N ) ) e. _V
13 6 12 eqeltri 
 |-  H e. _V
14 1 2 elefmndbas2 
 |-  ( H e. _V -> ( H e. B <-> H : NN0 --> NN0 ) )
15 13 14 ax-mp 
 |-  ( H e. B <-> H : NN0 --> NN0 )
16 10 15 mpbir 
 |-  H e. B