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 ⁡ ℕ 0
smndex2dbas.b ⊢ B = Base M
smndex2dbas.0 ⊢ 0 ˙ = 0 M
smndex2dbas.d ⊢ D = x ∈ ℕ 0 ⟼ 2 ⁢ x
smndex2hbas.n ⊢ N ∈ ℕ 0
smndex2hbas.h ⊢ H = x ∈ ℕ 0 ⟼ if 2 ∥ x x 2 N
Assertion smndex2hbas ⊢ H ∈ B

Proof

Step Hyp Ref Expression
1 smndex2dbas.m ⊢ M = EndoFMnd ⁡ ℕ 0
2 smndex2dbas.b ⊢ B = Base M
3 smndex2dbas.0 ⊢ 0 ˙ = 0 M
4 smndex2dbas.d ⊢ D = x ∈ ℕ 0 ⟼ 2 ⁢ x
5 smndex2hbas.n ⊢ N ∈ ℕ 0
6 smndex2hbas.h ⊢ H = x ∈ ℕ 0 ⟼ if 2 ∥ x x 2 N
7 nn0ehalf ⊢ x ∈ ℕ 0 ∧ 2 ∥ x → x 2 ∈ ℕ 0
8 5 a1i ⊢ x ∈ ℕ 0 ∧ ¬ 2 ∥ x → N ∈ ℕ 0
9 7 8 ifclda ⊢ x ∈ ℕ 0 → if 2 ∥ x x 2 N ∈ ℕ 0
10 6 9 fmpti ⊢ H : ℕ 0 ⟶ ℕ 0
11 nn0ex ⊢ ℕ 0 ∈ V
12 11 mptex ⊢ x ∈ ℕ 0 ⟼ if 2 ∥ x x 2 N ∈ V
13 6 12 eqeltri ⊢ H ∈ V
14 1 2 elefmndbas2 ⊢ H ∈ V → H ∈ B ↔ H : ℕ 0 ⟶ ℕ 0
15 13 14 ax-mp ⊢ H ∈ B ↔ H : ℕ 0 ⟶ ℕ 0
16 10 15 mpbir ⊢ H ∈ B