Step | Hyp | Ref
| Expression |
1 | | iswomnimap 7088 |
. 2
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) |
2 | | fveq1 5460 |
. . . . . . . . 9
⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (𝑔‘𝑥) = ((◡𝐺 ∘ 𝑓)‘𝑥)) |
3 | 2 | eqeq1d 2163 |
. . . . . . . 8
⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → ((𝑔‘𝑥) = 1o ↔ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o)) |
4 | 3 | ralbidv 2454 |
. . . . . . 7
⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o ↔ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o)) |
5 | 4 | dcbid 824 |
. . . . . 6
⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o ↔ DECID
∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o)) |
6 | | simplr 520 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) |
7 | | iswomninnlem.g |
. . . . . . . . . . 11
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) |
8 | 7 | 012of 13506 |
. . . . . . . . . 10
⊢ (◡𝐺 ↾ {0, 1}):{0,
1}⟶2o |
9 | | elmapi 6604 |
. . . . . . . . . 10
⊢ (𝑓 ∈ ({0, 1}
↑𝑚 𝐴) → 𝑓:𝐴⟶{0, 1}) |
10 | | fco2 5329 |
. . . . . . . . . 10
⊢ (((◡𝐺 ↾ {0, 1}):{0, 1}⟶2o
∧ 𝑓:𝐴⟶{0, 1}) → (◡𝐺 ∘ 𝑓):𝐴⟶2o) |
11 | 8, 9, 10 | sylancr 411 |
. . . . . . . . 9
⊢ (𝑓 ∈ ({0, 1}
↑𝑚 𝐴) → (◡𝐺 ∘ 𝑓):𝐴⟶2o) |
12 | 11 | adantl 275 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → (◡𝐺 ∘ 𝑓):𝐴⟶2o) |
13 | | 2onn 6457 |
. . . . . . . . . 10
⊢
2o ∈ ω |
14 | 13 | a1i 9 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → 2o
∈ ω) |
15 | | simpl 108 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → 𝐴 ∈ 𝑉) |
16 | 14, 15 | elmapd 6596 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → ((◡𝐺 ∘ 𝑓) ∈ (2o
↑𝑚 𝐴) ↔ (◡𝐺 ∘ 𝑓):𝐴⟶2o)) |
17 | 12, 16 | mpbird 166 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → (◡𝐺 ∘ 𝑓) ∈ (2o
↑𝑚 𝐴)) |
18 | 17 | adantlr 469 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → (◡𝐺 ∘ 𝑓) ∈ (2o
↑𝑚 𝐴)) |
19 | 5, 6, 18 | rspcdva 2818 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) →
DECID ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) |
20 | | nfv 1505 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝐴 ∈ 𝑉 |
21 | | nfcv 2296 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(2o ↑𝑚
𝐴) |
22 | | nfra1 2485 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o |
23 | 22 | nfdc 1636 |
. . . . . . . . . 10
⊢
Ⅎ𝑥DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o |
24 | 21, 23 | nfralxy 2492 |
. . . . . . . . 9
⊢
Ⅎ𝑥∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o |
25 | 20, 24 | nfan 1542 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) |
26 | | nfv 1505 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑓 ∈ ({0, 1}
↑𝑚 𝐴) |
27 | 25, 26 | nfan 1542 |
. . . . . . 7
⊢
Ⅎ𝑥((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) |
28 | 9 | ad2antlr 481 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑓:𝐴⟶{0, 1}) |
29 | | fvco3 5532 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴⟶{0, 1} ∧ 𝑥 ∈ 𝐴) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥))) |
30 | 28, 29 | sylancom 417 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥))) |
31 | 30 | eqeq1d 2163 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → (((◡𝐺 ∘ 𝑓)‘𝑥) = 1o ↔ (◡𝐺‘(𝑓‘𝑥)) = 1o)) |
32 | | df-1o 6353 |
. . . . . . . . . . . 12
⊢
1o = suc ∅ |
33 | 32 | fveq2i 5464 |
. . . . . . . . . . 11
⊢ (𝐺‘1o) = (𝐺‘suc
∅) |
34 | | 0zd 9158 |
. . . . . . . . . . . . 13
⊢ (⊤
→ 0 ∈ ℤ) |
35 | | peano1 4547 |
. . . . . . . . . . . . . 14
⊢ ∅
∈ ω |
36 | 35 | a1i 9 |
. . . . . . . . . . . . 13
⊢ (⊤
→ ∅ ∈ ω) |
37 | 34, 7, 36 | frec2uzsucd 10278 |
. . . . . . . . . . . 12
⊢ (⊤
→ (𝐺‘suc
∅) = ((𝐺‘∅) + 1)) |
38 | 37 | mptru 1341 |
. . . . . . . . . . 11
⊢ (𝐺‘suc ∅) = ((𝐺‘∅) +
1) |
39 | 34, 7 | frec2uz0d 10276 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ (𝐺‘∅) =
0) |
40 | 39 | mptru 1341 |
. . . . . . . . . . . . 13
⊢ (𝐺‘∅) =
0 |
41 | 40 | oveq1i 5824 |
. . . . . . . . . . . 12
⊢ ((𝐺‘∅) + 1) = (0 +
1) |
42 | | 0p1e1 8926 |
. . . . . . . . . . . 12
⊢ (0 + 1) =
1 |
43 | 41, 42 | eqtri 2175 |
. . . . . . . . . . 11
⊢ ((𝐺‘∅) + 1) =
1 |
44 | 33, 38, 43 | 3eqtri 2179 |
. . . . . . . . . 10
⊢ (𝐺‘1o) =
1 |
45 | 44 | eqeq2i 2165 |
. . . . . . . . 9
⊢ ((𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘1o) ↔ (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = 1) |
46 | 7 | frechashgf1o 10305 |
. . . . . . . . . . . . 13
⊢ 𝐺:ω–1-1-onto→ℕ0 |
47 | | f1ocnv 5420 |
. . . . . . . . . . . . 13
⊢ (𝐺:ω–1-1-onto→ℕ0 → ◡𝐺:ℕ0–1-1-onto→ω) |
48 | | f1of 5407 |
. . . . . . . . . . . . 13
⊢ (◡𝐺:ℕ0–1-1-onto→ω → ◡𝐺:ℕ0⟶ω) |
49 | 46, 47, 48 | mp2b 8 |
. . . . . . . . . . . 12
⊢ ◡𝐺:ℕ0⟶ω |
50 | 49 | a1i 9 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → ◡𝐺:ℕ0⟶ω) |
51 | | 0nn0 9084 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℕ0 |
52 | | 1nn0 9085 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℕ0 |
53 | | prssi 3710 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1}
⊆ ℕ0) |
54 | 51, 52, 53 | mp2an 423 |
. . . . . . . . . . . 12
⊢ {0, 1}
⊆ ℕ0 |
55 | | simpr 109 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
56 | 28, 55 | ffvelrnd 5596 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ {0, 1}) |
57 | 54, 56 | sseldi 3122 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈
ℕ0) |
58 | 50, 57 | ffvelrnd 5596 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → (◡𝐺‘(𝑓‘𝑥)) ∈ ω) |
59 | | 1onn 6456 |
. . . . . . . . . . 11
⊢
1o ∈ ω |
60 | | f1of1 5406 |
. . . . . . . . . . . . 13
⊢ (𝐺:ω–1-1-onto→ℕ0 → 𝐺:ω–1-1→ℕ0) |
61 | 46, 60 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ 𝐺:ω–1-1→ℕ0 |
62 | | f1fveq 5713 |
. . . . . . . . . . . 12
⊢ ((𝐺:ω–1-1→ℕ0 ∧ ((◡𝐺‘(𝑓‘𝑥)) ∈ ω ∧ 1o ∈
ω)) → ((𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘1o) ↔ (◡𝐺‘(𝑓‘𝑥)) = 1o)) |
63 | 61, 62 | mpan 421 |
. . . . . . . . . . 11
⊢ (((◡𝐺‘(𝑓‘𝑥)) ∈ ω ∧ 1o ∈
ω) → ((𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘1o) ↔ (◡𝐺‘(𝑓‘𝑥)) = 1o)) |
64 | 59, 63 | mpan2 422 |
. . . . . . . . . 10
⊢ ((◡𝐺‘(𝑓‘𝑥)) ∈ ω → ((𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘1o) ↔ (◡𝐺‘(𝑓‘𝑥)) = 1o)) |
65 | 58, 64 | syl 14 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘1o) ↔ (◡𝐺‘(𝑓‘𝑥)) = 1o)) |
66 | 45, 65 | bitr3id 193 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘(◡𝐺‘(𝑓‘𝑥))) = 1 ↔ (◡𝐺‘(𝑓‘𝑥)) = 1o)) |
67 | | f1ocnvfv2 5719 |
. . . . . . . . . 10
⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑓‘𝑥) ∈ ℕ0) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥)) |
68 | 46, 57, 67 | sylancr 411 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥)) |
69 | 68 | eqeq1d 2163 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘(◡𝐺‘(𝑓‘𝑥))) = 1 ↔ (𝑓‘𝑥) = 1)) |
70 | 31, 66, 69 | 3bitr2d 215 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → (((◡𝐺 ∘ 𝑓)‘𝑥) = 1o ↔ (𝑓‘𝑥) = 1)) |
71 | 27, 70 | ralbida 2448 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → (∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o ↔ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) |
72 | 71 | dcbid 824 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) →
(DECID ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o ↔ DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) |
73 | 19, 72 | mpbid 146 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) →
DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) |
74 | 73 | ralrimiva 2527 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) → ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) |
75 | | fveq1 5460 |
. . . . . . . . 9
⊢ (𝑓 = (𝐺 ∘ 𝑔) → (𝑓‘𝑥) = ((𝐺 ∘ 𝑔)‘𝑥)) |
76 | 75 | eqeq1d 2163 |
. . . . . . . 8
⊢ (𝑓 = (𝐺 ∘ 𝑔) → ((𝑓‘𝑥) = 1 ↔ ((𝐺 ∘ 𝑔)‘𝑥) = 1)) |
77 | 76 | ralbidv 2454 |
. . . . . . 7
⊢ (𝑓 = (𝐺 ∘ 𝑔) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 ↔ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1)) |
78 | 77 | dcbid 824 |
. . . . . 6
⊢ (𝑓 = (𝐺 ∘ 𝑔) → (DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 ↔ DECID
∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1)) |
79 | | simplr 520 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) |
80 | 7 | 2o01f 13507 |
. . . . . . . 8
⊢ (𝐺 ↾
2o):2o⟶{0, 1} |
81 | | elmapi 6604 |
. . . . . . . . 9
⊢ (𝑔 ∈ (2o
↑𝑚 𝐴) → 𝑔:𝐴⟶2o) |
82 | 81 | adantl 275 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → 𝑔:𝐴⟶2o) |
83 | | fco2 5329 |
. . . . . . . 8
⊢ (((𝐺 ↾
2o):2o⟶{0, 1} ∧ 𝑔:𝐴⟶2o) → (𝐺 ∘ 𝑔):𝐴⟶{0, 1}) |
84 | 80, 82, 83 | sylancr 411 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → (𝐺 ∘ 𝑔):𝐴⟶{0, 1}) |
85 | | prexg 4166 |
. . . . . . . . . 10
⊢ ((0
∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1}
∈ V) |
86 | 51, 52, 85 | mp2an 423 |
. . . . . . . . 9
⊢ {0, 1}
∈ V |
87 | 86 | a1i 9 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → {0, 1} ∈ V) |
88 | | simpll 519 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → 𝐴 ∈ 𝑉) |
89 | 87, 88 | elmapd 6596 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → ((𝐺 ∘ 𝑔) ∈ ({0, 1} ↑𝑚
𝐴) ↔ (𝐺 ∘ 𝑔):𝐴⟶{0, 1})) |
90 | 84, 89 | mpbird 166 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → (𝐺 ∘ 𝑔) ∈ ({0, 1} ↑𝑚
𝐴)) |
91 | 78, 79, 90 | rspcdva 2818 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → DECID ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1) |
92 | | nfcv 2296 |
. . . . . . . . . 10
⊢
Ⅎ𝑥({0,
1} ↑𝑚 𝐴) |
93 | | nfra1 2485 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 |
94 | 93 | nfdc 1636 |
. . . . . . . . . 10
⊢
Ⅎ𝑥DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 |
95 | 92, 94 | nfralxy 2492 |
. . . . . . . . 9
⊢
Ⅎ𝑥∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 |
96 | 20, 95 | nfan 1542 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) |
97 | | nfv 1505 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑔 ∈ (2o
↑𝑚 𝐴) |
98 | 96, 97 | nfan 1542 |
. . . . . . 7
⊢
Ⅎ𝑥((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) |
99 | 81 | ad2antlr 481 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑔:𝐴⟶2o) |
100 | | fvco3 5532 |
. . . . . . . . . 10
⊢ ((𝑔:𝐴⟶2o ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝑔)‘𝑥) = (𝐺‘(𝑔‘𝑥))) |
101 | 99, 100 | sylancom 417 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝑔)‘𝑥) = (𝐺‘(𝑔‘𝑥))) |
102 | 101 | eqeq1d 2163 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 1 ↔ (𝐺‘(𝑔‘𝑥)) = 1)) |
103 | | f1of 5407 |
. . . . . . . . . . 11
⊢ (𝐺:ω–1-1-onto→ℕ0 → 𝐺:ω⟶ℕ0) |
104 | 46, 103 | mp1i 10 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝐺:ω⟶ℕ0) |
105 | | omelon 4562 |
. . . . . . . . . . . . . 14
⊢ ω
∈ On |
106 | 105 | onelssi 4384 |
. . . . . . . . . . . . 13
⊢
(2o ∈ ω → 2o ⊆
ω) |
107 | 13, 106 | mp1i 10 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 2o ⊆
ω) |
108 | 99, 107 | fssd 5325 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑔:𝐴⟶ω) |
109 | | simpr 109 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
110 | 108, 109 | ffvelrnd 5596 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ω) |
111 | 104, 110 | ffvelrnd 5596 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘(𝑔‘𝑥)) ∈
ℕ0) |
112 | | f1ocnvfv 5720 |
. . . . . . . . . . . . 13
⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ 1o ∈
ω) → ((𝐺‘1o) = 1 → (◡𝐺‘1) = 1o)) |
113 | 46, 59, 112 | mp2an 423 |
. . . . . . . . . . . 12
⊢ ((𝐺‘1o) = 1 →
(◡𝐺‘1) = 1o) |
114 | 44, 113 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (◡𝐺‘1) = 1o |
115 | 114 | eqeq2i 2165 |
. . . . . . . . . 10
⊢ ((◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘1) ↔ (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = 1o) |
116 | | f1of1 5406 |
. . . . . . . . . . . . 13
⊢ (◡𝐺:ℕ0–1-1-onto→ω → ◡𝐺:ℕ0–1-1→ω) |
117 | 46, 47, 116 | mp2b 8 |
. . . . . . . . . . . 12
⊢ ◡𝐺:ℕ0–1-1→ω |
118 | | f1fveq 5713 |
. . . . . . . . . . . 12
⊢ ((◡𝐺:ℕ0–1-1→ω ∧ ((𝐺‘(𝑔‘𝑥)) ∈ ℕ0 ∧ 1 ∈
ℕ0)) → ((◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘1) ↔ (𝐺‘(𝑔‘𝑥)) = 1)) |
119 | 117, 118 | mpan 421 |
. . . . . . . . . . 11
⊢ (((𝐺‘(𝑔‘𝑥)) ∈ ℕ0 ∧ 1 ∈
ℕ0) → ((◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘1) ↔ (𝐺‘(𝑔‘𝑥)) = 1)) |
120 | 52, 119 | mpan2 422 |
. . . . . . . . . 10
⊢ ((𝐺‘(𝑔‘𝑥)) ∈ ℕ0 → ((◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘1) ↔ (𝐺‘(𝑔‘𝑥)) = 1)) |
121 | 115, 120 | bitr3id 193 |
. . . . . . . . 9
⊢ ((𝐺‘(𝑔‘𝑥)) ∈ ℕ0 → ((◡𝐺‘(𝐺‘(𝑔‘𝑥))) = 1o ↔ (𝐺‘(𝑔‘𝑥)) = 1)) |
122 | 111, 121 | syl 14 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((◡𝐺‘(𝐺‘(𝑔‘𝑥))) = 1o ↔ (𝐺‘(𝑔‘𝑥)) = 1)) |
123 | | f1ocnvfv1 5718 |
. . . . . . . . . 10
⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑔‘𝑥) ∈ ω) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥)) |
124 | 46, 110, 123 | sylancr 411 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥)) |
125 | 124 | eqeq1d 2163 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((◡𝐺‘(𝐺‘(𝑔‘𝑥))) = 1o ↔ (𝑔‘𝑥) = 1o)) |
126 | 102, 122,
125 | 3bitr2d 215 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 1 ↔ (𝑔‘𝑥) = 1o)) |
127 | 98, 126 | ralbida 2448 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1 ↔ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) |
128 | 127 | dcbid 824 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → (DECID
∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1 ↔ DECID
∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) |
129 | 91, 128 | mpbid 146 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) |
130 | 129 | ralrimiva 2527 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) → ∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) |
131 | 74, 130 | impbida 586 |
. 2
⊢ (𝐴 ∈ 𝑉 → (∀𝑔 ∈ (2o
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o ↔ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) |
132 | 1, 131 | bitrd 187 |
1
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) |