Metamath Proof Explorer

Theorem ackendofnn0

Description: The Ackermann function at any nonnegative integer is an endofunction on the nonnegative integers. (Contributed by AV, 8-May-2024)

Ref Expression
Assertion ackendofnn0 ( 𝑀 ∈ ℕ0 → ( Ack ‘ 𝑀 ) : ℕ0 ⟶ ℕ0 )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑥 = 0 → ( Ack ‘ 𝑥 ) = ( Ack ‘ 0 ) )
2 1 feq1d ⊢ ( 𝑥 = 0 → ( ( Ack ‘ 𝑥 ) : ℕ0 ⟶ ℕ0 ↔ ( Ack ‘ 0 ) : ℕ0 ⟶ ℕ0 ) )
3 fveq2 ⊢ ( 𝑥 = 𝑦 → ( Ack ‘ 𝑥 ) = ( Ack ‘ 𝑦 ) )
4 3 feq1d ⊢ ( 𝑥 = 𝑦 → ( ( Ack ‘ 𝑥 ) : ℕ0 ⟶ ℕ0 ↔ ( Ack ‘ 𝑦 ) : ℕ0 ⟶ ℕ0 ) )
5 fveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( Ack ‘ 𝑥 ) = ( Ack ‘ ( 𝑦 + 1 ) ) )
6 5 feq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( Ack ‘ 𝑥 ) : ℕ0 ⟶ ℕ0 ↔ ( Ack ‘ ( 𝑦 + 1 ) ) : ℕ0 ⟶ ℕ0 ) )
7 fveq2 ⊢ ( 𝑥 = 𝑀 → ( Ack ‘ 𝑥 ) = ( Ack ‘ 𝑀 ) )
8 7 feq1d ⊢ ( 𝑥 = 𝑀 → ( ( Ack ‘ 𝑥 ) : ℕ0 ⟶ ℕ0 ↔ ( Ack ‘ 𝑀 ) : ℕ0 ⟶ ℕ0 ) )
9 ackval0 ⊢ ( Ack ‘ 0 ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 + 1 ) )
10 peano2nn0 ⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 + 1 ) ∈ ℕ0 )
11 9 10 fmpti ⊢ ( Ack ‘ 0 ) : ℕ0 ⟶ ℕ0
12 nn0ex ⊢ ℕ0 ∈ V
13 12 a1i ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( Ack ‘ 𝑦 ) : ℕ0 ⟶ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ℕ0 ∈ V )
14 simplr ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( Ack ‘ 𝑦 ) : ℕ0 ⟶ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( Ack ‘ 𝑦 ) : ℕ0 ⟶ ℕ0 )
15 10 adantl ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( Ack ‘ 𝑦 ) : ℕ0 ⟶ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 + 1 ) ∈ ℕ0 )
16 13 14 15 itcovalendof ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( Ack ‘ 𝑦 ) : ℕ0 ⟶ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( IterComp ‘ ( Ack ‘ 𝑦 ) ) ‘ ( 𝑛 + 1 ) ) : ℕ0 ⟶ ℕ0 )
17 1nn0 ⊢ 1 ∈ ℕ0
18 ffvelrn ⊢ ( ( ( ( IterComp ‘ ( Ack ‘ 𝑦 ) ) ‘ ( 𝑛 + 1 ) ) : ℕ0 ⟶ ℕ0 ∧ 1 ∈ ℕ0 ) → ( ( ( IterComp ‘ ( Ack ‘ 𝑦 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) ∈ ℕ0 )
19 16 17 18 sylancl ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( Ack ‘ 𝑦 ) : ℕ0 ⟶ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( IterComp ‘ ( Ack ‘ 𝑦 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) ∈ ℕ0 )
20 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ ( Ack ‘ 𝑦 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ ( Ack ‘ 𝑦 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) )
21 19 20 fmptd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( Ack ‘ 𝑦 ) : ℕ0 ⟶ ℕ0 ) → ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ ( Ack ‘ 𝑦 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) ) : ℕ0 ⟶ ℕ0 )
22 ackvalsuc1mpt ⊢ ( 𝑦 ∈ ℕ0 → ( Ack ‘ ( 𝑦 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ ( Ack ‘ 𝑦 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) ) )
23 22 adantr ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( Ack ‘ 𝑦 ) : ℕ0 ⟶ ℕ0 ) → ( Ack ‘ ( 𝑦 + 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ ( Ack ‘ 𝑦 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) ) )
24 23 feq1d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( Ack ‘ 𝑦 ) : ℕ0 ⟶ ℕ0 ) → ( ( Ack ‘ ( 𝑦 + 1 ) ) : ℕ0 ⟶ ℕ0 ↔ ( 𝑛 ∈ ℕ0 ↦ ( ( ( IterComp ‘ ( Ack ‘ 𝑦 ) ) ‘ ( 𝑛 + 1 ) ) ‘ 1 ) ) : ℕ0 ⟶ ℕ0 ) )
25 21 24 mpbird ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( Ack ‘ 𝑦 ) : ℕ0 ⟶ ℕ0 ) → ( Ack ‘ ( 𝑦 + 1 ) ) : ℕ0 ⟶ ℕ0 )
26 25 ex ⊢ ( 𝑦 ∈ ℕ0 → ( ( Ack ‘ 𝑦 ) : ℕ0 ⟶ ℕ0 → ( Ack ‘ ( 𝑦 + 1 ) ) : ℕ0 ⟶ ℕ0 ) )
27 2 4 6 8 11 26 nn0ind ⊢ ( 𝑀 ∈ ℕ0 → ( Ack ‘ 𝑀 ) : ℕ0 ⟶ ℕ0 )