Step | Hyp | Ref
| Expression |
1 | | ismkvmap 7076 |
. 2
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅))) |
2 | | nfv 1505 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝐴 ∈ 𝑉 |
3 | | nfcv 2296 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(2o ↑𝑚
𝐴) |
4 | | nfra1 2485 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o |
5 | 4 | nfn 1635 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 ¬
∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o |
6 | | nfre1 2497 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ |
7 | 5, 6 | nfim 1549 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(¬
∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅) |
8 | 3, 7 | nfralxy 2492 |
. . . . . . . . 9
⊢
Ⅎ𝑥∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅) |
9 | 2, 8 | nfan 1542 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) |
10 | | nfv 1505 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑓 ∈ ({0, 1}
↑𝑚 𝐴) |
11 | 9, 10 | nfan 1542 |
. . . . . . 7
⊢
Ⅎ𝑥((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) |
12 | | ismkvnnlem.g |
. . . . . . . . . . . 12
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) |
13 | 12 | frechashgf1o 10305 |
. . . . . . . . . . 11
⊢ 𝐺:ω–1-1-onto→ℕ0 |
14 | | 0nn0 9084 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℕ0 |
15 | | 1nn0 9085 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℕ0 |
16 | | prssi 3710 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1}
⊆ ℕ0) |
17 | 14, 15, 16 | mp2an 423 |
. . . . . . . . . . . 12
⊢ {0, 1}
⊆ ℕ0 |
18 | | elmapi 6604 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ ({0, 1}
↑𝑚 𝐴) → 𝑓:𝐴⟶{0, 1}) |
19 | 18 | ad2antlr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑓:𝐴⟶{0, 1}) |
20 | | simpr 109 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
21 | 19, 20 | ffvelrnd 5596 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ {0, 1}) |
22 | 17, 21 | sseldi 3122 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈
ℕ0) |
23 | | f1ocnvfv2 5719 |
. . . . . . . . . . 11
⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑓‘𝑥) ∈ ℕ0) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥)) |
24 | 13, 22, 23 | sylancr 411 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥)) |
25 | 24 | adantr 274 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥)) |
26 | | fvco3 5532 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐴⟶{0, 1} ∧ 𝑥 ∈ 𝐴) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥))) |
27 | 19, 26 | sylancom 417 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥))) |
28 | 27 | adantr 274 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥))) |
29 | | simpr 109 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) |
30 | 28, 29 | eqtr3d 2189 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (◡𝐺‘(𝑓‘𝑥)) = 1o) |
31 | 30 | fveq2d 5465 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 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, 12, 36 | frec2uzsucd 10278 |
. . . . . . . . . . . 12
⊢ (⊤
→ (𝐺‘suc
∅) = ((𝐺‘∅) + 1)) |
38 | 37 | mptru 1341 |
. . . . . . . . . . 11
⊢ (𝐺‘suc ∅) = ((𝐺‘∅) +
1) |
39 | 34, 12 | 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 | 31, 44 | eqtrdi 2203 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = 1) |
46 | 25, 45 | eqtr3d 2189 |
. . . . . . . 8
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (𝑓‘𝑥) = 1) |
47 | 46 | ex 114 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → (((◡𝐺 ∘ 𝑓)‘𝑥) = 1o → (𝑓‘𝑥) = 1)) |
48 | 11, 47 | ralimdaa 2520 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → (∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o → ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) |
49 | 48 | con3d 621 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → (¬
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ¬ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o)) |
50 | | fveq1 5460 |
. . . . . . . . . 10
⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (𝑔‘𝑥) = ((◡𝐺 ∘ 𝑓)‘𝑥)) |
51 | 50 | eqeq1d 2163 |
. . . . . . . . 9
⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → ((𝑔‘𝑥) = 1o ↔ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o)) |
52 | 51 | ralbidv 2454 |
. . . . . . . 8
⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o ↔ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o)) |
53 | 52 | notbid 657 |
. . . . . . 7
⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o ↔ ¬ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o)) |
54 | 50 | eqeq1d 2163 |
. . . . . . . 8
⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → ((𝑔‘𝑥) = ∅ ↔ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅)) |
55 | 54 | rexbidv 2455 |
. . . . . . 7
⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ↔ ∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅)) |
56 | 53, 55 | imbi12d 233 |
. . . . . 6
⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → ((¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅) ↔ (¬ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅))) |
57 | | simplr 520 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) |
58 | 12 | 012of 13506 |
. . . . . . . 8
⊢ (◡𝐺 ↾ {0, 1}):{0,
1}⟶2o |
59 | 18 | adantl 275 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → 𝑓:𝐴⟶{0, 1}) |
60 | | fco2 5329 |
. . . . . . . 8
⊢ (((◡𝐺 ↾ {0, 1}):{0, 1}⟶2o
∧ 𝑓:𝐴⟶{0, 1}) → (◡𝐺 ∘ 𝑓):𝐴⟶2o) |
61 | 58, 59, 60 | sylancr 411 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → (◡𝐺 ∘ 𝑓):𝐴⟶2o) |
62 | | 2onn 6457 |
. . . . . . . . 9
⊢
2o ∈ ω |
63 | 62 | a1i 9 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → 2o
∈ ω) |
64 | | simpll 519 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → 𝐴 ∈ 𝑉) |
65 | 63, 64 | elmapd 6596 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → ((◡𝐺 ∘ 𝑓) ∈ (2o
↑𝑚 𝐴) ↔ (◡𝐺 ∘ 𝑓):𝐴⟶2o)) |
66 | 61, 65 | mpbird 166 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → (◡𝐺 ∘ 𝑓) ∈ (2o
↑𝑚 𝐴)) |
67 | 56, 57, 66 | rspcdva 2818 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → (¬
∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅)) |
68 | 24 | adantr 274 |
. . . . . . . 8
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥)) |
69 | 27 | eqeq1d 2163 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → (((◡𝐺 ∘ 𝑓)‘𝑥) = ∅ ↔ (◡𝐺‘(𝑓‘𝑥)) = ∅)) |
70 | 69 | biimpa 294 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (◡𝐺‘(𝑓‘𝑥)) = ∅) |
71 | 70 | fveq2d 5465 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘∅)) |
72 | 71, 40 | eqtrdi 2203 |
. . . . . . . 8
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = 0) |
73 | 68, 72 | eqtr3d 2189 |
. . . . . . 7
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (𝑓‘𝑥) = 0) |
74 | 73 | exp31 362 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → (𝑥 ∈ 𝐴 → (((◡𝐺 ∘ 𝑓)‘𝑥) = ∅ → (𝑓‘𝑥) = 0))) |
75 | 11, 74 | reximdai 2552 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → (∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅ → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) |
76 | 49, 67, 75 | 3syld 57 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → (¬
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) |
77 | 76 | ralrimiva 2527 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) → ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) |
78 | | nfcv 2296 |
. . . . . . . . . 10
⊢
Ⅎ𝑥({0,
1} ↑𝑚 𝐴) |
79 | | nfra1 2485 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 |
80 | 79 | nfn 1635 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 ¬
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 |
81 | | nfre1 2497 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 |
82 | 80, 81 | nfim 1549 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(¬
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0) |
83 | 78, 82 | nfralxy 2492 |
. . . . . . . . 9
⊢
Ⅎ𝑥∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0) |
84 | 2, 83 | nfan 1542 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) |
85 | | nfv 1505 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑔 ∈ (2o
↑𝑚 𝐴) |
86 | 84, 85 | nfan 1542 |
. . . . . . 7
⊢
Ⅎ𝑥((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) |
87 | | elmapi 6604 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ (2o
↑𝑚 𝐴) → 𝑔:𝐴⟶2o) |
88 | 87 | ad2antlr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑔:𝐴⟶2o) |
89 | | omelon 4562 |
. . . . . . . . . . . . . . . 16
⊢ ω
∈ On |
90 | 89 | onelssi 4384 |
. . . . . . . . . . . . . . 15
⊢
(2o ∈ ω → 2o ⊆
ω) |
91 | 62, 90 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
2o ⊆ ω |
92 | 91 | a1i 9 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 2o ⊆
ω) |
93 | 88, 92 | fssd 5325 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑔:𝐴⟶ω) |
94 | | simpr 109 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
95 | 93, 94 | ffvelrnd 5596 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ω) |
96 | | f1ocnvfv1 5718 |
. . . . . . . . . . 11
⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑔‘𝑥) ∈ ω) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥)) |
97 | 13, 95, 96 | sylancr 411 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥)) |
98 | 97 | adantr 274 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥)) |
99 | | fvco3 5532 |
. . . . . . . . . . . . . 14
⊢ ((𝑔:𝐴⟶2o ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝑔)‘𝑥) = (𝐺‘(𝑔‘𝑥))) |
100 | 88, 99 | sylancom 417 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝑔)‘𝑥) = (𝐺‘(𝑔‘𝑥))) |
101 | 100 | eqeq1d 2163 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 1 ↔ (𝐺‘(𝑔‘𝑥)) = 1)) |
102 | 101 | biimpa 294 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (𝐺‘(𝑔‘𝑥)) = 1) |
103 | 102 | fveq2d 5465 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘1)) |
104 | | 1onn 6456 |
. . . . . . . . . . . 12
⊢
1o ∈ ω |
105 | | f1ocnvfv 5720 |
. . . . . . . . . . . 12
⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ 1o ∈
ω) → ((𝐺‘1o) = 1 → (◡𝐺‘1) = 1o)) |
106 | 13, 104, 105 | mp2an 423 |
. . . . . . . . . . 11
⊢ ((𝐺‘1o) = 1 →
(◡𝐺‘1) = 1o) |
107 | 44, 106 | ax-mp 5 |
. . . . . . . . . 10
⊢ (◡𝐺‘1) = 1o |
108 | 103, 107 | eqtrdi 2203 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = 1o) |
109 | 98, 108 | eqtr3d 2189 |
. . . . . . . 8
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (𝑔‘𝑥) = 1o) |
110 | 109 | ex 114 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 1 → (𝑔‘𝑥) = 1o)) |
111 | 86, 110 | ralimdaa 2520 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1 → ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) |
112 | 111 | con3d 621 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → (¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ¬ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1)) |
113 | | fveq1 5460 |
. . . . . . . . . 10
⊢ (𝑓 = (𝐺 ∘ 𝑔) → (𝑓‘𝑥) = ((𝐺 ∘ 𝑔)‘𝑥)) |
114 | 113 | eqeq1d 2163 |
. . . . . . . . 9
⊢ (𝑓 = (𝐺 ∘ 𝑔) → ((𝑓‘𝑥) = 1 ↔ ((𝐺 ∘ 𝑔)‘𝑥) = 1)) |
115 | 114 | ralbidv 2454 |
. . . . . . . 8
⊢ (𝑓 = (𝐺 ∘ 𝑔) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 ↔ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1)) |
116 | 115 | notbid 657 |
. . . . . . 7
⊢ (𝑓 = (𝐺 ∘ 𝑔) → (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 ↔ ¬ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1)) |
117 | 113 | eqeq1d 2163 |
. . . . . . . 8
⊢ (𝑓 = (𝐺 ∘ 𝑔) → ((𝑓‘𝑥) = 0 ↔ ((𝐺 ∘ 𝑔)‘𝑥) = 0)) |
118 | 117 | rexbidv 2455 |
. . . . . . 7
⊢ (𝑓 = (𝐺 ∘ 𝑔) → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ↔ ∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0)) |
119 | 116, 118 | imbi12d 233 |
. . . . . 6
⊢ (𝑓 = (𝐺 ∘ 𝑔) → ((¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0) ↔ (¬ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0))) |
120 | | simplr 520 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) |
121 | 12 | 2o01f 13507 |
. . . . . . . 8
⊢ (𝐺 ↾
2o):2o⟶{0, 1} |
122 | 87 | adantl 275 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → 𝑔:𝐴⟶2o) |
123 | | fco2 5329 |
. . . . . . . 8
⊢ (((𝐺 ↾
2o):2o⟶{0, 1} ∧ 𝑔:𝐴⟶2o) → (𝐺 ∘ 𝑔):𝐴⟶{0, 1}) |
124 | 121, 122,
123 | sylancr 411 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → (𝐺 ∘ 𝑔):𝐴⟶{0, 1}) |
125 | | prexg 4166 |
. . . . . . . . . 10
⊢ ((0
∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1}
∈ V) |
126 | 14, 15, 125 | mp2an 423 |
. . . . . . . . 9
⊢ {0, 1}
∈ V |
127 | 126 | a1i 9 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → {0, 1} ∈ V) |
128 | | simpll 519 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → 𝐴 ∈ 𝑉) |
129 | 127, 128 | elmapd 6596 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → ((𝐺 ∘ 𝑔) ∈ ({0, 1} ↑𝑚
𝐴) ↔ (𝐺 ∘ 𝑔):𝐴⟶{0, 1})) |
130 | 124, 129 | mpbird 166 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → (𝐺 ∘ 𝑔) ∈ ({0, 1} ↑𝑚
𝐴)) |
131 | 119, 120,
130 | rspcdva 2818 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → (¬ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0)) |
132 | 97 | adantr 274 |
. . . . . . . 8
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥)) |
133 | 100 | eqeq1d 2163 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 0 ↔ (𝐺‘(𝑔‘𝑥)) = 0)) |
134 | 133 | biimpa 294 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (𝐺‘(𝑔‘𝑥)) = 0) |
135 | 134 | fveq2d 5465 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘0)) |
136 | | f1ocnvfv 5720 |
. . . . . . . . . . 11
⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ ∅ ∈
ω) → ((𝐺‘∅) = 0 → (◡𝐺‘0) = ∅)) |
137 | 13, 35, 136 | mp2an 423 |
. . . . . . . . . 10
⊢ ((𝐺‘∅) = 0 →
(◡𝐺‘0) = ∅) |
138 | 40, 137 | ax-mp 5 |
. . . . . . . . 9
⊢ (◡𝐺‘0) = ∅ |
139 | 135, 138 | eqtrdi 2203 |
. . . . . . . 8
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = ∅) |
140 | 132, 139 | eqtr3d 2189 |
. . . . . . 7
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (𝑔‘𝑥) = ∅) |
141 | 140 | exp31 362 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → (𝑥 ∈ 𝐴 → (((𝐺 ∘ 𝑔)‘𝑥) = 0 → (𝑔‘𝑥) = ∅))) |
142 | 86, 141 | reximdai 2552 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → (∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0 → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) |
143 | 112, 131,
142 | 3syld 57 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → (¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) |
144 | 143 | ralrimiva 2527 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) → ∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) |
145 | 77, 144 | impbida 586 |
. 2
⊢ (𝐴 ∈ 𝑉 → (∀𝑔 ∈ (2o
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅) ↔ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))) |
146 | 1, 145 | bitrd 187 |
1
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))) |