Step | Hyp | Ref
| Expression |
1 | | sge0f1o.4 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
2 | | sge0f1o.5 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) |
3 | | f1ofo 6286 |
. . . . . . 7
⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶–onto→𝐴) |
4 | 2, 3 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐶–onto→𝐴) |
5 | | fornex 7285 |
. . . . . 6
⊢ (𝐶 ∈ 𝑉 → (𝐹:𝐶–onto→𝐴 → 𝐴 ∈ V)) |
6 | 1, 4, 5 | sylc 65 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ V) |
7 | 6 | adantr 466 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐴 ∈ V) |
8 | | sge0f1o.1 |
. . . . . 6
⊢
Ⅎ𝑘𝜑 |
9 | | sge0f1o.7 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) |
10 | | eqid 2771 |
. . . . . 6
⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵) |
11 | 8, 9, 10 | fmptdf 6531 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶(0[,]+∞)) |
12 | 11 | adantr 466 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶(0[,]+∞)) |
13 | | pnfex 10298 |
. . . . . . . 8
⊢ +∞
∈ V |
14 | | eqid 2771 |
. . . . . . . . 9
⊢ (𝑛 ∈ 𝐶 ↦ 𝐷) = (𝑛 ∈ 𝐶 ↦ 𝐷) |
15 | 14 | elrnmpt 5509 |
. . . . . . . 8
⊢ (+∞
∈ V → (+∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) ↔ ∃𝑛 ∈ 𝐶 +∞ = 𝐷)) |
16 | 13, 15 | ax-mp 5 |
. . . . . . 7
⊢ (+∞
∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) ↔ ∃𝑛 ∈ 𝐶 +∞ = 𝐷) |
17 | 16 | biimpi 206 |
. . . . . 6
⊢ (+∞
∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) → ∃𝑛 ∈ 𝐶 +∞ = 𝐷) |
18 | 17 | adantl 467 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → ∃𝑛 ∈ 𝐶 +∞ = 𝐷) |
19 | | sge0f1o.2 |
. . . . . . 7
⊢
Ⅎ𝑛𝜑 |
20 | | nfv 1995 |
. . . . . . 7
⊢
Ⅎ𝑛+∞
∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵) |
21 | | simp3 1132 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → +∞ = 𝐷) |
22 | | f1of 6279 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶⟶𝐴) |
23 | 2, 22 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:𝐶⟶𝐴) |
24 | 23 | ffvelrnda 6504 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) ∈ 𝐴) |
25 | | sge0f1o.6 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) |
26 | | nfcv 2913 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘(𝐹‘𝑛) |
27 | | nfv 1995 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘(𝐹‘𝑛) = 𝐺 |
28 | 26 | nfcsb1 3697 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵 |
29 | | nfcv 2913 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘𝐷 |
30 | 28, 29 | nfeq 2925 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷 |
31 | 27, 30 | nfim 1977 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘((𝐹‘𝑛) = 𝐺 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷) |
32 | | eqeq1 2775 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝐹‘𝑛) → (𝑘 = 𝐺 ↔ (𝐹‘𝑛) = 𝐺)) |
33 | | csbeq1a 3691 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵) |
34 | 33 | eqeq1d 2773 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝐹‘𝑛) → (𝐵 = 𝐷 ↔ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)) |
35 | 32, 34 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝐹‘𝑛) → ((𝑘 = 𝐺 → 𝐵 = 𝐷) ↔ ((𝐹‘𝑛) = 𝐺 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷))) |
36 | | sge0f1o.3 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷) |
37 | 26, 31, 35, 36 | vtoclgf 3415 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑛) ∈ 𝐴 → ((𝐹‘𝑛) = 𝐺 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)) |
38 | 24, 25, 37 | sylc 65 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷) |
39 | 38 | eqcomd 2777 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵) |
40 | 39 | 3adant3 1126 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → 𝐷 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵) |
41 | 21, 40 | eqtrd 2805 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → +∞ = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵) |
42 | | simpl 468 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝜑) |
43 | 42, 24 | jca 501 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴)) |
44 | | nfv 1995 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘(𝐹‘𝑛) ∈ 𝐴 |
45 | 8, 44 | nfan 1980 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘(𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) |
46 | 28 | nfel1 2928 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞) |
47 | 45, 46 | nfim 1977 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘((𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)) |
48 | | eleq1 2838 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝐹‘𝑛) → (𝑘 ∈ 𝐴 ↔ (𝐹‘𝑛) ∈ 𝐴)) |
49 | 48 | anbi2d 614 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝐹‘𝑛) → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴))) |
50 | 33 | eleq1d 2835 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝐹‘𝑛) → (𝐵 ∈ (0[,]+∞) ↔
⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞))) |
51 | 49, 50 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝐹‘𝑛) → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)))) |
52 | 26, 47, 51, 9 | vtoclgf 3415 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑛) ∈ 𝐴 → ((𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞))) |
53 | 24, 43, 52 | sylc 65 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)) |
54 | 28, 10, 33 | elrnmpt1sf 39895 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑛) ∈ 𝐴 ∧ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)) →
⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)) |
55 | 24, 53, 54 | syl2anc 573 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)) |
56 | 55 | 3adant3 1126 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)) |
57 | 41, 56 | eqeltrd 2850 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)) |
58 | 57 | 3exp 1112 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ 𝐶 → (+∞ = 𝐷 → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)))) |
59 | 19, 20, 58 | rexlimd 3174 |
. . . . . 6
⊢ (𝜑 → (∃𝑛 ∈ 𝐶 +∞ = 𝐷 → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))) |
60 | 59 | adantr 466 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (∃𝑛 ∈ 𝐶 +∞ = 𝐷 → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))) |
61 | 18, 60 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)) |
62 | 7, 12, 61 | sge0pnfval 41104 |
. . 3
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = +∞) |
63 | 1 | adantr 466 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐶 ∈ 𝑉) |
64 | 39, 53 | eqeltrd 2850 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ (0[,]+∞)) |
65 | 19, 64, 14 | fmptdf 6531 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ 𝐶 ↦ 𝐷):𝐶⟶(0[,]+∞)) |
66 | 65 | adantr 466 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (𝑛 ∈ 𝐶 ↦ 𝐷):𝐶⟶(0[,]+∞)) |
67 | | simpr 471 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) |
68 | 63, 66, 67 | sge0pnfval 41104 |
. . 3
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) →
(Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷)) = +∞) |
69 | 62, 68 | eqtr4d 2808 |
. 2
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) =
(Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷))) |
70 | | sumex 14625 |
. . . . . . 7
⊢
Σ𝑘 ∈
𝑦 𝐵 ∈ V |
71 | 70 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑘 ∈ 𝑦 𝐵 ∈ V) |
72 | | cnvimass 5625 |
. . . . . . . . . . . . 13
⊢ (◡𝐹 “ 𝑦) ⊆ dom 𝐹 |
73 | 72 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡𝐹 “ 𝑦) ⊆ dom 𝐹) |
74 | 23 | fdmd 6193 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom 𝐹 = 𝐶) |
75 | 73, 74 | sseqtrd 3790 |
. . . . . . . . . . 11
⊢ (𝜑 → (◡𝐹 “ 𝑦) ⊆ 𝐶) |
76 | | fex 6635 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐶⟶𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐹 ∈ V) |
77 | 23, 1, 76 | syl2anc 573 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 ∈ V) |
78 | | cnvexg 7262 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ V → ◡𝐹 ∈ V) |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ◡𝐹 ∈ V) |
80 | | imaexg 7253 |
. . . . . . . . . . . . 13
⊢ (◡𝐹 ∈ V → (◡𝐹 “ 𝑦) ∈ V) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡𝐹 “ 𝑦) ∈ V) |
82 | | elpwg 4306 |
. . . . . . . . . . . 12
⊢ ((◡𝐹 “ 𝑦) ∈ V → ((◡𝐹 “ 𝑦) ∈ 𝒫 𝐶 ↔ (◡𝐹 “ 𝑦) ⊆ 𝐶)) |
83 | 81, 82 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((◡𝐹 “ 𝑦) ∈ 𝒫 𝐶 ↔ (◡𝐹 “ 𝑦) ⊆ 𝐶)) |
84 | 75, 83 | mpbird 247 |
. . . . . . . . . 10
⊢ (𝜑 → (◡𝐹 “ 𝑦) ∈ 𝒫 𝐶) |
85 | 84 | adantr 466 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (◡𝐹 “ 𝑦) ∈ 𝒫 𝐶) |
86 | | f1ocnv 6291 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝐶–1-1-onto→𝐴 → ◡𝐹:𝐴–1-1-onto→𝐶) |
87 | 2, 86 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ◡𝐹:𝐴–1-1-onto→𝐶) |
88 | | f1ofun 6281 |
. . . . . . . . . . . 12
⊢ (◡𝐹:𝐴–1-1-onto→𝐶 → Fun ◡𝐹) |
89 | 87, 88 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → Fun ◡𝐹) |
90 | 89 | adantr 466 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Fun ◡𝐹) |
91 | | elinel2 3951 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin) |
92 | 91 | adantl 467 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ∈ Fin) |
93 | | imafi 8418 |
. . . . . . . . . 10
⊢ ((Fun
◡𝐹 ∧ 𝑦 ∈ Fin) → (◡𝐹 “ 𝑦) ∈ Fin) |
94 | 90, 92, 93 | syl2anc 573 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (◡𝐹 “ 𝑦) ∈ Fin) |
95 | 85, 94 | elind 3949 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) |
96 | 95 | adantlr 694 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) |
97 | | nfv 1995 |
. . . . . . . . . 10
⊢
Ⅎ𝑘 ¬
+∞ ∈ ran (𝑛
∈ 𝐶 ↦ 𝐷) |
98 | 8, 97 | nfan 1980 |
. . . . . . . . 9
⊢
Ⅎ𝑘(𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) |
99 | | nfv 1995 |
. . . . . . . . 9
⊢
Ⅎ𝑘 𝑦 ∈ (𝒫 𝐴 ∩ Fin) |
100 | 98, 99 | nfan 1980 |
. . . . . . . 8
⊢
Ⅎ𝑘((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) |
101 | | nfcv 2913 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛+∞ |
102 | | nfmpt1 4882 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛(𝑛 ∈ 𝐶 ↦ 𝐷) |
103 | 102 | nfrn 5505 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛ran
(𝑛 ∈ 𝐶 ↦ 𝐷) |
104 | 101, 103 | nfel 2926 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛+∞
∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) |
105 | 104 | nfn 1935 |
. . . . . . . . . 10
⊢
Ⅎ𝑛 ¬
+∞ ∈ ran (𝑛
∈ 𝐶 ↦ 𝐷) |
106 | 19, 105 | nfan 1980 |
. . . . . . . . 9
⊢
Ⅎ𝑛(𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) |
107 | | nfv 1995 |
. . . . . . . . 9
⊢
Ⅎ𝑛 𝑦 ∈ (𝒫 𝐴 ∩ Fin) |
108 | 106, 107 | nfan 1980 |
. . . . . . . 8
⊢
Ⅎ𝑛((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) |
109 | 94 | adantlr 694 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (◡𝐹 “ 𝑦) ∈ Fin) |
110 | | f1of1 6278 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶–1-1→𝐴) |
111 | 2, 110 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝐶–1-1→𝐴) |
112 | 111 | adantr 466 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐹:𝐶–1-1→𝐴) |
113 | 83 | adantr 466 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((◡𝐹 “ 𝑦) ∈ 𝒫 𝐶 ↔ (◡𝐹 “ 𝑦) ⊆ 𝐶)) |
114 | 85, 113 | mpbid 222 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (◡𝐹 “ 𝑦) ⊆ 𝐶) |
115 | | f1ores 6293 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐶–1-1→𝐴 ∧ (◡𝐹 “ 𝑦) ⊆ 𝐶) → (𝐹 ↾ (◡𝐹 “ 𝑦)):(◡𝐹 “ 𝑦)–1-1-onto→(𝐹 “ (◡𝐹 “ 𝑦))) |
116 | 112, 114,
115 | syl2anc 573 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ (◡𝐹 “ 𝑦)):(◡𝐹 “ 𝑦)–1-1-onto→(𝐹 “ (◡𝐹 “ 𝑦))) |
117 | 4 | adantr 466 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐹:𝐶–onto→𝐴) |
118 | | elpwinss 39737 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ⊆ 𝐴) |
119 | 118 | adantl 467 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ⊆ 𝐴) |
120 | | foimacnv 6296 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐶–onto→𝐴 ∧ 𝑦 ⊆ 𝐴) → (𝐹 “ (◡𝐹 “ 𝑦)) = 𝑦) |
121 | 117, 119,
120 | syl2anc 573 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 “ (◡𝐹 “ 𝑦)) = 𝑦) |
122 | 121 | f1oeq3d 6276 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐹 ↾ (◡𝐹 “ 𝑦)):(◡𝐹 “ 𝑦)–1-1-onto→(𝐹 “ (◡𝐹 “ 𝑦)) ↔ (𝐹 ↾ (◡𝐹 “ 𝑦)):(◡𝐹 “ 𝑦)–1-1-onto→𝑦)) |
123 | 116, 122 | mpbid 222 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ (◡𝐹 “ 𝑦)):(◡𝐹 “ 𝑦)–1-1-onto→𝑦) |
124 | 123 | adantlr 694 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ (◡𝐹 “ 𝑦)):(◡𝐹 “ 𝑦)–1-1-onto→𝑦) |
125 | 81 | ad2antrr 705 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → (◡𝐹 “ 𝑦) ∈ V) |
126 | | simpll 750 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → 𝜑) |
127 | 95 | adantr 466 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) |
128 | | simpr 471 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → 𝑛 ∈ (◡𝐹 “ 𝑦)) |
129 | 126, 127,
128 | jca31 504 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → ((𝜑 ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦))) |
130 | | eleq1 2838 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↔ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))) |
131 | 130 | anbi2d 614 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (◡𝐹 “ 𝑦) → ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ↔ (𝜑 ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)))) |
132 | | eleq2 2839 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (𝑛 ∈ 𝑥 ↔ 𝑛 ∈ (◡𝐹 “ 𝑦))) |
133 | 131, 132 | anbi12d 616 |
. . . . . . . . . . . 12
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) ↔ ((𝜑 ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)))) |
134 | | reseq2 5528 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (𝐹 ↾ 𝑥) = (𝐹 ↾ (◡𝐹 “ 𝑦))) |
135 | 134 | fveq1d 6335 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (◡𝐹 “ 𝑦) → ((𝐹 ↾ 𝑥)‘𝑛) = ((𝐹 ↾ (◡𝐹 “ 𝑦))‘𝑛)) |
136 | 135 | eqeq1d 2773 |
. . . . . . . . . . . 12
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (((𝐹 ↾ 𝑥)‘𝑛) = 𝐺 ↔ ((𝐹 ↾ (◡𝐹 “ 𝑦))‘𝑛) = 𝐺)) |
137 | 133, 136 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑥 = (◡𝐹 “ 𝑦) → ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = 𝐺) ↔ (((𝜑 ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → ((𝐹 ↾ (◡𝐹 “ 𝑦))‘𝑛) = 𝐺))) |
138 | | fvres 6350 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ 𝑥 → ((𝐹 ↾ 𝑥)‘𝑛) = (𝐹‘𝑛)) |
139 | 138 | adantl 467 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = (𝐹‘𝑛)) |
140 | | simpll 750 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → 𝜑) |
141 | | elpwinss 39737 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝒫 𝐶 ∩ Fin) → 𝑥 ⊆ 𝐶) |
142 | 141 | adantl 467 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝑥 ⊆ 𝐶) |
143 | 142 | sselda 3752 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → 𝑛 ∈ 𝐶) |
144 | 140, 143,
25 | syl2anc 573 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → (𝐹‘𝑛) = 𝐺) |
145 | 139, 144 | eqtrd 2805 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = 𝐺) |
146 | 137, 145 | vtoclg 3417 |
. . . . . . . . . 10
⊢ ((◡𝐹 “ 𝑦) ∈ V → (((𝜑 ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → ((𝐹 ↾ (◡𝐹 “ 𝑦))‘𝑛) = 𝐺)) |
147 | 125, 129,
146 | sylc 65 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → ((𝐹 ↾ (◡𝐹 “ 𝑦))‘𝑛) = 𝐺) |
148 | 147 | adantllr 698 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → ((𝐹 ↾ (◡𝐹 “ 𝑦))‘𝑛) = 𝐺) |
149 | 81 | ad3antrrr 709 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (◡𝐹 “ 𝑦) ∈ V) |
150 | | simpll 750 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))) |
151 | 84 | ad3antrrr 709 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (◡𝐹 “ 𝑦) ∈ 𝒫 𝐶) |
152 | 109 | adantr 466 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (◡𝐹 “ 𝑦) ∈ Fin) |
153 | 151, 152 | elind 3949 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) |
154 | | simpr 471 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝑦) |
155 | 121 | eqcomd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 = (𝐹 “ (◡𝐹 “ 𝑦))) |
156 | 155 | adantr 466 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑦 = (𝐹 “ (◡𝐹 “ 𝑦))) |
157 | 154, 156 | eleqtrd 2852 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ (𝐹 “ (◡𝐹 “ 𝑦))) |
158 | 157 | adantllr 698 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ (𝐹 “ (◡𝐹 “ 𝑦))) |
159 | 150, 153,
158 | jca31 504 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (◡𝐹 “ 𝑦)))) |
160 | 130 | anbi2d 614 |
. . . . . . . . . . . 12
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ↔ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)))) |
161 | | imaeq2 5602 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (𝐹 “ 𝑥) = (𝐹 “ (◡𝐹 “ 𝑦))) |
162 | 161 | eleq2d 2836 |
. . . . . . . . . . . 12
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (𝑘 ∈ (𝐹 “ 𝑥) ↔ 𝑘 ∈ (𝐹 “ (◡𝐹 “ 𝑦)))) |
163 | 160, 162 | anbi12d 616 |
. . . . . . . . . . 11
⊢ (𝑥 = (◡𝐹 “ 𝑦) → ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) ↔ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (◡𝐹 “ 𝑦))))) |
164 | 163 | imbi1d 330 |
. . . . . . . . . 10
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ ℂ) ↔ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (◡𝐹 “ 𝑦))) → 𝐵 ∈ ℂ))) |
165 | | rge0ssre 12486 |
. . . . . . . . . . . . 13
⊢
(0[,)+∞) ⊆ ℝ |
166 | | ax-resscn 10198 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℂ |
167 | 165, 166 | sstri 3761 |
. . . . . . . . . . . 12
⊢
(0[,)+∞) ⊆ ℂ |
168 | | simplll 758 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝜑) |
169 | | simpllr 760 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) |
170 | | fimass 6222 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝐶⟶𝐴 → (𝐹 “ 𝑥) ⊆ 𝐴) |
171 | 23, 170 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹 “ 𝑥) ⊆ 𝐴) |
172 | 171 | ad2antrr 705 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → (𝐹 “ 𝑥) ⊆ 𝐴) |
173 | | simpr 471 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝑘 ∈ (𝐹 “ 𝑥)) |
174 | 172, 173 | sseldd 3753 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝑘 ∈ 𝐴) |
175 | 174 | adantllr 698 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝑘 ∈ 𝐴) |
176 | | foelrni 6388 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝐶–onto→𝐴 ∧ 𝑘 ∈ 𝐴) → ∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘) |
177 | 4, 176 | sylan 569 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘) |
178 | 177 | adantlr 694 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → ∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘) |
179 | | nfv 1995 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛 𝑘 ∈ 𝐴 |
180 | 106, 179 | nfan 1980 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) |
181 | | nfv 1995 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛 𝐵 ∈
(0[,)+∞) |
182 | | csbid 3690 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
⦋𝑘 /
𝑘⦌𝐵 = 𝐵 |
183 | 182 | eqcomi 2780 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐵 = ⦋𝑘 / 𝑘⦌𝐵 |
184 | 183 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 = ⦋𝑘 / 𝑘⦌𝐵) |
185 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹‘𝑛) = 𝑘 → (𝐹‘𝑛) = 𝑘) |
186 | 185 | eqcomd 2777 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹‘𝑛) = 𝑘 → 𝑘 = (𝐹‘𝑛)) |
187 | 186 | csbeq1d 3689 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹‘𝑛) = 𝑘 → ⦋𝑘 / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵) |
188 | 187 | 3ad2ant3 1129 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → ⦋𝑘 / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵) |
189 | 38 | idi 2 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷) |
190 | 189 | 3adant3 1126 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷) |
191 | 184, 188,
190 | 3eqtrd 2809 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 = 𝐷) |
192 | 191 | 3adant1r 1187 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 = 𝐷) |
193 | | 0xr 10291 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 ∈
ℝ* |
194 | 193 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 0 ∈
ℝ*) |
195 | | pnfxr 10297 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ +∞
∈ ℝ* |
196 | 195 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞
∈ ℝ*) |
197 | 64 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 𝐷 ∈
(0[,]+∞)) |
198 | | simpr 471 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → ¬ 𝐷 ∈
(0[,)+∞)) |
199 | 194, 196,
197, 198 | eliccnelico 40271 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 𝐷 = +∞) |
200 | 199 | eqcomd 2777 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞ =
𝐷) |
201 | | simpr 471 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝑛 ∈ 𝐶) |
202 | 64 | idi 2 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ (0[,]+∞)) |
203 | 14 | elrnmpt1 5511 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑛 ∈ 𝐶 ∧ 𝐷 ∈ (0[,]+∞)) → 𝐷 ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) |
204 | 201, 202,
203 | syl2anc 573 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) |
205 | 204 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 𝐷 ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) |
206 | 200, 205 | eqeltrd 2850 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞
∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) |
207 | 206 | adantllr 698 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞
∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) |
208 | | simpllr 760 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → ¬
+∞ ∈ ran (𝑛
∈ 𝐶 ↦ 𝐷)) |
209 | 207, 208 | condan 819 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ (0[,)+∞)) |
210 | 209 | 3adant3 1126 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐷 ∈ (0[,)+∞)) |
211 | 192, 210 | eqeltrd 2850 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 ∈ (0[,)+∞)) |
212 | 211 | 3exp 1112 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) → (𝑛 ∈ 𝐶 → ((𝐹‘𝑛) = 𝑘 → 𝐵 ∈ (0[,)+∞)))) |
213 | 212 | adantr 466 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → (𝑛 ∈ 𝐶 → ((𝐹‘𝑛) = 𝑘 → 𝐵 ∈ (0[,)+∞)))) |
214 | 180, 181,
213 | rexlimd 3174 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → (∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘 → 𝐵 ∈ (0[,)+∞))) |
215 | 178, 214 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) |
216 | 168, 169,
175, 215 | syl21anc 1475 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ (0[,)+∞)) |
217 | 167, 216 | sseldi 3750 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ ℂ) |
218 | 217 | idi 2 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ ℂ) |
219 | 164, 218 | vtoclg 3417 |
. . . . . . . . 9
⊢ ((◡𝐹 “ 𝑦) ∈ V → ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (◡𝐹 “ 𝑦))) → 𝐵 ∈ ℂ)) |
220 | 149, 159,
219 | sylc 65 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝐵 ∈ ℂ) |
221 | 100, 108,
36, 109, 124, 148, 220 | fsumf1of 40321 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ (◡𝐹 “ 𝑦)𝐷) |
222 | | sumeq1 14626 |
. . . . . . . . 9
⊢ (𝑥 = (◡𝐹 “ 𝑦) → Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑛 ∈ (◡𝐹 “ 𝑦)𝐷) |
223 | 222 | eqeq2d 2781 |
. . . . . . . 8
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ 𝑥 𝐷 ↔ Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ (◡𝐹 “ 𝑦)𝐷)) |
224 | 223 | rspcev 3460 |
. . . . . . 7
⊢ (((◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin) ∧ Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ (◡𝐹 “ 𝑦)𝐷) → ∃𝑥 ∈ (𝒫 𝐶 ∩ Fin)Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ 𝑥 𝐷) |
225 | 96, 221, 224 | syl2anc 573 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ∃𝑥 ∈ (𝒫 𝐶 ∩ Fin)Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ 𝑥 𝐷) |
226 | 71, 225 | rnmptssrn 39887 |
. . . . 5
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) → ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵) ⊆ ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷)) |
227 | | sumex 14625 |
. . . . . . 7
⊢
Σ𝑛 ∈
𝑥 𝐷 ∈ V |
228 | 227 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Σ𝑛 ∈ 𝑥 𝐷 ∈ V) |
229 | 6, 171 | ssexd 4940 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 “ 𝑥) ∈ V) |
230 | | elpwg 4306 |
. . . . . . . . . . . 12
⊢ ((𝐹 “ 𝑥) ∈ V → ((𝐹 “ 𝑥) ∈ 𝒫 𝐴 ↔ (𝐹 “ 𝑥) ⊆ 𝐴)) |
231 | 229, 230 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐹 “ 𝑥) ∈ 𝒫 𝐴 ↔ (𝐹 “ 𝑥) ⊆ 𝐴)) |
232 | 171, 231 | mpbird 247 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 “ 𝑥) ∈ 𝒫 𝐴) |
233 | 232 | adantr 466 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ 𝒫 𝐴) |
234 | 23 | ffund 6188 |
. . . . . . . . . . 11
⊢ (𝜑 → Fun 𝐹) |
235 | 234 | adantr 466 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Fun 𝐹) |
236 | | elinel2 3951 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝒫 𝐶 ∩ Fin) → 𝑥 ∈ Fin) |
237 | 236 | adantl 467 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝑥 ∈ Fin) |
238 | | imafi 8418 |
. . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ Fin) → (𝐹 “ 𝑥) ∈ Fin) |
239 | 235, 237,
238 | syl2anc 573 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ Fin) |
240 | 233, 239 | elind 3949 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ (𝒫 𝐴 ∩ Fin)) |
241 | 240 | adantlr 694 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ (𝒫 𝐴 ∩ Fin)) |
242 | | nfv 1995 |
. . . . . . . . . 10
⊢
Ⅎ𝑘 𝑥 ∈ (𝒫 𝐶 ∩ Fin) |
243 | 98, 242 | nfan 1980 |
. . . . . . . . 9
⊢
Ⅎ𝑘((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) |
244 | | nfv 1995 |
. . . . . . . . . 10
⊢
Ⅎ𝑛 𝑥 ∈ (𝒫 𝐶 ∩ Fin) |
245 | 106, 244 | nfan 1980 |
. . . . . . . . 9
⊢
Ⅎ𝑛((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) |
246 | 236 | adantl 467 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝑥 ∈ Fin) |
247 | 111 | adantr 466 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝐹:𝐶–1-1→𝐴) |
248 | | f1ores 6293 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐶–1-1→𝐴 ∧ 𝑥 ⊆ 𝐶) → (𝐹 ↾ 𝑥):𝑥–1-1-onto→(𝐹 “ 𝑥)) |
249 | 247, 142,
248 | syl2anc 573 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥–1-1-onto→(𝐹 “ 𝑥)) |
250 | 249 | adantlr 694 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥–1-1-onto→(𝐹 “ 𝑥)) |
251 | 145 | adantllr 698 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = 𝐺) |
252 | 243, 245,
36, 246, 250, 251, 217 | fsumf1of 40321 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵 = Σ𝑛 ∈ 𝑥 𝐷) |
253 | 252 | eqcomd 2777 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵) |
254 | | sumeq1 14626 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹 “ 𝑥) → Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵) |
255 | 254 | eqeq2d 2781 |
. . . . . . . 8
⊢ (𝑦 = (𝐹 “ 𝑥) → (Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ 𝑦 𝐵 ↔ Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵)) |
256 | 255 | rspcev 3460 |
. . . . . . 7
⊢ (((𝐹 “ 𝑥) ∈ (𝒫 𝐴 ∩ Fin) ∧ Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵) → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ 𝑦 𝐵) |
257 | 241, 253,
256 | syl2anc 573 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ 𝑦 𝐵) |
258 | 228, 257 | rnmptssrn 39887 |
. . . . 5
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) → ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷) ⊆ ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵)) |
259 | 226, 258 | eqssd 3769 |
. . . 4
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) → ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵) = ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷)) |
260 | 259 | supeq1d 8511 |
. . 3
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) → sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ*, < ) = sup(ran
(𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷), ℝ*, <
)) |
261 | 6 | adantr 466 |
. . . 4
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐴 ∈ V) |
262 | 98, 261, 215 | sge0revalmpt 41109 |
. . 3
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ*, <
)) |
263 | 1 | adantr 466 |
. . . 4
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐶 ∈ 𝑉) |
264 | 106, 263,
209 | sge0revalmpt 41109 |
. . 3
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) →
(Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷)) = sup(ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷), ℝ*, <
)) |
265 | 260, 262,
264 | 3eqtr4d 2815 |
. 2
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) =
(Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷))) |
266 | 69, 265 | pm2.61dan 814 |
1
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) =
(Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷))) |