| Step | Hyp | Ref
| Expression |
| 1 | | simpl1 1192 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → 𝐴 ∈ Fin) |
| 2 | | simpl2 1193 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) |
| 3 | | simpr 484 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) |
| 4 | | r19.26 3111 |
. . . . 5
⊢
(∀𝑛 ∈
𝐴 (𝐵 ∈ dom vol ∧ (vol‘𝐵) ∈ ℝ) ↔
(∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ)) |
| 5 | 2, 3, 4 | sylanbrc 583 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → ∀𝑛 ∈ 𝐴 (𝐵 ∈ dom vol ∧ (vol‘𝐵) ∈
ℝ)) |
| 6 | | simpl3 1194 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → Disj 𝑛 ∈ 𝐴 𝐵) |
| 7 | | volfiniun 25582 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 (𝐵 ∈ dom vol ∧ (vol‘𝐵) ∈ ℝ) ∧
Disj 𝑛 ∈ 𝐴 𝐵) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ𝑛 ∈ 𝐴 (vol‘𝐵)) |
| 8 | 1, 5, 6, 7 | syl3anc 1373 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ𝑛 ∈ 𝐴 (vol‘𝐵)) |
| 9 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑛𝐴 |
| 10 | 9 | nfel1 2922 |
. . . . . 6
⊢
Ⅎ𝑛 𝐴 ∈ Fin |
| 11 | | nfra1 3284 |
. . . . . 6
⊢
Ⅎ𝑛∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol |
| 12 | | nfdisj1 5124 |
. . . . . 6
⊢
Ⅎ𝑛Disj
𝑛 ∈ 𝐴 𝐵 |
| 13 | 10, 11, 12 | nf3an 1901 |
. . . . 5
⊢
Ⅎ𝑛(𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) |
| 14 | | nfra1 3284 |
. . . . 5
⊢
Ⅎ𝑛∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ |
| 15 | 13, 14 | nfan 1899 |
. . . 4
⊢
Ⅎ𝑛((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) |
| 16 | 3 | r19.21bi 3251 |
. . . . 5
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ ℝ) |
| 17 | | rspa 3248 |
. . . . . . . 8
⊢
((∀𝑛 ∈
𝐴 𝐵 ∈ dom vol ∧ 𝑛 ∈ 𝐴) → 𝐵 ∈ dom vol) |
| 18 | | volf 25564 |
. . . . . . . . 9
⊢ vol:dom
vol⟶(0[,]+∞) |
| 19 | 18 | ffvelcdmi 7103 |
. . . . . . . 8
⊢ (𝐵 ∈ dom vol →
(vol‘𝐵) ∈
(0[,]+∞)) |
| 20 | 17, 19 | syl 17 |
. . . . . . 7
⊢
((∀𝑛 ∈
𝐴 𝐵 ∈ dom vol ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,]+∞)) |
| 21 | 2, 20 | sylan 580 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,]+∞)) |
| 22 | | 0xr 11308 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
| 23 | | pnfxr 11315 |
. . . . . . . 8
⊢ +∞
∈ ℝ* |
| 24 | | elicc1 13431 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ*) →
((vol‘𝐵) ∈
(0[,]+∞) ↔ ((vol‘𝐵) ∈ ℝ* ∧ 0 ≤
(vol‘𝐵) ∧
(vol‘𝐵) ≤
+∞))) |
| 25 | 22, 23, 24 | mp2an 692 |
. . . . . . 7
⊢
((vol‘𝐵)
∈ (0[,]+∞) ↔ ((vol‘𝐵) ∈ ℝ* ∧ 0 ≤
(vol‘𝐵) ∧
(vol‘𝐵) ≤
+∞)) |
| 26 | 25 | simp2bi 1147 |
. . . . . 6
⊢
((vol‘𝐵)
∈ (0[,]+∞) → 0 ≤ (vol‘𝐵)) |
| 27 | 21, 26 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → 0 ≤ (vol‘𝐵)) |
| 28 | | ltpnf 13162 |
. . . . . 6
⊢
((vol‘𝐵)
∈ ℝ → (vol‘𝐵) < +∞) |
| 29 | 16, 28 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) < +∞) |
| 30 | | 0re 11263 |
. . . . . 6
⊢ 0 ∈
ℝ |
| 31 | | elico2 13451 |
. . . . . 6
⊢ ((0
∈ ℝ ∧ +∞ ∈ ℝ*) →
((vol‘𝐵) ∈
(0[,)+∞) ↔ ((vol‘𝐵) ∈ ℝ ∧ 0 ≤
(vol‘𝐵) ∧
(vol‘𝐵) <
+∞))) |
| 32 | 30, 23, 31 | mp2an 692 |
. . . . 5
⊢
((vol‘𝐵)
∈ (0[,)+∞) ↔ ((vol‘𝐵) ∈ ℝ ∧ 0 ≤
(vol‘𝐵) ∧
(vol‘𝐵) <
+∞)) |
| 33 | 16, 27, 29, 32 | syl3anbrc 1344 |
. . . 4
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,)+∞)) |
| 34 | 9, 15, 1, 33 | esumpfinvalf 34077 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) →
Σ*𝑛 ∈
𝐴(vol‘𝐵) = Σ𝑛 ∈ 𝐴 (vol‘𝐵)) |
| 35 | 8, 34 | eqtr4d 2780 |
. 2
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ*𝑛 ∈ 𝐴(vol‘𝐵)) |
| 36 | | simpr 484 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) |
| 37 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑘(vol‘𝐵) = +∞ |
| 38 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛vol |
| 39 | | nfcsb1v 3923 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐵 |
| 40 | 38, 39 | nffv 6916 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(vol‘⦋𝑘 / 𝑛⦌𝐵) |
| 41 | 40 | nfeq1 2921 |
. . . . . . . . 9
⊢
Ⅎ𝑛(vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ |
| 42 | | csbeq1a 3913 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → 𝐵 = ⦋𝑘 / 𝑛⦌𝐵) |
| 43 | 42 | fveqeq2d 6914 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → ((vol‘𝐵) = +∞ ↔
(vol‘⦋𝑘
/ 𝑛⦌𝐵) = +∞)) |
| 44 | 37, 41, 43 | cbvrexw 3307 |
. . . . . . . 8
⊢
(∃𝑛 ∈
𝐴 (vol‘𝐵) = +∞ ↔ ∃𝑘 ∈ 𝐴 (vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞) |
| 45 | 36, 44 | sylib 218 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∃𝑘 ∈ 𝐴 (vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞) |
| 46 | 39 | nfel1 2922 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol |
| 47 | 42 | eleq1d 2826 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑘 → (𝐵 ∈ dom vol ↔ ⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol)) |
| 48 | 46, 47 | rspc 3610 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝐴 → (∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol → ⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol)) |
| 49 | 48 | impcom 407 |
. . . . . . . . . . . 12
⊢
((∀𝑛 ∈
𝐴 𝐵 ∈ dom vol ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol) |
| 50 | 49 | adantll 714 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑛⦌𝐵 ∈ dom vol) |
| 51 | | finiunmbl 25579 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol) |
| 52 | 51 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ 𝐴) → ∪
𝑛 ∈ 𝐴 𝐵 ∈ dom vol) |
| 53 | | nfcv 2905 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛𝑘 |
| 54 | 9, 53, 39, 42 | ssiun2sf 32572 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝐴 → ⦋𝑘 / 𝑛⦌𝐵 ⊆ ∪
𝑛 ∈ 𝐴 𝐵) |
| 55 | 54 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑛⦌𝐵 ⊆ ∪
𝑛 ∈ 𝐴 𝐵) |
| 56 | | volss 25568 |
. . . . . . . . . . 11
⊢
((⦋𝑘 /
𝑛⦌𝐵 ∈ dom vol ∧ ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ ⦋𝑘 / 𝑛⦌𝐵 ⊆ ∪
𝑛 ∈ 𝐴 𝐵) → (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
| 57 | 50, 52, 55, 56 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) ∧ 𝑘 ∈ 𝐴) → (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
| 58 | 57 | 3adantl3 1169 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ 𝑘 ∈ 𝐴) → (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
| 59 | 58 | adantlr 715 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) ∧ 𝑘 ∈ 𝐴) → (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
| 60 | 59 | ralrimiva 3146 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∀𝑘 ∈ 𝐴 (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
| 61 | | r19.29r 3116 |
. . . . . . 7
⊢
((∃𝑘 ∈
𝐴
(vol‘⦋𝑘
/ 𝑛⦌𝐵) = +∞ ∧ ∀𝑘 ∈ 𝐴 (vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) → ∃𝑘 ∈ 𝐴 ((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ ∧
(vol‘⦋𝑘
/ 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))) |
| 62 | 45, 60, 61 | syl2anc 584 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∃𝑘 ∈ 𝐴 ((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ ∧
(vol‘⦋𝑘
/ 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))) |
| 63 | | breq1 5146 |
. . . . . . . 8
⊢
((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ →
((vol‘⦋𝑘 / 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ↔ +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵))) |
| 64 | 63 | biimpa 476 |
. . . . . . 7
⊢
(((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ ∧
(vol‘⦋𝑘
/ 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) → +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
| 65 | 64 | reximi 3084 |
. . . . . 6
⊢
(∃𝑘 ∈
𝐴
((vol‘⦋𝑘 / 𝑛⦌𝐵) = +∞ ∧
(vol‘⦋𝑘
/ 𝑛⦌𝐵) ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) → ∃𝑘 ∈ 𝐴 +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
| 66 | 62, 65 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → ∃𝑘 ∈ 𝐴 +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
| 67 | | rexex 3076 |
. . . . . 6
⊢
(∃𝑘 ∈
𝐴 +∞ ≤
(vol‘∪ 𝑛 ∈ 𝐴 𝐵) → ∃𝑘+∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
| 68 | | 19.9v 1983 |
. . . . . 6
⊢
(∃𝑘+∞
≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ↔ +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
| 69 | 67, 68 | sylib 218 |
. . . . 5
⊢
(∃𝑘 ∈
𝐴 +∞ ≤
(vol‘∪ 𝑛 ∈ 𝐴 𝐵) → +∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
| 70 | 66, 69 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → +∞ ≤
(vol‘∪ 𝑛 ∈ 𝐴 𝐵)) |
| 71 | | iccssxr 13470 |
. . . . . . . . 9
⊢
(0[,]+∞) ⊆ ℝ* |
| 72 | 18 | ffvelcdmi 7103 |
. . . . . . . . 9
⊢ (∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈ (0[,]+∞)) |
| 73 | 71, 72 | sselid 3981 |
. . . . . . . 8
⊢ (∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈
ℝ*) |
| 74 | 51, 73 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈
ℝ*) |
| 75 | 74 | 3adant3 1133 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈
ℝ*) |
| 76 | 75 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈
ℝ*) |
| 77 | | xgepnf 13207 |
. . . . 5
⊢
((vol‘∪ 𝑛 ∈ 𝐴 𝐵) ∈ ℝ* →
(+∞ ≤ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) ↔ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = +∞)) |
| 78 | 76, 77 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → (+∞ ≤
(vol‘∪ 𝑛 ∈ 𝐴 𝐵) ↔ (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = +∞)) |
| 79 | 70, 78 | mpbid 232 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = +∞) |
| 80 | | nfre1 3285 |
. . . . 5
⊢
Ⅎ𝑛∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞ |
| 81 | 13, 80 | nfan 1899 |
. . . 4
⊢
Ⅎ𝑛((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) |
| 82 | | simpl1 1192 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → 𝐴 ∈ Fin) |
| 83 | 20 | 3ad2antl2 1187 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,]+∞)) |
| 84 | 83 | adantlr 715 |
. . . 4
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) ∧ 𝑛 ∈ 𝐴) → (vol‘𝐵) ∈ (0[,]+∞)) |
| 85 | 81, 82, 84, 36 | esumpinfval 34074 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) →
Σ*𝑛 ∈
𝐴(vol‘𝐵) = +∞) |
| 86 | 79, 85 | eqtr4d 2780 |
. 2
⊢ (((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) ∧ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ*𝑛 ∈ 𝐴(vol‘𝐵)) |
| 87 | | exmid 895 |
. . . . 5
⊢
(∀𝑛 ∈
𝐴 (vol‘𝐵) ∈ ℝ ∨ ¬
∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) |
| 88 | | rexnal 3100 |
. . . . . 6
⊢
(∃𝑛 ∈
𝐴 ¬ (vol‘𝐵) ∈ ℝ ↔ ¬
∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ) |
| 89 | 88 | orbi2i 913 |
. . . . 5
⊢
((∀𝑛 ∈
𝐴 (vol‘𝐵) ∈ ℝ ∨
∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ) ↔
(∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ¬ ∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ)) |
| 90 | 87, 89 | mpbir 231 |
. . . 4
⊢
(∀𝑛 ∈
𝐴 (vol‘𝐵) ∈ ℝ ∨
∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈
ℝ) |
| 91 | | r19.29 3114 |
. . . . . . 7
⊢
((∀𝑛 ∈
𝐴 𝐵 ∈ dom vol ∧ ∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ) → ∃𝑛 ∈ 𝐴 (𝐵 ∈ dom vol ∧ ¬ (vol‘𝐵) ∈
ℝ)) |
| 92 | | xrge0nre 13493 |
. . . . . . . . 9
⊢
(((vol‘𝐵)
∈ (0[,]+∞) ∧ ¬ (vol‘𝐵) ∈ ℝ) → (vol‘𝐵) = +∞) |
| 93 | 19, 92 | sylan 580 |
. . . . . . . 8
⊢ ((𝐵 ∈ dom vol ∧ ¬
(vol‘𝐵) ∈
ℝ) → (vol‘𝐵) = +∞) |
| 94 | 93 | reximi 3084 |
. . . . . . 7
⊢
(∃𝑛 ∈
𝐴 (𝐵 ∈ dom vol ∧ ¬ (vol‘𝐵) ∈ ℝ) →
∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) |
| 95 | 91, 94 | syl 17 |
. . . . . 6
⊢
((∀𝑛 ∈
𝐴 𝐵 ∈ dom vol ∧ ∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ) → ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞) |
| 96 | 95 | ex 412 |
. . . . 5
⊢
(∀𝑛 ∈
𝐴 𝐵 ∈ dom vol → (∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ → ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞)) |
| 97 | 96 | orim2d 969 |
. . . 4
⊢
(∀𝑛 ∈
𝐴 𝐵 ∈ dom vol → ((∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ∃𝑛 ∈ 𝐴 ¬ (vol‘𝐵) ∈ ℝ) → (∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞))) |
| 98 | 90, 97 | mpi 20 |
. . 3
⊢
(∀𝑛 ∈
𝐴 𝐵 ∈ dom vol → (∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞)) |
| 99 | 98 | 3ad2ant2 1135 |
. 2
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) → (∀𝑛 ∈ 𝐴 (vol‘𝐵) ∈ ℝ ∨ ∃𝑛 ∈ 𝐴 (vol‘𝐵) = +∞)) |
| 100 | 35, 86, 99 | mpjaodan 961 |
1
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ*𝑛 ∈ 𝐴(vol‘𝐵)) |