Step | Hyp | Ref
| Expression |
1 | | simpl1 1057 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → 𝐴 ∈ Fin) |
2 | | simpl2 1058 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) |
3 | | simpr 476 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) |
4 | | r19.26 3046 |
. . . . 5
⊢
(∀𝑛 ∈
𝐴 (𝐵 ∈ dom vol ∧ (vol‘𝐵) ∈ ℝ) ↔
(∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ)) |
5 | 2, 3, 4 | sylanbrc 695 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → ∀𝑛 ∈ 𝐴 (𝐵 ∈ dom vol ∧ (vol‘𝐵) ∈
ℝ)) |
6 | | simpl3 1059 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → Disj 𝑛 ∈ 𝐴 𝐵) |
7 | | volfiniun 23122 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 (𝐵 ∈ dom vol ∧ (vol‘𝐵) ∈ ℝ) ∧
Disj 𝑛 ∈ 𝐴 𝐵) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ𝑛 ∈ 𝐴 (vol‘𝐵)) |
8 | 1, 5, 6, 7 | syl3anc 1318 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ𝑛 ∈ 𝐴 (vol‘𝐵)) |
9 | | nfcv 2751 |
. . . 4
⊢
Ⅎ𝑛𝐴 |
10 | 9 | nfel1 2765 |
. . . . . 6
⊢
Ⅎ𝑛 𝐴 ∈ Fin |
11 | | nfra1 2925 |
. . . . . 6
⊢
Ⅎ𝑛∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol |
12 | | nfdisj1 4566 |
. . . . . 6
⊢
Ⅎ𝑛Disj
𝑛 ∈ 𝐴 𝐵 |
13 | 10, 11, 12 | nf3an 1819 |
. . . . 5
⊢
Ⅎ𝑛(𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) |
14 | | nfra1 2925 |
. . . . 5
⊢
Ⅎ𝑛∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ |
15 | 13, 14 | nfan 1816 |
. . . 4
⊢
Ⅎ𝑛((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) |
16 | 3 | r19.21bi 2916 |
. . . . 5
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ ℝ) |
17 | | rspa 2914 |
. . . . . . . 8
⊢
((∀𝑛 ∈
𝐴 𝐵 ∈ dom vol ∧ 𝑛 ∈ 𝐴) → 𝐵 ∈ dom vol) |
18 | | volf 23104 |
. . . . . . . . 9
⊢ vol:dom
vol⟶(0[,]+∞) |
19 | 18 | ffvelrni 6266 |
. . . . . . . 8
⊢ (𝐵 ∈ dom vol →
(vol‘𝐵) ∈
(0[,]+∞)) |
20 | 17, 19 | syl 17 |
. . . . . . 7
⊢
((∀𝑛 ∈
𝐴 𝐵 ∈ dom vol ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,]+∞)) |
21 | 2, 20 | sylan 487 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,]+∞)) |
22 | | 0xr 9965 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
23 | | pnfxr 9971 |
. . . . . . . 8
⊢ +∞
∈ ℝ* |
24 | | elicc1 12090 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ*) →
((vol‘𝐵) ∈
(0[,]+∞) ↔ ((vol‘𝐵) ∈ ℝ* ∧ 0 ≤
(vol‘𝐵) ∧
(vol‘𝐵) ≤
+∞))) |
25 | 22, 23, 24 | mp2an 704 |
. . . . . . 7
⊢
((vol‘𝐵)
∈ (0[,]+∞) ↔ ((vol‘𝐵) ∈ ℝ* ∧ 0 ≤
(vol‘𝐵) ∧
(vol‘𝐵) ≤
+∞)) |
26 | 25 | simp2bi 1070 |
. . . . . 6
⊢
((vol‘𝐵)
∈ (0[,]+∞) → 0 ≤ (vol‘𝐵)) |
27 | 21, 26 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → 0 ≤ (vol‘𝐵)) |
28 | | ltpnf 11830 |
. . . . . 6
⊢
((vol‘𝐵)
∈ ℝ → (vol‘𝐵) < +∞) |
29 | 16, 28 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) < +∞) |
30 | | 0re 9919 |
. . . . . 6
⊢ 0 ∈
ℝ |
31 | | elico2 12108 |
. . . . . 6
⊢ ((0
∈ ℝ ∧ +∞ ∈ ℝ*) →
((vol‘𝐵) ∈
(0[,)+∞) ↔ ((vol‘𝐵) ∈ ℝ ∧ 0 ≤
(vol‘𝐵) ∧
(vol‘𝐵) <
+∞))) |
32 | 30, 23, 31 | mp2an 704 |
. . . . 5
⊢
((vol‘𝐵)
∈ (0[,)+∞) ↔ ((vol‘𝐵) ∈ ℝ ∧ 0 ≤
(vol‘𝐵) ∧
(vol‘𝐵) <
+∞)) |
33 | 16, 27, 29, 32 | syl3anbrc 1239 |
. . . 4
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,)+∞)) |
34 | 9, 15, 1, 33 | esumpfinvalf 29465 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) →
Σ*𝑛 ∈
𝐴(vol‘𝐵) = Σ𝑛 ∈ 𝐴 (vol‘𝐵)) |
35 | 8, 34 | eqtr4d 2647 |
. 2
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ*𝑛 ∈ 𝐴(vol‘𝐵)) |
36 | | simpr 476 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) |
37 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎ𝑘(vol‘𝐵) = +∞ |
38 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛vol |
39 | | nfcsb1v 3515 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐵 |
40 | 38, 39 | nffv 6110 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(vol‘⦋𝑘 / 𝑛⦌𝐵) |
41 | 40 | nfeq1 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑛(vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ |
42 | | csbeq1a 3508 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → 𝐵 = ⦋𝑘 / 𝑛⦌𝐵) |
43 | 42 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (vol‘𝐵) = (vol‘⦋𝑘 / 𝑛⦌𝐵)) |
44 | 43 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → ((vol‘𝐵) = +∞ ↔
(vol‘⦋𝑘
/ 𝑛⦌𝐵) = +∞)) |
45 | 37, 41, 44 | cbvrex 3144 |
. . . . . . . 8
⊢
(∃𝑛 ∈
𝐴 (vol‘𝐵) = +∞ ↔ ∃𝑘 ∈ 𝐴 (vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞) |
46 | 36, 45 | sylib 207 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∃𝑘 ∈ 𝐴 (vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞) |
47 | 39 | nfel1 2765 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol |
48 | 42 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑘 → (𝐵 ∈ dom vol ↔ ⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol)) |
49 | 47, 48 | rspc 3276 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝐴 → (∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol)) |
50 | 49 | impcom 445 |
. . . . . . . . . . . 12
⊢
((∀𝑛 ∈
𝐴 𝐵 ∈ dom vol ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol) |
51 | 50 | adantll 746 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol) |
52 | | finiunmbl 23119 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol) |
53 | 52 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ 𝐴) → ∪
𝑛 ∈ 𝐴 𝐵 ∈ dom vol) |
54 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛𝑘 |
55 | 9, 54, 39, 42 | ssiun2sf 28760 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝐴 → ⦋𝑘 / 𝑛⦌𝐵 ⊆ ∪
𝑛 ∈ 𝐴 𝐵) |
56 | 55 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑛⦌𝐵 ⊆ ∪
𝑛 ∈ 𝐴 𝐵) |
57 | | volss 23108 |
. . . . . . . . . . 11
⊢
((⦋𝑘 /
𝑛⦌𝐵 ∈ dom vol ∧ ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ ⦋𝑘 / 𝑛⦌𝐵 ⊆ ∪
𝑛 ∈ 𝐴 𝐵) → (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
58 | 51, 53, 56, 57 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ 𝐴) → (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
59 | 58 | 3adantl3 1212 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ 𝑘 ∈ 𝐴) → (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
60 | 59 | adantlr 747 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) ∧ 𝑘 ∈ 𝐴) → (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
61 | 60 | ralrimiva 2949 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∀𝑘 ∈ 𝐴 (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
62 | | r19.29r 3055 |
. . . . . . 7
⊢
((∃𝑘 ∈
𝐴
(vol‘⦋𝑘
/ 𝑛⦌𝐵) = +∞ ∧ ∀𝑘 ∈ 𝐴 (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) → ∃𝑘 ∈ 𝐴 ((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ ∧
(vol‘⦋𝑘
/ 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))) |
63 | 46, 61, 62 | syl2anc 691 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∃𝑘 ∈ 𝐴 ((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ ∧
(vol‘⦋𝑘
/ 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))) |
64 | | breq1 4586 |
. . . . . . . 8
⊢
((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ →
((vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ↔ +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))) |
65 | 64 | biimpa 500 |
. . . . . . 7
⊢
(((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ ∧
(vol‘⦋𝑘
/ 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) → +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
66 | 65 | reximi 2994 |
. . . . . 6
⊢
(∃𝑘 ∈
𝐴
((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ ∧
(vol‘⦋𝑘
/ 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) → ∃𝑘 ∈ 𝐴 +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
67 | 63, 66 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∃𝑘 ∈ 𝐴 +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
68 | | rexex 2985 |
. . . . . 6
⊢
(∃𝑘 ∈
𝐴 +∞ ≤
(vol‘∪ 𝑛 ∈ 𝐴 𝐵) → ∃𝑘+∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
69 | | 19.9v 1883 |
. . . . . 6
⊢
(∃𝑘+∞
≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ↔ +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
70 | 68, 69 | sylib 207 |
. . . . 5
⊢
(∃𝑘 ∈
𝐴 +∞ ≤
(vol‘∪ 𝑛 ∈ 𝐴 𝐵) → +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
71 | 67, 70 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → +∞ ≤
(vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
72 | | iccssxr 12127 |
. . . . . . . . 9
⊢
(0[,]+∞) ⊆ ℝ* |
73 | 18 | ffvelrni 6266 |
. . . . . . . . 9
⊢ (∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈ (0[,]+∞)) |
74 | 72, 73 | sseldi 3566 |
. . . . . . . 8
⊢ (∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈
ℝ*) |
75 | 52, 74 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈
ℝ*) |
76 | 75 | 3adant3 1074 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈
ℝ*) |
77 | 76 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈
ℝ*) |
78 | | xgepnf 28904 |
. . . . 5
⊢
((vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈ ℝ* →
(+∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ↔ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = +∞)) |
79 | 77, 78 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → (+∞ ≤
(vol‘∪ 𝑛 ∈ 𝐴 𝐵) ↔ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = +∞)) |
80 | 71, 79 | mpbid 221 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = +∞) |
81 | | nfre1 2988 |
. . . . 5
⊢
Ⅎ𝑛∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞ |
82 | 13, 81 | nfan 1816 |
. . . 4
⊢
Ⅎ𝑛((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) |
83 | | simpl1 1057 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → 𝐴 ∈ Fin) |
84 | 20 | 3ad2antl2 1217 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,]+∞)) |
85 | 84 | adantlr 747 |
. . . 4
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,]+∞)) |
86 | 82, 83, 85, 36 | esumpinfval 29462 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) →
Σ*𝑛 ∈
𝐴(vol‘𝐵) = +∞) |
87 | 80, 86 | eqtr4d 2647 |
. 2
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ*𝑛 ∈ 𝐴(vol‘𝐵)) |
88 | | exmid 430 |
. . . . 5
⊢
(∀𝑛 ∈
𝐴 (vol‘𝐵) ∈ ℝ ∨ ¬
∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) |
89 | | rexnal 2978 |
. . . . . 6
⊢
(∃𝑛 ∈
𝐴 ¬ (vol‘𝐵) ∈ ℝ ↔ ¬
∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) |
90 | 89 | orbi2i 540 |
. . . . 5
⊢
((∀𝑛 ∈
𝐴 (vol‘𝐵) ∈ ℝ ∨
∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ) ↔
(∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ¬ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ)) |
91 | 88, 90 | mpbir 220 |
. . . 4
⊢
(∀𝑛 ∈
𝐴 (vol‘𝐵) ∈ ℝ ∨
∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈
ℝ) |
92 | | r19.29 3054 |
. . . . . . 7
⊢
((∀𝑛 ∈
𝐴 𝐵 ∈ dom vol ∧ ∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ) → ∃𝑛 ∈ 𝐴 (𝐵 ∈ dom vol ∧ ¬ (vol‘𝐵) ∈
ℝ)) |
93 | | xrge0nre 12148 |
. . . . . . . . 9
⊢
(((vol‘𝐵)
∈ (0[,]+∞) ∧ ¬ (vol‘𝐵) ∈ ℝ) → (vol‘𝐵) = +∞) |
94 | 19, 93 | sylan 487 |
. . . . . . . 8
⊢ ((𝐵 ∈ dom vol ∧ ¬
(vol‘𝐵) ∈
ℝ) → (vol‘𝐵) = +∞) |
95 | 94 | reximi 2994 |
. . . . . . 7
⊢
(∃𝑛 ∈
𝐴 (𝐵 ∈ dom vol ∧ ¬ (vol‘𝐵) ∈ ℝ) →
∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) |
96 | 92, 95 | syl 17 |
. . . . . 6
⊢
((∀𝑛 ∈
𝐴 𝐵 ∈ dom vol ∧ ∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ) → ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) |
97 | 96 | ex 449 |
. . . . 5
⊢
(∀𝑛 ∈
𝐴 𝐵 ∈ dom vol → (∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ → ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞)) |
98 | 97 | orim2d 881 |
. . . 4
⊢
(∀𝑛 ∈
𝐴 𝐵 ∈ dom vol → ((∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ) → (∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞))) |
99 | 91, 98 | mpi 20 |
. . 3
⊢
(∀𝑛 ∈
𝐴 𝐵 ∈ dom vol → (∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞)) |
100 | 99 | 3ad2ant2 1076 |
. 2
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) → (∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞)) |
101 | 35, 87, 100 | mpjaodan 823 |
1
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ*𝑛 ∈ 𝐴(vol‘𝐵)) |