Step | Hyp | Ref
| Expression |
1 | | iuneq1 4470 |
. . . . . 6
⊢ (𝐴 = ∅ → ∪ 𝑛 ∈ 𝐴 𝐵 = ∪ 𝑛 ∈ ∅ 𝐵) |
2 | | 0iun 4513 |
. . . . . 6
⊢ ∪ 𝑛 ∈ ∅ 𝐵 = ∅ |
3 | 1, 2 | syl6eq 2660 |
. . . . 5
⊢ (𝐴 = ∅ → ∪ 𝑛 ∈ 𝐴 𝐵 = ∅) |
4 | 3 | fveq2d 6107 |
. . . 4
⊢ (𝐴 = ∅ →
(vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = (vol*‘∅)) |
5 | | ovol0 23068 |
. . . 4
⊢
(vol*‘∅) = 0 |
6 | 4, 5 | syl6eq 2660 |
. . 3
⊢ (𝐴 = ∅ →
(vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0) |
7 | 6 | a1i 11 |
. 2
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (𝐴 = ∅ →
(vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0)) |
8 | | reldom 7847 |
. . . . . 6
⊢ Rel
≼ |
9 | 8 | brrelexi 5082 |
. . . . 5
⊢ (𝐴 ≼ ℕ → 𝐴 ∈ V) |
10 | 9 | adantr 480 |
. . . 4
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → 𝐴 ∈ V) |
11 | | 0sdomg 7974 |
. . . 4
⊢ (𝐴 ∈ V → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
12 | 10, 11 | syl 17 |
. . 3
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (∅ ≺
𝐴 ↔ 𝐴 ≠ ∅)) |
13 | | fodomr 7996 |
. . . . . 6
⊢ ((∅
≺ 𝐴 ∧ 𝐴 ≼ ℕ) →
∃𝑓 𝑓:ℕ–onto→𝐴) |
14 | 13 | expcom 450 |
. . . . 5
⊢ (𝐴 ≼ ℕ → (∅
≺ 𝐴 →
∃𝑓 𝑓:ℕ–onto→𝐴)) |
15 | 14 | adantr 480 |
. . . 4
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (∅ ≺
𝐴 → ∃𝑓 𝑓:ℕ–onto→𝐴)) |
16 | | eliun 4460 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝐴 𝐵 ↔ ∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵) |
17 | | nfv 1830 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛 𝑓:ℕ–onto→𝐴 |
18 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛ℕ |
19 | | nfcsb1v 3515 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛⦋(𝑓‘𝑘) / 𝑛⦌𝐵 |
20 | 18, 19 | nfiun 4484 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛∪ 𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵 |
21 | 20 | nfcri 2745 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛 𝑥 ∈ ∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵 |
22 | | foelrn 6286 |
. . . . . . . . . . . . 13
⊢ ((𝑓:ℕ–onto→𝐴 ∧ 𝑛 ∈ 𝐴) → ∃𝑘 ∈ ℕ 𝑛 = (𝑓‘𝑘)) |
23 | 22 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝑓:ℕ–onto→𝐴 → (𝑛 ∈ 𝐴 → ∃𝑘 ∈ ℕ 𝑛 = (𝑓‘𝑘))) |
24 | | csbeq1a 3508 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = (𝑓‘𝑘) → 𝐵 = ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) |
25 | 24 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:ℕ–onto→𝐴 ∧ 𝑛 = (𝑓‘𝑘)) → 𝐵 = ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) |
26 | 25 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:ℕ–onto→𝐴 ∧ 𝑛 = (𝑓‘𝑘)) → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
27 | 26 | biimpd 218 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:ℕ–onto→𝐴 ∧ 𝑛 = (𝑓‘𝑘)) → (𝑥 ∈ 𝐵 → 𝑥 ∈ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
28 | 27 | impancom 455 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:ℕ–onto→𝐴 ∧ 𝑥 ∈ 𝐵) → (𝑛 = (𝑓‘𝑘) → 𝑥 ∈ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
29 | 28 | reximdv 2999 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:ℕ–onto→𝐴 ∧ 𝑥 ∈ 𝐵) → (∃𝑘 ∈ ℕ 𝑛 = (𝑓‘𝑘) → ∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
30 | | eliun 4460 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ↔ ∃𝑘 ∈ ℕ 𝑥 ∈ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) |
31 | 29, 30 | syl6ibr 241 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:ℕ–onto→𝐴 ∧ 𝑥 ∈ 𝐵) → (∃𝑘 ∈ ℕ 𝑛 = (𝑓‘𝑘) → 𝑥 ∈ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
32 | 31 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝑓:ℕ–onto→𝐴 → (𝑥 ∈ 𝐵 → (∃𝑘 ∈ ℕ 𝑛 = (𝑓‘𝑘) → 𝑥 ∈ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵))) |
33 | 32 | com23 84 |
. . . . . . . . . . . 12
⊢ (𝑓:ℕ–onto→𝐴 → (∃𝑘 ∈ ℕ 𝑛 = (𝑓‘𝑘) → (𝑥 ∈ 𝐵 → 𝑥 ∈ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵))) |
34 | 23, 33 | syld 46 |
. . . . . . . . . . 11
⊢ (𝑓:ℕ–onto→𝐴 → (𝑛 ∈ 𝐴 → (𝑥 ∈ 𝐵 → 𝑥 ∈ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵))) |
35 | 17, 21, 34 | rexlimd 3008 |
. . . . . . . . . 10
⊢ (𝑓:ℕ–onto→𝐴 → (∃𝑛 ∈ 𝐴 𝑥 ∈ 𝐵 → 𝑥 ∈ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
36 | 16, 35 | syl5bi 231 |
. . . . . . . . 9
⊢ (𝑓:ℕ–onto→𝐴 → (𝑥 ∈ ∪
𝑛 ∈ 𝐴 𝐵 → 𝑥 ∈ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
37 | 36 | ssrdv 3574 |
. . . . . . . 8
⊢ (𝑓:ℕ–onto→𝐴 → ∪
𝑛 ∈ 𝐴 𝐵 ⊆ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵) |
38 | 37 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → ∪
𝑛 ∈ 𝐴 𝐵 ⊆ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵) |
39 | | fof 6028 |
. . . . . . . . . . . . 13
⊢ (𝑓:ℕ–onto→𝐴 → 𝑓:ℕ⟶𝐴) |
40 | 39 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → 𝑓:ℕ⟶𝐴) |
41 | 40 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ ((((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) ∈ 𝐴) |
42 | | simpllr 795 |
. . . . . . . . . . 11
⊢ ((((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑘 ∈ ℕ) → ∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) |
43 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛ℝ |
44 | 19, 43 | nfss 3561 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ |
45 | | nfcv 2751 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛vol* |
46 | 45, 19 | nffv 6110 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) |
47 | 46 | nfeq1 2764 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0 |
48 | 44, 47 | nfan 1816 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ ∧
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0) |
49 | 24 | sseq1d 3595 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑓‘𝑘) → (𝐵 ⊆ ℝ ↔
⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ)) |
50 | 24 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑓‘𝑘) → (vol*‘𝐵) = (vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
51 | 50 | eqeq1d 2612 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑓‘𝑘) → ((vol*‘𝐵) = 0 ↔
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0)) |
52 | 49, 51 | anbi12d 743 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝑓‘𝑘) → ((𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0) ↔
(⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ ∧
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0))) |
53 | 48, 52 | rspc 3276 |
. . . . . . . . . . 11
⊢ ((𝑓‘𝑘) ∈ 𝐴 → (∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0) →
(⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ ∧
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0))) |
54 | 41, 42, 53 | sylc 63 |
. . . . . . . . . 10
⊢ ((((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑘 ∈ ℕ) →
(⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ ∧
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0)) |
55 | 54 | simpld 474 |
. . . . . . . . 9
⊢ ((((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑘 ∈ ℕ) → ⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ) |
56 | 55 | ralrimiva 2949 |
. . . . . . . 8
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → ∀𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ) |
57 | | iunss 4497 |
. . . . . . . 8
⊢ (∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ ↔ ∀𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ) |
58 | 56, 57 | sylibr 223 |
. . . . . . 7
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ) |
59 | | eqid 2610 |
. . . . . . . . . 10
⊢ seq1( + ,
(𝑘 ∈ ℕ ↦
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵))) = seq1( + , (𝑘 ∈ ℕ ↦
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵))) |
60 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ ↦
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) = (𝑘 ∈ ℕ ↦
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
61 | 54 | simprd 478 |
. . . . . . . . . . 11
⊢ ((((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑘 ∈ ℕ) →
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0) |
62 | | 0re 9919 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
63 | 61, 62 | syl6eqel 2696 |
. . . . . . . . . 10
⊢ ((((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑘 ∈ ℕ) →
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) ∈ ℝ) |
64 | 61 | mpteq2dva 4672 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → (𝑘 ∈ ℕ ↦
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) = (𝑘 ∈ ℕ ↦ 0)) |
65 | | fconstmpt 5085 |
. . . . . . . . . . . . . 14
⊢ (ℕ
× {0}) = (𝑘 ∈
ℕ ↦ 0) |
66 | | nnuz 11599 |
. . . . . . . . . . . . . . 15
⊢ ℕ =
(ℤ≥‘1) |
67 | 66 | xpeq1i 5059 |
. . . . . . . . . . . . . 14
⊢ (ℕ
× {0}) = ((ℤ≥‘1) × {0}) |
68 | 65, 67 | eqtr3i 2634 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ ↦ 0) =
((ℤ≥‘1) × {0}) |
69 | 64, 68 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → (𝑘 ∈ ℕ ↦
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) = ((ℤ≥‘1)
× {0})) |
70 | 69 | seqeq3d 12671 |
. . . . . . . . . . 11
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → seq1( + , (𝑘 ∈ ℕ ↦
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵))) = seq1( + ,
((ℤ≥‘1) × {0}))) |
71 | | 1z 11284 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
72 | | serclim0 14156 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℤ → seq1( + , ((ℤ≥‘1) × {0}))
⇝ 0) |
73 | | seqex 12665 |
. . . . . . . . . . . . 13
⊢ seq1( + ,
((ℤ≥‘1) × {0})) ∈ V |
74 | | c0ex 9913 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
75 | 73, 74 | breldm 5251 |
. . . . . . . . . . . 12
⊢ (seq1( +
, ((ℤ≥‘1) × {0})) ⇝ 0 → seq1( + ,
((ℤ≥‘1) × {0})) ∈ dom ⇝
) |
76 | 71, 72, 75 | mp2b 10 |
. . . . . . . . . . 11
⊢ seq1( + ,
((ℤ≥‘1) × {0})) ∈ dom
⇝ |
77 | 70, 76 | syl6eqel 2696 |
. . . . . . . . . 10
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → seq1( + , (𝑘 ∈ ℕ ↦
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵))) ∈ dom ⇝ ) |
78 | 59, 60, 55, 63, 77 | ovoliun2 23081 |
. . . . . . . . 9
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) ≤ Σ𝑘 ∈ ℕ
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
79 | 61 | sumeq2dv 14281 |
. . . . . . . . . 10
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → Σ𝑘 ∈ ℕ
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = Σ𝑘 ∈ ℕ 0) |
80 | 66 | eqimssi 3622 |
. . . . . . . . . . . 12
⊢ ℕ
⊆ (ℤ≥‘1) |
81 | 80 | orci 404 |
. . . . . . . . . . 11
⊢ (ℕ
⊆ (ℤ≥‘1) ∨ ℕ ∈
Fin) |
82 | | sumz 14300 |
. . . . . . . . . . 11
⊢ ((ℕ
⊆ (ℤ≥‘1) ∨ ℕ ∈ Fin) →
Σ𝑘 ∈ ℕ 0 =
0) |
83 | 81, 82 | ax-mp 5 |
. . . . . . . . . 10
⊢
Σ𝑘 ∈
ℕ 0 = 0 |
84 | 79, 83 | syl6eq 2660 |
. . . . . . . . 9
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → Σ𝑘 ∈ ℕ
(vol*‘⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0) |
85 | 78, 84 | breqtrd 4609 |
. . . . . . . 8
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) ≤ 0) |
86 | | ovolge0 23056 |
. . . . . . . . 9
⊢ (∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ → 0 ≤
(vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
87 | 58, 86 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → 0 ≤ (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵)) |
88 | | ovolcl 23053 |
. . . . . . . . . 10
⊢ (∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ → (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) ∈
ℝ*) |
89 | 58, 88 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) ∈
ℝ*) |
90 | | 0xr 9965 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
91 | | xrletri3 11861 |
. . . . . . . . 9
⊢
(((vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) ∈ ℝ* ∧ 0 ∈
ℝ*) → ((vol*‘∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0 ↔ ((vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) ≤ 0 ∧ 0 ≤ (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵)))) |
92 | 89, 90, 91 | sylancl 693 |
. . . . . . . 8
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → ((vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0 ↔ ((vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) ≤ 0 ∧ 0 ≤ (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵)))) |
93 | 85, 87, 92 | mpbir2and 959 |
. . . . . . 7
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0) |
94 | | ovolssnul 23062 |
. . . . . . 7
⊢
((∪ 𝑛 ∈ 𝐴 𝐵 ⊆ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ∧ ∪
𝑘 ∈ ℕ
⦋(𝑓‘𝑘) / 𝑛⦌𝐵 ⊆ ℝ ∧ (vol*‘∪ 𝑘 ∈ ℕ ⦋(𝑓‘𝑘) / 𝑛⦌𝐵) = 0) → (vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0) |
95 | 38, 58, 93, 94 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) ∧ 𝑓:ℕ–onto→𝐴) → (vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0) |
96 | 95 | ex 449 |
. . . . 5
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (𝑓:ℕ–onto→𝐴 → (vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0)) |
97 | 96 | exlimdv 1848 |
. . . 4
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (∃𝑓 𝑓:ℕ–onto→𝐴 → (vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0)) |
98 | 15, 97 | syld 46 |
. . 3
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (∅ ≺
𝐴 →
(vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0)) |
99 | 12, 98 | sylbird 249 |
. 2
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (𝐴 ≠ ∅ →
(vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0)) |
100 | 7, 99 | pm2.61dne 2868 |
1
⊢ ((𝐴 ≼ ℕ ∧
∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) →
(vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0) |