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

Metamath Proof Explorer

Theorem ackvalsuc1

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

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

Proof

Step Hyp Ref Expression
1 ackvalsuc1mpt ⊢ ( 𝑀 ∈ ℕ0 → ( Ack ‘ ( 𝑀 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) ) )
2 1 adantr ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( Ack ‘ ( 𝑀 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) ) )
3 fvoveq1 ⊢ ( 𝑛 = 𝑁 → ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑛 + 1 ) ) = ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) )
4 3 fveq1d ⊢ ( 𝑛 = 𝑁 → ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) = ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) ‘ 1 ) )
5 4 adantl ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑛 = 𝑁 ) → ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) = ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) ‘ 1 ) )
6 simpr ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
7 fvexd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) ‘ 1 ) ∈ V )
8 2 5 6 7 fvmptd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( Ack ‘ ( 𝑀 + 1 ) ) ‘ 𝑁 ) = ( ( ( IterComp ‘ ( Ack ‘ 𝑀 ) ) ‘ ( 𝑁 + 1 ) ) ‘ 1 ) )