Step | Hyp | Ref
| Expression |
1 | | 012of.g |
. . . . . 6
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) |
2 | 1 | frechashgf1o 10305 |
. . . . 5
⊢ 𝐺:ω–1-1-onto→ℕ0 |
3 | | f1ocnv 5420 |
. . . . 5
⊢ (𝐺:ω–1-1-onto→ℕ0 → ◡𝐺:ℕ0–1-1-onto→ω) |
4 | | f1of 5407 |
. . . . 5
⊢ (◡𝐺:ℕ0–1-1-onto→ω → ◡𝐺:ℕ0⟶ω) |
5 | 2, 3, 4 | mp2b 8 |
. . . 4
⊢ ◡𝐺:ℕ0⟶ω |
6 | | 0nn0 9084 |
. . . . 5
⊢ 0 ∈
ℕ0 |
7 | | 1nn0 9085 |
. . . . 5
⊢ 1 ∈
ℕ0 |
8 | | prssi 3710 |
. . . . 5
⊢ ((0
∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1}
⊆ ℕ0) |
9 | 6, 7, 8 | mp2an 423 |
. . . 4
⊢ {0, 1}
⊆ ℕ0 |
10 | | fssres 5338 |
. . . 4
⊢ ((◡𝐺:ℕ0⟶ω ∧
{0, 1} ⊆ ℕ0) → (◡𝐺 ↾ {0, 1}):{0,
1}⟶ω) |
11 | 5, 9, 10 | mp2an 423 |
. . 3
⊢ (◡𝐺 ↾ {0, 1}):{0,
1}⟶ω |
12 | | ffn 5312 |
. . 3
⊢ ((◡𝐺 ↾ {0, 1}):{0, 1}⟶ω
→ (◡𝐺 ↾ {0, 1}) Fn {0, 1}) |
13 | 11, 12 | ax-mp 5 |
. 2
⊢ (◡𝐺 ↾ {0, 1}) Fn {0, 1} |
14 | | fvres 5485 |
. . . 4
⊢ (𝑗 ∈ {0, 1} → ((◡𝐺 ↾ {0, 1})‘𝑗) = (◡𝐺‘𝑗)) |
15 | | elpri 3579 |
. . . . 5
⊢ (𝑗 ∈ {0, 1} → (𝑗 = 0 ∨ 𝑗 = 1)) |
16 | | fveq2 5461 |
. . . . . . 7
⊢ (𝑗 = 0 → (◡𝐺‘𝑗) = (◡𝐺‘0)) |
17 | | 0zd 9158 |
. . . . . . . . . . 11
⊢ (⊤
→ 0 ∈ ℤ) |
18 | 17, 1 | frec2uz0d 10276 |
. . . . . . . . . 10
⊢ (⊤
→ (𝐺‘∅) =
0) |
19 | 18 | mptru 1341 |
. . . . . . . . 9
⊢ (𝐺‘∅) =
0 |
20 | | peano1 4547 |
. . . . . . . . . 10
⊢ ∅
∈ ω |
21 | | f1ocnvfv 5720 |
. . . . . . . . . 10
⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ ∅ ∈
ω) → ((𝐺‘∅) = 0 → (◡𝐺‘0) = ∅)) |
22 | 2, 20, 21 | mp2an 423 |
. . . . . . . . 9
⊢ ((𝐺‘∅) = 0 →
(◡𝐺‘0) = ∅) |
23 | 19, 22 | ax-mp 5 |
. . . . . . . 8
⊢ (◡𝐺‘0) = ∅ |
24 | | 0lt2o 6378 |
. . . . . . . 8
⊢ ∅
∈ 2o |
25 | 23, 24 | eqeltri 2227 |
. . . . . . 7
⊢ (◡𝐺‘0) ∈
2o |
26 | 16, 25 | eqeltrdi 2245 |
. . . . . 6
⊢ (𝑗 = 0 → (◡𝐺‘𝑗) ∈ 2o) |
27 | | fveq2 5461 |
. . . . . . 7
⊢ (𝑗 = 1 → (◡𝐺‘𝑗) = (◡𝐺‘1)) |
28 | | df-1o 6353 |
. . . . . . . . . . 11
⊢
1o = suc ∅ |
29 | 28 | fveq2i 5464 |
. . . . . . . . . 10
⊢ (𝐺‘1o) = (𝐺‘suc
∅) |
30 | 20 | a1i 9 |
. . . . . . . . . . . 12
⊢ (⊤
→ ∅ ∈ ω) |
31 | 17, 1, 30 | frec2uzsucd 10278 |
. . . . . . . . . . 11
⊢ (⊤
→ (𝐺‘suc
∅) = ((𝐺‘∅) + 1)) |
32 | 31 | mptru 1341 |
. . . . . . . . . 10
⊢ (𝐺‘suc ∅) = ((𝐺‘∅) +
1) |
33 | 19 | oveq1i 5824 |
. . . . . . . . . . 11
⊢ ((𝐺‘∅) + 1) = (0 +
1) |
34 | | 0p1e1 8926 |
. . . . . . . . . . 11
⊢ (0 + 1) =
1 |
35 | 33, 34 | eqtri 2175 |
. . . . . . . . . 10
⊢ ((𝐺‘∅) + 1) =
1 |
36 | 29, 32, 35 | 3eqtri 2179 |
. . . . . . . . 9
⊢ (𝐺‘1o) =
1 |
37 | | 1onn 6456 |
. . . . . . . . . 10
⊢
1o ∈ ω |
38 | | f1ocnvfv 5720 |
. . . . . . . . . 10
⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ 1o ∈
ω) → ((𝐺‘1o) = 1 → (◡𝐺‘1) = 1o)) |
39 | 2, 37, 38 | mp2an 423 |
. . . . . . . . 9
⊢ ((𝐺‘1o) = 1 →
(◡𝐺‘1) = 1o) |
40 | 36, 39 | ax-mp 5 |
. . . . . . . 8
⊢ (◡𝐺‘1) = 1o |
41 | | 1lt2o 6379 |
. . . . . . . 8
⊢
1o ∈ 2o |
42 | 40, 41 | eqeltri 2227 |
. . . . . . 7
⊢ (◡𝐺‘1) ∈
2o |
43 | 27, 42 | eqeltrdi 2245 |
. . . . . 6
⊢ (𝑗 = 1 → (◡𝐺‘𝑗) ∈ 2o) |
44 | 26, 43 | jaoi 706 |
. . . . 5
⊢ ((𝑗 = 0 ∨ 𝑗 = 1) → (◡𝐺‘𝑗) ∈ 2o) |
45 | 15, 44 | syl 14 |
. . . 4
⊢ (𝑗 ∈ {0, 1} → (◡𝐺‘𝑗) ∈ 2o) |
46 | 14, 45 | eqeltrd 2231 |
. . 3
⊢ (𝑗 ∈ {0, 1} → ((◡𝐺 ↾ {0, 1})‘𝑗) ∈ 2o) |
47 | 46 | rgen 2507 |
. 2
⊢
∀𝑗 ∈ {0,
1} ((◡𝐺 ↾ {0, 1})‘𝑗) ∈ 2o |
48 | | ffnfv 5618 |
. 2
⊢ ((◡𝐺 ↾ {0, 1}):{0, 1}⟶2o
↔ ((◡𝐺 ↾ {0, 1}) Fn {0, 1} ∧
∀𝑗 ∈ {0, 1}
((◡𝐺 ↾ {0, 1})‘𝑗) ∈ 2o)) |
49 | 13, 47, 48 | mpbir2an 927 |
1
⊢ (◡𝐺 ↾ {0, 1}):{0,
1}⟶2o |