Step | Hyp | Ref
| Expression |
1 | | nfv 1830 |
. . . 4
⊢
Ⅎ𝑥𝜑 |
2 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑥Σ^ |
3 | | nfiu1 4486 |
. . . . . . 7
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵 |
4 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥𝐶 |
5 | 3, 4 | nfmpt 4674 |
. . . . . 6
⊢
Ⅎ𝑥(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) |
6 | 2, 5 | nffv 6110 |
. . . . 5
⊢
Ⅎ𝑥(Σ^‘(𝑘 ∈ ∪ 𝑥
∈ 𝐴 𝐵 ↦ 𝐶)) |
7 | | nfmpt1 4675 |
. . . . . 6
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) |
8 | 2, 7 | nffv 6110 |
. . . . 5
⊢
Ⅎ𝑥(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) |
9 | 6, 8 | nfeq 2762 |
. . . 4
⊢
Ⅎ𝑥(Σ^‘(𝑘 ∈ ∪ 𝑥
∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) |
10 | | sge0iunmpt.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
11 | | sge0iunmpt.b |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) |
12 | 11 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) |
13 | | iunexg 7035 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪
𝑥 ∈ 𝐴 𝐵 ∈ V) |
14 | 10, 12, 13 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V) |
15 | | eliun 4460 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵) |
16 | 15 | biimpi 205 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵) |
17 | 16 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵) |
18 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥𝑘 |
19 | 18, 3 | nfel 2763 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 |
20 | 1, 19 | nfan 1816 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝜑 ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
21 | 4 | nfel1 2765 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥 𝐶 ∈
(0[,]+∞) |
22 | | sge0iunmpt.c |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) |
23 | 22 | 3exp 1256 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞)))) |
24 | 23 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → (𝑥 ∈ 𝐴 → (𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞)))) |
25 | 20, 21, 24 | rexlimd 3008 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → (∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞))) |
26 | 17, 25 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞)) |
27 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) = (𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) |
28 | 26, 27 | fmptd 6292 |
. . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶):∪ 𝑥 ∈ 𝐴 𝐵⟶(0[,]+∞)) |
29 | 14, 28 | sge0xrcl 39278 |
. . . . . . . 8
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ∈
ℝ*) |
30 | 29 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ∈
ℝ*) |
31 | | id 22 |
. . . . . . . . . . 11
⊢
((Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) |
32 | 31 | eqcomd 2616 |
. . . . . . . . . 10
⊢
((Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ → +∞ =
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) |
33 | 32 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ =
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) |
34 | 33 | 3adant1 1072 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ =
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) |
35 | 14 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪
𝑥 ∈ 𝐴 𝐵 ∈ V) |
36 | 26 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞)) |
37 | | ssiun2 4499 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪
𝑥 ∈ 𝐴 𝐵) |
38 | 37 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ ∪
𝑥 ∈ 𝐴 𝐵) |
39 | 35, 36, 38 | sge0lessmpt 39292 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶))) |
40 | 39 | 3adant3 1074 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶))) |
41 | 34, 40 | eqbrtrd 4605 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ ≤
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶))) |
42 | 30, 41 | xrgepnfd 38488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = +∞) |
43 | 10 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → 𝐴 ∈ 𝑉) |
44 | | nfv 1830 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ 𝐴) |
45 | | nfcsb1v 3515 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 |
46 | | nfcsb1v 3515 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝑊 |
47 | 45, 46 | nfel 2763 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊 |
48 | 44, 47 | nfim 1813 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊) |
49 | | eleq1 2676 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
50 | 49 | anbi2d 736 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑦 ∈ 𝐴))) |
51 | | csbeq1a 3508 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵) |
52 | | csbeq1a 3508 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → 𝑊 = ⦋𝑦 / 𝑥⦌𝑊) |
53 | 51, 52 | eleq12d 2682 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝐵 ∈ 𝑊 ↔ ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊)) |
54 | 50, 53 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊))) |
55 | 48, 54, 11 | chvar 2250 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊) |
56 | 55 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊) |
57 | 45, 4 | nfmpt 4674 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶) |
58 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(0[,]+∞) |
59 | 57, 45, 58 | nff 5954 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞) |
60 | 44, 59 | nfim 1813 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)) |
61 | 51 | mpteq1d 4666 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)) |
62 | 61, 51 | feq12d 5946 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ((𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞) ↔ (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))) |
63 | 50, 62 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞)) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)))) |
64 | 23 | imp31 447 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) |
65 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑘 ∈ 𝐵 ↦ 𝐶) |
66 | 64, 65 | fmptd 6292 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞)) |
67 | 60, 63, 66 | chvar 2250 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)) |
68 | 67 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)) |
69 | 56, 68 | sge0cl 39274 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) →
(Σ^‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)) ∈ (0[,]+∞)) |
70 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) |
71 | 2, 57 | nffv 6110 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(Σ^‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)) |
72 | 61 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶))) |
73 | 70, 71, 72 | cbvmpt 4677 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑦 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶))) |
74 | 69, 73 | fmptd 6292 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞)) |
75 | 74 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞)) |
76 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴) |
77 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ V |
78 | 77 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ V) |
79 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) |
80 | 79 | elrnmpt1 5295 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ V) →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ran (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) |
81 | 76, 78, 80 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ran (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) |
82 | 81 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ran (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) |
83 | 33, 82 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ ∈ ran
(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) |
84 | 83 | 3adant1 1072 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ ∈ ran
(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) |
85 | 43, 75, 84 | sge0pnfval 39266 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) →
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = +∞) |
86 | 42, 85 | eqtr4d 2647 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) |
87 | 86 | 3exp 1256 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 →
((Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))))))) |
88 | 1, 9, 87 | rexlimd 3008 |
. . 3
⊢ (𝜑 → (∃𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))) |
89 | 88 | imp 444 |
. 2
⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) |
90 | | simpl 472 |
. . 3
⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → 𝜑) |
91 | | ralnex 2975 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ¬
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ ↔ ¬ ∃𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) |
92 | | df-ne 2782 |
. . . . . . 7
⊢
((Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ↔ ¬
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) |
93 | 92 | bicomi 213 |
. . . . . 6
⊢ (¬
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ ↔
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) |
94 | 93 | ralbii 2963 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ¬
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ ↔ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) |
95 | 91, 94 | sylbb1 226 |
. . . 4
⊢ (¬
∃𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ → ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) |
96 | 95 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) |
97 | 10 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → 𝐴 ∈ 𝑉) |
98 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑊 |
99 | 45, 98 | nfel 2763 |
. . . . . . . 8
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊 |
100 | 44, 99 | nfim 1813 |
. . . . . . 7
⊢
Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊) |
101 | 51 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝐵 ∈ 𝑊 ↔ ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊)) |
102 | 50, 101 | imbi12d 333 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊))) |
103 | 100, 102,
11 | chvar 2250 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊) |
104 | 103 | adantlr 747 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊) |
105 | | sge0iunmpt.dj |
. . . . . . 7
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) |
106 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑦𝐵 |
107 | 106, 45, 51 | cbvdisj 4563 |
. . . . . . 7
⊢
(Disj 𝑥
∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) |
108 | 105, 107 | sylib 207 |
. . . . . 6
⊢ (𝜑 → Disj 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) |
109 | 108 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → Disj 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) |
110 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑘(𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) |
111 | | nfcsb1v 3515 |
. . . . . . . . 9
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐶 |
112 | 111 | nfel1 2765 |
. . . . . . . 8
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞) |
113 | 110, 112 | nfim 1813 |
. . . . . . 7
⊢
Ⅎ𝑘((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)) |
114 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↔ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵)) |
115 | 114 | 3anbi3d 1397 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) ↔ (𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵))) |
116 | | csbeq1a 3508 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → 𝐶 = ⦋𝑗 / 𝑘⦌𝐶) |
117 | 116 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (𝐶 ∈ (0[,]+∞) ↔
⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))) |
118 | 115, 117 | imbi12d 333 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → (((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)))) |
119 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑦 ∈ 𝐴 |
120 | 18, 45 | nfel 2763 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 |
121 | 1, 119, 120 | nf3an 1819 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) |
122 | 121, 21 | nfim 1813 |
. . . . . . . 8
⊢
Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,]+∞)) |
123 | 51 | eleq2d 2673 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑘 ∈ 𝐵 ↔ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵)) |
124 | 49, 123 | 3anbi23d 1394 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) ↔ (𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵))) |
125 | 124 | imbi1d 330 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,]+∞)))) |
126 | 122, 125,
22 | chvar 2250 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,]+∞)) |
127 | 113, 118,
126 | chvar 2250 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)) |
128 | 127 | 3adant1r 1311 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)) |
129 | | simpr 476 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴) |
130 | | simpl 472 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ∧ 𝑦 ∈ 𝐴) → ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) |
131 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → 𝑦 ∈ 𝐴) |
132 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) |
133 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥⦋𝑗 / 𝑘⦌𝐶 |
134 | 45, 133 | nfmpt 4674 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) |
135 | 2, 134 | nffv 6110 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) |
136 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥+∞ |
137 | 135, 136 | nfne 2882 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞ |
138 | | nfcv 2751 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑗𝐶 |
139 | 138, 111,
116 | cbvmpt 4677 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) |
140 | 139 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) |
141 | 61, 140 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) |
142 | 141 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))) |
143 | 142 | neeq1d 2841 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 →
((Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ↔
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞)) |
144 | 137, 143 | rspc 3276 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐴 → (∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ →
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞)) |
145 | 131, 132,
144 | sylc 63 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) →
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞) |
146 | 129, 130,
145 | syl2anc 691 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ∧ 𝑦 ∈ 𝐴) →
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞) |
147 | 146 | neneqd 2787 |
. . . . . . 7
⊢
((∀𝑥 ∈
𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ∧ 𝑦 ∈ 𝐴) → ¬
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) = +∞) |
148 | 147 | adantll 746 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → ¬
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) = +∞) |
149 | 127 | 3expa 1257 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)) |
150 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) |
151 | 149, 150 | fmptd 6292 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)) |
152 | 151 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)) |
153 | 104, 152 | sge0repnf 39279 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) →
((Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈ ℝ ↔ ¬
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) = +∞)) |
154 | 148, 153 | mpbird 246 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) →
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈ ℝ) |
155 | 138, 111,
116 | cbvmpt 4677 |
. . . . . . . . 9
⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) = (𝑗 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) |
156 | 106, 45, 51 | cbviun 4493 |
. . . . . . . . . 10
⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 |
157 | 156 | mpteq1i 4667 |
. . . . . . . . 9
⊢ (𝑗 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) = (𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) |
158 | 155, 157 | eqtri 2632 |
. . . . . . . 8
⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) = (𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) |
159 | 158 | fveq2i 6106 |
. . . . . . 7
⊢
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) |
160 | 159, 29 | syl5eqelr 2693 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈
ℝ*) |
161 | 160 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) →
(Σ^‘(𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈
ℝ*) |
162 | 70, 135, 142 | cbvmpt 4677 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑦 ∈ 𝐴 ↦
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))) |
163 | 162 | fveq2i 6106 |
. . . . . . 7
⊢
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) =
(Σ^‘(𝑦 ∈ 𝐴 ↦
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))) |
164 | 11, 66 | sge0cl 39274 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ (0[,]+∞)) |
165 | 164, 79 | fmptd 6292 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞)) |
166 | 10, 165 | sge0xrcl 39278 |
. . . . . . 7
⊢ (𝜑 →
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ∈
ℝ*) |
167 | 163, 166 | syl5eqelr 2693 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑦 ∈ 𝐴 ↦
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))) ∈
ℝ*) |
168 | 167 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) →
(Σ^‘(𝑦 ∈ 𝐴 ↦
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))) ∈
ℝ*) |
169 | | eliun 4460 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) |
170 | 169 | biimpi 205 |
. . . . . . . . 9
⊢ (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 → ∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) |
171 | 170 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → ∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) |
172 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑦𝜑 |
173 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦𝑗 |
174 | | nfiu1 4486 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 |
175 | 173, 174 | nfel 2763 |
. . . . . . . . . 10
⊢
Ⅎ𝑦 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 |
176 | 172, 175 | nfan 1816 |
. . . . . . . . 9
⊢
Ⅎ𝑦(𝜑 ∧ 𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) |
177 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎ𝑦⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞) |
178 | 149 | exp31 628 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ 𝐴 → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)))) |
179 | 178 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → (𝑦 ∈ 𝐴 → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)))) |
180 | 176, 177,
179 | rexlimd 3008 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → (∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))) |
181 | 171, 180 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)) |
182 | | eqid 2610 |
. . . . . . 7
⊢ (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) = (𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) |
183 | 181, 182 | fmptd 6292 |
. . . . . 6
⊢ (𝜑 → (𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)) |
184 | 183 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)) |
185 | 156, 14 | syl5eqelr 2693 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ∈ V) |
186 | 185 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ∈ V) |
187 | 97, 104, 109, 128, 154, 161, 168, 184, 186 | sge0iunmptlemre 39308 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) →
(Σ^‘(𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) =
(Σ^‘(𝑦 ∈ 𝐴 ↦
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))))) |
188 | 159 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))) |
189 | 163 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) →
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) =
(Σ^‘(𝑦 ∈ 𝐴 ↦
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))))) |
190 | 187, 188,
189 | 3eqtr4d 2654 |
. . 3
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) |
191 | 90, 96, 190 | syl2anc 691 |
. 2
⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) |
192 | 89, 191 | pm2.61dan 828 |
1
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) |