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