Step | Hyp | Ref
| Expression |
1 | | df-ack 45424 |
. . 3
⊢ Ack =
seq0((𝑓 ∈ V, 𝑗 ∈ V ↦ (𝑛 ∈ ℕ0
↦ (((IterComp‘𝑓)‘(𝑛 + 1))‘1))), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖))) |
2 | 1 | fveq1i 6652 |
. 2
⊢
(Ack‘(𝑀 + 1))
= (seq0((𝑓 ∈ V, 𝑗 ∈ V ↦ (𝑛 ∈ ℕ0
↦ (((IterComp‘𝑓)‘(𝑛 + 1))‘1))), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖)))‘(𝑀 + 1)) |
3 | | nn0uz 12305 |
. . . 4
⊢
ℕ0 = (ℤ≥‘0) |
4 | | id 22 |
. . . 4
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℕ0) |
5 | | eqid 2759 |
. . . 4
⊢ (𝑀 + 1) = (𝑀 + 1) |
6 | 1 | eqcomi 2768 |
. . . . . 6
⊢
seq0((𝑓 ∈ V,
𝑗 ∈ V ↦ (𝑛 ∈ ℕ0
↦ (((IterComp‘𝑓)‘(𝑛 + 1))‘1))), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖))) = Ack |
7 | 6 | fveq1i 6652 |
. . . . 5
⊢
(seq0((𝑓 ∈ V,
𝑗 ∈ V ↦ (𝑛 ∈ ℕ0
↦ (((IterComp‘𝑓)‘(𝑛 + 1))‘1))), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖)))‘𝑀) = (Ack‘𝑀) |
8 | 7 | a1i 11 |
. . . 4
⊢ (𝑀 ∈ ℕ0
→ (seq0((𝑓 ∈ V,
𝑗 ∈ V ↦ (𝑛 ∈ ℕ0
↦ (((IterComp‘𝑓)‘(𝑛 + 1))‘1))), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖)))‘𝑀) = (Ack‘𝑀)) |
9 | | eqidd 2760 |
. . . . 5
⊢ (𝑀 ∈ ℕ0
→ (𝑖 ∈
ℕ0 ↦ if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖))) |
10 | | nn0p1gt0 11948 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ0
→ 0 < (𝑀 +
1)) |
11 | 10 | gt0ne0d 11227 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ≠
0) |
12 | 11 | adantr 485 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝑖 = (𝑀 + 1)) → (𝑀 + 1) ≠ 0) |
13 | | neeq1 3011 |
. . . . . . . . . 10
⊢ (𝑖 = (𝑀 + 1) → (𝑖 ≠ 0 ↔ (𝑀 + 1) ≠ 0)) |
14 | 13 | adantl 486 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝑖 = (𝑀 + 1)) → (𝑖 ≠ 0 ↔ (𝑀 + 1) ≠ 0)) |
15 | 12, 14 | mpbird 260 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑖 = (𝑀 + 1)) → 𝑖 ≠ 0) |
16 | 15 | neneqd 2954 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑖 = (𝑀 + 1)) → ¬ 𝑖 = 0) |
17 | 16 | iffalsed 4424 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑖 = (𝑀 + 1)) → if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖) = 𝑖) |
18 | | simpr 489 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑖 = (𝑀 + 1)) → 𝑖 = (𝑀 + 1)) |
19 | 17, 18 | eqtrd 2794 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑖 = (𝑀 + 1)) → if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖) = (𝑀 + 1)) |
20 | | peano2nn0 11959 |
. . . . 5
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
ℕ0) |
21 | 9, 19, 20, 20 | fvmptd 6759 |
. . . 4
⊢ (𝑀 ∈ ℕ0
→ ((𝑖 ∈
ℕ0 ↦ if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖))‘(𝑀 + 1)) = (𝑀 + 1)) |
22 | 3, 4, 5, 8, 21 | seqp1d 13420 |
. . 3
⊢ (𝑀 ∈ ℕ0
→ (seq0((𝑓 ∈ V,
𝑗 ∈ V ↦ (𝑛 ∈ ℕ0
↦ (((IterComp‘𝑓)‘(𝑛 + 1))‘1))), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖)))‘(𝑀 + 1)) = ((Ack‘𝑀)(𝑓 ∈ V, 𝑗 ∈ V ↦ (𝑛 ∈ ℕ0 ↦
(((IterComp‘𝑓)‘(𝑛 + 1))‘1)))(𝑀 + 1))) |
23 | | eqidd 2760 |
. . . 4
⊢ (𝑀 ∈ ℕ0
→ (𝑓 ∈ V, 𝑗 ∈ V ↦ (𝑛 ∈ ℕ0
↦ (((IterComp‘𝑓)‘(𝑛 + 1))‘1))) = (𝑓 ∈ V, 𝑗 ∈ V ↦ (𝑛 ∈ ℕ0 ↦
(((IterComp‘𝑓)‘(𝑛 + 1))‘1)))) |
24 | | fveq2 6651 |
. . . . . . . 8
⊢ (𝑓 = (Ack‘𝑀) → (IterComp‘𝑓) = (IterComp‘(Ack‘𝑀))) |
25 | 24 | fveq1d 6653 |
. . . . . . 7
⊢ (𝑓 = (Ack‘𝑀) → ((IterComp‘𝑓)‘(𝑛 + 1)) = ((IterComp‘(Ack‘𝑀))‘(𝑛 + 1))) |
26 | 25 | fveq1d 6653 |
. . . . . 6
⊢ (𝑓 = (Ack‘𝑀) → (((IterComp‘𝑓)‘(𝑛 + 1))‘1) =
(((IterComp‘(Ack‘𝑀))‘(𝑛 + 1))‘1)) |
27 | 26 | mpteq2dv 5121 |
. . . . 5
⊢ (𝑓 = (Ack‘𝑀) → (𝑛 ∈ ℕ0 ↦
(((IterComp‘𝑓)‘(𝑛 + 1))‘1)) = (𝑛 ∈ ℕ0 ↦
(((IterComp‘(Ack‘𝑀))‘(𝑛 + 1))‘1))) |
28 | 27 | ad2antrl 728 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ (𝑓 = (Ack‘𝑀) ∧ 𝑗 = (𝑀 + 1))) → (𝑛 ∈ ℕ0 ↦
(((IterComp‘𝑓)‘(𝑛 + 1))‘1)) = (𝑛 ∈ ℕ0 ↦
(((IterComp‘(Ack‘𝑀))‘(𝑛 + 1))‘1))) |
29 | | fvexd 6666 |
. . . 4
⊢ (𝑀 ∈ ℕ0
→ (Ack‘𝑀) ∈
V) |
30 | | ovexd 7178 |
. . . 4
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
V) |
31 | | nn0ex 11925 |
. . . . . 6
⊢
ℕ0 ∈ V |
32 | 31 | mptex 6970 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
↦ (((IterComp‘(Ack‘𝑀))‘(𝑛 + 1))‘1)) ∈ V |
33 | 32 | a1i 11 |
. . . 4
⊢ (𝑀 ∈ ℕ0
→ (𝑛 ∈
ℕ0 ↦ (((IterComp‘(Ack‘𝑀))‘(𝑛 + 1))‘1)) ∈ V) |
34 | 23, 28, 29, 30, 33 | ovmpod 7290 |
. . 3
⊢ (𝑀 ∈ ℕ0
→ ((Ack‘𝑀)(𝑓 ∈ V, 𝑗 ∈ V ↦ (𝑛 ∈ ℕ0 ↦
(((IterComp‘𝑓)‘(𝑛 + 1))‘1)))(𝑀 + 1)) = (𝑛 ∈ ℕ0 ↦
(((IterComp‘(Ack‘𝑀))‘(𝑛 + 1))‘1))) |
35 | 22, 34 | eqtrd 2794 |
. 2
⊢ (𝑀 ∈ ℕ0
→ (seq0((𝑓 ∈ V,
𝑗 ∈ V ↦ (𝑛 ∈ ℕ0
↦ (((IterComp‘𝑓)‘(𝑛 + 1))‘1))), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖)))‘(𝑀 + 1)) = (𝑛 ∈ ℕ0 ↦
(((IterComp‘(Ack‘𝑀))‘(𝑛 + 1))‘1))) |
36 | 2, 35 | syl5eq 2806 |
1
⊢ (𝑀 ∈ ℕ0
→ (Ack‘(𝑀 + 1))
= (𝑛 ∈
ℕ0 ↦ (((IterComp‘(Ack‘𝑀))‘(𝑛 + 1))‘1))) |