Step | Hyp | Ref
| Expression |
1 | | sge0f1o.4 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
2 | | sge0f1o.5 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) |
3 | | f1ofo 6855 |
. . . . . . 7
⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶–onto→𝐴) |
4 | 2, 3 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐶–onto→𝐴) |
5 | | focdmex 7978 |
. . . . . 6
⊢ (𝐶 ∈ 𝑉 → (𝐹:𝐶–onto→𝐴 → 𝐴 ∈ V)) |
6 | 1, 4, 5 | sylc 65 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ V) |
7 | 6 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐴 ∈ V) |
8 | | sge0f1o.1 |
. . . . . 6
⊢
Ⅎ𝑘𝜑 |
9 | | sge0f1o.7 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) |
10 | 8, 9 | fmptd2f 45177 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶(0[,]+∞)) |
11 | 10 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶(0[,]+∞)) |
12 | | sge0f1o.2 |
. . . . . 6
⊢
Ⅎ𝑛𝜑 |
13 | | nfv 1911 |
. . . . . 6
⊢
Ⅎ𝑛+∞
∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵) |
14 | | simp3 1137 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → +∞ = 𝐷) |
15 | | f1of 6848 |
. . . . . . . . . . . . . 14
⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶⟶𝐴) |
16 | 2, 15 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:𝐶⟶𝐴) |
17 | 16 | ffvelcdmda 7103 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) ∈ 𝐴) |
18 | | sge0f1o.6 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) |
19 | | nfv 1911 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘(𝐹‘𝑛) = 𝐺 |
20 | | nfcsb1v 3932 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵 |
21 | 20 | nfeq1 2918 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷 |
22 | 19, 21 | nfim 1893 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘((𝐹‘𝑛) = 𝐺 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷) |
23 | | eqeq1 2738 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝐹‘𝑛) → (𝑘 = 𝐺 ↔ (𝐹‘𝑛) = 𝐺)) |
24 | | csbeq1a 3921 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵) |
25 | 24 | eqeq1d 2736 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝐹‘𝑛) → (𝐵 = 𝐷 ↔ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)) |
26 | 23, 25 | imbi12d 344 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝐹‘𝑛) → ((𝑘 = 𝐺 → 𝐵 = 𝐷) ↔ ((𝐹‘𝑛) = 𝐺 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷))) |
27 | | sge0f1o.3 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷) |
28 | 22, 26, 27 | vtoclg1f 3569 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑛) ∈ 𝐴 → ((𝐹‘𝑛) = 𝐺 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)) |
29 | 17, 18, 28 | sylc 65 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷) |
30 | 29 | eqcomd 2740 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵) |
31 | 30 | 3adant3 1131 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → 𝐷 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵) |
32 | 14, 31 | eqtrd 2774 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → +∞ = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵) |
33 | | simpl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝜑) |
34 | 33, 17 | jca 511 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴)) |
35 | | nfv 1911 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘(𝐹‘𝑛) ∈ 𝐴 |
36 | 8, 35 | nfan 1896 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘(𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) |
37 | 20 | nfel1 2919 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞) |
38 | 36, 37 | nfim 1893 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘((𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)) |
39 | | eleq1 2826 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝐹‘𝑛) → (𝑘 ∈ 𝐴 ↔ (𝐹‘𝑛) ∈ 𝐴)) |
40 | 39 | anbi2d 630 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝐹‘𝑛) → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴))) |
41 | 24 | eleq1d 2823 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝐹‘𝑛) → (𝐵 ∈ (0[,]+∞) ↔
⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞))) |
42 | 40, 41 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝐹‘𝑛) → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)))) |
43 | 38, 42, 9 | vtoclg1f 3569 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑛) ∈ 𝐴 → ((𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞))) |
44 | 17, 34, 43 | sylc 65 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)) |
45 | | eqid 2734 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵) |
46 | 20, 45, 24 | elrnmpt1sf 45131 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑛) ∈ 𝐴 ∧ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)) →
⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)) |
47 | 17, 44, 46 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)) |
48 | 47 | 3adant3 1131 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)) |
49 | 32, 48 | eqeltrd 2838 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)) |
50 | 49 | 3exp 1118 |
. . . . . 6
⊢ (𝜑 → (𝑛 ∈ 𝐶 → (+∞ = 𝐷 → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)))) |
51 | 12, 13, 50 | rexlimd 3263 |
. . . . 5
⊢ (𝜑 → (∃𝑛 ∈ 𝐶 +∞ = 𝐷 → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))) |
52 | | pnfex 11311 |
. . . . . . 7
⊢ +∞
∈ V |
53 | | eqid 2734 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝐶 ↦ 𝐷) = (𝑛 ∈ 𝐶 ↦ 𝐷) |
54 | 53 | elrnmpt 5971 |
. . . . . . 7
⊢ (+∞
∈ V → (+∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) ↔ ∃𝑛 ∈ 𝐶 +∞ = 𝐷)) |
55 | 52, 54 | ax-mp 5 |
. . . . . 6
⊢ (+∞
∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) ↔ ∃𝑛 ∈ 𝐶 +∞ = 𝐷) |
56 | 55 | biimpi 216 |
. . . . 5
⊢ (+∞
∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) → ∃𝑛 ∈ 𝐶 +∞ = 𝐷) |
57 | 51, 56 | impel 505 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)) |
58 | 7, 11, 57 | sge0pnfval 46328 |
. . 3
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = +∞) |
59 | 1 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐶 ∈ 𝑉) |
60 | 30, 44 | eqeltrd 2838 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ (0[,]+∞)) |
61 | 12, 60 | fmptd2f 45177 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ 𝐶 ↦ 𝐷):𝐶⟶(0[,]+∞)) |
62 | 61 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (𝑛 ∈ 𝐶 ↦ 𝐷):𝐶⟶(0[,]+∞)) |
63 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) |
64 | 59, 62, 63 | sge0pnfval 46328 |
. . 3
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) →
(Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷)) = +∞) |
65 | 58, 64 | eqtr4d 2777 |
. 2
⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) =
(Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷))) |
66 | | sumex 15720 |
. . . . . . 7
⊢
Σ𝑘 ∈
𝑦 𝐵 ∈ V |
67 | 66 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑘 ∈ 𝑦 𝐵 ∈ V) |
68 | | cnvimass 6101 |
. . . . . . . . . . . 12
⊢ (◡𝐹 “ 𝑦) ⊆ dom 𝐹 |
69 | 68, 16 | fssdm 6755 |
. . . . . . . . . . 11
⊢ (𝜑 → (◡𝐹 “ 𝑦) ⊆ 𝐶) |
70 | 1, 69 | sselpwd 5333 |
. . . . . . . . . 10
⊢ (𝜑 → (◡𝐹 “ 𝑦) ∈ 𝒫 𝐶) |
71 | 70 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (◡𝐹 “ 𝑦) ∈ 𝒫 𝐶) |
72 | | f1ocnv 6860 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐶–1-1-onto→𝐴 → ◡𝐹:𝐴–1-1-onto→𝐶) |
73 | 2, 72 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ◡𝐹:𝐴–1-1-onto→𝐶) |
74 | | f1ofun 6850 |
. . . . . . . . . . 11
⊢ (◡𝐹:𝐴–1-1-onto→𝐶 → Fun ◡𝐹) |
75 | 73, 74 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → Fun ◡𝐹) |
76 | | elinel2 4211 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin) |
77 | | imafi 9350 |
. . . . . . . . . 10
⊢ ((Fun
◡𝐹 ∧ 𝑦 ∈ Fin) → (◡𝐹 “ 𝑦) ∈ Fin) |
78 | 75, 76, 77 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (◡𝐹 “ 𝑦) ∈ Fin) |
79 | 71, 78 | elind 4209 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) |
80 | 79 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) |
81 | | nfv 1911 |
. . . . . . . . . 10
⊢
Ⅎ𝑘 ¬
+∞ ∈ ran (𝑛
∈ 𝐶 ↦ 𝐷) |
82 | 8, 81 | nfan 1896 |
. . . . . . . . 9
⊢
Ⅎ𝑘(𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) |
83 | | nfv 1911 |
. . . . . . . . 9
⊢
Ⅎ𝑘 𝑦 ∈ (𝒫 𝐴 ∩ Fin) |
84 | 82, 83 | nfan 1896 |
. . . . . . . 8
⊢
Ⅎ𝑘((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) |
85 | | nfmpt1 5255 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛(𝑛 ∈ 𝐶 ↦ 𝐷) |
86 | 85 | nfrn 5965 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛ran
(𝑛 ∈ 𝐶 ↦ 𝐷) |
87 | 86 | nfel2 2921 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛+∞
∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) |
88 | 87 | nfn 1854 |
. . . . . . . . . 10
⊢
Ⅎ𝑛 ¬
+∞ ∈ ran (𝑛
∈ 𝐶 ↦ 𝐷) |
89 | 12, 88 | nfan 1896 |
. . . . . . . . 9
⊢
Ⅎ𝑛(𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) |
90 | | nfv 1911 |
. . . . . . . . 9
⊢
Ⅎ𝑛 𝑦 ∈ (𝒫 𝐴 ∩ Fin) |
91 | 89, 90 | nfan 1896 |
. . . . . . . 8
⊢
Ⅎ𝑛((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) |
92 | 78 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (◡𝐹 “ 𝑦) ∈ Fin) |
93 | | f1of1 6847 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶–1-1→𝐴) |
94 | 2, 93 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝐶–1-1→𝐴) |
95 | 94 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐹:𝐶–1-1→𝐴) |
96 | 69 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (◡𝐹 “ 𝑦) ⊆ 𝐶) |
97 | | f1ores 6862 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐶–1-1→𝐴 ∧ (◡𝐹 “ 𝑦) ⊆ 𝐶) → (𝐹 ↾ (◡𝐹 “ 𝑦)):(◡𝐹 “ 𝑦)–1-1-onto→(𝐹 “ (◡𝐹 “ 𝑦))) |
98 | 95, 96, 97 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ (◡𝐹 “ 𝑦)):(◡𝐹 “ 𝑦)–1-1-onto→(𝐹 “ (◡𝐹 “ 𝑦))) |
99 | | elpwinss 44988 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ⊆ 𝐴) |
100 | | foimacnv 6865 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐶–onto→𝐴 ∧ 𝑦 ⊆ 𝐴) → (𝐹 “ (◡𝐹 “ 𝑦)) = 𝑦) |
101 | 4, 99, 100 | syl2an 596 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 “ (◡𝐹 “ 𝑦)) = 𝑦) |
102 | 101 | f1oeq3d 6845 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐹 ↾ (◡𝐹 “ 𝑦)):(◡𝐹 “ 𝑦)–1-1-onto→(𝐹 “ (◡𝐹 “ 𝑦)) ↔ (𝐹 ↾ (◡𝐹 “ 𝑦)):(◡𝐹 “ 𝑦)–1-1-onto→𝑦)) |
103 | 98, 102 | mpbid 232 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ (◡𝐹 “ 𝑦)):(◡𝐹 “ 𝑦)–1-1-onto→𝑦) |
104 | 103 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ (◡𝐹 “ 𝑦)):(◡𝐹 “ 𝑦)–1-1-onto→𝑦) |
105 | 16, 1 | fexd 7246 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ V) |
106 | | cnvexg 7946 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ V → ◡𝐹 ∈ V) |
107 | 105, 106 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ◡𝐹 ∈ V) |
108 | 107 | imaexd 7938 |
. . . . . . . . . . 11
⊢ (𝜑 → (◡𝐹 “ 𝑦) ∈ V) |
109 | 108 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → (◡𝐹 “ 𝑦) ∈ V) |
110 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → 𝜑) |
111 | 79 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) |
112 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → 𝑛 ∈ (◡𝐹 “ 𝑦)) |
113 | 110, 111,
112 | jca31 514 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → ((𝜑 ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦))) |
114 | | eleq1 2826 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↔ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))) |
115 | 114 | anbi2d 630 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (◡𝐹 “ 𝑦) → ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ↔ (𝜑 ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)))) |
116 | | eleq2w2 2730 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (𝑛 ∈ 𝑥 ↔ 𝑛 ∈ (◡𝐹 “ 𝑦))) |
117 | 115, 116 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) ↔ ((𝜑 ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)))) |
118 | | reseq2 5994 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (𝐹 ↾ 𝑥) = (𝐹 ↾ (◡𝐹 “ 𝑦))) |
119 | 118 | fveq1d 6908 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (◡𝐹 “ 𝑦) → ((𝐹 ↾ 𝑥)‘𝑛) = ((𝐹 ↾ (◡𝐹 “ 𝑦))‘𝑛)) |
120 | 119 | eqeq1d 2736 |
. . . . . . . . . . . 12
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (((𝐹 ↾ 𝑥)‘𝑛) = 𝐺 ↔ ((𝐹 ↾ (◡𝐹 “ 𝑦))‘𝑛) = 𝐺)) |
121 | 117, 120 | imbi12d 344 |
. . . . . . . . . . 11
⊢ (𝑥 = (◡𝐹 “ 𝑦) → ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = 𝐺) ↔ (((𝜑 ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → ((𝐹 ↾ (◡𝐹 “ 𝑦))‘𝑛) = 𝐺))) |
122 | | fvres 6925 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ 𝑥 → ((𝐹 ↾ 𝑥)‘𝑛) = (𝐹‘𝑛)) |
123 | 122 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = (𝐹‘𝑛)) |
124 | | simpll 767 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → 𝜑) |
125 | | elpwinss 44988 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝒫 𝐶 ∩ Fin) → 𝑥 ⊆ 𝐶) |
126 | 125 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝑥 ⊆ 𝐶) |
127 | 126 | sselda 3994 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → 𝑛 ∈ 𝐶) |
128 | 124, 127,
18 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → (𝐹‘𝑛) = 𝐺) |
129 | 123, 128 | eqtrd 2774 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = 𝐺) |
130 | 121, 129 | vtoclg 3553 |
. . . . . . . . . 10
⊢ ((◡𝐹 “ 𝑦) ∈ V → (((𝜑 ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → ((𝐹 ↾ (◡𝐹 “ 𝑦))‘𝑛) = 𝐺)) |
131 | 109, 113,
130 | sylc 65 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → ((𝐹 ↾ (◡𝐹 “ 𝑦))‘𝑛) = 𝐺) |
132 | 131 | adantllr 719 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (◡𝐹 “ 𝑦)) → ((𝐹 ↾ (◡𝐹 “ 𝑦))‘𝑛) = 𝐺) |
133 | 108 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (◡𝐹 “ 𝑦) ∈ V) |
134 | | simpll 767 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))) |
135 | 70 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (◡𝐹 “ 𝑦) ∈ 𝒫 𝐶) |
136 | 92 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (◡𝐹 “ 𝑦) ∈ Fin) |
137 | 135, 136 | elind 4209 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) |
138 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝑦) |
139 | 101 | eqcomd 2740 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 = (𝐹 “ (◡𝐹 “ 𝑦))) |
140 | 139 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑦 = (𝐹 “ (◡𝐹 “ 𝑦))) |
141 | 138, 140 | eleqtrd 2840 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ (𝐹 “ (◡𝐹 “ 𝑦))) |
142 | 141 | adantllr 719 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ (𝐹 “ (◡𝐹 “ 𝑦))) |
143 | 134, 137,
142 | jca31 514 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (◡𝐹 “ 𝑦)))) |
144 | 114 | anbi2d 630 |
. . . . . . . . . . . 12
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ↔ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)))) |
145 | | imaeq2 6075 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (𝐹 “ 𝑥) = (𝐹 “ (◡𝐹 “ 𝑦))) |
146 | 145 | eleq2d 2824 |
. . . . . . . . . . . 12
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (𝑘 ∈ (𝐹 “ 𝑥) ↔ 𝑘 ∈ (𝐹 “ (◡𝐹 “ 𝑦)))) |
147 | 144, 146 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑥 = (◡𝐹 “ 𝑦) → ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) ↔ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (◡𝐹 “ 𝑦))))) |
148 | 147 | imbi1d 341 |
. . . . . . . . . 10
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ ℂ) ↔ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (◡𝐹 “ 𝑦))) → 𝐵 ∈ ℂ))) |
149 | | rge0ssre 13492 |
. . . . . . . . . . . 12
⊢
(0[,)+∞) ⊆ ℝ |
150 | | ax-resscn 11209 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℂ |
151 | 149, 150 | sstri 4004 |
. . . . . . . . . . 11
⊢
(0[,)+∞) ⊆ ℂ |
152 | | simplll 775 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝜑) |
153 | | simpllr 776 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) |
154 | 16 | fimassd 6757 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹 “ 𝑥) ⊆ 𝐴) |
155 | 154 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → (𝐹 “ 𝑥) ⊆ 𝐴) |
156 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝑘 ∈ (𝐹 “ 𝑥)) |
157 | 155, 156 | sseldd 3995 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝑘 ∈ 𝐴) |
158 | 157 | adantllr 719 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝑘 ∈ 𝐴) |
159 | | foelcdmi 6969 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐶–onto→𝐴 ∧ 𝑘 ∈ 𝐴) → ∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘) |
160 | 4, 159 | sylan 580 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘) |
161 | 160 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → ∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘) |
162 | | nfv 1911 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛 𝑘 ∈ 𝐴 |
163 | 89, 162 | nfan 1896 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) |
164 | | nfv 1911 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛 𝐵 ∈
(0[,)+∞) |
165 | | csbid 3920 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
⦋𝑘 /
𝑘⦌𝐵 = 𝐵 |
166 | 165 | eqcomi 2743 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐵 = ⦋𝑘 / 𝑘⦌𝐵 |
167 | 166 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 = ⦋𝑘 / 𝑘⦌𝐵) |
168 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹‘𝑛) = 𝑘 → (𝐹‘𝑛) = 𝑘) |
169 | 168 | eqcomd 2740 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹‘𝑛) = 𝑘 → 𝑘 = (𝐹‘𝑛)) |
170 | 169 | csbeq1d 3911 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑛) = 𝑘 → ⦋𝑘 / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵) |
171 | 170 | 3ad2ant3 1134 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → ⦋𝑘 / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵) |
172 | 29 | 3adant3 1131 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷) |
173 | 167, 171,
172 | 3eqtrd 2778 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 = 𝐷) |
174 | 173 | 3adant1r 1176 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 = 𝐷) |
175 | | 0xr 11305 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
ℝ* |
176 | 175 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 0 ∈
ℝ*) |
177 | | pnfxr 11312 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ +∞
∈ ℝ* |
178 | 177 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞
∈ ℝ*) |
179 | 60 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 𝐷 ∈
(0[,]+∞)) |
180 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → ¬ 𝐷 ∈
(0[,)+∞)) |
181 | 176, 178,
179, 180 | eliccnelico 45481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 𝐷 = +∞) |
182 | 181 | eqcomd 2740 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞ =
𝐷) |
183 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝑛 ∈ 𝐶) |
184 | 53, 183, 60 | elrnmpt1d 5977 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) |
185 | 184 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 𝐷 ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) |
186 | 182, 185 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞
∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) |
187 | 186 | adantllr 719 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞
∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) |
188 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → ¬
+∞ ∈ ran (𝑛
∈ 𝐶 ↦ 𝐷)) |
189 | 187, 188 | condan 818 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ (0[,)+∞)) |
190 | 189 | 3adant3 1131 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐷 ∈ (0[,)+∞)) |
191 | 174, 190 | eqeltrd 2838 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 ∈ (0[,)+∞)) |
192 | 191 | 3exp 1118 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) → (𝑛 ∈ 𝐶 → ((𝐹‘𝑛) = 𝑘 → 𝐵 ∈ (0[,)+∞)))) |
193 | 192 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → (𝑛 ∈ 𝐶 → ((𝐹‘𝑛) = 𝑘 → 𝐵 ∈ (0[,)+∞)))) |
194 | 163, 164,
193 | rexlimd 3263 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → (∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘 → 𝐵 ∈ (0[,)+∞))) |
195 | 161, 194 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) |
196 | 152, 153,
158, 195 | syl21anc 838 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ (0[,)+∞)) |
197 | 151, 196 | sselid 3992 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ ℂ) |
198 | 148, 197 | vtoclg 3553 |
. . . . . . . . 9
⊢ ((◡𝐹 “ 𝑦) ∈ V → ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (◡𝐹 “ 𝑦))) → 𝐵 ∈ ℂ)) |
199 | 133, 143,
198 | sylc 65 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝐵 ∈ ℂ) |
200 | 84, 91, 27, 92, 104, 132, 199 | fsumf1of 45529 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ (◡𝐹 “ 𝑦)𝐷) |
201 | | sumeq1 15721 |
. . . . . . . 8
⊢ (𝑥 = (◡𝐹 “ 𝑦) → Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑛 ∈ (◡𝐹 “ 𝑦)𝐷) |
202 | 201 | rspceeqv 3644 |
. . . . . . 7
⊢ (((◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin) ∧ Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ (◡𝐹 “ 𝑦)𝐷) → ∃𝑥 ∈ (𝒫 𝐶 ∩ Fin)Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ 𝑥 𝐷) |
203 | 80, 200, 202 | syl2anc 584 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ∃𝑥 ∈ (𝒫 𝐶 ∩ Fin)Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ 𝑥 𝐷) |
204 | 67, 203 | rnmptssrn 45124 |
. . . . 5
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) → ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵) ⊆ ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷)) |
205 | | sumex 15720 |
. . . . . . 7
⊢
Σ𝑛 ∈
𝑥 𝐷 ∈ V |
206 | 205 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Σ𝑛 ∈ 𝑥 𝐷 ∈ V) |
207 | 6, 154 | sselpwd 5333 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 “ 𝑥) ∈ 𝒫 𝐴) |
208 | 207 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ 𝒫 𝐴) |
209 | 16 | ffund 6740 |
. . . . . . . . . 10
⊢ (𝜑 → Fun 𝐹) |
210 | | elinel2 4211 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝒫 𝐶 ∩ Fin) → 𝑥 ∈ Fin) |
211 | | imafi 9350 |
. . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ Fin) → (𝐹 “ 𝑥) ∈ Fin) |
212 | 209, 210,
211 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ Fin) |
213 | 208, 212 | elind 4209 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ (𝒫 𝐴 ∩ Fin)) |
214 | 213 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ (𝒫 𝐴 ∩ Fin)) |
215 | | nfv 1911 |
. . . . . . . . . 10
⊢
Ⅎ𝑘 𝑥 ∈ (𝒫 𝐶 ∩ Fin) |
216 | 82, 215 | nfan 1896 |
. . . . . . . . 9
⊢
Ⅎ𝑘((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) |
217 | | nfv 1911 |
. . . . . . . . . 10
⊢
Ⅎ𝑛 𝑥 ∈ (𝒫 𝐶 ∩ Fin) |
218 | 89, 217 | nfan 1896 |
. . . . . . . . 9
⊢
Ⅎ𝑛((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) |
219 | 210 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝑥 ∈ Fin) |
220 | | f1ores 6862 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐶–1-1→𝐴 ∧ 𝑥 ⊆ 𝐶) → (𝐹 ↾ 𝑥):𝑥–1-1-onto→(𝐹 “ 𝑥)) |
221 | 94, 125, 220 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥–1-1-onto→(𝐹 “ 𝑥)) |
222 | 221 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥–1-1-onto→(𝐹 “ 𝑥)) |
223 | 129 | adantllr 719 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = 𝐺) |
224 | 216, 218,
27, 219, 222, 223, 197 | fsumf1of 45529 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵 = Σ𝑛 ∈ 𝑥 𝐷) |
225 | 224 | eqcomd 2740 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵) |
226 | | sumeq1 15721 |
. . . . . . . 8
⊢ (𝑦 = (𝐹 “ 𝑥) → Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵) |
227 | 226 | rspceeqv 3644 |
. . . . . . 7
⊢ (((𝐹 “ 𝑥) ∈ (𝒫 𝐴 ∩ Fin) ∧ Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵) → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ 𝑦 𝐵) |
228 | 214, 225,
227 | syl2anc 584 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ 𝑦 𝐵) |
229 | 206, 228 | rnmptssrn 45124 |
. . . . 5
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) → ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷) ⊆ ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵)) |
230 | 204, 229 | eqssd 4012 |
. . . 4
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) → ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵) = ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷)) |
231 | 230 | supeq1d 9483 |
. . 3
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) → sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ*, < ) = sup(ran
(𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷), ℝ*, <
)) |
232 | 6 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐴 ∈ V) |
233 | 82, 232, 195 | sge0revalmpt 46333 |
. . 3
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ*, <
)) |
234 | 1 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐶 ∈ 𝑉) |
235 | 89, 234, 189 | sge0revalmpt 46333 |
. . 3
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) →
(Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷)) = sup(ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷), ℝ*, <
)) |
236 | 231, 233,
235 | 3eqtr4d 2784 |
. 2
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝑛 ∈ 𝐶 ↦ 𝐷)) →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) =
(Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷))) |
237 | 65, 236 | pm2.61dan 813 |
1
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) =
(Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷))) |