Step | Hyp | Ref
| Expression |
1 | | simpl1 1188 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → 𝐴 ∈ Fin) |
2 | | simpl2 1189 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) |
3 | | simpr 488 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) |
4 | | r19.26 3137 |
. . . . 5
⊢
(∀𝑛 ∈
𝐴 (𝐵 ∈ dom vol ∧ (vol‘𝐵) ∈ ℝ) ↔
(∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ)) |
5 | 2, 3, 4 | sylanbrc 586 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → ∀𝑛 ∈ 𝐴 (𝐵 ∈ dom vol ∧ (vol‘𝐵) ∈
ℝ)) |
6 | | simpl3 1190 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → Disj 𝑛 ∈ 𝐴 𝐵) |
7 | | volfiniun 24151 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 (𝐵 ∈ dom vol ∧ (vol‘𝐵) ∈ ℝ) ∧
Disj 𝑛 ∈ 𝐴 𝐵) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ𝑛 ∈ 𝐴 (vol‘𝐵)) |
8 | 1, 5, 6, 7 | syl3anc 1368 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ𝑛 ∈ 𝐴 (vol‘𝐵)) |
9 | | nfcv 2955 |
. . . 4
⊢
Ⅎ𝑛𝐴 |
10 | 9 | nfel1 2971 |
. . . . . 6
⊢
Ⅎ𝑛 𝐴 ∈ Fin |
11 | | nfra1 3183 |
. . . . . 6
⊢
Ⅎ𝑛∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol |
12 | | nfdisj1 5009 |
. . . . . 6
⊢
Ⅎ𝑛Disj
𝑛 ∈ 𝐴 𝐵 |
13 | 10, 11, 12 | nf3an 1902 |
. . . . 5
⊢
Ⅎ𝑛(𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) |
14 | | nfra1 3183 |
. . . . 5
⊢
Ⅎ𝑛∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ |
15 | 13, 14 | nfan 1900 |
. . . 4
⊢
Ⅎ𝑛((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) |
16 | 3 | r19.21bi 3173 |
. . . . 5
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ ℝ) |
17 | | rspa 3171 |
. . . . . . . 8
⊢
((∀𝑛 ∈
𝐴 𝐵 ∈ dom vol ∧ 𝑛 ∈ 𝐴) → 𝐵 ∈ dom vol) |
18 | | volf 24133 |
. . . . . . . . 9
⊢ vol:dom
vol⟶(0[,]+∞) |
19 | 18 | ffvelrni 6827 |
. . . . . . . 8
⊢ (𝐵 ∈ dom vol →
(vol‘𝐵) ∈
(0[,]+∞)) |
20 | 17, 19 | syl 17 |
. . . . . . 7
⊢
((∀𝑛 ∈
𝐴 𝐵 ∈ dom vol ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,]+∞)) |
21 | 2, 20 | sylan 583 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,]+∞)) |
22 | | 0xr 10677 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
23 | | pnfxr 10684 |
. . . . . . . 8
⊢ +∞
∈ ℝ* |
24 | | elicc1 12770 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ*) →
((vol‘𝐵) ∈
(0[,]+∞) ↔ ((vol‘𝐵) ∈ ℝ* ∧ 0 ≤
(vol‘𝐵) ∧
(vol‘𝐵) ≤
+∞))) |
25 | 22, 23, 24 | mp2an 691 |
. . . . . . 7
⊢
((vol‘𝐵)
∈ (0[,]+∞) ↔ ((vol‘𝐵) ∈ ℝ* ∧ 0 ≤
(vol‘𝐵) ∧
(vol‘𝐵) ≤
+∞)) |
26 | 25 | simp2bi 1143 |
. . . . . 6
⊢
((vol‘𝐵)
∈ (0[,]+∞) → 0 ≤ (vol‘𝐵)) |
27 | 21, 26 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → 0 ≤ (vol‘𝐵)) |
28 | | ltpnf 12503 |
. . . . . 6
⊢
((vol‘𝐵)
∈ ℝ → (vol‘𝐵) < +∞) |
29 | 16, 28 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) < +∞) |
30 | | 0re 10632 |
. . . . . 6
⊢ 0 ∈
ℝ |
31 | | elico2 12789 |
. . . . . 6
⊢ ((0
∈ ℝ ∧ +∞ ∈ ℝ*) →
((vol‘𝐵) ∈
(0[,)+∞) ↔ ((vol‘𝐵) ∈ ℝ ∧ 0 ≤
(vol‘𝐵) ∧
(vol‘𝐵) <
+∞))) |
32 | 30, 23, 31 | mp2an 691 |
. . . . 5
⊢
((vol‘𝐵)
∈ (0[,)+∞) ↔ ((vol‘𝐵) ∈ ℝ ∧ 0 ≤
(vol‘𝐵) ∧
(vol‘𝐵) <
+∞)) |
33 | 16, 27, 29, 32 | syl3anbrc 1340 |
. . . 4
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,)+∞)) |
34 | 9, 15, 1, 33 | esumpfinvalf 31445 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) →
Σ*𝑛 ∈
𝐴(vol‘𝐵) = Σ𝑛 ∈ 𝐴 (vol‘𝐵)) |
35 | 8, 34 | eqtr4d 2836 |
. 2
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ*𝑛 ∈ 𝐴(vol‘𝐵)) |
36 | | simpr 488 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) |
37 | | nfv 1915 |
. . . . . . . . 9
⊢
Ⅎ𝑘(vol‘𝐵) = +∞ |
38 | | nfcv 2955 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛vol |
39 | | nfcsb1v 3852 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐵 |
40 | 38, 39 | nffv 6655 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(vol‘⦋𝑘 / 𝑛⦌𝐵) |
41 | 40 | nfeq1 2970 |
. . . . . . . . 9
⊢
Ⅎ𝑛(vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ |
42 | | csbeq1a 3842 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → 𝐵 = ⦋𝑘 / 𝑛⦌𝐵) |
43 | 42 | fveqeq2d 6653 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → ((vol‘𝐵) = +∞ ↔
(vol‘⦋𝑘
/ 𝑛⦌𝐵) = +∞)) |
44 | 37, 41, 43 | cbvrexw 3388 |
. . . . . . . 8
⊢
(∃𝑛 ∈
𝐴 (vol‘𝐵) = +∞ ↔ ∃𝑘 ∈ 𝐴 (vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞) |
45 | 36, 44 | sylib 221 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∃𝑘 ∈ 𝐴 (vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞) |
46 | 39 | nfel1 2971 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol |
47 | 42 | eleq1d 2874 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑘 → (𝐵 ∈ dom vol ↔ ⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol)) |
48 | 46, 47 | rspc 3559 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝐴 → (∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol)) |
49 | 48 | impcom 411 |
. . . . . . . . . . . 12
⊢
((∀𝑛 ∈
𝐴 𝐵 ∈ dom vol ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol) |
50 | 49 | adantll 713 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol) |
51 | | finiunmbl 24148 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol) |
52 | 51 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ 𝐴) → ∪
𝑛 ∈ 𝐴 𝐵 ∈ dom vol) |
53 | | nfcv 2955 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛𝑘 |
54 | 9, 53, 39, 42 | ssiun2sf 30323 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝐴 → ⦋𝑘 / 𝑛⦌𝐵 ⊆ ∪
𝑛 ∈ 𝐴 𝐵) |
55 | 54 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑛⦌𝐵 ⊆ ∪
𝑛 ∈ 𝐴 𝐵) |
56 | | volss 24137 |
. . . . . . . . . . 11
⊢
((⦋𝑘 /
𝑛⦌𝐵 ∈ dom vol ∧ ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ ⦋𝑘 / 𝑛⦌𝐵 ⊆ ∪
𝑛 ∈ 𝐴 𝐵) → (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
57 | 50, 52, 55, 56 | syl3anc 1368 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ 𝐴) → (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
58 | 57 | 3adantl3 1165 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ 𝑘 ∈ 𝐴) → (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
59 | 58 | adantlr 714 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) ∧ 𝑘 ∈ 𝐴) → (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
60 | 59 | ralrimiva 3149 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∀𝑘 ∈ 𝐴 (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
61 | | r19.29r 3217 |
. . . . . . 7
⊢
((∃𝑘 ∈
𝐴
(vol‘⦋𝑘
/ 𝑛⦌𝐵) = +∞ ∧ ∀𝑘 ∈ 𝐴 (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) → ∃𝑘 ∈ 𝐴 ((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ ∧
(vol‘⦋𝑘
/ 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))) |
62 | 45, 60, 61 | syl2anc 587 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∃𝑘 ∈ 𝐴 ((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ ∧
(vol‘⦋𝑘
/ 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))) |
63 | | breq1 5033 |
. . . . . . . 8
⊢
((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ →
((vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ↔ +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))) |
64 | 63 | biimpa 480 |
. . . . . . 7
⊢
(((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ ∧
(vol‘⦋𝑘
/ 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) → +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
65 | 64 | reximi 3206 |
. . . . . 6
⊢
(∃𝑘 ∈
𝐴
((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ ∧
(vol‘⦋𝑘
/ 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) → ∃𝑘 ∈ 𝐴 +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
66 | 62, 65 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∃𝑘 ∈ 𝐴 +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
67 | | rexex 3203 |
. . . . . 6
⊢
(∃𝑘 ∈
𝐴 +∞ ≤
(vol‘∪ 𝑛 ∈ 𝐴 𝐵) → ∃𝑘+∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
68 | | 19.9v 1988 |
. . . . . 6
⊢
(∃𝑘+∞
≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ↔ +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
69 | 67, 68 | sylib 221 |
. . . . 5
⊢
(∃𝑘 ∈
𝐴 +∞ ≤
(vol‘∪ 𝑛 ∈ 𝐴 𝐵) → +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
70 | 66, 69 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → +∞ ≤
(vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
71 | | iccssxr 12808 |
. . . . . . . . 9
⊢
(0[,]+∞) ⊆ ℝ* |
72 | 18 | ffvelrni 6827 |
. . . . . . . . 9
⊢ (∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈ (0[,]+∞)) |
73 | 71, 72 | sseldi 3913 |
. . . . . . . 8
⊢ (∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈
ℝ*) |
74 | 51, 73 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈
ℝ*) |
75 | 74 | 3adant3 1129 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈
ℝ*) |
76 | 75 | adantr 484 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈
ℝ*) |
77 | | xgepnf 12546 |
. . . . 5
⊢
((vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈ ℝ* →
(+∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ↔ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = +∞)) |
78 | 76, 77 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → (+∞ ≤
(vol‘∪ 𝑛 ∈ 𝐴 𝐵) ↔ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = +∞)) |
79 | 70, 78 | mpbid 235 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = +∞) |
80 | | nfre1 3265 |
. . . . 5
⊢
Ⅎ𝑛∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞ |
81 | 13, 80 | nfan 1900 |
. . . 4
⊢
Ⅎ𝑛((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) |
82 | | simpl1 1188 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → 𝐴 ∈ Fin) |
83 | 20 | 3ad2antl2 1183 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,]+∞)) |
84 | 83 | adantlr 714 |
. . . 4
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,]+∞)) |
85 | 81, 82, 84, 36 | esumpinfval 31442 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) →
Σ*𝑛 ∈
𝐴(vol‘𝐵) = +∞) |
86 | 79, 85 | eqtr4d 2836 |
. 2
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ*𝑛 ∈ 𝐴(vol‘𝐵)) |
87 | | exmid 892 |
. . . . 5
⊢
(∀𝑛 ∈
𝐴 (vol‘𝐵) ∈ ℝ ∨ ¬
∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) |
88 | | rexnal 3201 |
. . . . . 6
⊢
(∃𝑛 ∈
𝐴 ¬ (vol‘𝐵) ∈ ℝ ↔ ¬
∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) |
89 | 88 | orbi2i 910 |
. . . . 5
⊢
((∀𝑛 ∈
𝐴 (vol‘𝐵) ∈ ℝ ∨
∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ) ↔
(∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ¬ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ)) |
90 | 87, 89 | mpbir 234 |
. . . 4
⊢
(∀𝑛 ∈
𝐴 (vol‘𝐵) ∈ ℝ ∨
∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈
ℝ) |
91 | | r19.29 3216 |
. . . . . . 7
⊢
((∀𝑛 ∈
𝐴 𝐵 ∈ dom vol ∧ ∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ) → ∃𝑛 ∈ 𝐴 (𝐵 ∈ dom vol ∧ ¬ (vol‘𝐵) ∈
ℝ)) |
92 | | xrge0nre 12831 |
. . . . . . . . 9
⊢
(((vol‘𝐵)
∈ (0[,]+∞) ∧ ¬ (vol‘𝐵) ∈ ℝ) → (vol‘𝐵) = +∞) |
93 | 19, 92 | sylan 583 |
. . . . . . . 8
⊢ ((𝐵 ∈ dom vol ∧ ¬
(vol‘𝐵) ∈
ℝ) → (vol‘𝐵) = +∞) |
94 | 93 | reximi 3206 |
. . . . . . 7
⊢
(∃𝑛 ∈
𝐴 (𝐵 ∈ dom vol ∧ ¬ (vol‘𝐵) ∈ ℝ) →
∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) |
95 | 91, 94 | syl 17 |
. . . . . 6
⊢
((∀𝑛 ∈
𝐴 𝐵 ∈ dom vol ∧ ∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ) → ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) |
96 | 95 | ex 416 |
. . . . 5
⊢
(∀𝑛 ∈
𝐴 𝐵 ∈ dom vol → (∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ → ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞)) |
97 | 96 | orim2d 964 |
. . . 4
⊢
(∀𝑛 ∈
𝐴 𝐵 ∈ dom vol → ((∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ) → (∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞))) |
98 | 90, 97 | mpi 20 |
. . 3
⊢
(∀𝑛 ∈
𝐴 𝐵 ∈ dom vol → (∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞)) |
99 | 98 | 3ad2ant2 1131 |
. 2
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) → (∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞)) |
100 | 35, 86, 99 | mpjaodan 956 |
1
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ*𝑛 ∈ 𝐴(vol‘𝐵)) |