Step | Hyp | Ref
| Expression |
1 | | unieq 4850 |
. . . . . . . . 9
⊢ (𝐴 = ∅ → ∪ 𝐴 =
∪ ∅) |
2 | | uni0 4869 |
. . . . . . . . 9
⊢ ∪ ∅ = ∅ |
3 | 1, 2 | eqtrdi 2794 |
. . . . . . . 8
⊢ (𝐴 = ∅ → ∪ 𝐴 =
∅) |
4 | 3 | fveq2d 6770 |
. . . . . . 7
⊢ (𝐴 = ∅ →
(vol*‘∪ 𝐴) = (vol*‘∅)) |
5 | | ovol0 24667 |
. . . . . . 7
⊢
(vol*‘∅) = 0 |
6 | 4, 5 | eqtr2di 2795 |
. . . . . 6
⊢ (𝐴 = ∅ → 0 =
(vol*‘∪ 𝐴)) |
7 | 6 | a1d 25 |
. . . . 5
⊢ (𝐴 = ∅ → ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol*‘∪ 𝐴))) |
8 | | ovolge0 24655 |
. . . . . . . 8
⊢ (∪ 𝐴
⊆ ℝ → 0 ≤ (vol*‘∪ 𝐴)) |
9 | 8 | ad2antll 726 |
. . . . . . 7
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 ≤ (vol*‘∪ 𝐴)) |
10 | | reldom 8726 |
. . . . . . . . . . . 12
⊢ Rel
≼ |
11 | 10 | brrelex1i 5638 |
. . . . . . . . . . 11
⊢ (𝐴 ≼ ℕ → 𝐴 ∈ V) |
12 | | 0sdomg 8878 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
13 | 11, 12 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ≼ ℕ → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
14 | 13 | biimparc 480 |
. . . . . . . . 9
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∅
≺ 𝐴) |
15 | | fodomr 8902 |
. . . . . . . . 9
⊢ ((∅
≺ 𝐴 ∧ 𝐴 ≼ ℕ) →
∃𝑓 𝑓:ℕ–onto→𝐴) |
16 | 14, 15 | sylancom 588 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) →
∃𝑓 𝑓:ℕ–onto→𝐴) |
17 | | unissb 4873 |
. . . . . . . . . . . 12
⊢ (∪ 𝐴
⊆ ℝ ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ) |
18 | 17 | anbi1i 624 |
. . . . . . . . . . 11
⊢ ((∪ 𝐴
⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ)) |
19 | | r19.26 3095 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ)) |
20 | 18, 19 | bitr4i 277 |
. . . . . . . . . 10
⊢ ((∪ 𝐴
⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ)) |
21 | | brdom2 8757 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ≼ ℕ ↔ (𝑥 ≺ ℕ ∨ 𝑥 ≈
ℕ)) |
22 | | nnenom 13710 |
. . . . . . . . . . . . . . . . 17
⊢ ℕ
≈ ω |
23 | | sdomen2 8896 |
. . . . . . . . . . . . . . . . 17
⊢ (ℕ
≈ ω → (𝑥
≺ ℕ ↔ 𝑥
≺ ω)) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ≺ ℕ ↔ 𝑥 ≺
ω) |
25 | | isfinite 9397 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ Fin ↔ 𝑥 ≺
ω) |
26 | 24, 25 | bitr4i 277 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ≺ ℕ ↔ 𝑥 ∈ Fin) |
27 | 26 | orbi1i 911 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ≺ ℕ ∨ 𝑥 ≈ ℕ) ↔ (𝑥 ∈ Fin ∨ 𝑥 ≈
ℕ)) |
28 | 21, 27 | bitri 274 |
. . . . . . . . . . . . 13
⊢ (𝑥 ≼ ℕ ↔ (𝑥 ∈ Fin ∨ 𝑥 ≈
ℕ)) |
29 | | ovolfi 24668 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ Fin ∧ 𝑥 ⊆ ℝ) →
(vol*‘𝑥) =
0) |
30 | 29 | expcom 414 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ⊆ ℝ → (𝑥 ∈ Fin →
(vol*‘𝑥) =
0)) |
31 | | ovolctb 24664 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≈ ℕ) →
(vol*‘𝑥) =
0) |
32 | 31 | ex 413 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ⊆ ℝ → (𝑥 ≈ ℕ →
(vol*‘𝑥) =
0)) |
33 | 30, 32 | jaod 856 |
. . . . . . . . . . . . 13
⊢ (𝑥 ⊆ ℝ → ((𝑥 ∈ Fin ∨ 𝑥 ≈ ℕ) →
(vol*‘𝑥) =
0)) |
34 | 28, 33 | syl5bi 241 |
. . . . . . . . . . . 12
⊢ (𝑥 ⊆ ℝ → (𝑥 ≼ ℕ →
(vol*‘𝑥) =
0)) |
35 | 34 | imdistani 569 |
. . . . . . . . . . 11
⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) =
0)) |
36 | 35 | ralimi 3087 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)) |
37 | 20, 36 | sylbi 216 |
. . . . . . . . 9
⊢ ((∪ 𝐴
⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)) |
38 | 37 | ancoms 459 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)) |
39 | | foima 6685 |
. . . . . . . . . . . . 13
⊢ (𝑓:ℕ–onto→𝐴 → (𝑓 “ ℕ) = 𝐴) |
40 | 39 | raleqdv 3346 |
. . . . . . . . . . . 12
⊢ (𝑓:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑓 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))) |
41 | | fofn 6682 |
. . . . . . . . . . . . 13
⊢ (𝑓:ℕ–onto→𝐴 → 𝑓 Fn ℕ) |
42 | | ssid 3942 |
. . . . . . . . . . . . 13
⊢ ℕ
⊆ ℕ |
43 | | sseq1 3945 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑓‘𝑙) → (𝑥 ⊆ ℝ ↔ (𝑓‘𝑙) ⊆ ℝ)) |
44 | | fveqeq2 6775 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑓‘𝑙) → ((vol*‘𝑥) = 0 ↔ (vol*‘(𝑓‘𝑙)) = 0)) |
45 | 43, 44 | anbi12d 631 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑓‘𝑙) → ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0))) |
46 | 45 | ralima 7106 |
. . . . . . . . . . . . 13
⊢ ((𝑓 Fn ℕ ∧ ℕ
⊆ ℕ) → (∀𝑥 ∈ (𝑓 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑙 ∈ ℕ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0))) |
47 | 41, 42, 46 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝑓:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑓 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑙 ∈ ℕ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0))) |
48 | 40, 47 | bitr3d 280 |
. . . . . . . . . . 11
⊢ (𝑓:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑙 ∈ ℕ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0))) |
49 | | fveq2 6766 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 = 𝑛 → (𝑓‘𝑙) = (𝑓‘𝑛)) |
50 | 49 | sseq1d 3951 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = 𝑛 → ((𝑓‘𝑙) ⊆ ℝ ↔ (𝑓‘𝑛) ⊆ ℝ)) |
51 | | 2fveq3 6771 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 = 𝑛 → (vol*‘(𝑓‘𝑙)) = (vol*‘(𝑓‘𝑛))) |
52 | 51 | eqeq1d 2740 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = 𝑛 → ((vol*‘(𝑓‘𝑙)) = 0 ↔ (vol*‘(𝑓‘𝑛)) = 0)) |
53 | 50, 52 | anbi12d 631 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 = 𝑛 → (((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0) ↔ ((𝑓‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑛)) = 0))) |
54 | 53 | cbvralvw 3380 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) ↔ ∀𝑛 ∈ ℕ ((𝑓‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑛)) = 0)) |
55 | | 0re 10987 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℝ |
56 | | eleq1a 2834 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 ∈
ℝ → ((vol*‘(𝑓‘𝑛)) = 0 → (vol*‘(𝑓‘𝑛)) ∈ ℝ)) |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
((vol*‘(𝑓‘𝑛)) = 0 → (vol*‘(𝑓‘𝑛)) ∈ ℝ) |
58 | 57 | anim2i 617 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑛)) = 0) → ((𝑓‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑛)) ∈ ℝ)) |
59 | 58 | ralimi 3087 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑛 ∈
ℕ ((𝑓‘𝑛) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑛)) = 0) → ∀𝑛 ∈ ℕ ((𝑓‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑛)) ∈ ℝ)) |
60 | 54, 59 | sylbi 216 |
. . . . . . . . . . . . . 14
⊢
(∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) → ∀𝑛 ∈ ℕ ((𝑓‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑛)) ∈ ℝ)) |
61 | | ovoliunnfl.0 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 Fn ℕ ∧ ∀𝑛 ∈ ℕ ((𝑓‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑛)) ∈ ℝ)) →
(vol*‘∪ 𝑚 ∈ ℕ (𝑓‘𝑚)) ≤ sup(ran seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑓‘𝑚)))), ℝ*, <
)) |
62 | 41, 60, 61 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ ((𝑓:ℕ–onto→𝐴 ∧ ∀𝑙 ∈ ℕ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0)) → (vol*‘∪ 𝑚 ∈ ℕ (𝑓‘𝑚)) ≤ sup(ran seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑓‘𝑚)))), ℝ*, <
)) |
63 | | fofun 6681 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:ℕ–onto→𝐴 → Fun 𝑓) |
64 | | funiunfv 7113 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
𝑓 → ∪ 𝑚 ∈ ℕ (𝑓‘𝑚) = ∪ (𝑓 “
ℕ)) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:ℕ–onto→𝐴 → ∪
𝑚 ∈ ℕ (𝑓‘𝑚) = ∪ (𝑓 “
ℕ)) |
66 | 39 | unieqd 4853 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:ℕ–onto→𝐴 → ∪ (𝑓 “ ℕ) = ∪ 𝐴) |
67 | 65, 66 | eqtrd 2778 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:ℕ–onto→𝐴 → ∪
𝑚 ∈ ℕ (𝑓‘𝑚) = ∪ 𝐴) |
68 | 67 | fveq2d 6770 |
. . . . . . . . . . . . . 14
⊢ (𝑓:ℕ–onto→𝐴 → (vol*‘∪ 𝑚 ∈ ℕ (𝑓‘𝑚)) = (vol*‘∪
𝐴)) |
69 | 68 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑓:ℕ–onto→𝐴 ∧ ∀𝑙 ∈ ℕ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0)) → (vol*‘∪ 𝑚 ∈ ℕ (𝑓‘𝑚)) = (vol*‘∪
𝐴)) |
70 | | fveq2 6766 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑙 = 𝑚 → (𝑓‘𝑙) = (𝑓‘𝑚)) |
71 | 70 | sseq1d 3951 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑙 = 𝑚 → ((𝑓‘𝑙) ⊆ ℝ ↔ (𝑓‘𝑚) ⊆ ℝ)) |
72 | | 2fveq3 6771 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑙 = 𝑚 → (vol*‘(𝑓‘𝑙)) = (vol*‘(𝑓‘𝑚))) |
73 | 72 | eqeq1d 2740 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑙 = 𝑚 → ((vol*‘(𝑓‘𝑙)) = 0 ↔ (vol*‘(𝑓‘𝑚)) = 0)) |
74 | 71, 73 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 = 𝑚 → (((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0) ↔ ((𝑓‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑚)) = 0))) |
75 | 74 | rspccva 3558 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) ∧ 𝑚 ∈ ℕ) → ((𝑓‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑚)) = 0)) |
76 | 75 | simprd 496 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) ∧ 𝑚 ∈ ℕ) → (vol*‘(𝑓‘𝑚)) = 0) |
77 | 76 | mpteq2dva 5173 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) → (𝑚 ∈ ℕ ↦
(vol*‘(𝑓‘𝑚))) = (𝑚 ∈ ℕ ↦ 0)) |
78 | 77 | seqeq3d 13739 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) → seq1( + , (𝑚 ∈ ℕ ↦
(vol*‘(𝑓‘𝑚)))) = seq1( + , (𝑚 ∈ ℕ ↦
0))) |
79 | 78 | rneqd 5840 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) → ran seq1( + ,
(𝑚 ∈ ℕ ↦
(vol*‘(𝑓‘𝑚)))) = ran seq1( + , (𝑚 ∈ ℕ ↦
0))) |
80 | 79 | supeq1d 9192 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) → sup(ran seq1( + ,
(𝑚 ∈ ℕ ↦
(vol*‘(𝑓‘𝑚)))), ℝ*, <
) = sup(ran seq1( + , (𝑚
∈ ℕ ↦ 0)), ℝ*, < )) |
81 | | 0cn 10977 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
ℂ |
82 | | ser1const 13789 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((0
∈ ℂ ∧ 𝑙
∈ ℕ) → (seq1( + , (ℕ × {0}))‘𝑙) = (𝑙 · 0)) |
83 | 81, 82 | mpan 687 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑙 ∈ ℕ → (seq1( +
, (ℕ × {0}))‘𝑙) = (𝑙 · 0)) |
84 | | nncn 11991 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑙 ∈ ℕ → 𝑙 ∈
ℂ) |
85 | 84 | mul01d 11184 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑙 ∈ ℕ → (𝑙 · 0) =
0) |
86 | 83, 85 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 ∈ ℕ → (seq1( +
, (ℕ × {0}))‘𝑙) = 0) |
87 | 86 | mpteq2ia 5176 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 ∈ ℕ ↦ (seq1( +
, (ℕ × {0}))‘𝑙)) = (𝑙 ∈ ℕ ↦ 0) |
88 | | fconstmpt 5644 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℕ
× {0}) = (𝑚 ∈
ℕ ↦ 0) |
89 | | seqeq3 13736 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((ℕ
× {0}) = (𝑚 ∈
ℕ ↦ 0) → seq1( + , (ℕ × {0})) = seq1( + , (𝑚 ∈ ℕ ↦
0))) |
90 | 88, 89 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ seq1( + ,
(ℕ × {0})) = seq1( + , (𝑚 ∈ ℕ ↦ 0)) |
91 | | 1z 12360 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℤ |
92 | | seqfn 13743 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (1 ∈
ℤ → seq1( + , (ℕ × {0})) Fn
(ℤ≥‘1)) |
93 | 91, 92 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ seq1( + ,
(ℕ × {0})) Fn (ℤ≥‘1) |
94 | | nnuz 12631 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ℕ =
(ℤ≥‘1) |
95 | 94 | fneq2i 6523 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (seq1( +
, (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) Fn
(ℤ≥‘1)) |
96 | | dffn5 6820 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (seq1( +
, (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) =
(𝑙 ∈ ℕ ↦
(seq1( + , (ℕ × {0}))‘𝑙))) |
97 | 95, 96 | bitr3i 276 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (seq1( +
, (ℕ × {0})) Fn (ℤ≥‘1) ↔ seq1( + ,
(ℕ × {0})) = (𝑙
∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑙))) |
98 | 93, 97 | mpbi 229 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ seq1( + ,
(ℕ × {0})) = (𝑙
∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑙)) |
99 | 90, 98 | eqtr3i 2768 |
. . . . . . . . . . . . . . . . . . . 20
⊢ seq1( + ,
(𝑚 ∈ ℕ ↦
0)) = (𝑙 ∈ ℕ
↦ (seq1( + , (ℕ × {0}))‘𝑙)) |
100 | | fconstmpt 5644 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℕ
× {0}) = (𝑙 ∈
ℕ ↦ 0) |
101 | 87, 99, 100 | 3eqtr4i 2776 |
. . . . . . . . . . . . . . . . . . 19
⊢ seq1( + ,
(𝑚 ∈ ℕ ↦
0)) = (ℕ × {0}) |
102 | 101 | rneqi 5839 |
. . . . . . . . . . . . . . . . . 18
⊢ ran seq1(
+ , (𝑚 ∈ ℕ
↦ 0)) = ran (ℕ × {0}) |
103 | | 1nn 11994 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℕ |
104 | | ne0i 4268 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 ∈
ℕ → ℕ ≠ ∅) |
105 | | rnxp 6066 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℕ
≠ ∅ → ran (ℕ × {0}) = {0}) |
106 | 103, 104,
105 | mp2b 10 |
. . . . . . . . . . . . . . . . . 18
⊢ ran
(ℕ × {0}) = {0} |
107 | 102, 106 | eqtri 2766 |
. . . . . . . . . . . . . . . . 17
⊢ ran seq1(
+ , (𝑚 ∈ ℕ
↦ 0)) = {0} |
108 | 107 | supeq1i 9193 |
. . . . . . . . . . . . . . . 16
⊢ sup(ran
seq1( + , (𝑚 ∈ ℕ
↦ 0)), ℝ*, < ) = sup({0}, ℝ*, <
) |
109 | | xrltso 12885 |
. . . . . . . . . . . . . . . . 17
⊢ < Or
ℝ* |
110 | | 0xr 11032 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
ℝ* |
111 | | supsn 9218 |
. . . . . . . . . . . . . . . . 17
⊢ (( <
Or ℝ* ∧ 0 ∈ ℝ*) → sup({0},
ℝ*, < ) = 0) |
112 | 109, 110,
111 | mp2an 689 |
. . . . . . . . . . . . . . . 16
⊢ sup({0},
ℝ*, < ) = 0 |
113 | 108, 112 | eqtri 2766 |
. . . . . . . . . . . . . . 15
⊢ sup(ran
seq1( + , (𝑚 ∈ ℕ
↦ 0)), ℝ*, < ) = 0 |
114 | 80, 113 | eqtrdi 2794 |
. . . . . . . . . . . . . 14
⊢
(∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) → sup(ran seq1( + ,
(𝑚 ∈ ℕ ↦
(vol*‘(𝑓‘𝑚)))), ℝ*, <
) = 0) |
115 | 114 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑓:ℕ–onto→𝐴 ∧ ∀𝑙 ∈ ℕ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0)) → sup(ran seq1( + , (𝑚 ∈ ℕ ↦
(vol*‘(𝑓‘𝑚)))), ℝ*, <
) = 0) |
116 | 62, 69, 115 | 3brtr3d 5104 |
. . . . . . . . . . . 12
⊢ ((𝑓:ℕ–onto→𝐴 ∧ ∀𝑙 ∈ ℕ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0)) → (vol*‘∪ 𝐴)
≤ 0) |
117 | 116 | ex 413 |
. . . . . . . . . . 11
⊢ (𝑓:ℕ–onto→𝐴 → (∀𝑙 ∈ ℕ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0) → (vol*‘∪ 𝐴)
≤ 0)) |
118 | 48, 117 | sylbid 239 |
. . . . . . . . . 10
⊢ (𝑓:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → (vol*‘∪ 𝐴)
≤ 0)) |
119 | 118 | exlimiv 1933 |
. . . . . . . . 9
⊢
(∃𝑓 𝑓:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → (vol*‘∪ 𝐴)
≤ 0)) |
120 | 119 | imp 407 |
. . . . . . . 8
⊢
((∃𝑓 𝑓:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)) → (vol*‘∪ 𝐴)
≤ 0) |
121 | 16, 38, 120 | syl2an 596 |
. . . . . . 7
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → (vol*‘∪ 𝐴) ≤ 0) |
122 | | ovolcl 24652 |
. . . . . . . . 9
⊢ (∪ 𝐴
⊆ ℝ → (vol*‘∪ 𝐴) ∈
ℝ*) |
123 | | xrletri3 12898 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ (vol*‘∪ 𝐴) ∈ ℝ*)
→ (0 = (vol*‘∪ 𝐴) ↔ (0 ≤ (vol*‘∪ 𝐴)
∧ (vol*‘∪ 𝐴) ≤ 0))) |
124 | 110, 122,
123 | sylancr 587 |
. . . . . . . 8
⊢ (∪ 𝐴
⊆ ℝ → (0 = (vol*‘∪ 𝐴) ↔ (0 ≤
(vol*‘∪ 𝐴) ∧ (vol*‘∪ 𝐴)
≤ 0))) |
125 | 124 | ad2antll 726 |
. . . . . . 7
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → (0 = (vol*‘∪ 𝐴) ↔ (0 ≤
(vol*‘∪ 𝐴) ∧ (vol*‘∪ 𝐴)
≤ 0))) |
126 | 9, 121, 125 | mpbir2and 710 |
. . . . . 6
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol*‘∪ 𝐴)) |
127 | 126 | expl 458 |
. . . . 5
⊢ (𝐴 ≠ ∅ → ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol*‘∪ 𝐴))) |
128 | 7, 127 | pm2.61ine 3028 |
. . . 4
⊢ ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol*‘∪ 𝐴)) |
129 | | renepnf 11033 |
. . . . . . 7
⊢ (0 ∈
ℝ → 0 ≠ +∞) |
130 | 55, 129 | mp1i 13 |
. . . . . 6
⊢ (∪ 𝐴 =
ℝ → 0 ≠ +∞) |
131 | | fveq2 6766 |
. . . . . . 7
⊢ (∪ 𝐴 =
ℝ → (vol*‘∪ 𝐴) = (vol*‘ℝ)) |
132 | | ovolre 24699 |
. . . . . . 7
⊢
(vol*‘ℝ) = +∞ |
133 | 131, 132 | eqtrdi 2794 |
. . . . . 6
⊢ (∪ 𝐴 =
ℝ → (vol*‘∪ 𝐴) = +∞) |
134 | 130, 133 | neeqtrrd 3018 |
. . . . 5
⊢ (∪ 𝐴 =
ℝ → 0 ≠ (vol*‘∪ 𝐴)) |
135 | 134 | necon2i 2978 |
. . . 4
⊢ (0 =
(vol*‘∪ 𝐴) → ∪ 𝐴 ≠ ℝ) |
136 | 128, 135 | syl 17 |
. . 3
⊢ ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → ∪ 𝐴 ≠ ℝ) |
137 | 136 | expr 457 |
. 2
⊢ ((𝐴 ≼ ℕ ∧
∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → (∪ 𝐴
⊆ ℝ → ∪ 𝐴 ≠ ℝ)) |
138 | | eqimss 3976 |
. . 3
⊢ (∪ 𝐴 =
ℝ → ∪ 𝐴 ⊆ ℝ) |
139 | 138 | necon3bi 2970 |
. 2
⊢ (¬
∪ 𝐴 ⊆ ℝ → ∪ 𝐴
≠ ℝ) |
140 | 137, 139 | pm2.61d1 180 |
1
⊢ ((𝐴 ≼ ℕ ∧
∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴
≠ ℝ) |