Metamath Proof Explorer

Theorem ackvalsucsucval

Description: The Ackermann function at the successors. This is the third equation of Péter's definition of the Ackermann function. (Contributed by AV, 8-May-2024)

Ref Expression
Assertion ackvalsucsucval ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( Ack ‘ ( 𝑀 + 1 ) ) ‘ ( 𝑁 + 1 ) ) = ( ( Ack ‘ 𝑀 ) ‘ ( ( Ack ‘ ( 𝑀 + 1 ) ) ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
2 ackvalsuc1 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ ( 𝑁 + 1 ) ∈ ℕ0 ) → ( ( Ack ‘ ( 𝑀 + 1 ) ) ‘ ( 𝑁 + 1 ) ) = ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( ( 𝑁 + 1 ) + 1 ) ) ‘ 1 ) )
3 1 2 sylan2 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( Ack ‘ ( 𝑀 + 1 ) ) ‘ ( 𝑁 + 1 ) ) = ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( ( 𝑁 + 1 ) + 1 ) ) ‘ 1 ) )
4 fvexd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( Ack ‘ 𝑀 ) ∈ V )
5 1 adantl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ℕ0 )
6 eqidd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) = ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) )
7 itcovalsucov ⊢ ( ( ( Ack ‘ 𝑀 ) ∈ V ∧ ( 𝑁 + 1 ) ∈ ℕ0 ∧ ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) = ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) ) → ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( ( 𝑁 + 1 ) + 1 ) ) = ( ( Ack ‘ 𝑀 ) ∘ ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) ) )
8 4 5 6 7 syl3anc ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( ( 𝑁 + 1 ) + 1 ) ) = ( ( Ack ‘ 𝑀 ) ∘ ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) ) )
9 8 fveq1d ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( ( 𝑁 + 1 ) + 1 ) ) ‘ 1 ) = ( ( ( Ack ‘ 𝑀 ) ∘ ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) ) ‘ 1 ) )
10 ackfnnn0 ⊢ ( 𝑀 ∈ ℕ0 → ( Ack ‘ 𝑀 ) Fn ℕ0 )
11 10 adantr ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( Ack ‘ 𝑀 ) Fn ℕ0 )
12 nn0ex ⊢ ℕ0 ∈ V
13 12 a1i ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ℕ0 ∈ V )
14 ackendofnn0 ⊢ ( 𝑀 ∈ ℕ0 → ( Ack ‘ 𝑀 ) : ℕ0 ⟶ ℕ0 )
15 14 adantr ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( Ack ‘ 𝑀 ) : ℕ0 ⟶ ℕ0 )
16 simpr ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
17 13 15 16 itcovalendof ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ 𝑁 ) : ℕ0 ⟶ ℕ0 )
18 17 ffnd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ 𝑁 ) Fn ℕ0 )
19 17 frnd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ran ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ 𝑁 ) ⊆ ℕ0 )
20 fnco ⊢ ( ( ( Ack ‘ 𝑀 ) Fn ℕ0 ∧ ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ 𝑁 ) Fn ℕ0 ∧ ran ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ 𝑁 ) ⊆ ℕ0 ) → ( ( Ack ‘ 𝑀 ) ∘ ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ 𝑁 ) ) Fn ℕ0 )
21 11 18 19 20 syl3anc ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( Ack ‘ 𝑀 ) ∘ ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ 𝑁 ) ) Fn ℕ0 )
22 eqidd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ 𝑁 ) = ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ 𝑁 ) )
23 itcovalsucov ⊢ ( ( ( Ack ‘ 𝑀 ) ∈ V ∧ 𝑁 ∈ ℕ0 ∧ ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ 𝑁 ) = ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ 𝑁 ) ) → ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) = ( ( Ack ‘ 𝑀 ) ∘ ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ 𝑁 ) ) )
24 4 16 22 23 syl3anc ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) = ( ( Ack ‘ 𝑀 ) ∘ ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ 𝑁 ) ) )
25 24 fneq1d ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) Fn ℕ0 ↔ ( ( Ack ‘ 𝑀 ) ∘ ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ 𝑁 ) ) Fn ℕ0 ) )
26 21 25 mpbird ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) Fn ℕ0 )
27 1nn0 ⊢ 1 ∈ ℕ0
28 fvco2 ⊢ ( ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) Fn ℕ0 ∧ 1 ∈ ℕ0 ) → ( ( ( Ack ‘ 𝑀 ) ∘ ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) ) ‘ 1 ) = ( ( Ack ‘ 𝑀 ) ‘ ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) ‘ 1 ) ) )
29 26 27 28 sylancl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( ( Ack ‘ 𝑀 ) ∘ ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) ) ‘ 1 ) = ( ( Ack ‘ 𝑀 ) ‘ ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) ‘ 1 ) ) )
30 9 29 eqtrd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( ( 𝑁 + 1 ) + 1 ) ) ‘ 1 ) = ( ( Ack ‘ 𝑀 ) ‘ ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) ‘ 1 ) ) )
31 ackvalsuc1 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( Ack ‘ ( 𝑀 + 1 ) ) ‘ 𝑁 ) = ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) ‘ 1 ) )
32 31 eqcomd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) ‘ 1 ) = ( ( Ack ‘ ( 𝑀 + 1 ) ) ‘ 𝑁 ) )
33 32 fveq2d ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( Ack ‘ 𝑀 ) ‘ ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) ‘ 1 ) ) = ( ( Ack ‘ 𝑀 ) ‘ ( ( Ack ‘ ( 𝑀 + 1 ) ) ‘ 𝑁 ) ) )
34 3 30 33 3eqtrd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( Ack ‘ ( 𝑀 + 1 ) ) ‘ ( 𝑁 + 1 ) ) = ( ( Ack ‘ 𝑀 ) ‘ ( ( Ack ‘ ( 𝑀 + 1 ) ) ‘ 𝑁 ) ) )