Step | Hyp | Ref
| Expression |
1 | | sge0f1o.4 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
2 | | sge0f1o.5 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) |
3 | | f1ofo 6057 |
. . . . . . 7
⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶–onto→𝐴) |
4 | 2, 3 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐶–onto→𝐴) |
5 | | fornex 7028 |
. . . . . 6
⊢ (𝐶 ∈ 𝑉 → (𝐹:𝐶–onto→𝐴 → 𝐴 ∈ V)) |
6 | 1, 4, 5 | sylc 63 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ V) |
7 | 6 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐴 ∈ V) |
8 | | sge0f1o.1 |
. . . . . 6
⊢
Ⅎ𝑘𝜑 |
9 | | sge0f1o.7 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) |
10 | | eqid 2610 |
. . . . . 6
⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵) |
11 | 8, 9, 10 | fmptdf 6294 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶(0[,]+∞)) |
12 | 11 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶(0[,]+∞)) |
13 | | pnfex 9972 |
. . . . . . . 8
⊢ +∞
∈ V |
14 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑛 ∈ 𝐶 ↦ 𝐷) = (𝑛 ∈ 𝐶 ↦ 𝐷) |
15 | 14 | elrnmpt 5293 |
. . . . . . . 8
⊢ (+∞
∈ V → (+∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) ↔ ∃𝑛 ∈ 𝐶 +∞ = 𝐷)) |
16 | 13, 15 | ax-mp 5 |
. . . . . . 7
⊢ (+∞
∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) ↔ ∃𝑛 ∈ 𝐶 +∞ = 𝐷) |
17 | 16 | biimpi 205 |
. . . . . 6
⊢ (+∞
∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) → ∃𝑛 ∈ 𝐶 +∞ = 𝐷) |
18 | 17 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → ∃𝑛 ∈ 𝐶 +∞ = 𝐷) |
19 | | sge0f1o.2 |
. . . . . . 7
⊢
Ⅎ𝑛𝜑 |
20 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑛+∞
∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵) |
21 | | simp3 1056 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → +∞ = 𝐷) |
22 | | f1of 6050 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶⟶𝐴) |
23 | 2, 22 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:𝐶⟶𝐴) |
24 | 23 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) ∈ 𝐴) |
25 | | sge0f1o.6 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) |
26 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘(𝐹‘𝑛) |
27 | | nfv 1830 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘(𝐹‘𝑛) = 𝐺 |
28 | 26 | nfcsb1 3514 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵 |
29 | | nfcv 2751 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘𝐷 |
30 | 28, 29 | nfeq 2762 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷 |
31 | 27, 30 | nfim 1813 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘((𝐹‘𝑛) = 𝐺 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷) |
32 | | eqeq1 2614 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝐹‘𝑛) → (𝑘 = 𝐺 ↔ (𝐹‘𝑛) = 𝐺)) |
33 | | csbeq1a 3508 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵) |
34 | 33 | eqeq1d 2612 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝐹‘𝑛) → (𝐵 = 𝐷 ↔ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)) |
35 | 32, 34 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝐹‘𝑛) → ((𝑘 = 𝐺 → 𝐵 = 𝐷) ↔ ((𝐹‘𝑛) = 𝐺 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷))) |
36 | | sge0f1o.3 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷) |
37 | 26, 31, 35, 36 | vtoclgf 3237 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑛) ∈ 𝐴 → ((𝐹‘𝑛) = 𝐺 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)) |
38 | 24, 25, 37 | sylc 63 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷) |
39 | 38 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵) |
40 | 39 | 3adant3 1074 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → 𝐷 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵) |
41 | 21, 40 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → +∞ = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵) |
42 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝜑) |
43 | 42, 24 | jca 553 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴)) |
44 | | nfv 1830 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘(𝐹‘𝑛) ∈ 𝐴 |
45 | 8, 44 | nfan 1816 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘(𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) |
46 | 28 | nfel1 2765 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞) |
47 | 45, 46 | nfim 1813 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘((𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)) |
48 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝐹‘𝑛) → (𝑘 ∈ 𝐴 ↔ (𝐹‘𝑛) ∈ 𝐴)) |
49 | 48 | anbi2d 736 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝐹‘𝑛) → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴))) |
50 | 33 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝐹‘𝑛) → (𝐵 ∈ (0[,]+∞) ↔
⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞))) |
51 | 49, 50 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝐹‘𝑛) → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)))) |
52 | 26, 47, 51, 9 | vtoclgf 3237 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑛) ∈ 𝐴 → ((𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞))) |
53 | 24, 43, 52 | sylc 63 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)) |
54 | 28, 10, 33 | elrnmpt1sf 38371 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑛) ∈ 𝐴 ∧ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)) →
⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)) |
55 | 24, 53, 54 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)) |
56 | 55 | 3adant3 1074 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)) |
57 | 41, 56 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)) |
58 | 57 | 3exp 1256 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ 𝐶 → (+∞ = 𝐷 → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)))) |
59 | 19, 20, 58 | rexlimd 3008 |
. . . . . 6
⊢ (𝜑 → (∃𝑛 ∈ 𝐶 +∞ = 𝐷 → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))) |
60 | 59 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (∃𝑛 ∈ 𝐶 +∞ = 𝐷 → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))) |
61 | 18, 60 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)) |
62 | 7, 12, 61 | sge0pnfval 39266 |
. . 3
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = +∞) |
63 | 1 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐶 ∈ 𝑉) |
64 | 39, 53 | eqeltrd 2688 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ (0[,]+∞)) |
65 | 19, 64, 14 | fmptdf 6294 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ 𝐶 ↦ 𝐷):𝐶⟶(0[,]+∞)) |
66 | 65 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (𝑛 ∈ 𝐶 ↦ 𝐷):𝐶⟶(0[,]+∞)) |
67 | | simpr 476 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) |
68 | 63, 66, 67 | sge0pnfval 39266 |
. . 3
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) →
(Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷)) = +∞) |
69 | 62, 68 | eqtr4d 2647 |
. 2
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) =
(Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷))) |
70 | | sumex 14266 |
. . . . . . 7
⊢
Σ𝑘 ∈
𝑦 𝐵 ∈ V |
71 | 70 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑘 ∈ 𝑦 𝐵 ∈ V) |
72 | | cnvimass 5404 |
. . . . . . . . . . . . 13
⊢ (◡𝐹 “ 𝑦) ⊆ dom 𝐹 |
73 | 72 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡𝐹 “ 𝑦) ⊆ dom 𝐹) |
74 | | fdm 5964 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝐶⟶𝐴 → dom 𝐹 = 𝐶) |
75 | 23, 74 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom 𝐹 = 𝐶) |
76 | 73, 75 | sseqtrd 3604 |
. . . . . . . . . . 11
⊢ (𝜑 → (◡𝐹 “ 𝑦) ⊆ 𝐶) |
77 | | fex 6394 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐶⟶𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐹 ∈ V) |
78 | 23, 1, 77 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 ∈ V) |
79 | | cnvexg 7005 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ V → ◡𝐹 ∈ V) |
80 | 78, 79 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ◡𝐹 ∈ V) |
81 | | imaexg 6995 |
. . . . . . . . . . . . 13
⊢ (◡𝐹 ∈ V → (◡𝐹 “ 𝑦) ∈ V) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡𝐹 “ 𝑦) ∈ V) |
83 | | elpwg 4116 |
. . . . . . . . . . . 12
⊢ ((◡𝐹 “ 𝑦) ∈ V → ((◡𝐹 “ 𝑦) ∈ 𝒫 𝐶 ↔ (◡𝐹 “ 𝑦) ⊆ 𝐶)) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((◡𝐹 “ 𝑦) ∈ 𝒫 𝐶 ↔ (◡𝐹 “ 𝑦) ⊆ 𝐶)) |
85 | 76, 84 | mpbird 246 |
. . . . . . . . . 10
⊢ (𝜑 → (◡𝐹 “ 𝑦) ∈ 𝒫 𝐶) |
86 | 85 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (◡𝐹 “ 𝑦) ∈ 𝒫 𝐶) |
87 | | f1ocnv 6062 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝐶–1-1-onto→𝐴 → ◡𝐹:𝐴–1-1-onto→𝐶) |
88 | 2, 87 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ◡𝐹:𝐴–1-1-onto→𝐶) |
89 | | f1ofun 6052 |
. . . . . . . . . . . 12
⊢ (◡𝐹:𝐴–1-1-onto→𝐶 → Fun ◡𝐹) |
90 | 88, 89 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → Fun ◡𝐹) |
91 | 90 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Fun ◡𝐹) |
92 | | elinel2 3762 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin) |
93 | 92 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ∈ Fin) |
94 | | imafi 8142 |
. . . . . . . . . 10
⊢ ((Fun
◡𝐹 ∧ 𝑦 ∈ Fin) → (◡𝐹 “ 𝑦) ∈ Fin) |
95 | 91, 93, 94 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (◡𝐹 “ 𝑦) ∈ Fin) |
96 | 86, 95 | elind 3760 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) |
97 | 96 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) |
98 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑘 ¬
+∞ ∈ ran (𝑛
∈ 𝐶 ↦ 𝐷) |
99 | 8, 98 | nfan 1816 |
. . . . . . . . 9
⊢
Ⅎ𝑘(𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) |
100 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎ𝑘 𝑦 ∈ (𝒫 𝐴 ∩ Fin) |
101 | 99, 100 | nfan 1816 |
. . . . . . . 8
⊢
Ⅎ𝑘((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) |
102 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛+∞ |
103 | | nfmpt1 4675 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛(𝑛 ∈ 𝐶 ↦ 𝐷) |
104 | 103 | nfrn 5289 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛ran
(𝑛 ∈ 𝐶 ↦ 𝐷) |
105 | 102, 104 | nfel 2763 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛+∞
∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) |
106 | 105 | nfn 1768 |
. . . . . . . . . 10
⊢
Ⅎ𝑛 ¬
+∞ ∈ ran (𝑛
∈ 𝐶 ↦ 𝐷) |
107 | 19, 106 | nfan 1816 |
. . . . . . . . 9
⊢
Ⅎ𝑛(𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) |
108 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎ𝑛 𝑦 ∈ (𝒫 𝐴 ∩ Fin) |
109 | 107, 108 | nfan 1816 |
. . . . . . . 8
⊢
Ⅎ𝑛((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) |
110 | 95 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (◡𝐹 “ 𝑦) ∈ Fin) |
111 | | f1of1 6049 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶–1-1→𝐴) |
112 | 2, 111 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝐶–1-1→𝐴) |
113 | 112 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐹:𝐶–1-1→𝐴) |
114 | 84 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((◡𝐹 “ 𝑦) ∈ 𝒫 𝐶 ↔ (◡𝐹 “ 𝑦) ⊆ 𝐶)) |
115 | 86, 114 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (◡𝐹 “ 𝑦) ⊆ 𝐶) |
116 | | f1ores 6064 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐶–1-1→𝐴 ∧ (◡𝐹 “ 𝑦) ⊆ 𝐶) → (𝐹 ↾ (◡𝐹 “ 𝑦)):(◡𝐹 “ 𝑦)–1-1-onto→(𝐹 “ (◡𝐹 “ 𝑦))) |
117 | 113, 115,
116 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ (◡𝐹 “ 𝑦)):(◡𝐹 “ 𝑦)–1-1-onto→(𝐹 “ (◡𝐹 “ 𝑦))) |
118 | 4 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐹:𝐶–onto→𝐴) |
119 | | elpwinss 38241 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ⊆ 𝐴) |
120 | 119 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ⊆ 𝐴) |
121 | | foimacnv 6067 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐶–onto→𝐴 ∧ 𝑦 ⊆ 𝐴) → (𝐹 “ (◡𝐹 “ 𝑦)) = 𝑦) |
122 | 118, 120,
121 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 “ (◡𝐹 “ 𝑦)) = 𝑦) |
123 | 122 | f1oeq3d 6047 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐹 ↾ (◡𝐹 “ 𝑦)):(◡𝐹 “ 𝑦)–1-1-onto→(𝐹 “ (◡𝐹 “ 𝑦)) ↔ (𝐹 ↾ (◡𝐹 “ 𝑦)):(◡𝐹 “ 𝑦)–1-1-onto→𝑦)) |
124 | 117, 123 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ (◡𝐹 “ 𝑦)):(◡𝐹 “ 𝑦)–1-1-onto→𝑦) |
125 | 124 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ (◡𝐹 “ 𝑦)):(◡𝐹 “ 𝑦)–1-1-onto→𝑦) |
126 | 82 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → (◡𝐹 “ 𝑦) ∈ V) |
127 | | simpll 786 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → 𝜑) |
128 | 96 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) |
129 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → 𝑛 ∈ (◡𝐹 “ 𝑦)) |
130 | 127, 128,
129 | jca31 555 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → ((𝜑 ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦))) |
131 | | eleq1 2676 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↔ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))) |
132 | 131 | anbi2d 736 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (◡𝐹 “ 𝑦) → ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ↔ (𝜑 ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)))) |
133 | | eleq2 2677 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (𝑛 ∈ 𝑥 ↔ 𝑛 ∈ (◡𝐹 “ 𝑦))) |
134 | 132, 133 | anbi12d 743 |
. . . . . . . . . . . 12
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) ↔ ((𝜑 ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)))) |
135 | | reseq2 5312 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (𝐹 ↾ 𝑥) = (𝐹 ↾ (◡𝐹 “ 𝑦))) |
136 | 135 | fveq1d 6105 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (◡𝐹 “ 𝑦) → ((𝐹 ↾ 𝑥)‘𝑛) = ((𝐹 ↾ (◡𝐹 “ 𝑦))‘𝑛)) |
137 | 136 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (((𝐹 ↾ 𝑥)‘𝑛) = 𝐺 ↔ ((𝐹 ↾ (◡𝐹 “ 𝑦))‘𝑛) = 𝐺)) |
138 | 134, 137 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑥 = (◡𝐹 “ 𝑦) → ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = 𝐺) ↔ (((𝜑 ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → ((𝐹 ↾ (◡𝐹 “ 𝑦))‘𝑛) = 𝐺))) |
139 | | fvres 6117 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ 𝑥 → ((𝐹 ↾ 𝑥)‘𝑛) = (𝐹‘𝑛)) |
140 | 139 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = (𝐹‘𝑛)) |
141 | | simpll 786 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → 𝜑) |
142 | | elpwinss 38241 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝒫 𝐶 ∩ Fin) → 𝑥 ⊆ 𝐶) |
143 | 142 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝑥 ⊆ 𝐶) |
144 | 143 | sselda 3568 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → 𝑛 ∈ 𝐶) |
145 | 141, 144,
25 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → (𝐹‘𝑛) = 𝐺) |
146 | 140, 145 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = 𝐺) |
147 | 138, 146 | vtoclg 3239 |
. . . . . . . . . 10
⊢ ((◡𝐹 “ 𝑦) ∈ V → (((𝜑 ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → ((𝐹 ↾ (◡𝐹 “ 𝑦))‘𝑛) = 𝐺)) |
148 | 126, 130,
147 | sylc 63 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → ((𝐹 ↾ (◡𝐹 “ 𝑦))‘𝑛) = 𝐺) |
149 | 148 | adantllr 751 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → ((𝐹 ↾ (◡𝐹 “ 𝑦))‘𝑛) = 𝐺) |
150 | 82 | ad3antrrr 762 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (◡𝐹 “ 𝑦) ∈ V) |
151 | | simpll 786 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))) |
152 | 85 | ad3antrrr 762 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (◡𝐹 “ 𝑦) ∈ 𝒫 𝐶) |
153 | 110 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (◡𝐹 “ 𝑦) ∈ Fin) |
154 | 152, 153 | elind 3760 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) |
155 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝑦) |
156 | 122 | eqcomd 2616 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 = (𝐹 “ (◡𝐹 “ 𝑦))) |
157 | 156 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑦 = (𝐹 “ (◡𝐹 “ 𝑦))) |
158 | 155, 157 | eleqtrd 2690 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ (𝐹 “ (◡𝐹 “ 𝑦))) |
159 | 158 | adantllr 751 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ (𝐹 “ (◡𝐹 “ 𝑦))) |
160 | 151, 154,
159 | jca31 555 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (◡𝐹 “ 𝑦)))) |
161 | 131 | anbi2d 736 |
. . . . . . . . . . . 12
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ↔ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)))) |
162 | | imaeq2 5381 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (𝐹 “ 𝑥) = (𝐹 “ (◡𝐹 “ 𝑦))) |
163 | 162 | eleq2d 2673 |
. . . . . . . . . . . 12
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (𝑘 ∈ (𝐹 “ 𝑥) ↔ 𝑘 ∈ (𝐹 “ (◡𝐹 “ 𝑦)))) |
164 | 161, 163 | anbi12d 743 |
. . . . . . . . . . 11
⊢ (𝑥 = (◡𝐹 “ 𝑦) → ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) ↔ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (◡𝐹 “ 𝑦))))) |
165 | 164 | imbi1d 330 |
. . . . . . . . . 10
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ ℂ) ↔ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (◡𝐹 “ 𝑦))) → 𝐵 ∈ ℂ))) |
166 | | rge0ssre 12151 |
. . . . . . . . . . . . 13
⊢
(0[,)+∞) ⊆ ℝ |
167 | | ax-resscn 9872 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℂ |
168 | 166, 167 | sstri 3577 |
. . . . . . . . . . . 12
⊢
(0[,)+∞) ⊆ ℂ |
169 | | simplll 794 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝜑) |
170 | | simpllr 795 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) |
171 | | fimass 5994 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝐶⟶𝐴 → (𝐹 “ 𝑥) ⊆ 𝐴) |
172 | 23, 171 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹 “ 𝑥) ⊆ 𝐴) |
173 | 172 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → (𝐹 “ 𝑥) ⊆ 𝐴) |
174 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝑘 ∈ (𝐹 “ 𝑥)) |
175 | 173, 174 | sseldd 3569 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝑘 ∈ 𝐴) |
176 | 175 | adantllr 751 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝑘 ∈ 𝐴) |
177 | | foelrni 6154 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝐶–onto→𝐴 ∧ 𝑘 ∈ 𝐴) → ∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘) |
178 | 4, 177 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘) |
179 | 178 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → ∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘) |
180 | | nfv 1830 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛 𝑘 ∈ 𝐴 |
181 | 107, 180 | nfan 1816 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) |
182 | | nfv 1830 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛 𝐵 ∈
(0[,)+∞) |
183 | | csbid 3507 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
⦋𝑘 /
𝑘⦌𝐵 = 𝐵 |
184 | 183 | eqcomi 2619 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐵 = ⦋𝑘 / 𝑘⦌𝐵 |
185 | 184 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 = ⦋𝑘 / 𝑘⦌𝐵) |
186 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹‘𝑛) = 𝑘 → (𝐹‘𝑛) = 𝑘) |
187 | 186 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹‘𝑛) = 𝑘 → 𝑘 = (𝐹‘𝑛)) |
188 | 187 | csbeq1d 3506 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹‘𝑛) = 𝑘 → ⦋𝑘 / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵) |
189 | 188 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → ⦋𝑘 / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵) |
190 | 38 | idi 2 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷) |
191 | 190 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷) |
192 | 185, 189,
191 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 = 𝐷) |
193 | 192 | 3adant1r 1311 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 = 𝐷) |
194 | | 0xr 9965 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 ∈
ℝ* |
195 | 194 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 0 ∈
ℝ*) |
196 | | pnfxr 9971 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ +∞
∈ ℝ* |
197 | 196 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞
∈ ℝ*) |
198 | 64 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 𝐷 ∈
(0[,]+∞)) |
199 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → ¬ 𝐷 ∈
(0[,)+∞)) |
200 | 195, 197,
198, 199 | eliccnelico 38603 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 𝐷 = +∞) |
201 | 200 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞ =
𝐷) |
202 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝑛 ∈ 𝐶) |
203 | 64 | idi 2 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ (0[,]+∞)) |
204 | 14 | elrnmpt1 5295 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑛 ∈ 𝐶 ∧ 𝐷 ∈ (0[,]+∞)) → 𝐷 ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) |
205 | 202, 203,
204 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) |
206 | 205 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 𝐷 ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) |
207 | 201, 206 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞
∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) |
208 | 207 | adantllr 751 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞
∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) |
209 | | simpllr 795 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → ¬
+∞ ∈ ran (𝑛
∈ 𝐶 ↦ 𝐷)) |
210 | 208, 209 | condan 831 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ (0[,)+∞)) |
211 | 210 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐷 ∈ (0[,)+∞)) |
212 | 193, 211 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 ∈ (0[,)+∞)) |
213 | 212 | 3exp 1256 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) → (𝑛 ∈ 𝐶 → ((𝐹‘𝑛) = 𝑘 → 𝐵 ∈ (0[,)+∞)))) |
214 | 213 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → (𝑛 ∈ 𝐶 → ((𝐹‘𝑛) = 𝑘 → 𝐵 ∈ (0[,)+∞)))) |
215 | 181, 182,
214 | rexlimd 3008 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → (∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘 → 𝐵 ∈ (0[,)+∞))) |
216 | 179, 215 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) |
217 | 169, 170,
176, 216 | syl21anc 1317 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ (0[,)+∞)) |
218 | 168, 217 | sseldi 3566 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ ℂ) |
219 | 218 | idi 2 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ ℂ) |
220 | 165, 219 | vtoclg 3239 |
. . . . . . . . 9
⊢ ((◡𝐹 “ 𝑦) ∈ V → ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (◡𝐹 “ 𝑦))) → 𝐵 ∈ ℂ)) |
221 | 150, 160,
220 | sylc 63 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝐵 ∈ ℂ) |
222 | 101, 109,
36, 110, 125, 149, 221 | fsumf1of 38641 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ (◡𝐹 “ 𝑦)𝐷) |
223 | | sumeq1 14267 |
. . . . . . . . 9
⊢ (𝑥 = (◡𝐹 “ 𝑦) → Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑛 ∈ (◡𝐹 “ 𝑦)𝐷) |
224 | 223 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ 𝑥 𝐷 ↔ Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ (◡𝐹 “ 𝑦)𝐷)) |
225 | 224 | rspcev 3282 |
. . . . . . 7
⊢ (((◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin) ∧ Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ (◡𝐹 “ 𝑦)𝐷) → ∃𝑥 ∈ (𝒫 𝐶 ∩ Fin)Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ 𝑥 𝐷) |
226 | 97, 222, 225 | syl2anc 691 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ∃𝑥 ∈ (𝒫 𝐶 ∩ Fin)Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ 𝑥 𝐷) |
227 | 71, 226 | rnmptssrn 38363 |
. . . . 5
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) → ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵) ⊆ ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷)) |
228 | | sumex 14266 |
. . . . . . 7
⊢
Σ𝑛 ∈
𝑥 𝐷 ∈ V |
229 | 228 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Σ𝑛 ∈ 𝑥 𝐷 ∈ V) |
230 | 6, 172 | ssexd 4733 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 “ 𝑥) ∈ V) |
231 | | elpwg 4116 |
. . . . . . . . . . . 12
⊢ ((𝐹 “ 𝑥) ∈ V → ((𝐹 “ 𝑥) ∈ 𝒫 𝐴 ↔ (𝐹 “ 𝑥) ⊆ 𝐴)) |
232 | 230, 231 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐹 “ 𝑥) ∈ 𝒫 𝐴 ↔ (𝐹 “ 𝑥) ⊆ 𝐴)) |
233 | 172, 232 | mpbird 246 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 “ 𝑥) ∈ 𝒫 𝐴) |
234 | 233 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ 𝒫 𝐴) |
235 | | ffun 5961 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐶⟶𝐴 → Fun 𝐹) |
236 | 23, 235 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → Fun 𝐹) |
237 | 236 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Fun 𝐹) |
238 | | elinel2 3762 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝒫 𝐶 ∩ Fin) → 𝑥 ∈ Fin) |
239 | 238 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝑥 ∈ Fin) |
240 | | imafi 8142 |
. . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ Fin) → (𝐹 “ 𝑥) ∈ Fin) |
241 | 237, 239,
240 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ Fin) |
242 | 234, 241 | elind 3760 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ (𝒫 𝐴 ∩ Fin)) |
243 | 242 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ (𝒫 𝐴 ∩ Fin)) |
244 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑘 𝑥 ∈ (𝒫 𝐶 ∩ Fin) |
245 | 99, 244 | nfan 1816 |
. . . . . . . . 9
⊢
Ⅎ𝑘((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) |
246 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑛 𝑥 ∈ (𝒫 𝐶 ∩ Fin) |
247 | 107, 246 | nfan 1816 |
. . . . . . . . 9
⊢
Ⅎ𝑛((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) |
248 | 238 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝑥 ∈ Fin) |
249 | 112 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝐹:𝐶–1-1→𝐴) |
250 | | f1ores 6064 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐶–1-1→𝐴 ∧ 𝑥 ⊆ 𝐶) → (𝐹 ↾ 𝑥):𝑥–1-1-onto→(𝐹 “ 𝑥)) |
251 | 249, 143,
250 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥–1-1-onto→(𝐹 “ 𝑥)) |
252 | 251 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥–1-1-onto→(𝐹 “ 𝑥)) |
253 | 146 | adantllr 751 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = 𝐺) |
254 | 245, 247,
36, 248, 252, 253, 218 | fsumf1of 38641 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵 = Σ𝑛 ∈ 𝑥 𝐷) |
255 | 254 | eqcomd 2616 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵) |
256 | | sumeq1 14267 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹 “ 𝑥) → Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵) |
257 | 256 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑦 = (𝐹 “ 𝑥) → (Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ 𝑦 𝐵 ↔ Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵)) |
258 | 257 | rspcev 3282 |
. . . . . . 7
⊢ (((𝐹 “ 𝑥) ∈ (𝒫 𝐴 ∩ Fin) ∧ Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵) → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ 𝑦 𝐵) |
259 | 243, 255,
258 | syl2anc 691 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ 𝑦 𝐵) |
260 | 229, 259 | rnmptssrn 38363 |
. . . . 5
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) → ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷) ⊆ ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵)) |
261 | 227, 260 | eqssd 3585 |
. . . 4
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) → ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵) = ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷)) |
262 | 261 | supeq1d 8235 |
. . 3
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) → sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ*, < ) = sup(ran
(𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷), ℝ*, <
)) |
263 | 6 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐴 ∈ V) |
264 | 99, 263, 216 | sge0revalmpt 39271 |
. . 3
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ*, <
)) |
265 | 1 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐶 ∈ 𝑉) |
266 | 107, 265,
210 | sge0revalmpt 39271 |
. . 3
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) →
(Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷)) = sup(ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷), ℝ*, <
)) |
267 | 262, 264,
266 | 3eqtr4d 2654 |
. 2
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) =
(Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷))) |
268 | 69, 267 | pm2.61dan 828 |
1
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) =
(Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷))) |