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