| Step | Hyp | Ref
| Expression |
| 1 | | nfv 1914 |
. . . 4
⊢
Ⅎ𝑥𝜑 |
| 2 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑥Σ^ |
| 3 | | nfiu1 5027 |
. . . . . . 7
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵 |
| 4 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑥𝐶 |
| 5 | 3, 4 | nfmpt 5249 |
. . . . . 6
⊢
Ⅎ𝑥(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) |
| 6 | 2, 5 | nffv 6916 |
. . . . 5
⊢
Ⅎ𝑥(Σ^‘(𝑘 ∈ ∪ 𝑥
∈ 𝐴 𝐵 ↦ 𝐶)) |
| 7 | | nfmpt1 5250 |
. . . . . 6
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) |
| 8 | 2, 7 | nffv 6916 |
. . . . 5
⊢
Ⅎ𝑥(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) |
| 9 | 6, 8 | nfeq 2919 |
. . . 4
⊢
Ⅎ𝑥(Σ^‘(𝑘 ∈ ∪ 𝑥
∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) |
| 10 | | sge0iunmpt.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 11 | | sge0iunmpt.b |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) |
| 12 | 11 | ralrimiva 3146 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) |
| 13 | | iunexg 7988 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪
𝑥 ∈ 𝐴 𝐵 ∈ V) |
| 14 | 10, 12, 13 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V) |
| 15 | | eliun 4995 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵) |
| 16 | 15 | biimpi 216 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵) |
| 17 | 16 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵) |
| 18 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥𝑘 |
| 19 | 18, 3 | nfel 2920 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 |
| 20 | 1, 19 | nfan 1899 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝜑 ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
| 21 | 4 | nfel1 2922 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥 𝐶 ∈
(0[,]+∞) |
| 22 | | sge0iunmpt.c |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) |
| 23 | 22 | 3exp 1120 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞)))) |
| 24 | 23 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → (𝑥 ∈ 𝐴 → (𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞)))) |
| 25 | 20, 21, 24 | rexlimd 3266 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → (∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞))) |
| 26 | 17, 25 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞)) |
| 27 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) = (𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) |
| 28 | 26, 27 | fmptd 7134 |
. . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶):∪ 𝑥 ∈ 𝐴 𝐵⟶(0[,]+∞)) |
| 29 | 14, 28 | sge0xrcl 46400 |
. . . . . . . 8
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ∈
ℝ*) |
| 30 | 29 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ∈
ℝ*) |
| 31 | | id 22 |
. . . . . . . . . . 11
⊢
((Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) |
| 32 | 31 | eqcomd 2743 |
. . . . . . . . . 10
⊢
((Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ → +∞ =
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) |
| 33 | 32 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ =
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) |
| 34 | 33 | 3adant1 1131 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ =
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) |
| 35 | 14 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪
𝑥 ∈ 𝐴 𝐵 ∈ V) |
| 36 | 26 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞)) |
| 37 | | ssiun2 5047 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪
𝑥 ∈ 𝐴 𝐵) |
| 38 | 37 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ ∪
𝑥 ∈ 𝐴 𝐵) |
| 39 | 35, 36, 38 | sge0lessmpt 46414 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶))) |
| 40 | 39 | 3adant3 1133 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶))) |
| 41 | 34, 40 | eqbrtrd 5165 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ ≤
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶))) |
| 42 | 30, 41 | xrgepnfd 45342 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = +∞) |
| 43 | 10 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → 𝐴 ∈ 𝑉) |
| 44 | | nfv 1914 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ 𝐴) |
| 45 | | nfcsb1v 3923 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 |
| 46 | | nfcsb1v 3923 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝑊 |
| 47 | 45, 46 | nfel 2920 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊 |
| 48 | 44, 47 | nfim 1896 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊) |
| 49 | | eleq1w 2824 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
| 50 | 49 | anbi2d 630 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑦 ∈ 𝐴))) |
| 51 | | csbeq1a 3913 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵) |
| 52 | | csbeq1a 3913 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → 𝑊 = ⦋𝑦 / 𝑥⦌𝑊) |
| 53 | 51, 52 | eleq12d 2835 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝐵 ∈ 𝑊 ↔ ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊)) |
| 54 | 50, 53 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊))) |
| 55 | 48, 54, 11 | chvarfv 2240 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊) |
| 56 | 55 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊) |
| 57 | 45, 4 | nfmpt 5249 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶) |
| 58 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(0[,]+∞) |
| 59 | 57, 45, 58 | nff 6732 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞) |
| 60 | 44, 59 | nfim 1896 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)) |
| 61 | 51 | mpteq1d 5237 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)) |
| 62 | 61, 51 | feq12d 6724 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ((𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞) ↔ (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))) |
| 63 | 50, 62 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞)) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)))) |
| 64 | 23 | imp31 417 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) |
| 65 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑘 ∈ 𝐵 ↦ 𝐶) |
| 66 | 64, 65 | fmptd 7134 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞)) |
| 67 | 60, 63, 66 | chvarfv 2240 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)) |
| 68 | 67 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)) |
| 69 | 56, 68 | sge0cl 46396 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) →
(Σ^‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)) ∈ (0[,]+∞)) |
| 70 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) |
| 71 | 2, 57 | nffv 6916 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(Σ^‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)) |
| 72 | 61 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶))) |
| 73 | 70, 71, 72 | cbvmpt 5253 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑦 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶))) |
| 74 | 69, 73 | fmptd 7134 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞)) |
| 75 | 74 | 3adant3 1133 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞)) |
| 76 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴) |
| 77 | | fvexd 6921 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ V) |
| 78 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) |
| 79 | 78 | elrnmpt1 5971 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ V) →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ran (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) |
| 80 | 76, 77, 79 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ran (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) |
| 81 | 80 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ran (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) |
| 82 | 33, 81 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ ∈ ran
(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) |
| 83 | 82 | 3adant1 1131 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ ∈ ran
(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) |
| 84 | 43, 75, 83 | sge0pnfval 46388 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) →
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = +∞) |
| 85 | 42, 84 | eqtr4d 2780 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) |
| 86 | 85 | 3exp 1120 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 →
((Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))))))) |
| 87 | 1, 9, 86 | rexlimd 3266 |
. . 3
⊢ (𝜑 → (∃𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))) |
| 88 | 87 | imp 406 |
. 2
⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) |
| 89 | | simpl 482 |
. . 3
⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → 𝜑) |
| 90 | | ralnex 3072 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ¬
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ ↔ ¬ ∃𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) |
| 91 | | df-ne 2941 |
. . . . . . 7
⊢
((Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ↔ ¬
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) |
| 92 | 91 | bicomi 224 |
. . . . . 6
⊢ (¬
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ ↔
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) |
| 93 | 92 | ralbii 3093 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ¬
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ ↔ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) |
| 94 | 90, 93 | sylbb1 237 |
. . . 4
⊢ (¬
∃𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ → ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) |
| 95 | 94 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) |
| 96 | 10 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → 𝐴 ∈ 𝑉) |
| 97 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑊 |
| 98 | 45, 97 | nfel 2920 |
. . . . . . . 8
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊 |
| 99 | 44, 98 | nfim 1896 |
. . . . . . 7
⊢
Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊) |
| 100 | 51 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝐵 ∈ 𝑊 ↔ ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊)) |
| 101 | 50, 100 | imbi12d 344 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊))) |
| 102 | 99, 101, 11 | chvarfv 2240 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊) |
| 103 | 102 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊) |
| 104 | | sge0iunmpt.dj |
. . . . . . 7
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) |
| 105 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑦𝐵 |
| 106 | 105, 45, 51 | cbvdisj 5120 |
. . . . . . 7
⊢
(Disj 𝑥
∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) |
| 107 | 104, 106 | sylib 218 |
. . . . . 6
⊢ (𝜑 → Disj 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) |
| 108 | 107 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → Disj 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) |
| 109 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑘(𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) |
| 110 | | nfcsb1v 3923 |
. . . . . . . . 9
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐶 |
| 111 | 110 | nfel1 2922 |
. . . . . . . 8
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞) |
| 112 | 109, 111 | nfim 1896 |
. . . . . . 7
⊢
Ⅎ𝑘((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)) |
| 113 | | eleq1w 2824 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↔ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵)) |
| 114 | 113 | 3anbi3d 1444 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) ↔ (𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵))) |
| 115 | | csbeq1a 3913 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → 𝐶 = ⦋𝑗 / 𝑘⦌𝐶) |
| 116 | 115 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (𝐶 ∈ (0[,]+∞) ↔
⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))) |
| 117 | 114, 116 | imbi12d 344 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → (((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)))) |
| 118 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑦 ∈ 𝐴 |
| 119 | 18, 45 | nfel 2920 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 |
| 120 | 1, 118, 119 | nf3an 1901 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) |
| 121 | 120, 21 | nfim 1896 |
. . . . . . . 8
⊢
Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,]+∞)) |
| 122 | 51 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑘 ∈ 𝐵 ↔ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵)) |
| 123 | 49, 122 | 3anbi23d 1441 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) ↔ (𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵))) |
| 124 | 123 | imbi1d 341 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,]+∞)))) |
| 125 | 121, 124,
22 | chvarfv 2240 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,]+∞)) |
| 126 | 112, 117,
125 | chvarfv 2240 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)) |
| 127 | 126 | 3adant1r 1178 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)) |
| 128 | | simpr 484 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴) |
| 129 | | simpl 482 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ∧ 𝑦 ∈ 𝐴) → ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) |
| 130 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → 𝑦 ∈ 𝐴) |
| 131 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) |
| 132 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥⦋𝑗 / 𝑘⦌𝐶 |
| 133 | 45, 132 | nfmpt 5249 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) |
| 134 | 2, 133 | nffv 6916 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) |
| 135 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥+∞ |
| 136 | 134, 135 | nfne 3043 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞ |
| 137 | | nfcv 2905 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑗𝐶 |
| 138 | 137, 110,
115 | cbvmpt 5253 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) |
| 139 | 138 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) |
| 140 | 61, 139 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) |
| 141 | 140 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))) |
| 142 | 141 | neeq1d 3000 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 →
((Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ↔
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞)) |
| 143 | 136, 142 | rspc 3610 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐴 → (∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ →
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞)) |
| 144 | 130, 131,
143 | sylc 65 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) →
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞) |
| 145 | 128, 129,
144 | syl2anc 584 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ∧ 𝑦 ∈ 𝐴) →
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞) |
| 146 | 145 | neneqd 2945 |
. . . . . . 7
⊢
((∀𝑥 ∈
𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ∧ 𝑦 ∈ 𝐴) → ¬
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) = +∞) |
| 147 | 146 | adantll 714 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → ¬
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) = +∞) |
| 148 | 126 | 3expa 1119 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)) |
| 149 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) |
| 150 | 148, 149 | fmptd 7134 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)) |
| 151 | 150 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)) |
| 152 | 103, 151 | sge0repnf 46401 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) →
((Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈ ℝ ↔ ¬
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) = +∞)) |
| 153 | 147, 152 | mpbird 257 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) →
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈ ℝ) |
| 154 | 137, 110,
115 | cbvmpt 5253 |
. . . . . . . . 9
⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) = (𝑗 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) |
| 155 | 105, 45, 51 | cbviun 5036 |
. . . . . . . . . 10
⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 |
| 156 | 155 | mpteq1i 5238 |
. . . . . . . . 9
⊢ (𝑗 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) = (𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) |
| 157 | 154, 156 | eqtri 2765 |
. . . . . . . 8
⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) = (𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) |
| 158 | 157 | fveq2i 6909 |
. . . . . . 7
⊢
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) |
| 159 | 158, 29 | eqeltrrid 2846 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈
ℝ*) |
| 160 | 159 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) →
(Σ^‘(𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈
ℝ*) |
| 161 | 70, 134, 141 | cbvmpt 5253 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑦 ∈ 𝐴 ↦
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))) |
| 162 | 161 | fveq2i 6909 |
. . . . . . 7
⊢
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) =
(Σ^‘(𝑦 ∈ 𝐴 ↦
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))) |
| 163 | 11, 66 | sge0cl 46396 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ (0[,]+∞)) |
| 164 | 163, 78 | fmptd 7134 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞)) |
| 165 | 10, 164 | sge0xrcl 46400 |
. . . . . . 7
⊢ (𝜑 →
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ∈
ℝ*) |
| 166 | 162, 165 | eqeltrrid 2846 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑦 ∈ 𝐴 ↦
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))) ∈
ℝ*) |
| 167 | 166 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) →
(Σ^‘(𝑦 ∈ 𝐴 ↦
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))) ∈
ℝ*) |
| 168 | | eliun 4995 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) |
| 169 | 168 | biimpi 216 |
. . . . . . . . 9
⊢ (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 → ∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) |
| 170 | 169 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → ∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) |
| 171 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑦𝜑 |
| 172 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦𝑗 |
| 173 | | nfiu1 5027 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 |
| 174 | 172, 173 | nfel 2920 |
. . . . . . . . . 10
⊢
Ⅎ𝑦 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 |
| 175 | 171, 174 | nfan 1899 |
. . . . . . . . 9
⊢
Ⅎ𝑦(𝜑 ∧ 𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) |
| 176 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑦⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞) |
| 177 | 148 | exp31 419 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ 𝐴 → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)))) |
| 178 | 177 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → (𝑦 ∈ 𝐴 → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)))) |
| 179 | 175, 176,
178 | rexlimd 3266 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → (∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))) |
| 180 | 170, 179 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)) |
| 181 | | eqid 2737 |
. . . . . . 7
⊢ (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) = (𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) |
| 182 | 180, 181 | fmptd 7134 |
. . . . . 6
⊢ (𝜑 → (𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)) |
| 183 | 182 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)) |
| 184 | 155, 14 | eqeltrrid 2846 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ∈ V) |
| 185 | 184 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ∈ V) |
| 186 | 96, 103, 108, 127, 153, 160, 167, 183, 185 | sge0iunmptlemre 46430 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) →
(Σ^‘(𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) =
(Σ^‘(𝑦 ∈ 𝐴 ↦
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))))) |
| 187 | 158 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑗 ∈ ∪
𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))) |
| 188 | 162 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) →
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) =
(Σ^‘(𝑦 ∈ 𝐴 ↦
(Σ^‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))))) |
| 189 | 186, 187,
188 | 3eqtr4d 2787 |
. . 3
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) |
| 190 | 89, 95, 189 | syl2anc 584 |
. 2
⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ 𝐴
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) |
| 191 | 88, 190 | pm2.61dan 813 |
1
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑥 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) |