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 ⊢ 𝑀 = ( 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 ⊢ 𝐻 ∈ 𝐵