Theorem smndex2hbas

Description: The halving functions H are endofunctions on NN0 . (Contributed by AV, 18-Feb-2024)

	Ref	Expression
Hypotheses	smndex2dbas.m	$$⊢M=\mathrm{EndoFMnd}\left({\mathbb{N}}_0\right)$$
	smndex2dbas.b	$$⊢B={\mathrm{Base}}_M$$
	smndex2dbas.0	$$⊢\underset{\dot{}}{0}=0_M$$
	smndex2dbas.d	$$⊢D=\left(x\in {\mathbb{N}}_0⟼2x\right)$$
	smndex2hbas.n	$$⊢N\in {\mathbb{N}}_0$$
	smndex2hbas.h	$$⊢H=\left(x\in {\mathbb{N}}_0⟼if\left(2\parallel x,\frac{x}{2},N\right)\right)$$
Assertion	smndex2hbas	$$⊢H\in B$$

Proof

Step	Hyp	Ref	Expression
1		smndex2dbas.m	$$⊢M=\mathrm{EndoFMnd}\left({\mathbb{N}}_0\right)$$
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		smndex2hbas.n	$$⊢N\in {\mathbb{N}}_0$$
6		smndex2hbas.h	$$⊢H=\left(x\in {\mathbb{N}}_0⟼if\left(2\parallel x,\frac{x}{2},N\right)\right)$$
7		nn0ehalf	$$⊢\left(x\in {\mathbb{N}}_0\wedge 2\parallel x\right)\to \frac{x}{2}\in {\mathbb{N}}_0$$
8	5	a1i	$$⊢\left(x\in {\mathbb{N}}_0\wedge \neg 2\parallel x\right)\to N\in {\mathbb{N}}_0$$
9	7 8	ifclda	$$⊢x\in {\mathbb{N}}_0\to if\left(2\parallel x,\frac{x}{2},N\right)\in {\mathbb{N}}_0$$
10	6 9	fmpti	$$⊢H:{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
11		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
12	11	mptex	$$⊢\left(x\in {\mathbb{N}}_0⟼if\left(2\parallel x,\frac{x}{2},N\right)\right)\in \mathrm{V}$$
13	6 12	eqeltri	$$⊢H\in \mathrm{V}$$
14	1 2	elefmndbas2	$$⊢H\in \mathrm{V}\to \left(H\in B\leftrightarrow H:{\mathbb{N}}_0⟶{\mathbb{N}}_0\right)$$
15	13 14	ax-mp	$$⊢H\in B\leftrightarrow H:{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
16	10 15	mpbir	$$⊢H\in B$$