Metamath Proof Explorer

Theorem ackvalsuc1mpt

Description: The Ackermann function at a successor of the first argument as a mapping of the second argument. (Contributed by Thierry Arnoux, 28-Apr-2024) (Revised by AV, 4-May-2024)

Ref Expression
Assertion ackvalsuc1mpt ⊢ M ∈ ℕ 0 → Ack ⁡ M + 1 = n ∈ ℕ 0 ⟼ IterComp ⁡ Ack ⁡ M ⁡ n + 1 ⁡ 1

Proof

Step Hyp Ref Expression
1 df-ack ⊢ Ack = seq 0 f ∈ V , j ∈ V ⟼ n ∈ ℕ 0 ⟼ IterComp ⁡ f ⁡ n + 1 ⁡ 1 i ∈ ℕ 0 ⟼ if i = 0 n ∈ ℕ 0 ⟼ n + 1 i
2 1 fveq1i ⊢ Ack ⁡ M + 1 = seq 0 f ∈ V , j ∈ V ⟼ n ∈ ℕ 0 ⟼ IterComp ⁡ f ⁡ n + 1 ⁡ 1 i ∈ ℕ 0 ⟼ if i = 0 n ∈ ℕ 0 ⟼ n + 1 i ⁡ M + 1
3 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
4 id ⊢ M ∈ ℕ 0 → M ∈ ℕ 0
5 eqid ⊢ M + 1 = M + 1
6 1 eqcomi ⊢ seq 0 f ∈ V , j ∈ V ⟼ n ∈ ℕ 0 ⟼ IterComp ⁡ f ⁡ n + 1 ⁡ 1 i ∈ ℕ 0 ⟼ if i = 0 n ∈ ℕ 0 ⟼ n + 1 i = Ack
7 6 fveq1i ⊢ seq 0 f ∈ V , j ∈ V ⟼ n ∈ ℕ 0 ⟼ IterComp ⁡ f ⁡ n + 1 ⁡ 1 i ∈ ℕ 0 ⟼ if i = 0 n ∈ ℕ 0 ⟼ n + 1 i ⁡ M = Ack ⁡ M
8 7 a1i ⊢ M ∈ ℕ 0 → seq 0 f ∈ V , j ∈ V ⟼ n ∈ ℕ 0 ⟼ IterComp ⁡ f ⁡ n + 1 ⁡ 1 i ∈ ℕ 0 ⟼ if i = 0 n ∈ ℕ 0 ⟼ n + 1 i ⁡ M = Ack ⁡ M
9 eqidd ⊢ M ∈ ℕ 0 → i ∈ ℕ 0 ⟼ if i = 0 n ∈ ℕ 0 ⟼ n + 1 i = i ∈ ℕ 0 ⟼ if i = 0 n ∈ ℕ 0 ⟼ n + 1 i
10 nn0p1gt0 ⊢ M ∈ ℕ 0 → 0 < M + 1
11 10 gt0ne0d ⊢ M ∈ ℕ 0 → M + 1 ≠ 0
12 11 adantr ⊢ M ∈ ℕ 0 ∧ i = M + 1 → M + 1 ≠ 0
13 neeq1 ⊢ i = M + 1 → i ≠ 0 ↔ M + 1 ≠ 0
14 13 adantl ⊢ M ∈ ℕ 0 ∧ i = M + 1 → i ≠ 0 ↔ M + 1 ≠ 0
15 12 14 mpbird ⊢ M ∈ ℕ 0 ∧ i = M + 1 → i ≠ 0
16 15 neneqd ⊢ M ∈ ℕ 0 ∧ i = M + 1 → ¬ i = 0
17 16 iffalsed ⊢ M ∈ ℕ 0 ∧ i = M + 1 → if i = 0 n ∈ ℕ 0 ⟼ n + 1 i = i
18 simpr ⊢ M ∈ ℕ 0 ∧ i = M + 1 → i = M + 1
19 17 18 eqtrd ⊢ M ∈ ℕ 0 ∧ i = M + 1 → if i = 0 n ∈ ℕ 0 ⟼ n + 1 i = M + 1
20 peano2nn0 ⊢ M ∈ ℕ 0 → M + 1 ∈ ℕ 0
21 9 19 20 20 fvmptd ⊢ M ∈ ℕ 0 → i ∈ ℕ 0 ⟼ if i = 0 n ∈ ℕ 0 ⟼ n + 1 i ⁡ M + 1 = M + 1
22 3 4 5 8 21 seqp1d ⊢ M ∈ ℕ 0 → seq 0 f ∈ V , j ∈ V ⟼ n ∈ ℕ 0 ⟼ IterComp ⁡ f ⁡ n + 1 ⁡ 1 i ∈ ℕ 0 ⟼ if i = 0 n ∈ ℕ 0 ⟼ n + 1 i ⁡ M + 1 = Ack ⁡ M f ∈ V , j ∈ V ⟼ n ∈ ℕ 0 ⟼ IterComp ⁡ f ⁡ n + 1 ⁡ 1 M + 1
23 eqidd ⊢ M ∈ ℕ 0 → f ∈ V , j ∈ V ⟼ n ∈ ℕ 0 ⟼ IterComp ⁡ f ⁡ n + 1 ⁡ 1 = f ∈ V , j ∈ V ⟼ n ∈ ℕ 0 ⟼ IterComp ⁡ f ⁡ n + 1 ⁡ 1
24 fveq2 ⊢ f = Ack ⁡ M → IterComp ⁡ f = IterComp ⁡ Ack ⁡ M
25 24 fveq1d ⊢ f = Ack ⁡ M → IterComp ⁡ f ⁡ n + 1 = IterComp ⁡ Ack ⁡ M ⁡ n + 1
26 25 fveq1d ⊢ f = Ack ⁡ M → IterComp ⁡ f ⁡ n + 1 ⁡ 1 = IterComp ⁡ Ack ⁡ M ⁡ n + 1 ⁡ 1
27 26 mpteq2dv ⊢ f = Ack ⁡ M → n ∈ ℕ 0 ⟼ IterComp ⁡ f ⁡ n + 1 ⁡ 1 = n ∈ ℕ 0 ⟼ IterComp ⁡ Ack ⁡ M ⁡ n + 1 ⁡ 1
28 27 ad2antrl ⊢ M ∈ ℕ 0 ∧ f = Ack ⁡ M ∧ j = M + 1 → n ∈ ℕ 0 ⟼ IterComp ⁡ f ⁡ n + 1 ⁡ 1 = n ∈ ℕ 0 ⟼ IterComp ⁡ Ack ⁡ M ⁡ n + 1 ⁡ 1
29 fvexd ⊢ M ∈ ℕ 0 → Ack ⁡ M ∈ V
30 ovexd ⊢ M ∈ ℕ 0 → M + 1 ∈ V
31 nn0ex ⊢ ℕ 0 ∈ V
32 31 mptex ⊢ n ∈ ℕ 0 ⟼ IterComp ⁡ Ack ⁡ M ⁡ n + 1 ⁡ 1 ∈ V
33 32 a1i ⊢ M ∈ ℕ 0 → n ∈ ℕ 0 ⟼ IterComp ⁡ Ack ⁡ M ⁡ n + 1 ⁡ 1 ∈ V
34 23 28 29 30 33 ovmpod ⊢ M ∈ ℕ 0 → Ack ⁡ M f ∈ V , j ∈ V ⟼ n ∈ ℕ 0 ⟼ IterComp ⁡ f ⁡ n + 1 ⁡ 1 M + 1 = n ∈ ℕ 0 ⟼ IterComp ⁡ Ack ⁡ M ⁡ n + 1 ⁡ 1
35 22 34 eqtrd ⊢ M ∈ ℕ 0 → seq 0 f ∈ V , j ∈ V ⟼ n ∈ ℕ 0 ⟼ IterComp ⁡ f ⁡ n + 1 ⁡ 1 i ∈ ℕ 0 ⟼ if i = 0 n ∈ ℕ 0 ⟼ n + 1 i ⁡ M + 1 = n ∈ ℕ 0 ⟼ IterComp ⁡ Ack ⁡ M ⁡ n + 1 ⁡ 1
36 2 35 eqtrid ⊢ M ∈ ℕ 0 → Ack ⁡ M + 1 = n ∈ ℕ 0 ⟼ IterComp ⁡ Ack ⁡ M ⁡ n + 1 ⁡ 1