This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑀 ∈ ℕ0 → ( Ack ‘ ( 𝑀 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) ) )

Proof

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