Proof of Theorem ackvalsucsucval
Step | Hyp | Ref
| Expression |
1 | | peano2nn0 11959 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
2 | | ackvalsuc1 45443 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ (𝑁 + 1) ∈
ℕ0) → ((Ack‘(𝑀 + 1))‘(𝑁 + 1)) = (((IterComp‘(Ack‘𝑀))‘((𝑁 + 1) + 1))‘1)) |
3 | 1, 2 | sylan2 596 |
. 2
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((Ack‘(𝑀 + 1))‘(𝑁 + 1)) = (((IterComp‘(Ack‘𝑀))‘((𝑁 + 1) + 1))‘1)) |
4 | | fvexd 6666 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (Ack‘𝑀) ∈ V) |
5 | 1 | adantl 486 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 + 1) ∈
ℕ0) |
6 | | eqidd 2760 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((IterComp‘(Ack‘𝑀))‘(𝑁 + 1)) = ((IterComp‘(Ack‘𝑀))‘(𝑁 + 1))) |
7 | | itcovalsucov 45432 |
. . . . 5
⊢
(((Ack‘𝑀)
∈ V ∧ (𝑁 + 1)
∈ ℕ0 ∧ ((IterComp‘(Ack‘𝑀))‘(𝑁 + 1)) = ((IterComp‘(Ack‘𝑀))‘(𝑁 + 1))) →
((IterComp‘(Ack‘𝑀))‘((𝑁 + 1) + 1)) = ((Ack‘𝑀) ∘ ((IterComp‘(Ack‘𝑀))‘(𝑁 + 1)))) |
8 | 4, 5, 6, 7 | syl3anc 1369 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((IterComp‘(Ack‘𝑀))‘((𝑁 + 1) + 1)) = ((Ack‘𝑀) ∘ ((IterComp‘(Ack‘𝑀))‘(𝑁 + 1)))) |
9 | 8 | fveq1d 6653 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (((IterComp‘(Ack‘𝑀))‘((𝑁 + 1) + 1))‘1) = (((Ack‘𝑀) ∘
((IterComp‘(Ack‘𝑀))‘(𝑁 + 1)))‘1)) |
10 | | ackfnnn0 45449 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ0
→ (Ack‘𝑀) Fn
ℕ0) |
11 | 10 | adantr 485 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (Ack‘𝑀) Fn ℕ0) |
12 | | nn0ex 11925 |
. . . . . . . . 9
⊢
ℕ0 ∈ V |
13 | 12 | a1i 11 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ℕ0 ∈ V) |
14 | | ackendofnn0 45448 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ0
→ (Ack‘𝑀):ℕ0⟶ℕ0) |
15 | 14 | adantr 485 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (Ack‘𝑀):ℕ0⟶ℕ0) |
16 | | simpr 489 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝑁 ∈
ℕ0) |
17 | 13, 15, 16 | itcovalendof 45433 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((IterComp‘(Ack‘𝑀))‘𝑁):ℕ0⟶ℕ0) |
18 | 17 | ffnd 6492 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((IterComp‘(Ack‘𝑀))‘𝑁) Fn ℕ0) |
19 | 17 | frnd 6498 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ran ((IterComp‘(Ack‘𝑀))‘𝑁) ⊆
ℕ0) |
20 | | fnco 6441 |
. . . . . 6
⊢
(((Ack‘𝑀) Fn
ℕ0 ∧ ((IterComp‘(Ack‘𝑀))‘𝑁) Fn ℕ0 ∧ ran
((IterComp‘(Ack‘𝑀))‘𝑁) ⊆ ℕ0) →
((Ack‘𝑀) ∘
((IterComp‘(Ack‘𝑀))‘𝑁)) Fn ℕ0) |
21 | 11, 18, 19, 20 | syl3anc 1369 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((Ack‘𝑀) ∘ ((IterComp‘(Ack‘𝑀))‘𝑁)) Fn ℕ0) |
22 | | eqidd 2760 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((IterComp‘(Ack‘𝑀))‘𝑁) = ((IterComp‘(Ack‘𝑀))‘𝑁)) |
23 | | itcovalsucov 45432 |
. . . . . . 7
⊢
(((Ack‘𝑀)
∈ V ∧ 𝑁 ∈
ℕ0 ∧ ((IterComp‘(Ack‘𝑀))‘𝑁) = ((IterComp‘(Ack‘𝑀))‘𝑁)) → ((IterComp‘(Ack‘𝑀))‘(𝑁 + 1)) = ((Ack‘𝑀) ∘ ((IterComp‘(Ack‘𝑀))‘𝑁))) |
24 | 4, 16, 22, 23 | syl3anc 1369 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((IterComp‘(Ack‘𝑀))‘(𝑁 + 1)) = ((Ack‘𝑀) ∘ ((IterComp‘(Ack‘𝑀))‘𝑁))) |
25 | 24 | fneq1d 6420 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (((IterComp‘(Ack‘𝑀))‘(𝑁 + 1)) Fn ℕ0 ↔
((Ack‘𝑀) ∘
((IterComp‘(Ack‘𝑀))‘𝑁)) Fn ℕ0)) |
26 | 21, 25 | mpbird 260 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((IterComp‘(Ack‘𝑀))‘(𝑁 + 1)) Fn
ℕ0) |
27 | | 1nn0 11935 |
. . . 4
⊢ 1 ∈
ℕ0 |
28 | | fvco2 6742 |
. . . 4
⊢
((((IterComp‘(Ack‘𝑀))‘(𝑁 + 1)) Fn ℕ0 ∧ 1 ∈
ℕ0) → (((Ack‘𝑀) ∘ ((IterComp‘(Ack‘𝑀))‘(𝑁 + 1)))‘1) = ((Ack‘𝑀)‘(((IterComp‘(Ack‘𝑀))‘(𝑁 + 1))‘1))) |
29 | 26, 27, 28 | sylancl 590 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (((Ack‘𝑀) ∘ ((IterComp‘(Ack‘𝑀))‘(𝑁 + 1)))‘1) = ((Ack‘𝑀)‘(((IterComp‘(Ack‘𝑀))‘(𝑁 + 1))‘1))) |
30 | 9, 29 | eqtrd 2794 |
. 2
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (((IterComp‘(Ack‘𝑀))‘((𝑁 + 1) + 1))‘1) = ((Ack‘𝑀)‘(((IterComp‘(Ack‘𝑀))‘(𝑁 + 1))‘1))) |
31 | | ackvalsuc1 45443 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((Ack‘(𝑀 + 1))‘𝑁) = (((IterComp‘(Ack‘𝑀))‘(𝑁 + 1))‘1)) |
32 | 31 | eqcomd 2765 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (((IterComp‘(Ack‘𝑀))‘(𝑁 + 1))‘1) = ((Ack‘(𝑀 + 1))‘𝑁)) |
33 | 32 | fveq2d 6655 |
. 2
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((Ack‘𝑀)‘(((IterComp‘(Ack‘𝑀))‘(𝑁 + 1))‘1)) = ((Ack‘𝑀)‘((Ack‘(𝑀 + 1))‘𝑁))) |
34 | 3, 30, 33 | 3eqtrd 2798 |
1
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((Ack‘(𝑀 + 1))‘(𝑁 + 1)) = ((Ack‘𝑀)‘((Ack‘(𝑀 + 1))‘𝑁))) |