| Step | Hyp | Ref
| Expression |
| 1 | | unieq 4918 |
. . . . . . . . 9
⊢ (𝐴 = ∅ → ∪ 𝐴 =
∪ ∅) |
| 2 | | uni0 4935 |
. . . . . . . . 9
⊢ ∪ ∅ = ∅ |
| 3 | 1, 2 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝐴 = ∅ → ∪ 𝐴 =
∅) |
| 4 | 3 | fveq2d 6910 |
. . . . . . 7
⊢ (𝐴 = ∅ →
(vol*‘∪ 𝐴) = (vol*‘∅)) |
| 5 | | ovol0 25528 |
. . . . . . 7
⊢
(vol*‘∅) = 0 |
| 6 | 4, 5 | eqtr2di 2794 |
. . . . . 6
⊢ (𝐴 = ∅ → 0 =
(vol*‘∪ 𝐴)) |
| 7 | 6 | a1d 25 |
. . . . 5
⊢ (𝐴 = ∅ → ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol*‘∪ 𝐴))) |
| 8 | | ovolge0 25516 |
. . . . . . . 8
⊢ (∪ 𝐴
⊆ ℝ → 0 ≤ (vol*‘∪ 𝐴)) |
| 9 | 8 | ad2antll 729 |
. . . . . . 7
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 ≤ (vol*‘∪ 𝐴)) |
| 10 | | reldom 8991 |
. . . . . . . . . . . 12
⊢ Rel
≼ |
| 11 | 10 | brrelex1i 5741 |
. . . . . . . . . . 11
⊢ (𝐴 ≼ ℕ → 𝐴 ∈ V) |
| 12 | | 0sdomg 9144 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
| 13 | 11, 12 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ≼ ℕ → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
| 14 | 13 | biimparc 479 |
. . . . . . . . 9
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∅
≺ 𝐴) |
| 15 | | fodomr 9168 |
. . . . . . . . 9
⊢ ((∅
≺ 𝐴 ∧ 𝐴 ≼ ℕ) →
∃𝑓 𝑓:ℕ–onto→𝐴) |
| 16 | 14, 15 | sylancom 588 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) →
∃𝑓 𝑓:ℕ–onto→𝐴) |
| 17 | | unissb 4939 |
. . . . . . . . . . . 12
⊢ (∪ 𝐴
⊆ ℝ ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ) |
| 18 | 17 | anbi1i 624 |
. . . . . . . . . . 11
⊢ ((∪ 𝐴
⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ)) |
| 19 | | r19.26 3111 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ)) |
| 20 | 18, 19 | bitr4i 278 |
. . . . . . . . . 10
⊢ ((∪ 𝐴
⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ)) |
| 21 | | brdom2 9022 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ≼ ℕ ↔ (𝑥 ≺ ℕ ∨ 𝑥 ≈
ℕ)) |
| 22 | | nnenom 14021 |
. . . . . . . . . . . . . . . . 17
⊢ ℕ
≈ ω |
| 23 | | sdomen2 9162 |
. . . . . . . . . . . . . . . . 17
⊢ (ℕ
≈ ω → (𝑥
≺ ℕ ↔ 𝑥
≺ ω)) |
| 24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ≺ ℕ ↔ 𝑥 ≺
ω) |
| 25 | | isfinite 9692 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ Fin ↔ 𝑥 ≺
ω) |
| 26 | 24, 25 | bitr4i 278 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ≺ ℕ ↔ 𝑥 ∈ Fin) |
| 27 | 26 | orbi1i 914 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ≺ ℕ ∨ 𝑥 ≈ ℕ) ↔ (𝑥 ∈ Fin ∨ 𝑥 ≈
ℕ)) |
| 28 | 21, 27 | bitri 275 |
. . . . . . . . . . . . 13
⊢ (𝑥 ≼ ℕ ↔ (𝑥 ∈ Fin ∨ 𝑥 ≈
ℕ)) |
| 29 | | ovolfi 25529 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ Fin ∧ 𝑥 ⊆ ℝ) →
(vol*‘𝑥) =
0) |
| 30 | 29 | expcom 413 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ⊆ ℝ → (𝑥 ∈ Fin →
(vol*‘𝑥) =
0)) |
| 31 | | ovolctb 25525 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≈ ℕ) →
(vol*‘𝑥) =
0) |
| 32 | 31 | ex 412 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ⊆ ℝ → (𝑥 ≈ ℕ →
(vol*‘𝑥) =
0)) |
| 33 | 30, 32 | jaod 860 |
. . . . . . . . . . . . 13
⊢ (𝑥 ⊆ ℝ → ((𝑥 ∈ Fin ∨ 𝑥 ≈ ℕ) →
(vol*‘𝑥) =
0)) |
| 34 | 28, 33 | biimtrid 242 |
. . . . . . . . . . . 12
⊢ (𝑥 ⊆ ℝ → (𝑥 ≼ ℕ →
(vol*‘𝑥) =
0)) |
| 35 | 34 | imdistani 568 |
. . . . . . . . . . 11
⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) =
0)) |
| 36 | 35 | ralimi 3083 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)) |
| 37 | 20, 36 | sylbi 217 |
. . . . . . . . 9
⊢ ((∪ 𝐴
⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)) |
| 38 | 37 | ancoms 458 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)) |
| 39 | | foima 6825 |
. . . . . . . . . . . . 13
⊢ (𝑓:ℕ–onto→𝐴 → (𝑓 “ ℕ) = 𝐴) |
| 40 | 39 | raleqdv 3326 |
. . . . . . . . . . . 12
⊢ (𝑓:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑓 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))) |
| 41 | | fofn 6822 |
. . . . . . . . . . . . 13
⊢ (𝑓:ℕ–onto→𝐴 → 𝑓 Fn ℕ) |
| 42 | | ssid 4006 |
. . . . . . . . . . . . 13
⊢ ℕ
⊆ ℕ |
| 43 | | sseq1 4009 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑓‘𝑙) → (𝑥 ⊆ ℝ ↔ (𝑓‘𝑙) ⊆ ℝ)) |
| 44 | | fveqeq2 6915 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑓‘𝑙) → ((vol*‘𝑥) = 0 ↔ (vol*‘(𝑓‘𝑙)) = 0)) |
| 45 | 43, 44 | anbi12d 632 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑓‘𝑙) → ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0))) |
| 46 | 45 | ralima 7257 |
. . . . . . . . . . . . 13
⊢ ((𝑓 Fn ℕ ∧ ℕ
⊆ ℕ) → (∀𝑥 ∈ (𝑓 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑙 ∈ ℕ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0))) |
| 47 | 41, 42, 46 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝑓:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑓 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑙 ∈ ℕ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0))) |
| 48 | 40, 47 | bitr3d 281 |
. . . . . . . . . . 11
⊢ (𝑓:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑙 ∈ ℕ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0))) |
| 49 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 = 𝑛 → (𝑓‘𝑙) = (𝑓‘𝑛)) |
| 50 | 49 | sseq1d 4015 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = 𝑛 → ((𝑓‘𝑙) ⊆ ℝ ↔ (𝑓‘𝑛) ⊆ ℝ)) |
| 51 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 = 𝑛 → (vol*‘(𝑓‘𝑙)) = (vol*‘(𝑓‘𝑛))) |
| 52 | 51 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = 𝑛 → ((vol*‘(𝑓‘𝑙)) = 0 ↔ (vol*‘(𝑓‘𝑛)) = 0)) |
| 53 | 50, 52 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 = 𝑛 → (((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0) ↔ ((𝑓‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑛)) = 0))) |
| 54 | 53 | cbvralvw 3237 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) ↔ ∀𝑛 ∈ ℕ ((𝑓‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑛)) = 0)) |
| 55 | | 0re 11263 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℝ |
| 56 | | eleq1a 2836 |
. . . . . . . . . . . . . . . . . 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 3083 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑛 ∈
ℕ ((𝑓‘𝑛) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑛)) = 0) → ∀𝑛 ∈ ℕ ((𝑓‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑛)) ∈ ℝ)) |
| 60 | 54, 59 | sylbi 217 |
. . . . . . . . . . . . . 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 6821 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:ℕ–onto→𝐴 → Fun 𝑓) |
| 64 | | funiunfv 7268 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
𝑓 → ∪ 𝑚 ∈ ℕ (𝑓‘𝑚) = ∪ (𝑓 “
ℕ)) |
| 65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:ℕ–onto→𝐴 → ∪
𝑚 ∈ ℕ (𝑓‘𝑚) = ∪ (𝑓 “
ℕ)) |
| 66 | 39 | unieqd 4920 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:ℕ–onto→𝐴 → ∪ (𝑓 “ ℕ) = ∪ 𝐴) |
| 67 | 65, 66 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:ℕ–onto→𝐴 → ∪
𝑚 ∈ ℕ (𝑓‘𝑚) = ∪ 𝐴) |
| 68 | 67 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ (𝑓:ℕ–onto→𝐴 → (vol*‘∪ 𝑚 ∈ ℕ (𝑓‘𝑚)) = (vol*‘∪
𝐴)) |
| 69 | 68 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑓:ℕ–onto→𝐴 ∧ ∀𝑙 ∈ ℕ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0)) → (vol*‘∪ 𝑚 ∈ ℕ (𝑓‘𝑚)) = (vol*‘∪
𝐴)) |
| 70 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑙 = 𝑚 → (𝑓‘𝑙) = (𝑓‘𝑚)) |
| 71 | 70 | sseq1d 4015 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑙 = 𝑚 → ((𝑓‘𝑙) ⊆ ℝ ↔ (𝑓‘𝑚) ⊆ ℝ)) |
| 72 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑙 = 𝑚 → (vol*‘(𝑓‘𝑙)) = (vol*‘(𝑓‘𝑚))) |
| 73 | 72 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑙 = 𝑚 → ((vol*‘(𝑓‘𝑙)) = 0 ↔ (vol*‘(𝑓‘𝑚)) = 0)) |
| 74 | 71, 73 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 = 𝑚 → (((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0) ↔ ((𝑓‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑚)) = 0))) |
| 75 | 74 | rspccva 3621 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) ∧ 𝑚 ∈ ℕ) → ((𝑓‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑚)) = 0)) |
| 76 | 75 | simprd 495 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) ∧ 𝑚 ∈ ℕ) → (vol*‘(𝑓‘𝑚)) = 0) |
| 77 | 76 | mpteq2dva 5242 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) → (𝑚 ∈ ℕ ↦
(vol*‘(𝑓‘𝑚))) = (𝑚 ∈ ℕ ↦ 0)) |
| 78 | 77 | seqeq3d 14050 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) → seq1( + , (𝑚 ∈ ℕ ↦
(vol*‘(𝑓‘𝑚)))) = seq1( + , (𝑚 ∈ ℕ ↦
0))) |
| 79 | 78 | rneqd 5949 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) → ran seq1( + ,
(𝑚 ∈ ℕ ↦
(vol*‘(𝑓‘𝑚)))) = ran seq1( + , (𝑚 ∈ ℕ ↦
0))) |
| 80 | 79 | supeq1d 9486 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) → sup(ran seq1( + ,
(𝑚 ∈ ℕ ↦
(vol*‘(𝑓‘𝑚)))), ℝ*, <
) = sup(ran seq1( + , (𝑚
∈ ℕ ↦ 0)), ℝ*, < )) |
| 81 | | 0cn 11253 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
ℂ |
| 82 | | ser1const 14099 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((0
∈ ℂ ∧ 𝑙
∈ ℕ) → (seq1( + , (ℕ × {0}))‘𝑙) = (𝑙 · 0)) |
| 83 | 81, 82 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑙 ∈ ℕ → (seq1( +
, (ℕ × {0}))‘𝑙) = (𝑙 · 0)) |
| 84 | | nncn 12274 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑙 ∈ ℕ → 𝑙 ∈
ℂ) |
| 85 | 84 | mul01d 11460 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑙 ∈ ℕ → (𝑙 · 0) =
0) |
| 86 | 83, 85 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 ∈ ℕ → (seq1( +
, (ℕ × {0}))‘𝑙) = 0) |
| 87 | 86 | mpteq2ia 5245 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 ∈ ℕ ↦ (seq1( +
, (ℕ × {0}))‘𝑙)) = (𝑙 ∈ ℕ ↦ 0) |
| 88 | | fconstmpt 5747 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℕ
× {0}) = (𝑚 ∈
ℕ ↦ 0) |
| 89 | | seqeq3 14047 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((ℕ
× {0}) = (𝑚 ∈
ℕ ↦ 0) → seq1( + , (ℕ × {0})) = seq1( + , (𝑚 ∈ ℕ ↦
0))) |
| 90 | 88, 89 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ seq1( + ,
(ℕ × {0})) = seq1( + , (𝑚 ∈ ℕ ↦ 0)) |
| 91 | | 1z 12647 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℤ |
| 92 | | seqfn 14054 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (1 ∈
ℤ → seq1( + , (ℕ × {0})) Fn
(ℤ≥‘1)) |
| 93 | 91, 92 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ seq1( + ,
(ℕ × {0})) Fn (ℤ≥‘1) |
| 94 | | nnuz 12921 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ℕ =
(ℤ≥‘1) |
| 95 | 94 | fneq2i 6666 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (seq1( +
, (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) Fn
(ℤ≥‘1)) |
| 96 | | dffn5 6967 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (seq1( +
, (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) =
(𝑙 ∈ ℕ ↦
(seq1( + , (ℕ × {0}))‘𝑙))) |
| 97 | 95, 96 | bitr3i 277 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (seq1( +
, (ℕ × {0})) Fn (ℤ≥‘1) ↔ seq1( + ,
(ℕ × {0})) = (𝑙
∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑙))) |
| 98 | 93, 97 | mpbi 230 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ seq1( + ,
(ℕ × {0})) = (𝑙
∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑙)) |
| 99 | 90, 98 | eqtr3i 2767 |
. . . . . . . . . . . . . . . . . . . 20
⊢ seq1( + ,
(𝑚 ∈ ℕ ↦
0)) = (𝑙 ∈ ℕ
↦ (seq1( + , (ℕ × {0}))‘𝑙)) |
| 100 | | fconstmpt 5747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℕ
× {0}) = (𝑙 ∈
ℕ ↦ 0) |
| 101 | 87, 99, 100 | 3eqtr4i 2775 |
. . . . . . . . . . . . . . . . . . 19
⊢ seq1( + ,
(𝑚 ∈ ℕ ↦
0)) = (ℕ × {0}) |
| 102 | 101 | rneqi 5948 |
. . . . . . . . . . . . . . . . . 18
⊢ ran seq1(
+ , (𝑚 ∈ ℕ
↦ 0)) = ran (ℕ × {0}) |
| 103 | | 1nn 12277 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℕ |
| 104 | | ne0i 4341 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 ∈
ℕ → ℕ ≠ ∅) |
| 105 | | rnxp 6190 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℕ
≠ ∅ → ran (ℕ × {0}) = {0}) |
| 106 | 103, 104,
105 | mp2b 10 |
. . . . . . . . . . . . . . . . . 18
⊢ ran
(ℕ × {0}) = {0} |
| 107 | 102, 106 | eqtri 2765 |
. . . . . . . . . . . . . . . . 17
⊢ ran seq1(
+ , (𝑚 ∈ ℕ
↦ 0)) = {0} |
| 108 | 107 | supeq1i 9487 |
. . . . . . . . . . . . . . . 16
⊢ sup(ran
seq1( + , (𝑚 ∈ ℕ
↦ 0)), ℝ*, < ) = sup({0}, ℝ*, <
) |
| 109 | | xrltso 13183 |
. . . . . . . . . . . . . . . . 17
⊢ < Or
ℝ* |
| 110 | | 0xr 11308 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
ℝ* |
| 111 | | supsn 9512 |
. . . . . . . . . . . . . . . . 17
⊢ (( <
Or ℝ* ∧ 0 ∈ ℝ*) → sup({0},
ℝ*, < ) = 0) |
| 112 | 109, 110,
111 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢ sup({0},
ℝ*, < ) = 0 |
| 113 | 108, 112 | eqtri 2765 |
. . . . . . . . . . . . . . 15
⊢ sup(ran
seq1( + , (𝑚 ∈ ℕ
↦ 0)), ℝ*, < ) = 0 |
| 114 | 80, 113 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
⊢
(∀𝑙 ∈
ℕ ((𝑓‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑓‘𝑙)) = 0) → sup(ran seq1( + ,
(𝑚 ∈ ℕ ↦
(vol*‘(𝑓‘𝑚)))), ℝ*, <
) = 0) |
| 115 | 114 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑓:ℕ–onto→𝐴 ∧ ∀𝑙 ∈ ℕ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0)) → sup(ran seq1( + , (𝑚 ∈ ℕ ↦
(vol*‘(𝑓‘𝑚)))), ℝ*, <
) = 0) |
| 116 | 62, 69, 115 | 3brtr3d 5174 |
. . . . . . . . . . . 12
⊢ ((𝑓:ℕ–onto→𝐴 ∧ ∀𝑙 ∈ ℕ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0)) → (vol*‘∪ 𝐴)
≤ 0) |
| 117 | 116 | ex 412 |
. . . . . . . . . . 11
⊢ (𝑓:ℕ–onto→𝐴 → (∀𝑙 ∈ ℕ ((𝑓‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑓‘𝑙)) = 0) → (vol*‘∪ 𝐴)
≤ 0)) |
| 118 | 48, 117 | sylbid 240 |
. . . . . . . . . 10
⊢ (𝑓:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → (vol*‘∪ 𝐴)
≤ 0)) |
| 119 | 118 | exlimiv 1930 |
. . . . . . . . 9
⊢
(∃𝑓 𝑓:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → (vol*‘∪ 𝐴)
≤ 0)) |
| 120 | 119 | imp 406 |
. . . . . . . 8
⊢
((∃𝑓 𝑓:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)) → (vol*‘∪ 𝐴)
≤ 0) |
| 121 | 16, 38, 120 | syl2an 596 |
. . . . . . 7
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → (vol*‘∪ 𝐴) ≤ 0) |
| 122 | | ovolcl 25513 |
. . . . . . . . 9
⊢ (∪ 𝐴
⊆ ℝ → (vol*‘∪ 𝐴) ∈
ℝ*) |
| 123 | | xrletri3 13196 |
. . . . . . . . 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 729 |
. . . . . . 7
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → (0 = (vol*‘∪ 𝐴) ↔ (0 ≤
(vol*‘∪ 𝐴) ∧ (vol*‘∪ 𝐴)
≤ 0))) |
| 126 | 9, 121, 125 | mpbir2and 713 |
. . . . . 6
⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol*‘∪ 𝐴)) |
| 127 | 126 | expl 457 |
. . . . 5
⊢ (𝐴 ≠ ∅ → ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol*‘∪ 𝐴))) |
| 128 | 7, 127 | pm2.61ine 3025 |
. . . 4
⊢ ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol*‘∪ 𝐴)) |
| 129 | | renepnf 11309 |
. . . . . . 7
⊢ (0 ∈
ℝ → 0 ≠ +∞) |
| 130 | 55, 129 | mp1i 13 |
. . . . . 6
⊢ (∪ 𝐴 =
ℝ → 0 ≠ +∞) |
| 131 | | fveq2 6906 |
. . . . . . 7
⊢ (∪ 𝐴 =
ℝ → (vol*‘∪ 𝐴) = (vol*‘ℝ)) |
| 132 | | ovolre 25560 |
. . . . . . 7
⊢
(vol*‘ℝ) = +∞ |
| 133 | 131, 132 | eqtrdi 2793 |
. . . . . 6
⊢ (∪ 𝐴 =
ℝ → (vol*‘∪ 𝐴) = +∞) |
| 134 | 130, 133 | neeqtrrd 3015 |
. . . . 5
⊢ (∪ 𝐴 =
ℝ → 0 ≠ (vol*‘∪ 𝐴)) |
| 135 | 134 | necon2i 2975 |
. . . 4
⊢ (0 =
(vol*‘∪ 𝐴) → ∪ 𝐴 ≠ ℝ) |
| 136 | 128, 135 | syl 17 |
. . 3
⊢ ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → ∪ 𝐴 ≠ ℝ) |
| 137 | 136 | expr 456 |
. 2
⊢ ((𝐴 ≼ ℕ ∧
∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → (∪ 𝐴
⊆ ℝ → ∪ 𝐴 ≠ ℝ)) |
| 138 | | eqimss 4042 |
. . 3
⊢ (∪ 𝐴 =
ℝ → ∪ 𝐴 ⊆ ℝ) |
| 139 | 138 | necon3bi 2967 |
. 2
⊢ (¬
∪ 𝐴 ⊆ ℝ → ∪ 𝐴
≠ ℝ) |
| 140 | 137, 139 | pm2.61d1 180 |
1
⊢ ((𝐴 ≼ ℕ ∧
∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴
≠ ℝ) |