Theorem smndex2hbas

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

	Ref	Expression
Hypotheses	smndex2dbas.m	⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
	smndex2dbas.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	smndex2dbas.0	⊢ 0 = ( 0g ‘ 𝑀 )
	smndex2dbas.d	⊢ 𝐷 = ( 𝑥 ∈ ℕ0 ↦ ( 2 · 𝑥 ) )
	smndex2hbas.n	⊢ 𝑁 ∈ ℕ0
	smndex2hbas.h	⊢ 𝐻 = ( 𝑥 ∈ ℕ0 ↦ if ( 2 ∥ 𝑥 , ( 𝑥 / 2 ) , 𝑁 ) )
Assertion	smndex2hbas	⊢ 𝐻 ∈ 𝐵

Proof

Step	Hyp	Ref	Expression
1		smndex2dbas.m	⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
2		smndex2dbas.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
3		smndex2dbas.0	⊢ 0 = ( 0g ‘ 𝑀 )
4		smndex2dbas.d	⊢ 𝐷 = ( 𝑥 ∈ ℕ0 ↦ ( 2 · 𝑥 ) )
5		smndex2hbas.n	⊢ 𝑁 ∈ ℕ0
6		smndex2hbas.h	⊢ 𝐻 = ( 𝑥 ∈ ℕ0 ↦ if ( 2 ∥ 𝑥 , ( 𝑥 / 2 ) , 𝑁 ) )
7		nn0ehalf	⊢ ( ( 𝑥 ∈ ℕ0 ∧ 2 ∥ 𝑥 ) → ( 𝑥 / 2 ) ∈ ℕ0 )
8	5	a1i	⊢ ( ( 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑥 ) → 𝑁 ∈ ℕ0 )
9	7 8	ifclda	⊢ ( 𝑥 ∈ ℕ0 → if ( 2 ∥ 𝑥 , ( 𝑥 / 2 ) , 𝑁 ) ∈ ℕ0 )
10	6 9	fmpti	⊢ 𝐻 : ℕ0 ⟶ ℕ0
11		nn0ex	⊢ ℕ0 ∈ V
12	11	mptex	⊢ ( 𝑥 ∈ ℕ0 ↦ if ( 2 ∥ 𝑥 , ( 𝑥 / 2 ) , 𝑁 ) ) ∈ V
13	6 12	eqeltri	⊢ 𝐻 ∈ V
14	1 2	elefmndbas2	⊢ ( 𝐻 ∈ V → ( 𝐻 ∈ 𝐵 ↔ 𝐻 : ℕ0 ⟶ ℕ0 ) )
15	13 14	ax-mp	⊢ ( 𝐻 ∈ 𝐵 ↔ 𝐻 : ℕ0 ⟶ ℕ0 )
16	10 15	mpbir	⊢ 𝐻 ∈ 𝐵