Step | Hyp | Ref
| Expression |
1 | | unieq 4444 |
. . . . . . . . 9
⊢ (𝐴 = ∅ → ∪ 𝐴 =
∪ ∅) |
2 | | uni0 4465 |
. . . . . . . . 9
⊢ ∪ ∅ = ∅ |
3 | 1, 2 | syl6eq 2672 |
. . . . . . . 8
⊢ (𝐴 = ∅ → ∪ 𝐴 =
∅) |
4 | 3 | fveq2d 6195 |
. . . . . . 7
⊢ (𝐴 = ∅ →
(vol*‘∪ 𝐴) = (vol*‘∅)) |
5 | | ovol0 23261 |
. . . . . . 7
⊢
(vol*‘∅) = 0 |
6 | 4, 5 | syl6req 2673 |
. . . . . 6
⊢ (𝐴 = ∅ → 0 =
(vol*‘∪ 𝐴)) |
7 | 6 | a1d 25 |
. . . . 5
⊢ (𝐴 = ∅ → ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol*‘∪ 𝐴))) |
8 | | ovolge0 23249 |
. . . . . . . 8
⊢ (∪ 𝐴
⊆ ℝ → 0 ≤ (vol*‘∪ 𝐴)) |
9 | 8 | ad2antll 765 |
. . . . . . 7
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 ≤ (vol*‘∪ 𝐴)) |
10 | | reldom 7961 |
. . . . . . . . . . . 12
⊢ Rel
≼ |
11 | 10 | brrelexi 5158 |
. . . . . . . . . . 11
⊢ (𝐴 ≼ ℕ → 𝐴 ∈ V) |
12 | | 0sdomg 8089 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
13 | 11, 12 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ≼ ℕ → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
14 | 13 | biimparc 504 |
. . . . . . . . 9
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∅
≺ 𝐴) |
15 | | fodomr 8111 |
. . . . . . . . 9
⊢ ((∅
≺ 𝐴 ∧ 𝐴 ≼ ℕ) →
∃𝑓 𝑓:ℕ–onto→𝐴) |
16 | 14, 15 | sylancom 701 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) →
∃𝑓 𝑓:ℕ–onto→𝐴) |
17 | | unissb 4469 |
. . . . . . . . . . . 12
⊢ (∪ 𝐴
⊆ ℝ ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ) |
18 | 17 | anbi1i 731 |
. . . . . . . . . . 11
⊢ ((∪ 𝐴
⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ)) |
19 | | r19.26 3064 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ)) |
20 | 18, 19 | bitr4i 267 |
. . . . . . . . . 10
⊢ ((∪ 𝐴
⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ)) |
21 | | brdom2 7985 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ≼ ℕ ↔ (𝑥 ≺ ℕ ∨ 𝑥 ≈
ℕ)) |
22 | | nnenom 12779 |
. . . . . . . . . . . . . . . . 17
⊢ ℕ
≈ ω |
23 | | sdomen2 8105 |
. . . . . . . . . . . . . . . . 17
⊢ (ℕ
≈ ω → (𝑥
≺ ℕ ↔ 𝑥
≺ ω)) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ≺ ℕ ↔ 𝑥 ≺
ω) |
25 | | isfinite 8549 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ Fin ↔ 𝑥 ≺
ω) |
26 | 24, 25 | bitr4i 267 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ≺ ℕ ↔ 𝑥 ∈ Fin) |
27 | 26 | orbi1i 542 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ≺ ℕ ∨ 𝑥 ≈ ℕ) ↔ (𝑥 ∈ Fin ∨ 𝑥 ≈
ℕ)) |
28 | 21, 27 | bitri 264 |
. . . . . . . . . . . . 13
⊢ (𝑥 ≼ ℕ ↔ (𝑥 ∈ Fin ∨ 𝑥 ≈
ℕ)) |
29 | | ovolfi 23262 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ Fin ∧ 𝑥 ⊆ ℝ) →
(vol*‘𝑥) =
0) |
30 | 29 | expcom 451 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ⊆ ℝ → (𝑥 ∈ Fin →
(vol*‘𝑥) =
0)) |
31 | | ovolctb 23258 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≈ ℕ) →
(vol*‘𝑥) =
0) |
32 | 31 | ex 450 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ⊆ ℝ → (𝑥 ≈ ℕ →
(vol*‘𝑥) =
0)) |
33 | 30, 32 | jaod 395 |
. . . . . . . . . . . . 13
⊢ (𝑥 ⊆ ℝ → ((𝑥 ∈ Fin ∨ 𝑥 ≈ ℕ) →
(vol*‘𝑥) =
0)) |
34 | 28, 33 | syl5bi 232 |
. . . . . . . . . . . 12
⊢ (𝑥 ⊆ ℝ → (𝑥 ≼ ℕ →
(vol*‘𝑥) =
0)) |
35 | 34 | imdistani 726 |
. . . . . . . . . . 11
⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) =
0)) |
36 | 35 | ralimi 2952 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)) |
37 | 20, 36 | sylbi 207 |
. . . . . . . . 9
⊢ ((∪ 𝐴
⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)) |
38 | 37 | ancoms 469 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)) |
39 | | foima 6120 |
. . . . . . . . . . . . 13
⊢ (𝑓:ℕ–onto→𝐴 → (𝑓 “ ℕ) = 𝐴) |
40 | 39 | raleqdv 3144 |
. . . . . . . . . . . 12
⊢ (𝑓:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑓 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))) |
41 | | fofn 6117 |
. . . . . . . . . . . . 13
⊢ (𝑓:ℕ–onto→𝐴 → 𝑓 Fn ℕ) |
42 | | ssid 3624 |
. . . . . . . . . . . . 13
⊢ ℕ
⊆ ℕ |
43 | | sseq1 3626 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑓‘𝑙) → (𝑥 ⊆ ℝ ↔ (𝑓‘𝑙) ⊆ ℝ)) |
44 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑓‘𝑙) → (vol*‘𝑥) = (vol*‘(𝑓‘𝑙))) |
45 | 44 | eqeq1d 2624 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑓‘𝑙) → ((vol*‘𝑥) = 0 ↔ (vol*‘(𝑓‘𝑙)) = 0)) |
46 | 43, 45 | anbi12d 747 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑓‘𝑙) → ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0))) |
47 | 46 | ralima 6498 |
. . . . . . . . . . . . 13
⊢ ((𝑓 Fn ℕ ∧ ℕ
⊆ ℕ) → (∀𝑥 ∈ (𝑓 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑙 ∈ ℕ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0))) |
48 | 41, 42, 47 | sylancl 694 |
. . . . . . . . . . . 12
⊢ (𝑓:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑓 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑙 ∈ ℕ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0))) |
49 | 40, 48 | bitr3d 270 |
. . . . . . . . . . 11
⊢ (𝑓:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑙 ∈ ℕ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0))) |
50 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 = 𝑛 → (𝑓‘𝑙) = (𝑓‘𝑛)) |
51 | 50 | sseq1d 3632 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = 𝑛 → ((𝑓‘𝑙) ⊆ ℝ ↔ (𝑓‘𝑛) ⊆ ℝ)) |
52 | 50 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 = 𝑛 → (vol*‘(𝑓‘𝑙)) = (vol*‘(𝑓‘𝑛))) |
53 | 52 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = 𝑛 → ((vol*‘(𝑓‘𝑙)) = 0 ↔ (vol*‘(𝑓‘𝑛)) = 0)) |
54 | 51, 53 | anbi12d 747 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 = 𝑛 → (((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0) ↔ ((𝑓‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑛)) = 0))) |
55 | 54 | cbvralv 3171 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) ↔ ∀𝑛 ∈ ℕ ((𝑓‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑛)) = 0)) |
56 | | 0re 10040 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℝ |
57 | | eleq1a 2696 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 ∈
ℝ → ((vol*‘(𝑓‘𝑛)) = 0 → (vol*‘(𝑓‘𝑛)) ∈ ℝ)) |
58 | 56, 57 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
((vol*‘(𝑓‘𝑛)) = 0 → (vol*‘(𝑓‘𝑛)) ∈ ℝ) |
59 | 58 | anim2i 593 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑛)) = 0) → ((𝑓‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑛)) ∈ ℝ)) |
60 | 59 | ralimi 2952 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑛 ∈
ℕ ((𝑓‘𝑛) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑛)) = 0) → ∀𝑛 ∈ ℕ ((𝑓‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑛)) ∈ ℝ)) |
61 | 55, 60 | sylbi 207 |
. . . . . . . . . . . . . 14
⊢
(∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) → ∀𝑛 ∈ ℕ ((𝑓‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑛)) ∈ ℝ)) |
62 | | ovoliunnfl.0 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 Fn ℕ ∧ ∀𝑛 ∈ ℕ ((𝑓‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑛)) ∈ ℝ)) →
(vol*‘∪ 𝑚 ∈ ℕ (𝑓‘𝑚)) ≤ sup(ran seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑓‘𝑚)))), ℝ*, <
)) |
63 | 41, 61, 62 | syl2an 494 |
. . . . . . . . . . . . 13
⊢ ((𝑓:ℕ–onto→𝐴 ∧ ∀𝑙 ∈ ℕ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0)) → (vol*‘∪ 𝑚 ∈ ℕ (𝑓‘𝑚)) ≤ sup(ran seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑓‘𝑚)))), ℝ*, <
)) |
64 | | fofun 6116 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:ℕ–onto→𝐴 → Fun 𝑓) |
65 | | funiunfv 6506 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
𝑓 → ∪ 𝑚 ∈ ℕ (𝑓‘𝑚) = ∪ (𝑓 “
ℕ)) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:ℕ–onto→𝐴 → ∪
𝑚 ∈ ℕ (𝑓‘𝑚) = ∪ (𝑓 “
ℕ)) |
67 | 39 | unieqd 4446 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:ℕ–onto→𝐴 → ∪ (𝑓 “ ℕ) = ∪ 𝐴) |
68 | 66, 67 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:ℕ–onto→𝐴 → ∪
𝑚 ∈ ℕ (𝑓‘𝑚) = ∪ 𝐴) |
69 | 68 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑓:ℕ–onto→𝐴 → (vol*‘∪ 𝑚 ∈ ℕ (𝑓‘𝑚)) = (vol*‘∪
𝐴)) |
70 | 69 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑓:ℕ–onto→𝐴 ∧ ∀𝑙 ∈ ℕ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0)) → (vol*‘∪ 𝑚 ∈ ℕ (𝑓‘𝑚)) = (vol*‘∪
𝐴)) |
71 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑙 = 𝑚 → (𝑓‘𝑙) = (𝑓‘𝑚)) |
72 | 71 | sseq1d 3632 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑙 = 𝑚 → ((𝑓‘𝑙) ⊆ ℝ ↔ (𝑓‘𝑚) ⊆ ℝ)) |
73 | 71 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑙 = 𝑚 → (vol*‘(𝑓‘𝑙)) = (vol*‘(𝑓‘𝑚))) |
74 | 73 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑙 = 𝑚 → ((vol*‘(𝑓‘𝑙)) = 0 ↔ (vol*‘(𝑓‘𝑚)) = 0)) |
75 | 72, 74 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 = 𝑚 → (((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0) ↔ ((𝑓‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑚)) = 0))) |
76 | 75 | rspccva 3308 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) ∧ 𝑚 ∈ ℕ) → ((𝑓‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑚)) = 0)) |
77 | 76 | simprd 479 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) ∧ 𝑚 ∈ ℕ) → (vol*‘(𝑓‘𝑚)) = 0) |
78 | 77 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) → (𝑚 ∈ ℕ ↦
(vol*‘(𝑓‘𝑚))) = (𝑚 ∈ ℕ ↦ 0)) |
79 | 78 | seqeq3d 12809 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) → seq1( + , (𝑚 ∈ ℕ ↦
(vol*‘(𝑓‘𝑚)))) = seq1( + , (𝑚 ∈ ℕ ↦
0))) |
80 | 79 | rneqd 5353 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) → ran seq1( + ,
(𝑚 ∈ ℕ ↦
(vol*‘(𝑓‘𝑚)))) = ran seq1( + , (𝑚 ∈ ℕ ↦
0))) |
81 | 80 | supeq1d 8352 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) → sup(ran seq1( + ,
(𝑚 ∈ ℕ ↦
(vol*‘(𝑓‘𝑚)))), ℝ*, <
) = sup(ran seq1( + , (𝑚
∈ ℕ ↦ 0)), ℝ*, < )) |
82 | | 0cn 10032 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
ℂ |
83 | | ser1const 12857 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((0
∈ ℂ ∧ 𝑙
∈ ℕ) → (seq1( + , (ℕ × {0}))‘𝑙) = (𝑙 · 0)) |
84 | 82, 83 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑙 ∈ ℕ → (seq1( +
, (ℕ × {0}))‘𝑙) = (𝑙 · 0)) |
85 | | nncn 11028 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑙 ∈ ℕ → 𝑙 ∈
ℂ) |
86 | 85 | mul01d 10235 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑙 ∈ ℕ → (𝑙 · 0) =
0) |
87 | 84, 86 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 ∈ ℕ → (seq1( +
, (ℕ × {0}))‘𝑙) = 0) |
88 | 87 | mpteq2ia 4740 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 ∈ ℕ ↦ (seq1( +
, (ℕ × {0}))‘𝑙)) = (𝑙 ∈ ℕ ↦ 0) |
89 | | fconstmpt 5163 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℕ
× {0}) = (𝑚 ∈
ℕ ↦ 0) |
90 | | seqeq3 12806 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((ℕ
× {0}) = (𝑚 ∈
ℕ ↦ 0) → seq1( + , (ℕ × {0})) = seq1( + , (𝑚 ∈ ℕ ↦
0))) |
91 | 89, 90 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ seq1( + ,
(ℕ × {0})) = seq1( + , (𝑚 ∈ ℕ ↦ 0)) |
92 | | 1z 11407 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℤ |
93 | | seqfn 12813 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (1 ∈
ℤ → seq1( + , (ℕ × {0})) Fn
(ℤ≥‘1)) |
94 | 92, 93 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ seq1( + ,
(ℕ × {0})) Fn (ℤ≥‘1) |
95 | | nnuz 11723 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ℕ =
(ℤ≥‘1) |
96 | 95 | fneq2i 5986 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (seq1( +
, (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) Fn
(ℤ≥‘1)) |
97 | | dffn5 6241 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (seq1( +
, (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) =
(𝑙 ∈ ℕ ↦
(seq1( + , (ℕ × {0}))‘𝑙))) |
98 | 96, 97 | bitr3i 266 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (seq1( +
, (ℕ × {0})) Fn (ℤ≥‘1) ↔ seq1( + ,
(ℕ × {0})) = (𝑙
∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑙))) |
99 | 94, 98 | mpbi 220 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ seq1( + ,
(ℕ × {0})) = (𝑙
∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑙)) |
100 | 91, 99 | eqtr3i 2646 |
. . . . . . . . . . . . . . . . . . . 20
⊢ seq1( + ,
(𝑚 ∈ ℕ ↦
0)) = (𝑙 ∈ ℕ
↦ (seq1( + , (ℕ × {0}))‘𝑙)) |
101 | | fconstmpt 5163 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℕ
× {0}) = (𝑙 ∈
ℕ ↦ 0) |
102 | 88, 100, 101 | 3eqtr4i 2654 |
. . . . . . . . . . . . . . . . . . 19
⊢ seq1( + ,
(𝑚 ∈ ℕ ↦
0)) = (ℕ × {0}) |
103 | 102 | rneqi 5352 |
. . . . . . . . . . . . . . . . . 18
⊢ ran seq1(
+ , (𝑚 ∈ ℕ
↦ 0)) = ran (ℕ × {0}) |
104 | | 1nn 11031 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℕ |
105 | | ne0i 3921 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 ∈
ℕ → ℕ ≠ ∅) |
106 | | rnxp 5564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℕ
≠ ∅ → ran (ℕ × {0}) = {0}) |
107 | 104, 105,
106 | mp2b 10 |
. . . . . . . . . . . . . . . . . 18
⊢ ran
(ℕ × {0}) = {0} |
108 | 103, 107 | eqtri 2644 |
. . . . . . . . . . . . . . . . 17
⊢ ran seq1(
+ , (𝑚 ∈ ℕ
↦ 0)) = {0} |
109 | 108 | supeq1i 8353 |
. . . . . . . . . . . . . . . 16
⊢ sup(ran
seq1( + , (𝑚 ∈ ℕ
↦ 0)), ℝ*, < ) = sup({0}, ℝ*, <
) |
110 | | xrltso 11974 |
. . . . . . . . . . . . . . . . 17
⊢ < Or
ℝ* |
111 | | 0xr 10086 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
ℝ* |
112 | | supsn 8378 |
. . . . . . . . . . . . . . . . 17
⊢ (( <
Or ℝ* ∧ 0 ∈ ℝ*) → sup({0},
ℝ*, < ) = 0) |
113 | 110, 111,
112 | mp2an 708 |
. . . . . . . . . . . . . . . 16
⊢ sup({0},
ℝ*, < ) = 0 |
114 | 109, 113 | eqtri 2644 |
. . . . . . . . . . . . . . 15
⊢ sup(ran
seq1( + , (𝑚 ∈ ℕ
↦ 0)), ℝ*, < ) = 0 |
115 | 81, 114 | syl6eq 2672 |
. . . . . . . . . . . . . 14
⊢
(∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) → sup(ran seq1( + ,
(𝑚 ∈ ℕ ↦
(vol*‘(𝑓‘𝑚)))), ℝ*, <
) = 0) |
116 | 115 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑓:ℕ–onto→𝐴 ∧ ∀𝑙 ∈ ℕ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0)) → sup(ran seq1( + , (𝑚 ∈ ℕ ↦
(vol*‘(𝑓‘𝑚)))), ℝ*, <
) = 0) |
117 | 63, 70, 116 | 3brtr3d 4684 |
. . . . . . . . . . . 12
⊢ ((𝑓:ℕ–onto→𝐴 ∧ ∀𝑙 ∈ ℕ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0)) → (vol*‘∪ 𝐴)
≤ 0) |
118 | 117 | ex 450 |
. . . . . . . . . . 11
⊢ (𝑓:ℕ–onto→𝐴 → (∀𝑙 ∈ ℕ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0) → (vol*‘∪ 𝐴)
≤ 0)) |
119 | 49, 118 | sylbid 230 |
. . . . . . . . . 10
⊢ (𝑓:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → (vol*‘∪ 𝐴)
≤ 0)) |
120 | 119 | exlimiv 1858 |
. . . . . . . . 9
⊢
(∃𝑓 𝑓:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → (vol*‘∪ 𝐴)
≤ 0)) |
121 | 120 | imp 445 |
. . . . . . . 8
⊢
((∃𝑓 𝑓:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)) → (vol*‘∪ 𝐴)
≤ 0) |
122 | 16, 38, 121 | syl2an 494 |
. . . . . . 7
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → (vol*‘∪ 𝐴) ≤ 0) |
123 | | ovolcl 23246 |
. . . . . . . . 9
⊢ (∪ 𝐴
⊆ ℝ → (vol*‘∪ 𝐴) ∈
ℝ*) |
124 | | xrletri3 11985 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ (vol*‘∪ 𝐴) ∈ ℝ*)
→ (0 = (vol*‘∪ 𝐴) ↔ (0 ≤ (vol*‘∪ 𝐴)
∧ (vol*‘∪ 𝐴) ≤ 0))) |
125 | 111, 123,
124 | sylancr 695 |
. . . . . . . 8
⊢ (∪ 𝐴
⊆ ℝ → (0 = (vol*‘∪ 𝐴) ↔ (0 ≤
(vol*‘∪ 𝐴) ∧ (vol*‘∪ 𝐴)
≤ 0))) |
126 | 125 | ad2antll 765 |
. . . . . . 7
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → (0 = (vol*‘∪ 𝐴) ↔ (0 ≤
(vol*‘∪ 𝐴) ∧ (vol*‘∪ 𝐴)
≤ 0))) |
127 | 9, 122, 126 | mpbir2and 957 |
. . . . . 6
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol*‘∪ 𝐴)) |
128 | 127 | expl 648 |
. . . . 5
⊢ (𝐴 ≠ ∅ → ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol*‘∪ 𝐴))) |
129 | 7, 128 | pm2.61ine 2877 |
. . . 4
⊢ ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol*‘∪ 𝐴)) |
130 | | renepnf 10087 |
. . . . . . 7
⊢ (0 ∈
ℝ → 0 ≠ +∞) |
131 | 56, 130 | mp1i 13 |
. . . . . 6
⊢ (∪ 𝐴 =
ℝ → 0 ≠ +∞) |
132 | | fveq2 6191 |
. . . . . . 7
⊢ (∪ 𝐴 =
ℝ → (vol*‘∪ 𝐴) = (vol*‘ℝ)) |
133 | | ovolre 23293 |
. . . . . . 7
⊢
(vol*‘ℝ) = +∞ |
134 | 132, 133 | syl6eq 2672 |
. . . . . 6
⊢ (∪ 𝐴 =
ℝ → (vol*‘∪ 𝐴) = +∞) |
135 | 131, 134 | neeqtrrd 2868 |
. . . . 5
⊢ (∪ 𝐴 =
ℝ → 0 ≠ (vol*‘∪ 𝐴)) |
136 | 135 | necon2i 2828 |
. . . 4
⊢ (0 =
(vol*‘∪ 𝐴) → ∪ 𝐴 ≠ ℝ) |
137 | 129, 136 | syl 17 |
. . 3
⊢ ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → ∪ 𝐴 ≠ ℝ) |
138 | 137 | expr 643 |
. 2
⊢ ((𝐴 ≼ ℕ ∧
∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → (∪ 𝐴
⊆ ℝ → ∪ 𝐴 ≠ ℝ)) |
139 | | eqimss 3657 |
. . 3
⊢ (∪ 𝐴 =
ℝ → ∪ 𝐴 ⊆ ℝ) |
140 | 139 | necon3bi 2820 |
. 2
⊢ (¬
∪ 𝐴 ⊆ ℝ → ∪ 𝐴
≠ ℝ) |
141 | 138, 140 | pm2.61d1 171 |
1
⊢ ((𝐴 ≼ ℕ ∧
∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴
≠ ℝ) |