Metamath Proof Explorer

Theorem ackval0012

Description: The Ackermann function at (0,0), (0,1), (0,2). (Contributed by AV, 2-May-2024)

Ref Expression
Assertion ackval0012 ⟨ ( ( Ack ‘ 0 ) ‘ 0 ) , ( ( Ack ‘ 0 ) ‘ 1 ) , ( ( Ack ‘ 0 ) ‘ 2 ) ⟩ = ⟨ 1 , 2 , 3 ⟩

Proof

Step Hyp Ref Expression
1 ackval0 ⊢ ( Ack ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) )
2 oveq1 ⊢ ( 𝑛 = 0 → ( 𝑛 + 1 ) = ( 0 + 1 ) )
3 0p1e1 ⊢ ( 0 + 1 ) = 1
4 2 3 eqtrdi ⊢ ( 𝑛 = 0 → ( 𝑛 + 1 ) = 1 )
5 0nn0 ⊢ 0 ∈ ℕ0
6 5 a1i ⊢ ( ( Ack ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) → 0 ∈ ℕ0 )
7 1nn0 ⊢ 1 ∈ ℕ0
8 7 a1i ⊢ ( ( Ack ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) → 1 ∈ ℕ0 )
9 1 4 6 8 fvmptd3 ⊢ ( ( Ack ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) → ( ( Ack ‘ 0 ) ‘ 0 ) = 1 )
10 oveq1 ⊢ ( 𝑛 = 1 → ( 𝑛 + 1 ) = ( 1 + 1 ) )
11 1p1e2 ⊢ ( 1 + 1 ) = 2
12 10 11 eqtrdi ⊢ ( 𝑛 = 1 → ( 𝑛 + 1 ) = 2 )
13 2nn0 ⊢ 2 ∈ ℕ0
14 13 a1i ⊢ ( ( Ack ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) → 2 ∈ ℕ0 )
15 1 12 8 14 fvmptd3 ⊢ ( ( Ack ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) → ( ( Ack ‘ 0 ) ‘ 1 ) = 2 )
16 oveq1 ⊢ ( 𝑛 = 2 → ( 𝑛 + 1 ) = ( 2 + 1 ) )
17 2p1e3 ⊢ ( 2 + 1 ) = 3
18 16 17 eqtrdi ⊢ ( 𝑛 = 2 → ( 𝑛 + 1 ) = 3 )
19 3nn0 ⊢ 3 ∈ ℕ0
20 19 a1i ⊢ ( ( Ack ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) → 3 ∈ ℕ0 )
21 1 18 14 20 fvmptd3 ⊢ ( ( Ack ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) → ( ( Ack ‘ 0 ) ‘ 2 ) = 3 )
22 9 15 21 oteq123d ⊢ ( ( Ack ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) ) → ⟨ ( ( Ack ‘ 0 ) ‘ 0 ) , ( ( Ack ‘ 0 ) ‘ 1 ) , ( ( Ack ‘ 0 ) ‘ 2 ) ⟩ = ⟨ 1 , 2 , 3 ⟩ )
23 1 22 ax-mp ⊢ ⟨ ( ( Ack ‘ 0 ) ‘ 0 ) , ( ( Ack ‘ 0 ) ‘ 1 ) , ( ( Ack ‘ 0 ) ‘ 2 ) ⟩ = ⟨ 1 , 2 , 3 ⟩