Step | Hyp | Ref
| Expression |
1 | | isomnimap 6959 |
. 2
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o))) |
2 | | fveq1 5374 |
. . . . . . . . 9
⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (𝑔‘𝑥) = ((◡𝐺 ∘ 𝑓)‘𝑥)) |
3 | 2 | eqeq1d 2123 |
. . . . . . . 8
⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → ((𝑔‘𝑥) = ∅ ↔ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅)) |
4 | 3 | rexbidv 2412 |
. . . . . . 7
⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ↔ ∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅)) |
5 | 2 | eqeq1d 2123 |
. . . . . . . 8
⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → ((𝑔‘𝑥) = 1o ↔ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o)) |
6 | 5 | ralbidv 2411 |
. . . . . . 7
⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → (∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o ↔ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o)) |
7 | 4, 6 | orbi12d 765 |
. . . . . 6
⊢ (𝑔 = (◡𝐺 ∘ 𝑓) → ((∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ↔ (∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o))) |
8 | | simplr 502 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) |
9 | | isomninnlem.g |
. . . . . . . . . . . . 13
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) |
10 | 9 | frechashgf1o 10094 |
. . . . . . . . . . . 12
⊢ 𝐺:ω–1-1-onto→ℕ0 |
11 | | f1ocnv 5336 |
. . . . . . . . . . . 12
⊢ (𝐺:ω–1-1-onto→ℕ0 → ◡𝐺:ℕ0–1-1-onto→ω) |
12 | | f1of 5323 |
. . . . . . . . . . . 12
⊢ (◡𝐺:ℕ0–1-1-onto→ω → ◡𝐺:ℕ0⟶ω) |
13 | 10, 11, 12 | mp2b 8 |
. . . . . . . . . . 11
⊢ ◡𝐺:ℕ0⟶ω |
14 | | 0nn0 8896 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℕ0 |
15 | | 1nn0 8897 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ0 |
16 | | prssi 3644 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1}
⊆ ℕ0) |
17 | 14, 15, 16 | mp2an 420 |
. . . . . . . . . . 11
⊢ {0, 1}
⊆ ℕ0 |
18 | | fssres 5256 |
. . . . . . . . . . 11
⊢ ((◡𝐺:ℕ0⟶ω ∧
{0, 1} ⊆ ℕ0) → (◡𝐺 ↾ {0, 1}):{0,
1}⟶ω) |
19 | 13, 17, 18 | mp2an 420 |
. . . . . . . . . 10
⊢ (◡𝐺 ↾ {0, 1}):{0,
1}⟶ω |
20 | | ffn 5230 |
. . . . . . . . . 10
⊢ ((◡𝐺 ↾ {0, 1}):{0, 1}⟶ω
→ (◡𝐺 ↾ {0, 1}) Fn {0, 1}) |
21 | 19, 20 | ax-mp 7 |
. . . . . . . . 9
⊢ (◡𝐺 ↾ {0, 1}) Fn {0, 1} |
22 | | fvres 5399 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ {0, 1} → ((◡𝐺 ↾ {0, 1})‘𝑗) = (◡𝐺‘𝑗)) |
23 | | elpri 3516 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ {0, 1} → (𝑗 = 0 ∨ 𝑗 = 1)) |
24 | | fveq2 5375 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 0 → (◡𝐺‘𝑗) = (◡𝐺‘0)) |
25 | | 0zd 8970 |
. . . . . . . . . . . . . . . . . 18
⊢ (⊤
→ 0 ∈ ℤ) |
26 | 25, 9 | frec2uz0d 10065 |
. . . . . . . . . . . . . . . . 17
⊢ (⊤
→ (𝐺‘∅) =
0) |
27 | 26 | mptru 1323 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺‘∅) =
0 |
28 | | peano1 4468 |
. . . . . . . . . . . . . . . . 17
⊢ ∅
∈ ω |
29 | | f1ocnvfv 5634 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ ∅ ∈
ω) → ((𝐺‘∅) = 0 → (◡𝐺‘0) = ∅)) |
30 | 10, 28, 29 | mp2an 420 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺‘∅) = 0 →
(◡𝐺‘0) = ∅) |
31 | 27, 30 | ax-mp 7 |
. . . . . . . . . . . . . . 15
⊢ (◡𝐺‘0) = ∅ |
32 | | 0lt2o 6292 |
. . . . . . . . . . . . . . 15
⊢ ∅
∈ 2o |
33 | 31, 32 | eqeltri 2187 |
. . . . . . . . . . . . . 14
⊢ (◡𝐺‘0) ∈
2o |
34 | 24, 33 | syl6eqel 2205 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 0 → (◡𝐺‘𝑗) ∈ 2o) |
35 | | fveq2 5375 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 1 → (◡𝐺‘𝑗) = (◡𝐺‘1)) |
36 | | df-1o 6267 |
. . . . . . . . . . . . . . . . . 18
⊢
1o = suc ∅ |
37 | 36 | fveq2i 5378 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺‘1o) = (𝐺‘suc
∅) |
38 | 28 | a1i 9 |
. . . . . . . . . . . . . . . . . . 19
⊢ (⊤
→ ∅ ∈ ω) |
39 | 25, 9, 38 | frec2uzsucd 10067 |
. . . . . . . . . . . . . . . . . 18
⊢ (⊤
→ (𝐺‘suc
∅) = ((𝐺‘∅) + 1)) |
40 | 39 | mptru 1323 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺‘suc ∅) = ((𝐺‘∅) +
1) |
41 | 27 | oveq1i 5738 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺‘∅) + 1) = (0 +
1) |
42 | | 0p1e1 8744 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 + 1) =
1 |
43 | 41, 42 | eqtri 2135 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺‘∅) + 1) =
1 |
44 | 37, 40, 43 | 3eqtri 2139 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺‘1o) =
1 |
45 | | 1onn 6370 |
. . . . . . . . . . . . . . . . 17
⊢
1o ∈ ω |
46 | | f1ocnvfv 5634 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ 1o ∈
ω) → ((𝐺‘1o) = 1 → (◡𝐺‘1) = 1o)) |
47 | 10, 45, 46 | mp2an 420 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺‘1o) = 1 →
(◡𝐺‘1) = 1o) |
48 | 44, 47 | ax-mp 7 |
. . . . . . . . . . . . . . 15
⊢ (◡𝐺‘1) = 1o |
49 | | 1lt2o 6293 |
. . . . . . . . . . . . . . 15
⊢
1o ∈ 2o |
50 | 48, 49 | eqeltri 2187 |
. . . . . . . . . . . . . 14
⊢ (◡𝐺‘1) ∈
2o |
51 | 35, 50 | syl6eqel 2205 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 1 → (◡𝐺‘𝑗) ∈ 2o) |
52 | 34, 51 | jaoi 688 |
. . . . . . . . . . . 12
⊢ ((𝑗 = 0 ∨ 𝑗 = 1) → (◡𝐺‘𝑗) ∈ 2o) |
53 | 23, 52 | syl 14 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ {0, 1} → (◡𝐺‘𝑗) ∈ 2o) |
54 | 22, 53 | eqeltrd 2191 |
. . . . . . . . . 10
⊢ (𝑗 ∈ {0, 1} → ((◡𝐺 ↾ {0, 1})‘𝑗) ∈ 2o) |
55 | 54 | rgen 2459 |
. . . . . . . . 9
⊢
∀𝑗 ∈ {0,
1} ((◡𝐺 ↾ {0, 1})‘𝑗) ∈ 2o |
56 | | ffnfv 5532 |
. . . . . . . . 9
⊢ ((◡𝐺 ↾ {0, 1}):{0, 1}⟶2o
↔ ((◡𝐺 ↾ {0, 1}) Fn {0, 1} ∧
∀𝑗 ∈ {0, 1}
((◡𝐺 ↾ {0, 1})‘𝑗) ∈ 2o)) |
57 | 21, 55, 56 | mpbir2an 909 |
. . . . . . . 8
⊢ (◡𝐺 ↾ {0, 1}):{0,
1}⟶2o |
58 | | elmapi 6518 |
. . . . . . . . 9
⊢ (𝑓 ∈ ({0, 1}
↑𝑚 𝐴) → 𝑓:𝐴⟶{0, 1}) |
59 | 58 | adantl 273 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → 𝑓:𝐴⟶{0, 1}) |
60 | | fco2 5247 |
. . . . . . . 8
⊢ (((◡𝐺 ↾ {0, 1}):{0, 1}⟶2o
∧ 𝑓:𝐴⟶{0, 1}) → (◡𝐺 ∘ 𝑓):𝐴⟶2o) |
61 | 57, 59, 60 | sylancr 408 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → (◡𝐺 ∘ 𝑓):𝐴⟶2o) |
62 | | 2onn 6371 |
. . . . . . . . 9
⊢
2o ∈ ω |
63 | 62 | a1i 9 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → 2o
∈ ω) |
64 | | simpll 501 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → 𝐴 ∈ 𝑉) |
65 | 63, 64 | elmapd 6510 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → ((◡𝐺 ∘ 𝑓) ∈ (2o
↑𝑚 𝐴) ↔ (◡𝐺 ∘ 𝑓):𝐴⟶2o)) |
66 | 61, 65 | mpbird 166 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → (◡𝐺 ∘ 𝑓) ∈ (2o
↑𝑚 𝐴)) |
67 | 7, 8, 66 | rspcdva 2765 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → (∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o)) |
68 | | nfv 1491 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝐴 ∈ 𝑉 |
69 | | nfcv 2255 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(2o ↑𝑚
𝐴) |
70 | | nfre1 2450 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ |
71 | | nfra1 2440 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o |
72 | 70, 71 | nfor 1536 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) |
73 | 69, 72 | nfralxy 2445 |
. . . . . . . . 9
⊢
Ⅎ𝑥∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) |
74 | 68, 73 | nfan 1527 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) |
75 | | nfv 1491 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑓 ∈ ({0, 1}
↑𝑚 𝐴) |
76 | 74, 75 | nfan 1527 |
. . . . . . 7
⊢
Ⅎ𝑥((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) |
77 | | simplr 502 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) |
78 | 77, 58 | syl 14 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑓:𝐴⟶{0, 1}) |
79 | | simpr 109 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
80 | 78, 79 | ffvelrnd 5510 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ {0, 1}) |
81 | 17, 80 | sseldi 3061 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈
ℕ0) |
82 | | f1ocnvfv2 5633 |
. . . . . . . . . . 11
⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑓‘𝑥) ∈ ℕ0) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥)) |
83 | 10, 81, 82 | sylancr 408 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥)) |
84 | 83 | adantr 272 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥)) |
85 | | fvco3 5446 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐴⟶{0, 1} ∧ 𝑥 ∈ 𝐴) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥))) |
86 | 78, 85 | sylancom 414 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥))) |
87 | 86 | eqeq1d 2123 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → (((◡𝐺 ∘ 𝑓)‘𝑥) = ∅ ↔ (◡𝐺‘(𝑓‘𝑥)) = ∅)) |
88 | 87 | biimpa 292 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (◡𝐺‘(𝑓‘𝑥)) = ∅) |
89 | 88 | fveq2d 5379 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘∅)) |
90 | 89, 27 | syl6eq 2163 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = 0) |
91 | 84, 90 | eqtr3d 2149 |
. . . . . . . 8
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅) → (𝑓‘𝑥) = 0) |
92 | 91 | exp31 359 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → (𝑥 ∈ 𝐴 → (((◡𝐺 ∘ 𝑓)‘𝑥) = ∅ → (𝑓‘𝑥) = 0))) |
93 | 76, 92 | reximdai 2504 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → (∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅ → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) |
94 | 83 | adantr 272 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝑓‘𝑥)) |
95 | 86 | adantr 272 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → ((◡𝐺 ∘ 𝑓)‘𝑥) = (◡𝐺‘(𝑓‘𝑥))) |
96 | | simpr 109 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) |
97 | 95, 96 | eqtr3d 2149 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (◡𝐺‘(𝑓‘𝑥)) = 1o) |
98 | 97 | fveq2d 5379 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = (𝐺‘1o)) |
99 | 98, 44 | syl6eq 2163 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (𝐺‘(◡𝐺‘(𝑓‘𝑥))) = 1) |
100 | 94, 99 | eqtr3d 2149 |
. . . . . . . 8
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (𝑓‘𝑥) = 1) |
101 | 100 | ex 114 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) ∧ 𝑥 ∈ 𝐴) → (((◡𝐺 ∘ 𝑓)‘𝑥) = 1o → (𝑓‘𝑥) = 1)) |
102 | 76, 101 | ralimdaa 2472 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → (∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o → ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) |
103 | 93, 102 | orim12d 758 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → ((∃𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 ((◡𝐺 ∘ 𝑓)‘𝑥) = 1o) → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))) |
104 | 67, 103 | mpd 13 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) ∧ 𝑓 ∈ ({0, 1} ↑𝑚
𝐴)) → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) |
105 | 104 | ralrimiva 2479 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) → ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) |
106 | | fveq1 5374 |
. . . . . . . . 9
⊢ (𝑓 = (𝐺 ∘ 𝑔) → (𝑓‘𝑥) = ((𝐺 ∘ 𝑔)‘𝑥)) |
107 | 106 | eqeq1d 2123 |
. . . . . . . 8
⊢ (𝑓 = (𝐺 ∘ 𝑔) → ((𝑓‘𝑥) = 0 ↔ ((𝐺 ∘ 𝑔)‘𝑥) = 0)) |
108 | 107 | rexbidv 2412 |
. . . . . . 7
⊢ (𝑓 = (𝐺 ∘ 𝑔) → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ↔ ∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0)) |
109 | 106 | eqeq1d 2123 |
. . . . . . . 8
⊢ (𝑓 = (𝐺 ∘ 𝑔) → ((𝑓‘𝑥) = 1 ↔ ((𝐺 ∘ 𝑔)‘𝑥) = 1)) |
110 | 109 | ralbidv 2411 |
. . . . . . 7
⊢ (𝑓 = (𝐺 ∘ 𝑔) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 ↔ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1)) |
111 | 108, 110 | orbi12d 765 |
. . . . . 6
⊢ (𝑓 = (𝐺 ∘ 𝑔) → ((∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) ↔ (∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1))) |
112 | | simplr 502 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) |
113 | | f1of 5323 |
. . . . . . . . . . . 12
⊢ (𝐺:ω–1-1-onto→ℕ0 → 𝐺:ω⟶ℕ0) |
114 | 10, 113 | ax-mp 7 |
. . . . . . . . . . 11
⊢ 𝐺:ω⟶ℕ0 |
115 | | omelon 4482 |
. . . . . . . . . . . . 13
⊢ ω
∈ On |
116 | 115 | onelssi 4311 |
. . . . . . . . . . . 12
⊢
(2o ∈ ω → 2o ⊆
ω) |
117 | 62, 116 | ax-mp 7 |
. . . . . . . . . . 11
⊢
2o ⊆ ω |
118 | | fssres 5256 |
. . . . . . . . . . 11
⊢ ((𝐺:ω⟶ℕ0 ∧
2o ⊆ ω) → (𝐺 ↾
2o):2o⟶ℕ0) |
119 | 114, 117,
118 | mp2an 420 |
. . . . . . . . . 10
⊢ (𝐺 ↾
2o):2o⟶ℕ0 |
120 | | ffn 5230 |
. . . . . . . . . 10
⊢ ((𝐺 ↾
2o):2o⟶ℕ0 → (𝐺 ↾ 2o) Fn
2o) |
121 | 119, 120 | ax-mp 7 |
. . . . . . . . 9
⊢ (𝐺 ↾ 2o) Fn
2o |
122 | | fvres 5399 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ 2o →
((𝐺 ↾
2o)‘𝑗) =
(𝐺‘𝑗)) |
123 | | elpri 3516 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ {∅, 1o}
→ (𝑗 = ∅ ∨
𝑗 =
1o)) |
124 | | df2o3 6281 |
. . . . . . . . . . . . 13
⊢
2o = {∅, 1o} |
125 | 123, 124 | eleq2s 2209 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ 2o →
(𝑗 = ∅ ∨ 𝑗 =
1o)) |
126 | | fveq2 5375 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = ∅ → (𝐺‘𝑗) = (𝐺‘∅)) |
127 | | c0ex 7684 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
V |
128 | 127 | prid1 3595 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
{0, 1} |
129 | 27, 128 | eqeltri 2187 |
. . . . . . . . . . . . . 14
⊢ (𝐺‘∅) ∈ {0,
1} |
130 | 126, 129 | syl6eqel 2205 |
. . . . . . . . . . . . 13
⊢ (𝑗 = ∅ → (𝐺‘𝑗) ∈ {0, 1}) |
131 | | fveq2 5375 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 1o → (𝐺‘𝑗) = (𝐺‘1o)) |
132 | | 1ex 7685 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
V |
133 | 132 | prid2 3596 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
{0, 1} |
134 | 44, 133 | eqeltri 2187 |
. . . . . . . . . . . . . 14
⊢ (𝐺‘1o) ∈ {0,
1} |
135 | 131, 134 | syl6eqel 2205 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 1o → (𝐺‘𝑗) ∈ {0, 1}) |
136 | 130, 135 | jaoi 688 |
. . . . . . . . . . . 12
⊢ ((𝑗 = ∅ ∨ 𝑗 = 1o) → (𝐺‘𝑗) ∈ {0, 1}) |
137 | 125, 136 | syl 14 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ 2o →
(𝐺‘𝑗) ∈ {0, 1}) |
138 | 122, 137 | eqeltrd 2191 |
. . . . . . . . . 10
⊢ (𝑗 ∈ 2o →
((𝐺 ↾
2o)‘𝑗)
∈ {0, 1}) |
139 | 138 | rgen 2459 |
. . . . . . . . 9
⊢
∀𝑗 ∈
2o ((𝐺 ↾
2o)‘𝑗)
∈ {0, 1} |
140 | | ffnfv 5532 |
. . . . . . . . 9
⊢ ((𝐺 ↾
2o):2o⟶{0, 1} ↔ ((𝐺 ↾ 2o) Fn 2o
∧ ∀𝑗 ∈
2o ((𝐺 ↾
2o)‘𝑗)
∈ {0, 1})) |
141 | 121, 139,
140 | mpbir2an 909 |
. . . . . . . 8
⊢ (𝐺 ↾
2o):2o⟶{0, 1} |
142 | | elmapi 6518 |
. . . . . . . . 9
⊢ (𝑔 ∈ (2o
↑𝑚 𝐴) → 𝑔:𝐴⟶2o) |
143 | 142 | adantl 273 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → 𝑔:𝐴⟶2o) |
144 | | fco2 5247 |
. . . . . . . 8
⊢ (((𝐺 ↾
2o):2o⟶{0, 1} ∧ 𝑔:𝐴⟶2o) → (𝐺 ∘ 𝑔):𝐴⟶{0, 1}) |
145 | 141, 143,
144 | sylancr 408 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → (𝐺 ∘ 𝑔):𝐴⟶{0, 1}) |
146 | | prexg 4093 |
. . . . . . . . . 10
⊢ ((0
∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1}
∈ V) |
147 | 14, 15, 146 | mp2an 420 |
. . . . . . . . 9
⊢ {0, 1}
∈ V |
148 | 147 | a1i 9 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → {0, 1} ∈ V) |
149 | | simpll 501 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → 𝐴 ∈ 𝑉) |
150 | 148, 149 | elmapd 6510 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → ((𝐺 ∘ 𝑔) ∈ ({0, 1} ↑𝑚
𝐴) ↔ (𝐺 ∘ 𝑔):𝐴⟶{0, 1})) |
151 | 145, 150 | mpbird 166 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → (𝐺 ∘ 𝑔) ∈ ({0, 1} ↑𝑚
𝐴)) |
152 | 111, 112,
151 | rspcdva 2765 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → (∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1)) |
153 | | nfcv 2255 |
. . . . . . . . . 10
⊢
Ⅎ𝑥({0,
1} ↑𝑚 𝐴) |
154 | | nfre1 2450 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 |
155 | | nfra1 2440 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 |
156 | 154, 155 | nfor 1536 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) |
157 | 153, 156 | nfralxy 2445 |
. . . . . . . . 9
⊢
Ⅎ𝑥∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1) |
158 | 68, 157 | nfan 1527 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) |
159 | | nfv 1491 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑔 ∈ (2o
↑𝑚 𝐴) |
160 | 158, 159 | nfan 1527 |
. . . . . . 7
⊢
Ⅎ𝑥((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) |
161 | 143 | adantr 272 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑔:𝐴⟶2o) |
162 | 117 | a1i 9 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 2o ⊆
ω) |
163 | 161, 162 | fssd 5243 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑔:𝐴⟶ω) |
164 | | simpr 109 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
165 | 163, 164 | ffvelrnd 5510 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ω) |
166 | | f1ocnvfv1 5632 |
. . . . . . . . . . 11
⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ (𝑔‘𝑥) ∈ ω) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥)) |
167 | 10, 165, 166 | sylancr 408 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥)) |
168 | 167 | adantr 272 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥)) |
169 | | fvco3 5446 |
. . . . . . . . . . . . . 14
⊢ ((𝑔:𝐴⟶2o ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝑔)‘𝑥) = (𝐺‘(𝑔‘𝑥))) |
170 | 161, 169 | sylancom 414 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝑔)‘𝑥) = (𝐺‘(𝑔‘𝑥))) |
171 | 170 | eqeq1d 2123 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 0 ↔ (𝐺‘(𝑔‘𝑥)) = 0)) |
172 | 171 | biimpa 292 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (𝐺‘(𝑔‘𝑥)) = 0) |
173 | 172 | fveq2d 5379 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘0)) |
174 | 173, 31 | syl6eq 2163 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = ∅) |
175 | 168, 174 | eqtr3d 2149 |
. . . . . . . 8
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 0) → (𝑔‘𝑥) = ∅) |
176 | 175 | exp31 359 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → (𝑥 ∈ 𝐴 → (((𝐺 ∘ 𝑔)‘𝑥) = 0 → (𝑔‘𝑥) = ∅))) |
177 | 160, 176 | reximdai 2504 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → (∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0 → ∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅)) |
178 | 167 | adantr 272 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (𝑔‘𝑥)) |
179 | 170 | eqeq1d 2123 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 1 ↔ (𝐺‘(𝑔‘𝑥)) = 1)) |
180 | 179 | biimpa 292 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (𝐺‘(𝑔‘𝑥)) = 1) |
181 | 180 | fveq2d 5379 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = (◡𝐺‘1)) |
182 | 181, 48 | syl6eq 2163 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (◡𝐺‘(𝐺‘(𝑔‘𝑥))) = 1o) |
183 | 178, 182 | eqtr3d 2149 |
. . . . . . . 8
⊢
(((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (𝑔‘𝑥) = 1o) |
184 | 183 | ex 114 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) ∧ 𝑥 ∈ 𝐴) → (((𝐺 ∘ 𝑔)‘𝑥) = 1 → (𝑔‘𝑥) = 1o)) |
185 | 160, 184 | ralimdaa 2472 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → (∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1 → ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) |
186 | 177, 185 | orim12d 758 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → ((∃𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 ((𝐺 ∘ 𝑔)‘𝑥) = 1) → (∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o))) |
187 | 152, 186 | mpd 13 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) ∧ 𝑔 ∈ (2o
↑𝑚 𝐴)) → (∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) |
188 | 187 | ralrimiva 2479 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑓 ∈ ({0, 1} ↑𝑚
𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) → ∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o)) |
189 | 105, 188 | impbida 568 |
. 2
⊢ (𝐴 ∈ 𝑉 → (∀𝑔 ∈ (2o
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑔‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) = 1o) ↔ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))) |
190 | 1, 189 | bitrd 187 |
1
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓 ∈ ({0, 1}
↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))) |