Step | Hyp | Ref
| Expression |
1 | | elmapi 7765 |
. . . . . . . . . 10
⊢ (𝑜 ∈ (ℕ0
↑𝑚 𝐽) → 𝑜:𝐽⟶ℕ0) |
2 | 1 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑜 ∈ (ℕ0
↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → 𝑜:𝐽⟶ℕ0) |
3 | | c0ex 9913 |
. . . . . . . . . . 11
⊢ 0 ∈
V |
4 | 3 | fconst 6004 |
. . . . . . . . . 10
⊢ ((ℕ
∖ 𝐽) ×
{0}):(ℕ ∖ 𝐽)⟶{0} |
5 | 4 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑜 ∈ (ℕ0
↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → ((ℕ ∖ 𝐽) × {0}):(ℕ ∖ 𝐽)⟶{0}) |
6 | | disjdif 3992 |
. . . . . . . . . 10
⊢ (𝐽 ∩ (ℕ ∖ 𝐽)) = ∅ |
7 | 6 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑜 ∈ (ℕ0
↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → (𝐽 ∩ (ℕ ∖ 𝐽)) = ∅) |
8 | | fun 5979 |
. . . . . . . . 9
⊢ (((𝑜:𝐽⟶ℕ0 ∧ ((ℕ
∖ 𝐽) ×
{0}):(ℕ ∖ 𝐽)⟶{0}) ∧ (𝐽 ∩ (ℕ ∖ 𝐽)) = ∅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):(𝐽 ∪ (ℕ ∖ 𝐽))⟶(ℕ0 ∪
{0})) |
9 | 2, 5, 7, 8 | syl21anc 1317 |
. . . . . . . 8
⊢ ((𝑜 ∈ (ℕ0
↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):(𝐽 ∪ (ℕ ∖ 𝐽))⟶(ℕ0 ∪
{0})) |
10 | | eulerpart.j |
. . . . . . . . . . 11
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} |
11 | | ssrab2 3650 |
. . . . . . . . . . 11
⊢ {𝑧 ∈ ℕ ∣ ¬ 2
∥ 𝑧} ⊆
ℕ |
12 | 10, 11 | eqsstri 3598 |
. . . . . . . . . 10
⊢ 𝐽 ⊆
ℕ |
13 | | undif 4001 |
. . . . . . . . . 10
⊢ (𝐽 ⊆ ℕ ↔ (𝐽 ∪ (ℕ ∖ 𝐽)) = ℕ) |
14 | 12, 13 | mpbi 219 |
. . . . . . . . 9
⊢ (𝐽 ∪ (ℕ ∖ 𝐽)) = ℕ |
15 | | 0nn0 11184 |
. . . . . . . . . . 11
⊢ 0 ∈
ℕ0 |
16 | | snssi 4280 |
. . . . . . . . . . 11
⊢ (0 ∈
ℕ0 → {0} ⊆ ℕ0) |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . . 10
⊢ {0}
⊆ ℕ0 |
18 | | ssequn2 3748 |
. . . . . . . . . 10
⊢ ({0}
⊆ ℕ0 ↔ (ℕ0 ∪ {0}) =
ℕ0) |
19 | 17, 18 | mpbi 219 |
. . . . . . . . 9
⊢
(ℕ0 ∪ {0}) = ℕ0 |
20 | 14, 19 | feq23i 5952 |
. . . . . . . 8
⊢ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):(𝐽 ∪ (ℕ ∖ 𝐽))⟶(ℕ0
∪ {0}) ↔ (𝑜 ∪
((ℕ ∖ 𝐽)
× {0})):ℕ⟶ℕ0) |
21 | 9, 20 | sylib 207 |
. . . . . . 7
⊢ ((𝑜 ∈ (ℕ0
↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → (𝑜 ∪ ((ℕ ∖ 𝐽) ×
{0})):ℕ⟶ℕ0) |
22 | | nn0ex 11175 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
23 | | nnex 10903 |
. . . . . . . 8
⊢ ℕ
∈ V |
24 | 22, 23 | elmap 7772 |
. . . . . . 7
⊢ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈
(ℕ0 ↑𝑚 ℕ) ↔ (𝑜 ∪ ((ℕ ∖ 𝐽) ×
{0})):ℕ⟶ℕ0) |
25 | 21, 24 | sylibr 223 |
. . . . . 6
⊢ ((𝑜 ∈ (ℕ0
↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (ℕ0
↑𝑚 ℕ)) |
26 | | cnvun 5457 |
. . . . . . . . 9
⊢ ◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) = (◡𝑜 ∪ ◡((ℕ ∖ 𝐽) × {0})) |
27 | 26 | imaeq1i 5382 |
. . . . . . . 8
⊢ (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) = ((◡𝑜 ∪ ◡((ℕ ∖ 𝐽) × {0})) “
ℕ) |
28 | | imaundir 5465 |
. . . . . . . 8
⊢ ((◡𝑜 ∪ ◡((ℕ ∖ 𝐽) × {0})) “ ℕ) = ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “
ℕ)) |
29 | 27, 28 | eqtri 2632 |
. . . . . . 7
⊢ (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) = ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “
ℕ)) |
30 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑜 ∈ V |
31 | | cnveq 5218 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑜 → ◡𝑓 = ◡𝑜) |
32 | 31 | imaeq1d 5384 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑜 → (◡𝑓 “ ℕ) = (◡𝑜 “ ℕ)) |
33 | 32 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑜 → ((◡𝑓 “ ℕ) ∈ Fin ↔ (◡𝑜 “ ℕ) ∈
Fin)) |
34 | | eulerpart.r |
. . . . . . . . . . 11
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈
Fin} |
35 | 30, 33, 34 | elab2 3323 |
. . . . . . . . . 10
⊢ (𝑜 ∈ 𝑅 ↔ (◡𝑜 “ ℕ) ∈
Fin) |
36 | 35 | biimpi 205 |
. . . . . . . . 9
⊢ (𝑜 ∈ 𝑅 → (◡𝑜 “ ℕ) ∈
Fin) |
37 | 36 | adantl 481 |
. . . . . . . 8
⊢ ((𝑜 ∈ (ℕ0
↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → (◡𝑜 “ ℕ) ∈
Fin) |
38 | | cnvxp 5470 |
. . . . . . . . . . . . . 14
⊢ ◡((ℕ ∖ 𝐽) × {0}) = ({0} × (ℕ
∖ 𝐽)) |
39 | 38 | dmeqi 5247 |
. . . . . . . . . . . . 13
⊢ dom ◡((ℕ ∖ 𝐽) × {0}) = dom ({0} × (ℕ
∖ 𝐽)) |
40 | | 2nn 11062 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℕ |
41 | | 2z 11286 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℤ |
42 | | iddvds 14833 |
. . . . . . . . . . . . . . . . 17
⊢ (2 ∈
ℤ → 2 ∥ 2) |
43 | 41, 42 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∥
2 |
44 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 2 → (2 ∥ 𝑧 ↔ 2 ∥
2)) |
45 | 44 | notbid 307 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 2 → (¬ 2 ∥
𝑧 ↔ ¬ 2 ∥
2)) |
46 | 45, 10 | elrab2 3333 |
. . . . . . . . . . . . . . . . 17
⊢ (2 ∈
𝐽 ↔ (2 ∈ ℕ
∧ ¬ 2 ∥ 2)) |
47 | 46 | simprbi 479 |
. . . . . . . . . . . . . . . 16
⊢ (2 ∈
𝐽 → ¬ 2 ∥
2) |
48 | 43, 47 | mt2 190 |
. . . . . . . . . . . . . . 15
⊢ ¬ 2
∈ 𝐽 |
49 | | eldif 3550 |
. . . . . . . . . . . . . . 15
⊢ (2 ∈
(ℕ ∖ 𝐽) ↔
(2 ∈ ℕ ∧ ¬ 2 ∈ 𝐽)) |
50 | 40, 48, 49 | mpbir2an 957 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
(ℕ ∖ 𝐽) |
51 | | ne0i 3880 |
. . . . . . . . . . . . . 14
⊢ (2 ∈
(ℕ ∖ 𝐽) →
(ℕ ∖ 𝐽) ≠
∅) |
52 | | dmxp 5265 |
. . . . . . . . . . . . . 14
⊢ ((ℕ
∖ 𝐽) ≠ ∅
→ dom ({0} × (ℕ ∖ 𝐽)) = {0}) |
53 | 50, 51, 52 | mp2b 10 |
. . . . . . . . . . . . 13
⊢ dom ({0}
× (ℕ ∖ 𝐽)) = {0} |
54 | 39, 53 | eqtri 2632 |
. . . . . . . . . . . 12
⊢ dom ◡((ℕ ∖ 𝐽) × {0}) = {0} |
55 | 54 | ineq1i 3772 |
. . . . . . . . . . 11
⊢ (dom
◡((ℕ ∖ 𝐽) × {0}) ∩ ℕ) = ({0} ∩
ℕ) |
56 | | incom 3767 |
. . . . . . . . . . 11
⊢ (ℕ
∩ {0}) = ({0} ∩ ℕ) |
57 | | 0nnn 10929 |
. . . . . . . . . . . 12
⊢ ¬ 0
∈ ℕ |
58 | | disjsn 4192 |
. . . . . . . . . . . 12
⊢ ((ℕ
∩ {0}) = ∅ ↔ ¬ 0 ∈ ℕ) |
59 | 57, 58 | mpbir 220 |
. . . . . . . . . . 11
⊢ (ℕ
∩ {0}) = ∅ |
60 | 55, 56, 59 | 3eqtr2i 2638 |
. . . . . . . . . 10
⊢ (dom
◡((ℕ ∖ 𝐽) × {0}) ∩ ℕ) =
∅ |
61 | | imadisj 5403 |
. . . . . . . . . 10
⊢ ((◡((ℕ ∖ 𝐽) × {0}) “ ℕ) = ∅
↔ (dom ◡((ℕ ∖ 𝐽) × {0}) ∩ ℕ) =
∅) |
62 | 60, 61 | mpbir 220 |
. . . . . . . . 9
⊢ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) =
∅ |
63 | | 0fin 8073 |
. . . . . . . . 9
⊢ ∅
∈ Fin |
64 | 62, 63 | eqeltri 2684 |
. . . . . . . 8
⊢ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) ∈
Fin |
65 | | unfi 8112 |
. . . . . . . 8
⊢ (((◡𝑜 “ ℕ) ∈ Fin ∧ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) ∈ Fin)
→ ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ)) ∈
Fin) |
66 | 37, 64, 65 | sylancl 693 |
. . . . . . 7
⊢ ((𝑜 ∈ (ℕ0
↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ)) ∈
Fin) |
67 | 29, 66 | syl5eqel 2692 |
. . . . . 6
⊢ ((𝑜 ∈ (ℕ0
↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) ∈
Fin) |
68 | | cnvimass 5404 |
. . . . . . . . 9
⊢ (◡𝑜 “ ℕ) ⊆ dom 𝑜 |
69 | | fdm 5964 |
. . . . . . . . . 10
⊢ (𝑜:𝐽⟶ℕ0 → dom 𝑜 = 𝐽) |
70 | 2, 69 | syl 17 |
. . . . . . . . 9
⊢ ((𝑜 ∈ (ℕ0
↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → dom 𝑜 = 𝐽) |
71 | 68, 70 | syl5sseq 3616 |
. . . . . . . 8
⊢ ((𝑜 ∈ (ℕ0
↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → (◡𝑜 “ ℕ) ⊆ 𝐽) |
72 | | 0ss 3924 |
. . . . . . . . . 10
⊢ ∅
⊆ 𝐽 |
73 | 62, 72 | eqsstri 3598 |
. . . . . . . . 9
⊢ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) ⊆
𝐽 |
74 | 73 | a1i 11 |
. . . . . . . 8
⊢ ((𝑜 ∈ (ℕ0
↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) ⊆
𝐽) |
75 | 71, 74 | unssd 3751 |
. . . . . . 7
⊢ ((𝑜 ∈ (ℕ0
↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ)) ⊆
𝐽) |
76 | 29, 75 | syl5eqss 3612 |
. . . . . 6
⊢ ((𝑜 ∈ (ℕ0
↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) ⊆
𝐽) |
77 | | eulerpart.p |
. . . . . . 7
⊢ 𝑃 = {𝑓 ∈ (ℕ0
↑𝑚 ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ ℕ
((𝑓‘𝑘) · 𝑘) = 𝑁)} |
78 | | eulerpart.o |
. . . . . . 7
⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} |
79 | | eulerpart.d |
. . . . . . 7
⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} |
80 | | eulerpart.f |
. . . . . . 7
⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦
((2↑𝑦) · 𝑥)) |
81 | | eulerpart.h |
. . . . . . 7
⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩
Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} |
82 | | eulerpart.m |
. . . . . . 7
⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) |
83 | | eulerpart.t |
. . . . . . 7
⊢ 𝑇 = {𝑓 ∈ (ℕ0
↑𝑚 ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} |
84 | 77, 78, 79, 10, 80, 81, 82, 34, 83 | eulerpartlemt0 29758 |
. . . . . 6
⊢ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (𝑇 ∩ 𝑅) ↔ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (ℕ0
↑𝑚 ℕ) ∧ (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) ∈ Fin
∧ (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) ⊆
𝐽)) |
85 | 25, 67, 76, 84 | syl3anbrc 1239 |
. . . . 5
⊢ ((𝑜 ∈ (ℕ0
↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (𝑇 ∩ 𝑅)) |
86 | | resundir 5331 |
. . . . . 6
⊢ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽) = ((𝑜 ↾ 𝐽) ∪ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽)) |
87 | | ffn 5958 |
. . . . . . . 8
⊢ (𝑜:𝐽⟶ℕ0 → 𝑜 Fn 𝐽) |
88 | | fnresdm 5914 |
. . . . . . . . 9
⊢ (𝑜 Fn 𝐽 → (𝑜 ↾ 𝐽) = 𝑜) |
89 | | incom 3767 |
. . . . . . . . . . . 12
⊢ ((ℕ
∖ 𝐽) ∩ 𝐽) = (𝐽 ∩ (ℕ ∖ 𝐽)) |
90 | 89, 6 | eqtri 2632 |
. . . . . . . . . . 11
⊢ ((ℕ
∖ 𝐽) ∩ 𝐽) = ∅ |
91 | | fnconstg 6006 |
. . . . . . . . . . . 12
⊢ (0 ∈
ℕ0 → ((ℕ ∖ 𝐽) × {0}) Fn (ℕ ∖ 𝐽)) |
92 | | fnresdisj 5915 |
. . . . . . . . . . . 12
⊢
(((ℕ ∖ 𝐽) × {0}) Fn (ℕ ∖ 𝐽) → (((ℕ ∖
𝐽) ∩ 𝐽) = ∅ ↔ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽) = ∅)) |
93 | 15, 91, 92 | mp2b 10 |
. . . . . . . . . . 11
⊢
(((ℕ ∖ 𝐽) ∩ 𝐽) = ∅ ↔ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽) = ∅) |
94 | 90, 93 | mpbi 219 |
. . . . . . . . . 10
⊢
(((ℕ ∖ 𝐽) × {0}) ↾ 𝐽) = ∅ |
95 | 94 | a1i 11 |
. . . . . . . . 9
⊢ (𝑜 Fn 𝐽 → (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽) = ∅) |
96 | 88, 95 | uneq12d 3730 |
. . . . . . . 8
⊢ (𝑜 Fn 𝐽 → ((𝑜 ↾ 𝐽) ∪ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽)) = (𝑜 ∪ ∅)) |
97 | 2, 87, 96 | 3syl 18 |
. . . . . . 7
⊢ ((𝑜 ∈ (ℕ0
↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → ((𝑜 ↾ 𝐽) ∪ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽)) = (𝑜 ∪ ∅)) |
98 | | un0 3919 |
. . . . . . 7
⊢ (𝑜 ∪ ∅) = 𝑜 |
99 | 97, 98 | syl6eq 2660 |
. . . . . 6
⊢ ((𝑜 ∈ (ℕ0
↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → ((𝑜 ↾ 𝐽) ∪ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽)) = 𝑜) |
100 | 86, 99 | syl5req 2657 |
. . . . 5
⊢ ((𝑜 ∈ (ℕ0
↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → 𝑜 = ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽)) |
101 | | reseq1 5311 |
. . . . . . 7
⊢ (𝑚 = (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) → (𝑚 ↾ 𝐽) = ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽)) |
102 | 101 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑚 = (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) → (𝑜 = (𝑚 ↾ 𝐽) ↔ 𝑜 = ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽))) |
103 | 102 | rspcev 3282 |
. . . . 5
⊢ (((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽)) → ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽)) |
104 | 85, 100, 103 | syl2anc 691 |
. . . 4
⊢ ((𝑜 ∈ (ℕ0
↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽)) |
105 | | simpr 476 |
. . . . . . 7
⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑜 = (𝑚 ↾ 𝐽)) |
106 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑚 ∈ (𝑇 ∩ 𝑅)) |
107 | 77, 78, 79, 10, 80, 81, 82, 34, 83 | eulerpartlemt0 29758 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) ↔ (𝑚 ∈ (ℕ0
↑𝑚 ℕ) ∧ (◡𝑚 “ ℕ) ∈ Fin ∧ (◡𝑚 “ ℕ) ⊆ 𝐽)) |
108 | 106, 107 | sylib 207 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑚 ∈ (ℕ0
↑𝑚 ℕ) ∧ (◡𝑚 “ ℕ) ∈ Fin ∧ (◡𝑚 “ ℕ) ⊆ 𝐽)) |
109 | 108 | simp1d 1066 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑚 ∈ (ℕ0
↑𝑚 ℕ)) |
110 | 22, 23 | elmap 7772 |
. . . . . . . . . 10
⊢ (𝑚 ∈ (ℕ0
↑𝑚 ℕ) ↔ 𝑚:ℕ⟶ℕ0) |
111 | 109, 110 | sylib 207 |
. . . . . . . . 9
⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑚:ℕ⟶ℕ0) |
112 | | fssres 5983 |
. . . . . . . . 9
⊢ ((𝑚:ℕ⟶ℕ0 ∧
𝐽 ⊆ ℕ) →
(𝑚 ↾ 𝐽):𝐽⟶ℕ0) |
113 | 111, 12, 112 | sylancl 693 |
. . . . . . . 8
⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑚 ↾ 𝐽):𝐽⟶ℕ0) |
114 | 10, 23 | rabex2 4742 |
. . . . . . . . 9
⊢ 𝐽 ∈ V |
115 | 22, 114 | elmap 7772 |
. . . . . . . 8
⊢ ((𝑚 ↾ 𝐽) ∈ (ℕ0
↑𝑚 𝐽) ↔ (𝑚 ↾ 𝐽):𝐽⟶ℕ0) |
116 | 113, 115 | sylibr 223 |
. . . . . . 7
⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑚 ↾ 𝐽) ∈ (ℕ0
↑𝑚 𝐽)) |
117 | 105, 116 | eqeltrd 2688 |
. . . . . 6
⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑜 ∈ (ℕ0
↑𝑚 𝐽)) |
118 | | ffun 5961 |
. . . . . . . . . 10
⊢ (𝑚:ℕ⟶ℕ0 →
Fun 𝑚) |
119 | | respreima 6252 |
. . . . . . . . . 10
⊢ (Fun
𝑚 → (◡(𝑚 ↾ 𝐽) “ ℕ) = ((◡𝑚 “ ℕ) ∩ 𝐽)) |
120 | 111, 118,
119 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (◡(𝑚 ↾ 𝐽) “ ℕ) = ((◡𝑚 “ ℕ) ∩ 𝐽)) |
121 | 108 | simp2d 1067 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (◡𝑚 “ ℕ) ∈
Fin) |
122 | | infi 8069 |
. . . . . . . . . 10
⊢ ((◡𝑚 “ ℕ) ∈ Fin → ((◡𝑚 “ ℕ) ∩ 𝐽) ∈ Fin) |
123 | 121, 122 | syl 17 |
. . . . . . . . 9
⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → ((◡𝑚 “ ℕ) ∩ 𝐽) ∈ Fin) |
124 | 120, 123 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (◡(𝑚 ↾ 𝐽) “ ℕ) ∈
Fin) |
125 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑚 ∈ V |
126 | 125 | resex 5363 |
. . . . . . . . 9
⊢ (𝑚 ↾ 𝐽) ∈ V |
127 | | cnveq 5218 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑚 ↾ 𝐽) → ◡𝑓 = ◡(𝑚 ↾ 𝐽)) |
128 | 127 | imaeq1d 5384 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑚 ↾ 𝐽) → (◡𝑓 “ ℕ) = (◡(𝑚 ↾ 𝐽) “ ℕ)) |
129 | 128 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑓 = (𝑚 ↾ 𝐽) → ((◡𝑓 “ ℕ) ∈ Fin ↔ (◡(𝑚 ↾ 𝐽) “ ℕ) ∈
Fin)) |
130 | 126, 129,
34 | elab2 3323 |
. . . . . . . 8
⊢ ((𝑚 ↾ 𝐽) ∈ 𝑅 ↔ (◡(𝑚 ↾ 𝐽) “ ℕ) ∈
Fin) |
131 | 124, 130 | sylibr 223 |
. . . . . . 7
⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑚 ↾ 𝐽) ∈ 𝑅) |
132 | 105, 131 | eqeltrd 2688 |
. . . . . 6
⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑜 ∈ 𝑅) |
133 | 117, 132 | jca 553 |
. . . . 5
⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑜 ∈ (ℕ0
↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅)) |
134 | 133 | rexlimiva 3010 |
. . . 4
⊢
(∃𝑚 ∈
(𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽) → (𝑜 ∈ (ℕ0
↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅)) |
135 | 104, 134 | impbii 198 |
. . 3
⊢ ((𝑜 ∈ (ℕ0
↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽)) |
136 | 135 | abbii 2726 |
. 2
⊢ {𝑜 ∣ (𝑜 ∈ (ℕ0
↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅)} = {𝑜 ∣ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽)} |
137 | | df-in 3547 |
. 2
⊢
((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) = {𝑜 ∣ (𝑜 ∈ (ℕ0
↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅)} |
138 | | eqid 2610 |
. . 3
⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) = (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) |
139 | 138 | rnmpt 5292 |
. 2
⊢ ran
(𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) = {𝑜 ∣ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽)} |
140 | 136, 137,
139 | 3eqtr4i 2642 |
1
⊢
((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) = ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) |