Step | Hyp | Ref
| Expression |
1 | | iuneq1 4920 |
. . . . . 6
⊢ (𝐴 = ∅ → ∪ 𝑛 ∈ 𝐴 𝐵 = ∪ 𝑛 ∈ ∅ 𝐵) |
2 | | 0iun 4971 |
. . . . . 6
⊢ ∪ 𝑛 ∈ ∅ 𝐵 = ∅ |
3 | 1, 2 | eqtrdi 2794 |
. . . . 5
⊢ (𝐴 = ∅ → ∪ 𝑛 ∈ 𝐴 𝐵 = ∅) |
4 | 3 | fveq2d 6721 |
. . . 4
⊢ (𝐴 = ∅ →
(vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = (vol*‘∅)) |
5 | | ovol0 24390 |
. . . 4
⊢
(vol*‘∅) = 0 |
6 | 4, 5 | eqtrdi 2794 |
. . 3
⊢ (𝐴 = ∅ →
(vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0) |
7 | 6 | a1i 11 |
. 2
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (𝐴 = ∅ →
(vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0)) |
8 | | reldom 8632 |
. . . . . 6
⊢ Rel
≼ |
9 | 8 | brrelex1i 5605 |
. . . . 5
⊢ (𝐴 ≼ ℕ → 𝐴 ∈ V) |
10 | 9 | adantr 484 |
. . . 4
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → 𝐴 ∈ V) |
11 | | 0sdomg 8775 |
. . . 4
⊢ (𝐴 ∈ V → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
12 | 10, 11 | syl 17 |
. . 3
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (∅ ≺
𝐴 ↔ 𝐴 ≠ ∅)) |
13 | | fodomr 8797 |
. . . . . 6
⊢ ((∅
≺ 𝐴 ∧ 𝐴 ≼ ℕ) →
∃𝑓 𝑓:ℕ–onto→𝐴) |
14 | 13 | expcom 417 |
. . . . 5
⊢ (𝐴 ≼ ℕ → (∅
≺ 𝐴 →
∃𝑓 𝑓:ℕ–onto→𝐴)) |
15 | 14 | adantr 484 |
. . . 4
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (∅ ≺
𝐴 → ∃𝑓 𝑓:ℕ–onto→𝐴)) |
16 | | eliun 4908 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝐴 𝐵 ↔ ∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵) |
17 | | nfv 1922 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛 𝑓:ℕ–onto→𝐴 |
18 | | nfcv 2904 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛ℕ |
19 | | nfcsb1v 3836 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛⦋(𝑓‘𝑘) / 𝑛⦌𝐵 |
20 | 18, 19 | nfiun 4934 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛∪ 𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵 |
21 | 20 | nfcri 2891 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛 𝑥 ∈ ∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵 |
22 | | foelrn 6925 |
. . . . . . . . . . . . 13
⊢ ((𝑓:ℕ–onto→𝐴 ∧ 𝑛 ∈ 𝐴) → ∃𝑘 ∈ ℕ 𝑛 = (𝑓‘𝑘)) |
23 | 22 | ex 416 |
. . . . . . . . . . . 12
⊢ (𝑓:ℕ–onto→𝐴 → (𝑛 ∈ 𝐴 → ∃𝑘 ∈ ℕ 𝑛 = (𝑓‘𝑘))) |
24 | | csbeq1a 3825 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = (𝑓‘𝑘) → 𝐵 = ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) |
25 | 24 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:ℕ–onto→𝐴 ∧ 𝑛 = (𝑓‘𝑘)) → 𝐵 = ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) |
26 | 25 | eleq2d 2823 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:ℕ–onto→𝐴 ∧ 𝑛 = (𝑓‘𝑘)) → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
27 | 26 | biimpd 232 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:ℕ–onto→𝐴 ∧ 𝑛 = (𝑓‘𝑘)) → (𝑥 ∈ 𝐵 → 𝑥 ∈ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
28 | 27 | impancom 455 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:ℕ–onto→𝐴 ∧ 𝑥 ∈ 𝐵) → (𝑛 = (𝑓‘𝑘) → 𝑥 ∈ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
29 | 28 | reximdv 3192 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:ℕ–onto→𝐴 ∧ 𝑥 ∈ 𝐵) → (∃𝑘 ∈ ℕ 𝑛 = (𝑓‘𝑘) → ∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
30 | | eliun 4908 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ↔ ∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) |
31 | 29, 30 | syl6ibr 255 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:ℕ–onto→𝐴 ∧ 𝑥 ∈ 𝐵) → (∃𝑘 ∈ ℕ 𝑛 = (𝑓‘𝑘) → 𝑥 ∈ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
32 | 31 | ex 416 |
. . . . . . . . . . . . 13
⊢ (𝑓:ℕ–onto→𝐴 → (𝑥 ∈ 𝐵 → (∃𝑘 ∈ ℕ 𝑛 = (𝑓‘𝑘) → 𝑥 ∈ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵))) |
33 | 32 | com23 86 |
. . . . . . . . . . . 12
⊢ (𝑓:ℕ–onto→𝐴 → (∃𝑘 ∈ ℕ 𝑛 = (𝑓‘𝑘) → (𝑥 ∈ 𝐵 → 𝑥 ∈ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵))) |
34 | 23, 33 | syld 47 |
. . . . . . . . . . 11
⊢ (𝑓:ℕ–onto→𝐴 → (𝑛 ∈ 𝐴 → (𝑥 ∈ 𝐵 → 𝑥 ∈ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵))) |
35 | 17, 21, 34 | rexlimd 3236 |
. . . . . . . . . 10
⊢ (𝑓:ℕ–onto→𝐴 → (∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵 → 𝑥 ∈ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
36 | 16, 35 | syl5bi 245 |
. . . . . . . . 9
⊢ (𝑓:ℕ–onto→𝐴 → (𝑥 ∈ ∪
𝑛 ∈ 𝐴 𝐵 → 𝑥 ∈ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
37 | 36 | ssrdv 3907 |
. . . . . . . 8
⊢ (𝑓:ℕ–onto→𝐴 → ∪
𝑛 ∈ 𝐴 𝐵 ⊆ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵) |
38 | 37 | adantl 485 |
. . . . . . 7
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → ∪
𝑛 ∈ 𝐴 𝐵 ⊆ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵) |
39 | | fof 6633 |
. . . . . . . . . . . . 13
⊢ (𝑓:ℕ–onto→𝐴 → 𝑓:ℕ⟶𝐴) |
40 | 39 | adantl 485 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → 𝑓:ℕ⟶𝐴) |
41 | 40 | ffvelrnda 6904 |
. . . . . . . . . . 11
⊢ ((((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) ∈ 𝐴) |
42 | | simpllr 776 |
. . . . . . . . . . 11
⊢ ((((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑘 ∈ ℕ) → ∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) |
43 | | nfcv 2904 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛ℝ |
44 | 19, 43 | nfss 3892 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ |
45 | | nfcv 2904 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛vol* |
46 | 45, 19 | nffv 6727 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) |
47 | 46 | nfeq1 2919 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0 |
48 | 44, 47 | nfan 1907 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ ∧
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0) |
49 | 24 | sseq1d 3932 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑓‘𝑘) → (𝐵 ⊆ ℝ ↔
⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ)) |
50 | 24 | fveqeq2d 6725 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑓‘𝑘) → ((vol*‘𝐵) = 0 ↔
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0)) |
51 | 49, 50 | anbi12d 634 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝑓‘𝑘) → ((𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0) ↔
(⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ ∧
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0))) |
52 | 48, 51 | rspc 3525 |
. . . . . . . . . . 11
⊢ ((𝑓‘𝑘) ∈ 𝐴 → (∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0) →
(⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ ∧
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0))) |
53 | 41, 42, 52 | sylc 65 |
. . . . . . . . . 10
⊢ ((((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑘 ∈ ℕ) →
(⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ ∧
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0)) |
54 | 53 | simpld 498 |
. . . . . . . . 9
⊢ ((((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑘 ∈ ℕ) → ⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ) |
55 | 54 | ralrimiva 3105 |
. . . . . . . 8
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → ∀𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ) |
56 | | iunss 4954 |
. . . . . . . 8
⊢ (∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ ↔ ∀𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ) |
57 | 55, 56 | sylibr 237 |
. . . . . . 7
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ) |
58 | | eqid 2737 |
. . . . . . . . . 10
⊢ seq1( + ,
(𝑘 ∈ ℕ ↦
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵))) = seq1( + , (𝑘 ∈ ℕ ↦
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵))) |
59 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ ↦
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) = (𝑘 ∈ ℕ ↦
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
60 | 53 | simprd 499 |
. . . . . . . . . . 11
⊢ ((((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑘 ∈ ℕ) →
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0) |
61 | | 0re 10835 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
62 | 60, 61 | eqeltrdi 2846 |
. . . . . . . . . 10
⊢ ((((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑘 ∈ ℕ) →
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) ∈ ℝ) |
63 | 60 | mpteq2dva 5150 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → (𝑘 ∈ ℕ ↦
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) = (𝑘 ∈ ℕ ↦ 0)) |
64 | | fconstmpt 5611 |
. . . . . . . . . . . . . 14
⊢ (ℕ
× {0}) = (𝑘 ∈
ℕ ↦ 0) |
65 | | nnuz 12477 |
. . . . . . . . . . . . . . 15
⊢ ℕ =
(ℤ≥‘1) |
66 | 65 | xpeq1i 5577 |
. . . . . . . . . . . . . 14
⊢ (ℕ
× {0}) = ((ℤ≥‘1) × {0}) |
67 | 64, 66 | eqtr3i 2767 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ ↦ 0) =
((ℤ≥‘1) × {0}) |
68 | 63, 67 | eqtrdi 2794 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → (𝑘 ∈ ℕ ↦
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) = ((ℤ≥‘1)
× {0})) |
69 | 68 | seqeq3d 13582 |
. . . . . . . . . . 11
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → seq1( + , (𝑘 ∈ ℕ ↦
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵))) = seq1( + ,
((ℤ≥‘1) × {0}))) |
70 | | 1z 12207 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
71 | | serclim0 15138 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℤ → seq1( + , ((ℤ≥‘1) × {0}))
⇝ 0) |
72 | | seqex 13576 |
. . . . . . . . . . . . 13
⊢ seq1( + ,
((ℤ≥‘1) × {0})) ∈ V |
73 | | c0ex 10827 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
74 | 72, 73 | breldm 5777 |
. . . . . . . . . . . 12
⊢ (seq1( +
, ((ℤ≥‘1) × {0})) ⇝ 0 → seq1( + ,
((ℤ≥‘1) × {0})) ∈ dom ⇝
) |
75 | 70, 71, 74 | mp2b 10 |
. . . . . . . . . . 11
⊢ seq1( + ,
((ℤ≥‘1) × {0})) ∈ dom
⇝ |
76 | 69, 75 | eqeltrdi 2846 |
. . . . . . . . . 10
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → seq1( + , (𝑘 ∈ ℕ ↦
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵))) ∈ dom ⇝ ) |
77 | 58, 59, 54, 62, 76 | ovoliun2 24403 |
. . . . . . . . 9
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) ≤ Σ𝑘 ∈ ℕ
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
78 | 60 | sumeq2dv 15267 |
. . . . . . . . . 10
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → Σ𝑘 ∈ ℕ
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = Σ𝑘 ∈ ℕ 0) |
79 | 65 | eqimssi 3959 |
. . . . . . . . . . . 12
⊢ ℕ
⊆ (ℤ≥‘1) |
80 | 79 | orci 865 |
. . . . . . . . . . 11
⊢ (ℕ
⊆ (ℤ≥‘1) ∨ ℕ ∈
Fin) |
81 | | sumz 15286 |
. . . . . . . . . . 11
⊢ ((ℕ
⊆ (ℤ≥‘1) ∨ ℕ ∈ Fin) →
Σ𝑘 ∈ ℕ 0 =
0) |
82 | 80, 81 | ax-mp 5 |
. . . . . . . . . 10
⊢
Σ𝑘 ∈
ℕ 0 = 0 |
83 | 78, 82 | eqtrdi 2794 |
. . . . . . . . 9
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → Σ𝑘 ∈ ℕ
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0) |
84 | 77, 83 | breqtrd 5079 |
. . . . . . . 8
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) ≤ 0) |
85 | | ovolge0 24378 |
. . . . . . . . 9
⊢ (∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ → 0 ≤
(vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
86 | 57, 85 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → 0 ≤ (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
87 | | ovolcl 24375 |
. . . . . . . . . 10
⊢ (∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ → (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) ∈
ℝ*) |
88 | 57, 87 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) ∈
ℝ*) |
89 | | 0xr 10880 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
90 | | xrletri3 12744 |
. . . . . . . . 9
⊢
(((vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) ∈ ℝ* ∧ 0 ∈
ℝ*) → ((vol*‘∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0 ↔ ((vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) ≤ 0 ∧ 0 ≤ (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵)))) |
91 | 88, 89, 90 | sylancl 589 |
. . . . . . . 8
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → ((vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0 ↔ ((vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) ≤ 0 ∧ 0 ≤ (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵)))) |
92 | 84, 86, 91 | mpbir2and 713 |
. . . . . . 7
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0) |
93 | | ovolssnul 24384 |
. . . . . . 7
⊢
((∪ 𝑛 ∈ 𝐴 𝐵 ⊆ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ∧ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ ∧ (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0) → (vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0) |
94 | 38, 57, 92, 93 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → (vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0) |
95 | 94 | ex 416 |
. . . . 5
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (𝑓:ℕ–onto→𝐴 → (vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0)) |
96 | 95 | exlimdv 1941 |
. . . 4
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (∃𝑓 𝑓:ℕ–onto→𝐴 → (vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0)) |
97 | 15, 96 | syld 47 |
. . 3
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (∅ ≺
𝐴 →
(vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0)) |
98 | 12, 97 | sylbird 263 |
. 2
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (𝐴 ≠ ∅ →
(vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0)) |
99 | 7, 98 | pm2.61dne 3028 |
1
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) →
(vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0) |