Step | Hyp | Ref
| Expression |
1 | | nfv 1922 |
. . . 4
⊢
Ⅎ𝑥𝜑 |
2 | | nfcv 2904 |
. . . . . 6
⊢
Ⅎ𝑥Σ^ |
3 | | nfiu1 4938 |
. . . . . . 7
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵 |
4 | | nfcv 2904 |
. . . . . . 7
⊢
Ⅎ𝑥𝐶 |
5 | 3, 4 | nfmpt 5152 |
. . . . . 6
⊢
Ⅎ𝑥(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) |
6 | 2, 5 | nffv 6727 |
. . . . 5
⊢
Ⅎ𝑥(Σ^‘(𝑘 ∈ ∪ 𝑥
∈ 𝐴 𝐵 ↦ 𝐶)) |
7 | | nfmpt1 5153 |
. . . . . 6
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) |
8 | 2, 7 | nffv 6727 |
. . . . 5
⊢
Ⅎ𝑥(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) |
9 | 6, 8 | nfeq 2917 |
. . . 4
⊢
Ⅎ𝑥(Σ^‘(𝑘 ∈ ∪ 𝑥
∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) |
10 | | sge0iunmpt.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
11 | | sge0iunmpt.b |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) |
12 | 11 | ralrimiva 3105 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) |
13 | | iunexg 7736 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪
𝑥 ∈ 𝐴 𝐵 ∈ V) |
14 | 10, 12, 13 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V) |
15 | | eliun 4908 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵) |
16 | 15 | biimpi 219 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵) |
17 | 16 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵) |
18 | | nfcv 2904 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥𝑘 |
19 | 18, 3 | nfel 2918 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 |
20 | 1, 19 | nfan 1907 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝜑 ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
21 | 4 | nfel1 2920 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥 𝐶 ∈
(0[,]+∞) |
22 | | sge0iunmpt.c |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) |
23 | 22 | 3exp 1121 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞)))) |
24 | 23 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → (𝑥 ∈ 𝐴 → (𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞)))) |
25 | 20, 21, 24 | rexlimd 3236 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → (∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞))) |
26 | 17, 25 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞)) |
27 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) = (𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) |
28 | 26, 27 | fmptd 6931 |
. . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶):∪ 𝑥 ∈ 𝐴 𝐵⟶(0[,]+∞)) |
29 | 14, 28 | sge0xrcl 43598 |
. . . . . . . 8
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ∈
ℝ*) |
30 | 29 | 3ad2ant1 1135 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ∈
ℝ*) |
31 | | id 22 |
. . . . . . . . . . 11
⊢
((Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) |
32 | 31 | eqcomd 2743 |
. . . . . . . . . 10
⊢
((Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ → +∞ =
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) |
33 | 32 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ =
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) |
34 | 33 | 3adant1 1132 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ =
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) |
35 | 14 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪
𝑥 ∈ 𝐴 𝐵 ∈ V) |
36 | 26 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞)) |
37 | | ssiun2 4956 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪
𝑥 ∈ 𝐴 𝐵) |
38 | 37 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ ∪
𝑥 ∈ 𝐴 𝐵) |
39 | 35, 36, 38 | sge0lessmpt 43612 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶))) |
40 | 39 | 3adant3 1134 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶))) |
41 | 34, 40 | eqbrtrd 5075 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ ≤
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶))) |
42 | 30, 41 | xrgepnfd 42543 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = +∞) |
43 | 10 | 3ad2ant1 1135 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → 𝐴 ∈ 𝑉) |
44 | | nfv 1922 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ 𝐴) |
45 | | nfcsb1v 3836 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 |
46 | | nfcsb1v 3836 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝑊 |
47 | 45, 46 | nfel 2918 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊 |
48 | 44, 47 | nfim 1904 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊) |
49 | | eleq1w 2820 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
50 | 49 | anbi2d 632 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑦 ∈ 𝐴))) |
51 | | csbeq1a 3825 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵) |
52 | | csbeq1a 3825 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → 𝑊 = ⦋𝑦 / 𝑥⦌𝑊) |
53 | 51, 52 | eleq12d 2832 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝐵 ∈ 𝑊 ↔ ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊)) |
54 | 50, 53 | imbi12d 348 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊))) |
55 | 48, 54, 11 | chvarfv 2238 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊) |
56 | 55 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊) |
57 | 45, 4 | nfmpt 5152 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶) |
58 | | nfcv 2904 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(0[,]+∞) |
59 | 57, 45, 58 | nff 6541 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞) |
60 | 44, 59 | nfim 1904 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)) |
61 | 51 | mpteq1d 5144 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)) |
62 | 61, 51 | feq12d 6533 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ((𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞) ↔ (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))) |
63 | 50, 62 | imbi12d 348 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞)) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)))) |
64 | 23 | imp31 421 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) |
65 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑘 ∈ 𝐵 ↦ 𝐶) |
66 | 64, 65 | fmptd 6931 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞)) |
67 | 60, 63, 66 | chvarfv 2238 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)) |
68 | 67 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)) |
69 | 56, 68 | sge0cl 43594 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) →
(Σ^‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)) ∈ (0[,]+∞)) |
70 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) |
71 | 2, 57 | nffv 6727 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(Σ^‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)) |
72 | 61 | fveq2d 6721 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶))) |
73 | 70, 71, 72 | cbvmpt 5156 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑦 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶))) |
74 | 69, 73 | fmptd 6931 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞)) |
75 | 74 | 3adant3 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞)) |
76 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴) |
77 | | fvexd 6732 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ V) |
78 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) |
79 | 78 | elrnmpt1 5827 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ V) →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ran (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) |
80 | 76, 77, 79 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ran (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) |
81 | 80 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ran (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) |
82 | 33, 81 | eqeltrd 2838 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ ∈ ran
(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) |
83 | 82 | 3adant1 1132 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ ∈ ran
(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) |
84 | 43, 75, 83 | sge0pnfval 43586 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) →
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = +∞) |
85 | 42, 84 | eqtr4d 2780 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) |
86 | 85 | 3exp 1121 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 →
((Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))))))) |
87 | 1, 9, 86 | rexlimd 3236 |
. . 3
⊢ (𝜑 → (∃𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))) |
88 | 87 | imp 410 |
. 2
⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) |
89 | | simpl 486 |
. . 3
⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → 𝜑) |
90 | | ralnex 3158 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ¬
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ ↔ ¬ ∃𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) |
91 | | df-ne 2941 |
. . . . . . 7
⊢
((Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ↔ ¬
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) |
92 | 91 | bicomi 227 |
. . . . . 6
⊢ (¬
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ ↔
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) |
93 | 92 | ralbii 3088 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ¬
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ ↔ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) |
94 | 90, 93 | sylbb1 240 |
. . . 4
⊢ (¬
∃𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ → ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) |
95 | 94 | adantl 485 |
. . 3
⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) |
96 | 10 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → 𝐴 ∈ 𝑉) |
97 | | nfcv 2904 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑊 |
98 | 45, 97 | nfel 2918 |
. . . . . . . 8
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊 |
99 | 44, 98 | nfim 1904 |
. . . . . . 7
⊢
Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊) |
100 | 51 | eleq1d 2822 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝐵 ∈ 𝑊 ↔ ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊)) |
101 | 50, 100 | imbi12d 348 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊))) |
102 | 99, 101, 11 | chvarfv 2238 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊) |
103 | 102 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊) |
104 | | sge0iunmpt.dj |
. . . . . . 7
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) |
105 | | nfcv 2904 |
. . . . . . . 8
⊢
Ⅎ𝑦𝐵 |
106 | 105, 45, 51 | cbvdisj 5028 |
. . . . . . 7
⊢
(Disj 𝑥
∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) |
107 | 104, 106 | sylib 221 |
. . . . . 6
⊢ (𝜑 → Disj 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) |
108 | 107 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → Disj 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) |
109 | | nfv 1922 |
. . . . . . . 8
⊢
Ⅎ𝑘(𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) |
110 | | nfcsb1v 3836 |
. . . . . . . . 9
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐶 |
111 | 110 | nfel1 2920 |
. . . . . . . 8
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞) |
112 | 109, 111 | nfim 1904 |
. . . . . . 7
⊢
Ⅎ𝑘((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)) |
113 | | eleq1w 2820 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↔ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵)) |
114 | 113 | 3anbi3d 1444 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) ↔ (𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵))) |
115 | | csbeq1a 3825 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → 𝐶 = ⦋𝑗 / 𝑘⦌𝐶) |
116 | 115 | eleq1d 2822 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (𝐶 ∈ (0[,]+∞) ↔
⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))) |
117 | 114, 116 | imbi12d 348 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → (((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)))) |
118 | | nfv 1922 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑦 ∈ 𝐴 |
119 | 18, 45 | nfel 2918 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 |
120 | 1, 118, 119 | nf3an 1909 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) |
121 | 120, 21 | nfim 1904 |
. . . . . . . 8
⊢
Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,]+∞)) |
122 | 51 | eleq2d 2823 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑘 ∈ 𝐵 ↔ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵)) |
123 | 49, 122 | 3anbi23d 1441 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) ↔ (𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵))) |
124 | 123 | imbi1d 345 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,]+∞)))) |
125 | 121, 124,
22 | chvarfv 2238 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,]+∞)) |
126 | 112, 117,
125 | chvarfv 2238 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)) |
127 | 126 | 3adant1r 1179 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)) |
128 | | simpr 488 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴) |
129 | | simpl 486 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ∧ 𝑦 ∈ 𝐴) → ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) |
130 | | simpl 486 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → 𝑦 ∈ 𝐴) |
131 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) |
132 | | nfcv 2904 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥⦋𝑗 / 𝑘⦌𝐶 |
133 | 45, 132 | nfmpt 5152 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) |
134 | 2, 133 | nffv 6727 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) |
135 | | nfcv 2904 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥+∞ |
136 | 134, 135 | nfne 3042 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞ |
137 | | nfcv 2904 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑗𝐶 |
138 | 137, 110,
115 | cbvmpt 5156 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) |
139 | 138 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) |
140 | 61, 139 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) |
141 | 140 | fveq2d 6721 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))) |
142 | 141 | neeq1d 3000 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 →
((Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ↔
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞)) |
143 | 136, 142 | rspc 3525 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐴 → (∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ →
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞)) |
144 | 130, 131,
143 | sylc 65 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) →
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞) |
145 | 128, 129,
144 | syl2anc 587 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ∧ 𝑦 ∈ 𝐴) →
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞) |
146 | 145 | neneqd 2945 |
. . . . . . 7
⊢
((∀𝑥 ∈
𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ∧ 𝑦 ∈ 𝐴) → ¬
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) = +∞) |
147 | 146 | adantll 714 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → ¬
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) = +∞) |
148 | 126 | 3expa 1120 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)) |
149 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) |
150 | 148, 149 | fmptd 6931 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)) |
151 | 150 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)) |
152 | 103, 151 | sge0repnf 43599 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) →
((Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈ ℝ ↔ ¬
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) = +∞)) |
153 | 147, 152 | mpbird 260 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) →
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈ ℝ) |
154 | 137, 110,
115 | cbvmpt 5156 |
. . . . . . . . 9
⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) = (𝑗 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) |
155 | 105, 45, 51 | cbviun 4945 |
. . . . . . . . . 10
⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 |
156 | 155 | mpteq1i 5145 |
. . . . . . . . 9
⊢ (𝑗 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) = (𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) |
157 | 154, 156 | eqtri 2765 |
. . . . . . . 8
⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) = (𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) |
158 | 157 | fveq2i 6720 |
. . . . . . 7
⊢
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) |
159 | 158, 29 | eqeltrrid 2843 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈
ℝ*) |
160 | 159 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) →
(Σ^‘(𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈
ℝ*) |
161 | 70, 134, 141 | cbvmpt 5156 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑦 ∈ 𝐴 ↦
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))) |
162 | 161 | fveq2i 6720 |
. . . . . . 7
⊢
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) =
(Σ^‘(𝑦 ∈ 𝐴 ↦
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))) |
163 | 11, 66 | sge0cl 43594 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ (0[,]+∞)) |
164 | 163, 78 | fmptd 6931 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞)) |
165 | 10, 164 | sge0xrcl 43598 |
. . . . . . 7
⊢ (𝜑 →
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ∈
ℝ*) |
166 | 162, 165 | eqeltrrid 2843 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑦 ∈ 𝐴 ↦
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))) ∈
ℝ*) |
167 | 166 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) →
(Σ^‘(𝑦 ∈ 𝐴 ↦
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))) ∈
ℝ*) |
168 | | eliun 4908 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) |
169 | 168 | biimpi 219 |
. . . . . . . . 9
⊢ (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 → ∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) |
170 | 169 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → ∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) |
171 | | nfv 1922 |
. . . . . . . . . 10
⊢
Ⅎ𝑦𝜑 |
172 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦𝑗 |
173 | | nfiu1 4938 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 |
174 | 172, 173 | nfel 2918 |
. . . . . . . . . 10
⊢
Ⅎ𝑦 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 |
175 | 171, 174 | nfan 1907 |
. . . . . . . . 9
⊢
Ⅎ𝑦(𝜑 ∧ 𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) |
176 | | nfv 1922 |
. . . . . . . . 9
⊢
Ⅎ𝑦⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞) |
177 | 148 | exp31 423 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ 𝐴 → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)))) |
178 | 177 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → (𝑦 ∈ 𝐴 → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)))) |
179 | 175, 176,
178 | rexlimd 3236 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → (∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))) |
180 | 170, 179 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)) |
181 | | eqid 2737 |
. . . . . . 7
⊢ (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) = (𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) |
182 | 180, 181 | fmptd 6931 |
. . . . . 6
⊢ (𝜑 → (𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)) |
183 | 182 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)) |
184 | 155, 14 | eqeltrrid 2843 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ∈ V) |
185 | 184 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ∈ V) |
186 | 96, 103, 108, 127, 153, 160, 167, 183, 185 | sge0iunmptlemre 43628 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) →
(Σ^‘(𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) =
(Σ^‘(𝑦 ∈ 𝐴 ↦
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))))) |
187 | 158 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))) |
188 | 162 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) →
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) =
(Σ^‘(𝑦 ∈ 𝐴 ↦
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))))) |
189 | 186, 187,
188 | 3eqtr4d 2787 |
. . 3
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) |
190 | 89, 95, 189 | syl2anc 587 |
. 2
⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) |
191 | 88, 190 | pm2.61dan 813 |
1
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) |