| Step | Hyp | Ref
| Expression |
| 1 | | iuneq1 5008 |
. . . . . 6
⊢ (𝐴 = ∅ → ∪ 𝑛 ∈ 𝐴 𝐵 = ∪ 𝑛 ∈ ∅ 𝐵) |
| 2 | | 0iun 5063 |
. . . . . 6
⊢ ∪ 𝑛 ∈ ∅ 𝐵 = ∅ |
| 3 | 1, 2 | eqtrdi 2793 |
. . . . 5
⊢ (𝐴 = ∅ → ∪ 𝑛 ∈ 𝐴 𝐵 = ∅) |
| 4 | 3 | fveq2d 6910 |
. . . 4
⊢ (𝐴 = ∅ →
(vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = (vol*‘∅)) |
| 5 | | ovol0 25528 |
. . . 4
⊢
(vol*‘∅) = 0 |
| 6 | 4, 5 | eqtrdi 2793 |
. . 3
⊢ (𝐴 = ∅ →
(vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0) |
| 7 | 6 | a1i 11 |
. 2
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (𝐴 = ∅ →
(vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0)) |
| 8 | | reldom 8991 |
. . . . . 6
⊢ Rel
≼ |
| 9 | 8 | brrelex1i 5741 |
. . . . 5
⊢ (𝐴 ≼ ℕ → 𝐴 ∈ V) |
| 10 | 9 | adantr 480 |
. . . 4
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → 𝐴 ∈ V) |
| 11 | | 0sdomg 9144 |
. . . 4
⊢ (𝐴 ∈ V → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
| 12 | 10, 11 | syl 17 |
. . 3
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (∅ ≺
𝐴 ↔ 𝐴 ≠ ∅)) |
| 13 | | fodomr 9168 |
. . . . . 6
⊢ ((∅
≺ 𝐴 ∧ 𝐴 ≼ ℕ) →
∃𝑓 𝑓:ℕ–onto→𝐴) |
| 14 | 13 | expcom 413 |
. . . . 5
⊢ (𝐴 ≼ ℕ → (∅
≺ 𝐴 →
∃𝑓 𝑓:ℕ–onto→𝐴)) |
| 15 | 14 | adantr 480 |
. . . 4
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (∅ ≺
𝐴 → ∃𝑓 𝑓:ℕ–onto→𝐴)) |
| 16 | | eliun 4995 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝐴 𝐵 ↔ ∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵) |
| 17 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛 𝑓:ℕ–onto→𝐴 |
| 18 | | nfcv 2905 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛ℕ |
| 19 | | nfcsb1v 3923 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛⦋(𝑓‘𝑘) / 𝑛⦌𝐵 |
| 20 | 18, 19 | nfiun 5023 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛∪ 𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵 |
| 21 | 20 | nfcri 2897 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛 𝑥 ∈ ∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵 |
| 22 | | foelrn 7127 |
. . . . . . . . . . . . 13
⊢ ((𝑓:ℕ–onto→𝐴 ∧ 𝑛 ∈ 𝐴) → ∃𝑘 ∈ ℕ 𝑛 = (𝑓‘𝑘)) |
| 23 | 22 | ex 412 |
. . . . . . . . . . . 12
⊢ (𝑓:ℕ–onto→𝐴 → (𝑛 ∈ 𝐴 → ∃𝑘 ∈ ℕ 𝑛 = (𝑓‘𝑘))) |
| 24 | | csbeq1a 3913 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = (𝑓‘𝑘) → 𝐵 = ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) |
| 25 | 24 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:ℕ–onto→𝐴 ∧ 𝑛 = (𝑓‘𝑘)) → 𝐵 = ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) |
| 26 | 25 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:ℕ–onto→𝐴 ∧ 𝑛 = (𝑓‘𝑘)) → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
| 27 | 26 | biimpd 229 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:ℕ–onto→𝐴 ∧ 𝑛 = (𝑓‘𝑘)) → (𝑥 ∈ 𝐵 → 𝑥 ∈ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
| 28 | 27 | impancom 451 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:ℕ–onto→𝐴 ∧ 𝑥 ∈ 𝐵) → (𝑛 = (𝑓‘𝑘) → 𝑥 ∈ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
| 29 | 28 | reximdv 3170 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:ℕ–onto→𝐴 ∧ 𝑥 ∈ 𝐵) → (∃𝑘 ∈ ℕ 𝑛 = (𝑓‘𝑘) → ∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
| 30 | | eliun 4995 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ↔ ∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) |
| 31 | 29, 30 | imbitrrdi 252 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:ℕ–onto→𝐴 ∧ 𝑥 ∈ 𝐵) → (∃𝑘 ∈ ℕ 𝑛 = (𝑓‘𝑘) → 𝑥 ∈ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
| 32 | 31 | ex 412 |
. . . . . . . . . . . . 13
⊢ (𝑓:ℕ–onto→𝐴 → (𝑥 ∈ 𝐵 → (∃𝑘 ∈ ℕ 𝑛 = (𝑓‘𝑘) → 𝑥 ∈ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵))) |
| 33 | 32 | com23 86 |
. . . . . . . . . . . 12
⊢ (𝑓:ℕ–onto→𝐴 → (∃𝑘 ∈ ℕ 𝑛 = (𝑓‘𝑘) → (𝑥 ∈ 𝐵 → 𝑥 ∈ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵))) |
| 34 | 23, 33 | syld 47 |
. . . . . . . . . . 11
⊢ (𝑓:ℕ–onto→𝐴 → (𝑛 ∈ 𝐴 → (𝑥 ∈ 𝐵 → 𝑥 ∈ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵))) |
| 35 | 17, 21, 34 | rexlimd 3266 |
. . . . . . . . . 10
⊢ (𝑓:ℕ–onto→𝐴 → (∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵 → 𝑥 ∈ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
| 36 | 16, 35 | biimtrid 242 |
. . . . . . . . 9
⊢ (𝑓:ℕ–onto→𝐴 → (𝑥 ∈ ∪
𝑛 ∈ 𝐴 𝐵 → 𝑥 ∈ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
| 37 | 36 | ssrdv 3989 |
. . . . . . . 8
⊢ (𝑓:ℕ–onto→𝐴 → ∪
𝑛 ∈ 𝐴 𝐵 ⊆ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵) |
| 38 | 37 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → ∪
𝑛 ∈ 𝐴 𝐵 ⊆ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵) |
| 39 | | fof 6820 |
. . . . . . . . . . . . 13
⊢ (𝑓:ℕ–onto→𝐴 → 𝑓:ℕ⟶𝐴) |
| 40 | 39 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → 𝑓:ℕ⟶𝐴) |
| 41 | 40 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ ((((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) ∈ 𝐴) |
| 42 | | simpllr 776 |
. . . . . . . . . . 11
⊢ ((((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑘 ∈ ℕ) → ∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) |
| 43 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛ℝ |
| 44 | 19, 43 | nfss 3976 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ |
| 45 | | nfcv 2905 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛vol* |
| 46 | 45, 19 | nffv 6916 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) |
| 47 | 46 | nfeq1 2921 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0 |
| 48 | 44, 47 | nfan 1899 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ ∧
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0) |
| 49 | 24 | sseq1d 4015 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑓‘𝑘) → (𝐵 ⊆ ℝ ↔
⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ)) |
| 50 | 24 | fveqeq2d 6914 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑓‘𝑘) → ((vol*‘𝐵) = 0 ↔
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0)) |
| 51 | 49, 50 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝑓‘𝑘) → ((𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0) ↔
(⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ ∧
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0))) |
| 52 | 48, 51 | rspc 3610 |
. . . . . . . . . . 11
⊢ ((𝑓‘𝑘) ∈ 𝐴 → (∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0) →
(⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ ∧
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0))) |
| 53 | 41, 42, 52 | sylc 65 |
. . . . . . . . . 10
⊢ ((((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑘 ∈ ℕ) →
(⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ ∧
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0)) |
| 54 | 53 | simpld 494 |
. . . . . . . . 9
⊢ ((((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑘 ∈ ℕ) → ⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ) |
| 55 | 54 | ralrimiva 3146 |
. . . . . . . 8
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → ∀𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ) |
| 56 | | iunss 5045 |
. . . . . . . 8
⊢ (∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ ↔ ∀𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ) |
| 57 | 55, 56 | sylibr 234 |
. . . . . . 7
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ) |
| 58 | | eqid 2737 |
. . . . . . . . . 10
⊢ seq1( + ,
(𝑘 ∈ ℕ ↦
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵))) = seq1( + , (𝑘 ∈ ℕ ↦
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵))) |
| 59 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ ↦
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) = (𝑘 ∈ ℕ ↦
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
| 60 | 53 | simprd 495 |
. . . . . . . . . . 11
⊢ ((((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑘 ∈ ℕ) →
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0) |
| 61 | | 0re 11263 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
| 62 | 60, 61 | eqeltrdi 2849 |
. . . . . . . . . 10
⊢ ((((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑘 ∈ ℕ) →
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) ∈ ℝ) |
| 63 | 60 | mpteq2dva 5242 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → (𝑘 ∈ ℕ ↦
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) = (𝑘 ∈ ℕ ↦ 0)) |
| 64 | | fconstmpt 5747 |
. . . . . . . . . . . . . 14
⊢ (ℕ
× {0}) = (𝑘 ∈
ℕ ↦ 0) |
| 65 | | nnuz 12921 |
. . . . . . . . . . . . . . 15
⊢ ℕ =
(ℤ≥‘1) |
| 66 | 65 | xpeq1i 5711 |
. . . . . . . . . . . . . 14
⊢ (ℕ
× {0}) = ((ℤ≥‘1) × {0}) |
| 67 | 64, 66 | eqtr3i 2767 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ ↦ 0) =
((ℤ≥‘1) × {0}) |
| 68 | 63, 67 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → (𝑘 ∈ ℕ ↦
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) = ((ℤ≥‘1)
× {0})) |
| 69 | 68 | seqeq3d 14050 |
. . . . . . . . . . 11
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → seq1( + , (𝑘 ∈ ℕ ↦
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵))) = seq1( + ,
((ℤ≥‘1) × {0}))) |
| 70 | | 1z 12647 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
| 71 | | serclim0 15613 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℤ → seq1( + , ((ℤ≥‘1) × {0}))
⇝ 0) |
| 72 | | seqex 14044 |
. . . . . . . . . . . . 13
⊢ seq1( + ,
((ℤ≥‘1) × {0})) ∈ V |
| 73 | | c0ex 11255 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
| 74 | 72, 73 | breldm 5919 |
. . . . . . . . . . . 12
⊢ (seq1( +
, ((ℤ≥‘1) × {0})) ⇝ 0 → seq1( + ,
((ℤ≥‘1) × {0})) ∈ dom ⇝
) |
| 75 | 70, 71, 74 | mp2b 10 |
. . . . . . . . . . 11
⊢ seq1( + ,
((ℤ≥‘1) × {0})) ∈ dom
⇝ |
| 76 | 69, 75 | eqeltrdi 2849 |
. . . . . . . . . 10
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → seq1( + , (𝑘 ∈ ℕ ↦
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵))) ∈ dom ⇝ ) |
| 77 | 58, 59, 54, 62, 76 | ovoliun2 25541 |
. . . . . . . . 9
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) ≤ Σ𝑘 ∈ ℕ
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
| 78 | 60 | sumeq2dv 15738 |
. . . . . . . . . 10
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → Σ𝑘 ∈ ℕ
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = Σ𝑘 ∈ ℕ 0) |
| 79 | 65 | eqimssi 4044 |
. . . . . . . . . . . 12
⊢ ℕ
⊆ (ℤ≥‘1) |
| 80 | 79 | orci 866 |
. . . . . . . . . . 11
⊢ (ℕ
⊆ (ℤ≥‘1) ∨ ℕ ∈
Fin) |
| 81 | | sumz 15758 |
. . . . . . . . . . 11
⊢ ((ℕ
⊆ (ℤ≥‘1) ∨ ℕ ∈ Fin) →
Σ𝑘 ∈ ℕ 0 =
0) |
| 82 | 80, 81 | ax-mp 5 |
. . . . . . . . . 10
⊢
Σ𝑘 ∈
ℕ 0 = 0 |
| 83 | 78, 82 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → Σ𝑘 ∈ ℕ
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0) |
| 84 | 77, 83 | breqtrd 5169 |
. . . . . . . 8
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) ≤ 0) |
| 85 | | ovolge0 25516 |
. . . . . . . . 9
⊢ (∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ → 0 ≤
(vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
| 86 | 57, 85 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → 0 ≤ (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
| 87 | | ovolcl 25513 |
. . . . . . . . . 10
⊢ (∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ → (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) ∈
ℝ*) |
| 88 | 57, 87 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) ∈
ℝ*) |
| 89 | | 0xr 11308 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
| 90 | | xrletri3 13196 |
. . . . . . . . 9
⊢
(((vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) ∈ ℝ* ∧ 0 ∈
ℝ*) → ((vol*‘∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0 ↔ ((vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) ≤ 0 ∧ 0 ≤ (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵)))) |
| 91 | 88, 89, 90 | sylancl 586 |
. . . . . . . 8
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → ((vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0 ↔ ((vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) ≤ 0 ∧ 0 ≤ (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵)))) |
| 92 | 84, 86, 91 | mpbir2and 713 |
. . . . . . 7
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0) |
| 93 | | ovolssnul 25522 |
. . . . . . 7
⊢
((∪ 𝑛 ∈ 𝐴 𝐵 ⊆ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ∧ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ ∧ (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0) → (vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0) |
| 94 | 38, 57, 92, 93 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → (vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0) |
| 95 | 94 | ex 412 |
. . . . 5
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (𝑓:ℕ–onto→𝐴 → (vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0)) |
| 96 | 95 | exlimdv 1933 |
. . . 4
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (∃𝑓 𝑓:ℕ–onto→𝐴 → (vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0)) |
| 97 | 15, 96 | syld 47 |
. . 3
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (∅ ≺
𝐴 →
(vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0)) |
| 98 | 12, 97 | sylbird 260 |
. 2
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (𝐴 ≠ ∅ →
(vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0)) |
| 99 | 7, 98 | pm2.61dne 3028 |
1
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) →
(vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0) |