| 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 | | 0mbl 25574 |
. . . . . . . . 9
⊢ ∅
∈ dom vol |
| 6 | | mblvol 25565 |
. . . . . . . . 9
⊢ (∅
∈ dom vol → (vol‘∅) =
(vol*‘∅)) |
| 7 | 5, 6 | ax-mp 5 |
. . . . . . . 8
⊢
(vol‘∅) = (vol*‘∅) |
| 8 | | ovol0 25528 |
. . . . . . . 8
⊢
(vol*‘∅) = 0 |
| 9 | 7, 8 | eqtri 2765 |
. . . . . . 7
⊢
(vol‘∅) = 0 |
| 10 | 4, 9 | eqtr2di 2794 |
. . . . . 6
⊢ (𝐴 = ∅ → 0 =
(vol‘∪ 𝐴)) |
| 11 | 10 | a1d 25 |
. . . . 5
⊢ (𝐴 = ∅ → ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol‘∪ 𝐴))) |
| 12 | | reldom 8991 |
. . . . . . . . . . 11
⊢ Rel
≼ |
| 13 | 12 | brrelex1i 5741 |
. . . . . . . . . 10
⊢ (𝐴 ≼ ℕ → 𝐴 ∈ V) |
| 14 | | 0sdomg 9144 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
| 15 | 13, 14 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ≼ ℕ → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
| 16 | 15 | biimparc 479 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∅
≺ 𝐴) |
| 17 | | fodomr 9168 |
. . . . . . . 8
⊢ ((∅
≺ 𝐴 ∧ 𝐴 ≼ ℕ) →
∃𝑔 𝑔:ℕ–onto→𝐴) |
| 18 | 16, 17 | sylancom 588 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) →
∃𝑔 𝑔:ℕ–onto→𝐴) |
| 19 | | unissb 4939 |
. . . . . . . . . . . . 13
⊢ (∪ 𝐴
⊆ ℝ ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ) |
| 20 | 19 | anbi1i 624 |
. . . . . . . . . . . 12
⊢ ((∪ 𝐴
⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ)) |
| 21 | | r19.26 3111 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ)) |
| 22 | 20, 21 | bitr4i 278 |
. . . . . . . . . . 11
⊢ ((∪ 𝐴
⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ)) |
| 23 | | ovolctb2 25527 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) →
(vol*‘𝑥) =
0) |
| 24 | 23 | ex 412 |
. . . . . . . . . . . . 13
⊢ (𝑥 ⊆ ℝ → (𝑥 ≼ ℕ →
(vol*‘𝑥) =
0)) |
| 25 | 24 | imdistani 568 |
. . . . . . . . . . . 12
⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) =
0)) |
| 26 | 25 | ralimi 3083 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)) |
| 27 | 22, 26 | sylbi 217 |
. . . . . . . . . 10
⊢ ((∪ 𝐴
⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)) |
| 28 | 27 | ancoms 458 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)) |
| 29 | | foima 6825 |
. . . . . . . . . . . 12
⊢ (𝑔:ℕ–onto→𝐴 → (𝑔 “ ℕ) = 𝐴) |
| 30 | 29 | raleqdv 3326 |
. . . . . . . . . . 11
⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))) |
| 31 | | fofn 6822 |
. . . . . . . . . . . 12
⊢ (𝑔:ℕ–onto→𝐴 → 𝑔 Fn ℕ) |
| 32 | | ssid 4006 |
. . . . . . . . . . . 12
⊢ ℕ
⊆ ℕ |
| 33 | | sseq1 4009 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑔‘𝑚) → (𝑥 ⊆ ℝ ↔ (𝑔‘𝑚) ⊆ ℝ)) |
| 34 | | fveqeq2 6915 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑔‘𝑚) → ((vol*‘𝑥) = 0 ↔ (vol*‘(𝑔‘𝑚)) = 0)) |
| 35 | 33, 34 | anbi12d 632 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑔‘𝑚) → ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0))) |
| 36 | 35 | ralima 7257 |
. . . . . . . . . . . 12
⊢ ((𝑔 Fn ℕ ∧ ℕ
⊆ ℕ) → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0))) |
| 37 | 31, 32, 36 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0))) |
| 38 | 30, 37 | bitr3d 281 |
. . . . . . . . . 10
⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0))) |
| 39 | | difss 4136 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ (𝑔‘𝑚) |
| 40 | | ovolssnul 25522 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ (𝑔‘𝑚) ∧ (𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) |
| 41 | 39, 40 | mp3an1 1450 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) |
| 42 | | ssdifss 4140 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔‘𝑚) ⊆ ℝ → ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ) |
| 43 | | nulmbl 25570 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol) |
| 44 | | mblvol 25565 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))) |
| 45 | 44 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → ((vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0 ↔ (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0)) |
| 46 | 45 | biimpar 477 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) |
| 47 | | 0re 11263 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
ℝ |
| 48 | 46, 47 | eqeltrdi 2849 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ) |
| 49 | 48 | expcom 413 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0 → (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)) |
| 50 | 49 | ancld 550 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0 → (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))) |
| 51 | 50 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))) |
| 52 | 43, 51 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)) |
| 53 | 42, 52 | sylan 580 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)) |
| 54 | 41, 53 | syldan 591 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)) |
| 55 | 54 | ralimi 3083 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) → ∀𝑚 ∈ ℕ (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)) |
| 56 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → (𝑔‘𝑚) = (𝑔‘𝑛)) |
| 57 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑛 → (1..^𝑚) = (1..^𝑛)) |
| 58 | 57 | iuneq1d 5019 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) |
| 59 | 56, 58 | difeq12d 4127 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑛 → ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) = ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) |
| 60 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) |
| 61 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔‘𝑛) ∈ V |
| 62 | | difexg 5329 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑔‘𝑛) ∈ V → ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ V) |
| 63 | 61, 62 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ V |
| 64 | 59, 60, 63 | fvmpt 7016 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) = ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) |
| 65 | 64 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ↔ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol)) |
| 66 | 64 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ →
(vol‘((𝑚 ∈
ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) |
| 67 | 66 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ →
((vol‘((𝑚 ∈
ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ ↔ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ)) |
| 68 | 65, 67 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → ((((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ↔ (((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ))) |
| 69 | 68 | ralbiia 3091 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
ℕ (((𝑚 ∈ ℕ
↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ↔ ∀𝑛 ∈ ℕ (((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ)) |
| 70 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑚 → (𝑔‘𝑛) = (𝑔‘𝑚)) |
| 71 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑚 → (1..^𝑛) = (1..^𝑚)) |
| 72 | 71 | iuneq1d 5019 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑚 → ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) |
| 73 | 70, 72 | difeq12d 4127 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑚 → ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) = ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) |
| 74 | 73 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑚 → (((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ↔ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol)) |
| 75 | 73 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑚 → (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))) |
| 76 | 75 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑚 → ((vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ ↔ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)) |
| 77 | 74, 76 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑚 → ((((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ) ↔ (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))) |
| 78 | 77 | cbvralvw 3237 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
ℕ (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ) ↔ ∀𝑚 ∈ ℕ (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)) |
| 79 | 69, 78 | bitri 275 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑛 ∈
ℕ (((𝑚 ∈ ℕ
↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ↔ ∀𝑚 ∈ ℕ (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)) |
| 80 | 55, 79 | sylibr 234 |
. . . . . . . . . . . . . 14
⊢
(∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) → ∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ)) |
| 81 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑙 → (𝑔‘𝑛) = (𝑔‘𝑙)) |
| 82 | 81 | iundisj2 25584 |
. . . . . . . . . . . . . . 15
⊢
Disj 𝑛 ∈
ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) |
| 83 | | disjeq2 5114 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
ℕ ((𝑚 ∈ ℕ
↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) = ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) → (Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) |
| 84 | 83, 64 | mprg 3067 |
. . . . . . . . . . . . . . 15
⊢
(Disj 𝑛
∈ ℕ ((𝑚 ∈
ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) |
| 85 | 82, 84 | mpbir 231 |
. . . . . . . . . . . . . 14
⊢
Disj 𝑛 ∈
ℕ ((𝑚 ∈ ℕ
↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) |
| 86 | | nnex 12272 |
. . . . . . . . . . . . . . . . 17
⊢ ℕ
∈ V |
| 87 | 86 | mptex 7243 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ V |
| 88 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (𝑓‘𝑛) = ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) |
| 89 | 88 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((𝑓‘𝑛) ∈ dom vol ↔ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol)) |
| 90 | 88 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (vol‘(𝑓‘𝑛)) = (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))) |
| 91 | 90 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((vol‘(𝑓‘𝑛)) ∈ ℝ ↔ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ)) |
| 92 | 89, 91 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ↔ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ))) |
| 93 | 92 | ralbidv 3178 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ↔ ∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ))) |
| 94 | 88 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) = ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) |
| 95 | 94 | disjeq2dv 5115 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (Disj 𝑛 ∈ ℕ (𝑓‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))) |
| 96 | 93, 95 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)) ↔ (∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))) |
| 97 | 88 | iuneq2d 5022 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ∪ 𝑛 ∈ ℕ (𝑓‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) |
| 98 | 97 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))) |
| 99 | | voliunnfl.1 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑆 = seq1( + , 𝐺) |
| 100 | | voliunnfl.2 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))) |
| 101 | | seqeq3 14047 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))) → seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))))) |
| 102 | 100, 101 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ seq1( + ,
𝐺) = seq1( + , (𝑛 ∈ ℕ ↦
(vol‘(𝑓‘𝑛)))) |
| 103 | 99, 102 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑆 = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))) |
| 104 | 103 | rneqi 5948 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ran 𝑆 = ran seq1( + , (𝑛 ∈ ℕ ↦
(vol‘(𝑓‘𝑛)))) |
| 105 | 104 | supeq1i 9487 |
. . . . . . . . . . . . . . . . . . 19
⊢ sup(ran
𝑆, ℝ*,
< ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))), ℝ*, <
) |
| 106 | 90 | mpteq2dv 5244 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))) |
| 107 | 106 | seqeq3d 14050 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))))) |
| 108 | 107 | rneqd 5949 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))) = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))))) |
| 109 | 108 | supeq1d 9486 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦
(vol‘(𝑓‘𝑛)))), ℝ*, <
) = sup(ran seq1( + , (𝑛
∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, <
)) |
| 110 | 105, 109 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → sup(ran 𝑆, ℝ*, < ) = sup(ran
seq1( + , (𝑛 ∈ ℕ
↦ (vol‘((𝑚
∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, <
)) |
| 111 | 98, 110 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = sup(ran 𝑆, ℝ*, < ) ↔
(vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, <
))) |
| 112 | 96, 111 | imbi12d 344 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (((∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = sup(ran 𝑆, ℝ*, < )) ↔
((∀𝑛 ∈ ℕ
(((𝑚 ∈ ℕ ↦
((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, <
)))) |
| 113 | | voliunnfl.3 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑛 ∈
ℕ ((𝑓‘𝑛) ∈ dom vol ∧
(vol‘(𝑓‘𝑛)) ∈ ℝ) ∧
Disj 𝑛 ∈
ℕ (𝑓‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = sup(ran 𝑆, ℝ*, <
)) |
| 114 | 87, 112, 113 | vtocl 3558 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑛 ∈
ℕ (((𝑚 ∈ ℕ
↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, <
)) |
| 115 | 64 | iuneq2i 5013 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) |
| 116 | 115 | fveq2i 6909 |
. . . . . . . . . . . . . . 15
⊢
(vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) |
| 117 | 66 | mpteq2ia 5245 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ ↦
(vol‘((𝑚 ∈
ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) |
| 118 | | seqeq3 14047 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℕ ↦
(vol‘((𝑚 ∈
ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) → seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))))) |
| 119 | 117, 118 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ seq1( + ,
(𝑛 ∈ ℕ ↦
(vol‘((𝑚 ∈
ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))) |
| 120 | 119 | rneqi 5948 |
. . . . . . . . . . . . . . . 16
⊢ ran seq1(
+ , (𝑛 ∈ ℕ
↦ (vol‘((𝑚
∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))) = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))) |
| 121 | 120 | supeq1i 9487 |
. . . . . . . . . . . . . . 15
⊢ sup(ran
seq1( + , (𝑛 ∈ ℕ
↦ (vol‘((𝑚
∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ) = sup(ran
seq1( + , (𝑛 ∈ ℕ
↦ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, <
) |
| 122 | 114, 116,
121 | 3eqtr3g 2800 |
. . . . . . . . . . . . . 14
⊢
((∀𝑛 ∈
ℕ (((𝑚 ∈ ℕ
↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, <
)) |
| 123 | 80, 85, 122 | sylancl 586 |
. . . . . . . . . . . . 13
⊢
(∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) →
(vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, <
)) |
| 124 | 123 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, <
)) |
| 125 | 81 | iundisj 25583 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) |
| 126 | | fofun 6821 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔:ℕ–onto→𝐴 → Fun 𝑔) |
| 127 | | funiunfv 7268 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
𝑔 → ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) = ∪ (𝑔 “
ℕ)) |
| 128 | 126, 127 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔:ℕ–onto→𝐴 → ∪
𝑛 ∈ ℕ (𝑔‘𝑛) = ∪ (𝑔 “
ℕ)) |
| 129 | 125, 128 | eqtr3id 2791 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:ℕ–onto→𝐴 → ∪
𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) = ∪ (𝑔 “
ℕ)) |
| 130 | 29 | unieqd 4920 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:ℕ–onto→𝐴 → ∪ (𝑔 “ ℕ) = ∪ 𝐴) |
| 131 | 129, 130 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (𝑔:ℕ–onto→𝐴 → ∪
𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) = ∪ 𝐴) |
| 132 | 131 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (𝑔:ℕ–onto→𝐴 → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol‘∪
𝐴)) |
| 133 | 132 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol‘∪
𝐴)) |
| 134 | 56 | sseq1d 4015 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → ((𝑔‘𝑚) ⊆ ℝ ↔ (𝑔‘𝑛) ⊆ ℝ)) |
| 135 | 56 | fveqeq2d 6914 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → ((vol*‘(𝑔‘𝑚)) = 0 ↔ (vol*‘(𝑔‘𝑛)) = 0)) |
| 136 | 134, 135 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑛 → (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) ↔ ((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0))) |
| 137 | 136 | rspccva 3621 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) ∧ 𝑛 ∈ ℕ) → ((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0)) |
| 138 | | ssdifss 4140 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔‘𝑛) ⊆ ℝ → ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ) |
| 139 | 138 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ) |
| 140 | | difss 4136 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ (𝑔‘𝑛) |
| 141 | | ovolssnul 25522 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol*‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0) |
| 142 | 140, 141 | mp3an1 1450 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol*‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0) |
| 143 | 139, 142 | jca 511 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0)) |
| 144 | | nulmbl 25570 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0) → ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol) |
| 145 | | mblvol 25565 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol → (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol*‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) |
| 146 | 143, 144,
145 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol*‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) |
| 147 | 146, 142 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0) |
| 148 | 137, 147 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) ∧ 𝑛 ∈ ℕ) → (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0) |
| 149 | 148 | mpteq2dva 5242 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) → (𝑛 ∈ ℕ ↦
(vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) = (𝑛 ∈ ℕ ↦ 0)) |
| 150 | 149 | seqeq3d 14050 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) → seq1( + , (𝑛 ∈ ℕ ↦
(vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))) = seq1( + , (𝑛 ∈ ℕ ↦ 0))) |
| 151 | 150 | rneqd 5949 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) → ran seq1( + ,
(𝑛 ∈ ℕ ↦
(vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))) = ran seq1( + , (𝑛 ∈ ℕ ↦ 0))) |
| 152 | 151 | supeq1d 9486 |
. . . . . . . . . . . . . 14
⊢
(∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) → sup(ran seq1( + ,
(𝑛 ∈ ℕ ↦
(vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ) = sup(ran
seq1( + , (𝑛 ∈ ℕ
↦ 0)), ℝ*, < )) |
| 153 | | 0cn 11253 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
ℂ |
| 154 | | ser1const 14099 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((0
∈ ℂ ∧ 𝑚
∈ ℕ) → (seq1( + , (ℕ × {0}))‘𝑚) = (𝑚 · 0)) |
| 155 | 153, 154 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ ℕ → (seq1( +
, (ℕ × {0}))‘𝑚) = (𝑚 · 0)) |
| 156 | | nncn 12274 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℂ) |
| 157 | 156 | mul01d 11460 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ ℕ → (𝑚 · 0) =
0) |
| 158 | 155, 157 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ ℕ → (seq1( +
, (ℕ × {0}))‘𝑚) = 0) |
| 159 | 158 | mpteq2ia 5245 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ ℕ ↦ (seq1( +
, (ℕ × {0}))‘𝑚)) = (𝑚 ∈ ℕ ↦ 0) |
| 160 | | fconstmpt 5747 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℕ
× {0}) = (𝑛 ∈
ℕ ↦ 0) |
| 161 | | seqeq3 14047 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((ℕ
× {0}) = (𝑛 ∈
ℕ ↦ 0) → seq1( + , (ℕ × {0})) = seq1( + , (𝑛 ∈ ℕ ↦
0))) |
| 162 | 160, 161 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ seq1( + ,
(ℕ × {0})) = seq1( + , (𝑛 ∈ ℕ ↦ 0)) |
| 163 | | 1z 12647 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
ℤ |
| 164 | | seqfn 14054 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1 ∈
ℤ → seq1( + , (ℕ × {0})) Fn
(ℤ≥‘1)) |
| 165 | 163, 164 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ seq1( + ,
(ℕ × {0})) Fn (ℤ≥‘1) |
| 166 | | nnuz 12921 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ℕ =
(ℤ≥‘1) |
| 167 | 166 | fneq2i 6666 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (seq1( +
, (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) Fn
(ℤ≥‘1)) |
| 168 | | dffn5 6967 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (seq1( +
, (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) =
(𝑚 ∈ ℕ ↦
(seq1( + , (ℕ × {0}))‘𝑚))) |
| 169 | 167, 168 | bitr3i 277 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (seq1( +
, (ℕ × {0})) Fn (ℤ≥‘1) ↔ seq1( + ,
(ℕ × {0})) = (𝑚
∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚))) |
| 170 | 165, 169 | mpbi 230 |
. . . . . . . . . . . . . . . . . . . 20
⊢ seq1( + ,
(ℕ × {0})) = (𝑚
∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚)) |
| 171 | 162, 170 | eqtr3i 2767 |
. . . . . . . . . . . . . . . . . . 19
⊢ seq1( + ,
(𝑛 ∈ ℕ ↦
0)) = (𝑚 ∈ ℕ
↦ (seq1( + , (ℕ × {0}))‘𝑚)) |
| 172 | | fconstmpt 5747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℕ
× {0}) = (𝑚 ∈
ℕ ↦ 0) |
| 173 | 159, 171,
172 | 3eqtr4i 2775 |
. . . . . . . . . . . . . . . . . 18
⊢ seq1( + ,
(𝑛 ∈ ℕ ↦
0)) = (ℕ × {0}) |
| 174 | 173 | rneqi 5948 |
. . . . . . . . . . . . . . . . 17
⊢ ran seq1(
+ , (𝑛 ∈ ℕ
↦ 0)) = ran (ℕ × {0}) |
| 175 | | 1nn 12277 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℕ |
| 176 | | ne0i 4341 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
ℕ → ℕ ≠ ∅) |
| 177 | | rnxp 6190 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℕ
≠ ∅ → ran (ℕ × {0}) = {0}) |
| 178 | 175, 176,
177 | mp2b 10 |
. . . . . . . . . . . . . . . . 17
⊢ ran
(ℕ × {0}) = {0} |
| 179 | 174, 178 | eqtri 2765 |
. . . . . . . . . . . . . . . 16
⊢ ran seq1(
+ , (𝑛 ∈ ℕ
↦ 0)) = {0} |
| 180 | 179 | supeq1i 9487 |
. . . . . . . . . . . . . . 15
⊢ sup(ran
seq1( + , (𝑛 ∈ ℕ
↦ 0)), ℝ*, < ) = sup({0}, ℝ*, <
) |
| 181 | | xrltso 13183 |
. . . . . . . . . . . . . . . 16
⊢ < Or
ℝ* |
| 182 | | 0xr 11308 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ* |
| 183 | | supsn 9512 |
. . . . . . . . . . . . . . . 16
⊢ (( <
Or ℝ* ∧ 0 ∈ ℝ*) → sup({0},
ℝ*, < ) = 0) |
| 184 | 181, 182,
183 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢ sup({0},
ℝ*, < ) = 0 |
| 185 | 180, 184 | eqtri 2765 |
. . . . . . . . . . . . . 14
⊢ sup(ran
seq1( + , (𝑛 ∈ ℕ
↦ 0)), ℝ*, < ) = 0 |
| 186 | 152, 185 | eqtrdi 2793 |
. . . . . . . . . . . . 13
⊢
(∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) → sup(ran seq1( + ,
(𝑛 ∈ ℕ ↦
(vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ) =
0) |
| 187 | 186 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦
(vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ) =
0) |
| 188 | 124, 133,
187 | 3eqtr3rd 2786 |
. . . . . . . . . . 11
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → 0 = (vol‘∪ 𝐴)) |
| 189 | 188 | ex 412 |
. . . . . . . . . 10
⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → 0 = (vol‘∪ 𝐴))) |
| 190 | 38, 189 | sylbid 240 |
. . . . . . . . 9
⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → 0 =
(vol‘∪ 𝐴))) |
| 191 | 28, 190 | syl5 34 |
. . . . . . . 8
⊢ (𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ) → 0 = (vol‘∪ 𝐴))) |
| 192 | 191 | exlimiv 1930 |
. . . . . . 7
⊢
(∃𝑔 𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ) → 0 = (vol‘∪ 𝐴))) |
| 193 | 18, 192 | syl 17 |
. . . . . 6
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) →
((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ) → 0 = (vol‘∪ 𝐴))) |
| 194 | 193 | expimpd 453 |
. . . . 5
⊢ (𝐴 ≠ ∅ → ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol‘∪ 𝐴))) |
| 195 | 11, 194 | pm2.61ine 3025 |
. . . 4
⊢ ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol‘∪ 𝐴)) |
| 196 | | renepnf 11309 |
. . . . . . 7
⊢ (0 ∈
ℝ → 0 ≠ +∞) |
| 197 | 47, 196 | mp1i 13 |
. . . . . 6
⊢ (∪ 𝐴 =
ℝ → 0 ≠ +∞) |
| 198 | | fveq2 6906 |
. . . . . . 7
⊢ (∪ 𝐴 =
ℝ → (vol‘∪ 𝐴) = (vol‘ℝ)) |
| 199 | | rembl 25575 |
. . . . . . . . 9
⊢ ℝ
∈ dom vol |
| 200 | | mblvol 25565 |
. . . . . . . . 9
⊢ (ℝ
∈ dom vol → (vol‘ℝ) =
(vol*‘ℝ)) |
| 201 | 199, 200 | ax-mp 5 |
. . . . . . . 8
⊢
(vol‘ℝ) = (vol*‘ℝ) |
| 202 | | ovolre 25560 |
. . . . . . . 8
⊢
(vol*‘ℝ) = +∞ |
| 203 | 201, 202 | eqtri 2765 |
. . . . . . 7
⊢
(vol‘ℝ) = +∞ |
| 204 | 198, 203 | eqtrdi 2793 |
. . . . . 6
⊢ (∪ 𝐴 =
ℝ → (vol‘∪ 𝐴) = +∞) |
| 205 | 197, 204 | neeqtrrd 3015 |
. . . . 5
⊢ (∪ 𝐴 =
ℝ → 0 ≠ (vol‘∪ 𝐴)) |
| 206 | 205 | necon2i 2975 |
. . . 4
⊢ (0 =
(vol‘∪ 𝐴) → ∪ 𝐴 ≠ ℝ) |
| 207 | 195, 206 | syl 17 |
. . 3
⊢ ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → ∪ 𝐴 ≠ ℝ) |
| 208 | 207 | expr 456 |
. 2
⊢ ((𝐴 ≼ ℕ ∧
∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → (∪ 𝐴
⊆ ℝ → ∪ 𝐴 ≠ ℝ)) |
| 209 | | eqimss 4042 |
. . 3
⊢ (∪ 𝐴 =
ℝ → ∪ 𝐴 ⊆ ℝ) |
| 210 | 209 | necon3bi 2967 |
. 2
⊢ (¬
∪ 𝐴 ⊆ ℝ → ∪ 𝐴
≠ ℝ) |
| 211 | 208, 210 | pm2.61d1 180 |
1
⊢ ((𝐴 ≼ ℕ ∧
∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴
≠ ℝ) |