Step | Hyp | Ref
| Expression |
1 | | unieq 4830 |
. . . . . . . . 9
⊢ (𝐴 = ∅ → ∪ 𝐴 =
∪ ∅) |
2 | | uni0 4849 |
. . . . . . . . 9
⊢ ∪ ∅ = ∅ |
3 | 1, 2 | eqtrdi 2794 |
. . . . . . . 8
⊢ (𝐴 = ∅ → ∪ 𝐴 =
∅) |
4 | 3 | fveq2d 6721 |
. . . . . . 7
⊢ (𝐴 = ∅ →
(vol‘∪ 𝐴) = (vol‘∅)) |
5 | | 0mbl 24436 |
. . . . . . . . 9
⊢ ∅
∈ dom vol |
6 | | mblvol 24427 |
. . . . . . . . 9
⊢ (∅
∈ dom vol → (vol‘∅) =
(vol*‘∅)) |
7 | 5, 6 | ax-mp 5 |
. . . . . . . 8
⊢
(vol‘∅) = (vol*‘∅) |
8 | | ovol0 24390 |
. . . . . . . 8
⊢
(vol*‘∅) = 0 |
9 | 7, 8 | eqtri 2765 |
. . . . . . 7
⊢
(vol‘∅) = 0 |
10 | 4, 9 | eqtr2di 2795 |
. . . . . 6
⊢ (𝐴 = ∅ → 0 =
(vol‘∪ 𝐴)) |
11 | 10 | a1d 25 |
. . . . 5
⊢ (𝐴 = ∅ → ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol‘∪ 𝐴))) |
12 | | reldom 8632 |
. . . . . . . . . . 11
⊢ Rel
≼ |
13 | 12 | brrelex1i 5605 |
. . . . . . . . . 10
⊢ (𝐴 ≼ ℕ → 𝐴 ∈ V) |
14 | | 0sdomg 8775 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ≼ ℕ → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
16 | 15 | biimparc 483 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∅
≺ 𝐴) |
17 | | fodomr 8797 |
. . . . . . . 8
⊢ ((∅
≺ 𝐴 ∧ 𝐴 ≼ ℕ) →
∃𝑔 𝑔:ℕ–onto→𝐴) |
18 | 16, 17 | sylancom 591 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) →
∃𝑔 𝑔:ℕ–onto→𝐴) |
19 | | unissb 4853 |
. . . . . . . . . . . . 13
⊢ (∪ 𝐴
⊆ ℝ ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ) |
20 | 19 | anbi1i 627 |
. . . . . . . . . . . 12
⊢ ((∪ 𝐴
⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ)) |
21 | | r19.26 3092 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ)) |
22 | 20, 21 | bitr4i 281 |
. . . . . . . . . . 11
⊢ ((∪ 𝐴
⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ)) |
23 | | ovolctb2 24389 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) →
(vol*‘𝑥) =
0) |
24 | 23 | ex 416 |
. . . . . . . . . . . . 13
⊢ (𝑥 ⊆ ℝ → (𝑥 ≼ ℕ →
(vol*‘𝑥) =
0)) |
25 | 24 | imdistani 572 |
. . . . . . . . . . . 12
⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) =
0)) |
26 | 25 | ralimi 3083 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)) |
27 | 22, 26 | sylbi 220 |
. . . . . . . . . 10
⊢ ((∪ 𝐴
⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)) |
28 | 27 | ancoms 462 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)) |
29 | | foima 6638 |
. . . . . . . . . . . 12
⊢ (𝑔:ℕ–onto→𝐴 → (𝑔 “ ℕ) = 𝐴) |
30 | 29 | raleqdv 3325 |
. . . . . . . . . . 11
⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))) |
31 | | fofn 6635 |
. . . . . . . . . . . 12
⊢ (𝑔:ℕ–onto→𝐴 → 𝑔 Fn ℕ) |
32 | | ssid 3923 |
. . . . . . . . . . . 12
⊢ ℕ
⊆ ℕ |
33 | | sseq1 3926 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑔‘𝑚) → (𝑥 ⊆ ℝ ↔ (𝑔‘𝑚) ⊆ ℝ)) |
34 | | fveqeq2 6726 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑔‘𝑚) → ((vol*‘𝑥) = 0 ↔ (vol*‘(𝑔‘𝑚)) = 0)) |
35 | 33, 34 | anbi12d 634 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑔‘𝑚) → ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0))) |
36 | 35 | ralima 7054 |
. . . . . . . . . . . 12
⊢ ((𝑔 Fn ℕ ∧ ℕ
⊆ ℕ) → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0))) |
37 | 31, 32, 36 | sylancl 589 |
. . . . . . . . . . 11
⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0))) |
38 | 30, 37 | bitr3d 284 |
. . . . . . . . . 10
⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0))) |
39 | | difss 4046 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ (𝑔‘𝑚) |
40 | | ovolssnul 24384 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ (𝑔‘𝑚) ∧ (𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) |
41 | 39, 40 | mp3an1 1450 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) |
42 | | ssdifss 4050 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔‘𝑚) ⊆ ℝ → ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ) |
43 | | nulmbl 24432 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol) |
44 | | mblvol 24427 |
. . . . . . . . . . . . . . . . . . . . . . . . 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 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) |
47 | | 0re 10835 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
ℝ |
48 | 46, 47 | eqeltrdi 2846 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ) |
49 | 48 | expcom 417 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0 → (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)) |
50 | 49 | ancld 554 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0 → (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))) |
51 | 50 | adantl 485 |
. . . . . . . . . . . . . . . . . . 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 583 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)) |
54 | 41, 53 | syldan 594 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)) |
55 | 54 | ralimi 3083 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) → ∀𝑚 ∈ ℕ (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)) |
56 | | fveq2 6717 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → (𝑔‘𝑚) = (𝑔‘𝑛)) |
57 | | oveq2 7221 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑛 → (1..^𝑚) = (1..^𝑛)) |
58 | 57 | iuneq1d 4931 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) |
59 | 56, 58 | difeq12d 4038 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑛 → ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) = ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) |
60 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) |
61 | | fvex 6730 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔‘𝑛) ∈ V |
62 | | difexg 5220 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑔‘𝑛) ∈ V → ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ V) |
63 | 61, 62 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ V |
64 | 59, 60, 63 | fvmpt 6818 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) = ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) |
65 | 64 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ↔ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol)) |
66 | 64 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ →
(vol‘((𝑚 ∈
ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) |
67 | 66 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ →
((vol‘((𝑚 ∈
ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ ↔ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ)) |
68 | 65, 67 | anbi12d 634 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → ((((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ↔ (((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ))) |
69 | 68 | ralbiia 3087 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
ℕ (((𝑚 ∈ ℕ
↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ↔ ∀𝑛 ∈ ℕ (((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ)) |
70 | | fveq2 6717 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑚 → (𝑔‘𝑛) = (𝑔‘𝑚)) |
71 | | oveq2 7221 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑚 → (1..^𝑛) = (1..^𝑚)) |
72 | 71 | iuneq1d 4931 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑚 → ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) |
73 | 70, 72 | difeq12d 4038 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑚 → ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) = ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) |
74 | 73 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑚 → (((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ↔ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol)) |
75 | 73 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑚 → (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))) |
76 | 75 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑚 → ((vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ ↔ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)) |
77 | 74, 76 | anbi12d 634 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑚 → ((((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ) ↔ (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))) |
78 | 77 | cbvralvw 3358 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
ℕ (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ) ↔ ∀𝑚 ∈ ℕ (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)) |
79 | 69, 78 | bitri 278 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑛 ∈
ℕ (((𝑚 ∈ ℕ
↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ↔ ∀𝑚 ∈ ℕ (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)) |
80 | 55, 79 | sylibr 237 |
. . . . . . . . . . . . . 14
⊢
(∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) → ∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ)) |
81 | | fveq2 6717 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑙 → (𝑔‘𝑛) = (𝑔‘𝑙)) |
82 | 81 | iundisj2 24446 |
. . . . . . . . . . . . . . 15
⊢
Disj 𝑛 ∈
ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) |
83 | | disjeq2 5022 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
ℕ ((𝑚 ∈ ℕ
↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) = ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) → (Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) |
84 | 83, 64 | mprg 3075 |
. . . . . . . . . . . . . . 15
⊢
(Disj 𝑛
∈ ℕ ((𝑚 ∈
ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) |
85 | 82, 84 | mpbir 234 |
. . . . . . . . . . . . . 14
⊢
Disj 𝑛 ∈
ℕ ((𝑚 ∈ ℕ
↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) |
86 | | nnex 11836 |
. . . . . . . . . . . . . . . . 17
⊢ ℕ
∈ V |
87 | 86 | mptex 7039 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ V |
88 | | fveq1 6716 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (𝑓‘𝑛) = ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) |
89 | 88 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((𝑓‘𝑛) ∈ dom vol ↔ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol)) |
90 | 88 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (vol‘(𝑓‘𝑛)) = (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))) |
91 | 90 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((vol‘(𝑓‘𝑛)) ∈ ℝ ↔ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ)) |
92 | 89, 91 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ↔ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ))) |
93 | 92 | ralbidv 3118 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ↔ ∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ))) |
94 | 88 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) = ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) |
95 | 94 | disjeq2dv 5023 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (Disj 𝑛 ∈ ℕ (𝑓‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))) |
96 | 93, 95 | anbi12d 634 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)) ↔ (∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))) |
97 | 88 | iuneq2d 4933 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ∪ 𝑛 ∈ ℕ (𝑓‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) |
98 | 97 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))) |
99 | | voliunnfl.1 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑆 = seq1( + , 𝐺) |
100 | | voliunnfl.2 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))) |
101 | | seqeq3 13579 |
. . . . . . . . . . . . . . . . . . . . . . 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 5806 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ran 𝑆 = ran seq1( + , (𝑛 ∈ ℕ ↦
(vol‘(𝑓‘𝑛)))) |
105 | 104 | supeq1i 9063 |
. . . . . . . . . . . . . . . . . . 19
⊢ sup(ran
𝑆, ℝ*,
< ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))), ℝ*, <
) |
106 | 90 | mpteq2dv 5151 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))) |
107 | 106 | seqeq3d 13582 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))))) |
108 | 107 | rneqd 5807 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))) = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))))) |
109 | 108 | supeq1d 9062 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦
(vol‘(𝑓‘𝑛)))), ℝ*, <
) = sup(ran seq1( + , (𝑛
∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, <
)) |
110 | 105, 109 | syl5eq 2790 |
. . . . . . . . . . . . . . . . . 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 348 |
. . . . . . . . . . . . . . . 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 3474 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑛 ∈
ℕ (((𝑚 ∈ ℕ
↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, <
)) |
115 | 64 | iuneq2i 4925 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) |
116 | 115 | fveq2i 6720 |
. . . . . . . . . . . . . . 15
⊢
(vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) |
117 | 66 | mpteq2ia 5146 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ ↦
(vol‘((𝑚 ∈
ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) |
118 | | seqeq3 13579 |
. . . . . . . . . . . . . . . . . 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 5806 |
. . . . . . . . . . . . . . . 16
⊢ ran seq1(
+ , (𝑛 ∈ ℕ
↦ (vol‘((𝑚
∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))) = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))) |
121 | 120 | supeq1i 9063 |
. . . . . . . . . . . . . . 15
⊢ sup(ran
seq1( + , (𝑛 ∈ ℕ
↦ (vol‘((𝑚
∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ) = sup(ran
seq1( + , (𝑛 ∈ ℕ
↦ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, <
) |
122 | 114, 116,
121 | 3eqtr3g 2801 |
. . . . . . . . . . . . . 14
⊢
((∀𝑛 ∈
ℕ (((𝑚 ∈ ℕ
↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, <
)) |
123 | 80, 85, 122 | sylancl 589 |
. . . . . . . . . . . . 13
⊢
(∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) →
(vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, <
)) |
124 | 123 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, <
)) |
125 | 81 | iundisj 24445 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) |
126 | | fofun 6634 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔:ℕ–onto→𝐴 → Fun 𝑔) |
127 | | funiunfv 7061 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
𝑔 → ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) = ∪ (𝑔 “
ℕ)) |
128 | 126, 127 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔:ℕ–onto→𝐴 → ∪
𝑛 ∈ ℕ (𝑔‘𝑛) = ∪ (𝑔 “
ℕ)) |
129 | 125, 128 | eqtr3id 2792 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:ℕ–onto→𝐴 → ∪
𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) = ∪ (𝑔 “
ℕ)) |
130 | 29 | unieqd 4833 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:ℕ–onto→𝐴 → ∪ (𝑔 “ ℕ) = ∪ 𝐴) |
131 | 129, 130 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (𝑔:ℕ–onto→𝐴 → ∪
𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) = ∪ 𝐴) |
132 | 131 | fveq2d 6721 |
. . . . . . . . . . . . 13
⊢ (𝑔:ℕ–onto→𝐴 → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol‘∪
𝐴)) |
133 | 132 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol‘∪
𝐴)) |
134 | 56 | sseq1d 3932 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → ((𝑔‘𝑚) ⊆ ℝ ↔ (𝑔‘𝑛) ⊆ ℝ)) |
135 | 56 | fveqeq2d 6725 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → ((vol*‘(𝑔‘𝑚)) = 0 ↔ (vol*‘(𝑔‘𝑛)) = 0)) |
136 | 134, 135 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑛 → (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) ↔ ((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0))) |
137 | 136 | rspccva 3536 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) ∧ 𝑛 ∈ ℕ) → ((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0)) |
138 | | ssdifss 4050 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔‘𝑛) ⊆ ℝ → ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ) |
139 | 138 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ) |
140 | | difss 4046 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ (𝑔‘𝑛) |
141 | | ovolssnul 24384 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol*‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0) |
142 | 140, 141 | mp3an1 1450 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol*‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0) |
143 | 139, 142 | jca 515 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0)) |
144 | | nulmbl 24432 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0) → ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol) |
145 | | mblvol 24427 |
. . . . . . . . . . . . . . . . . . . . 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 5150 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) → (𝑛 ∈ ℕ ↦
(vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) = (𝑛 ∈ ℕ ↦ 0)) |
150 | 149 | seqeq3d 13582 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) → seq1( + , (𝑛 ∈ ℕ ↦
(vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))) = seq1( + , (𝑛 ∈ ℕ ↦ 0))) |
151 | 150 | rneqd 5807 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) → ran seq1( + ,
(𝑛 ∈ ℕ ↦
(vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))) = ran seq1( + , (𝑛 ∈ ℕ ↦ 0))) |
152 | 151 | supeq1d 9062 |
. . . . . . . . . . . . . 14
⊢
(∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) → sup(ran seq1( + ,
(𝑛 ∈ ℕ ↦
(vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ) = sup(ran
seq1( + , (𝑛 ∈ ℕ
↦ 0)), ℝ*, < )) |
153 | | 0cn 10825 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
ℂ |
154 | | ser1const 13632 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((0
∈ ℂ ∧ 𝑚
∈ ℕ) → (seq1( + , (ℕ × {0}))‘𝑚) = (𝑚 · 0)) |
155 | 153, 154 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ ℕ → (seq1( +
, (ℕ × {0}))‘𝑚) = (𝑚 · 0)) |
156 | | nncn 11838 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℂ) |
157 | 156 | mul01d 11031 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ ℕ → (𝑚 · 0) =
0) |
158 | 155, 157 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ ℕ → (seq1( +
, (ℕ × {0}))‘𝑚) = 0) |
159 | 158 | mpteq2ia 5146 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ ℕ ↦ (seq1( +
, (ℕ × {0}))‘𝑚)) = (𝑚 ∈ ℕ ↦ 0) |
160 | | fconstmpt 5611 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℕ
× {0}) = (𝑛 ∈
ℕ ↦ 0) |
161 | | seqeq3 13579 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((ℕ
× {0}) = (𝑛 ∈
ℕ ↦ 0) → seq1( + , (ℕ × {0})) = seq1( + , (𝑛 ∈ ℕ ↦
0))) |
162 | 160, 161 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ seq1( + ,
(ℕ × {0})) = seq1( + , (𝑛 ∈ ℕ ↦ 0)) |
163 | | 1z 12207 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
ℤ |
164 | | seqfn 13586 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1 ∈
ℤ → seq1( + , (ℕ × {0})) Fn
(ℤ≥‘1)) |
165 | 163, 164 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ seq1( + ,
(ℕ × {0})) Fn (ℤ≥‘1) |
166 | | nnuz 12477 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ℕ =
(ℤ≥‘1) |
167 | 166 | fneq2i 6477 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (seq1( +
, (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) Fn
(ℤ≥‘1)) |
168 | | dffn5 6771 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (seq1( +
, (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) =
(𝑚 ∈ ℕ ↦
(seq1( + , (ℕ × {0}))‘𝑚))) |
169 | 167, 168 | bitr3i 280 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (seq1( +
, (ℕ × {0})) Fn (ℤ≥‘1) ↔ seq1( + ,
(ℕ × {0})) = (𝑚
∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚))) |
170 | 165, 169 | mpbi 233 |
. . . . . . . . . . . . . . . . . . . 20
⊢ seq1( + ,
(ℕ × {0})) = (𝑚
∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚)) |
171 | 162, 170 | eqtr3i 2767 |
. . . . . . . . . . . . . . . . . . 19
⊢ seq1( + ,
(𝑛 ∈ ℕ ↦
0)) = (𝑚 ∈ ℕ
↦ (seq1( + , (ℕ × {0}))‘𝑚)) |
172 | | fconstmpt 5611 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℕ
× {0}) = (𝑚 ∈
ℕ ↦ 0) |
173 | 159, 171,
172 | 3eqtr4i 2775 |
. . . . . . . . . . . . . . . . . 18
⊢ seq1( + ,
(𝑛 ∈ ℕ ↦
0)) = (ℕ × {0}) |
174 | 173 | rneqi 5806 |
. . . . . . . . . . . . . . . . 17
⊢ ran seq1(
+ , (𝑛 ∈ ℕ
↦ 0)) = ran (ℕ × {0}) |
175 | | 1nn 11841 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℕ |
176 | | ne0i 4249 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
ℕ → ℕ ≠ ∅) |
177 | | rnxp 6033 |
. . . . . . . . . . . . . . . . . 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 9063 |
. . . . . . . . . . . . . . 15
⊢ sup(ran
seq1( + , (𝑛 ∈ ℕ
↦ 0)), ℝ*, < ) = sup({0}, ℝ*, <
) |
181 | | xrltso 12731 |
. . . . . . . . . . . . . . . 16
⊢ < Or
ℝ* |
182 | | 0xr 10880 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ* |
183 | | supsn 9088 |
. . . . . . . . . . . . . . . 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 2794 |
. . . . . . . . . . . . 13
⊢
(∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) → sup(ran seq1( + ,
(𝑛 ∈ ℕ ↦
(vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ) =
0) |
187 | 186 | adantl 485 |
. . . . . . . . . . . 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 416 |
. . . . . . . . . 10
⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → 0 = (vol‘∪ 𝐴))) |
190 | 38, 189 | sylbid 243 |
. . . . . . . . 9
⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → 0 =
(vol‘∪ 𝐴))) |
191 | 28, 190 | syl5 34 |
. . . . . . . 8
⊢ (𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ) → 0 = (vol‘∪ 𝐴))) |
192 | 191 | exlimiv 1938 |
. . . . . . 7
⊢
(∃𝑔 𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ) → 0 = (vol‘∪ 𝐴))) |
193 | 18, 192 | syl 17 |
. . . . . 6
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) →
((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ) → 0 = (vol‘∪ 𝐴))) |
194 | 193 | expimpd 457 |
. . . . 5
⊢ (𝐴 ≠ ∅ → ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol‘∪ 𝐴))) |
195 | 11, 194 | pm2.61ine 3025 |
. . . 4
⊢ ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol‘∪ 𝐴)) |
196 | | renepnf 10881 |
. . . . . . 7
⊢ (0 ∈
ℝ → 0 ≠ +∞) |
197 | 47, 196 | mp1i 13 |
. . . . . 6
⊢ (∪ 𝐴 =
ℝ → 0 ≠ +∞) |
198 | | fveq2 6717 |
. . . . . . 7
⊢ (∪ 𝐴 =
ℝ → (vol‘∪ 𝐴) = (vol‘ℝ)) |
199 | | rembl 24437 |
. . . . . . . . 9
⊢ ℝ
∈ dom vol |
200 | | mblvol 24427 |
. . . . . . . . 9
⊢ (ℝ
∈ dom vol → (vol‘ℝ) =
(vol*‘ℝ)) |
201 | 199, 200 | ax-mp 5 |
. . . . . . . 8
⊢
(vol‘ℝ) = (vol*‘ℝ) |
202 | | ovolre 24422 |
. . . . . . . 8
⊢
(vol*‘ℝ) = +∞ |
203 | 201, 202 | eqtri 2765 |
. . . . . . 7
⊢
(vol‘ℝ) = +∞ |
204 | 198, 203 | eqtrdi 2794 |
. . . . . 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 460 |
. 2
⊢ ((𝐴 ≼ ℕ ∧
∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → (∪ 𝐴
⊆ ℝ → ∪ 𝐴 ≠ ℝ)) |
209 | | eqimss 3957 |
. . 3
⊢ (∪ 𝐴 =
ℝ → ∪ 𝐴 ⊆ ℝ) |
210 | 209 | necon3bi 2967 |
. 2
⊢ (¬
∪ 𝐴 ⊆ ℝ → ∪ 𝐴
≠ ℝ) |
211 | 208, 210 | pm2.61d1 183 |
1
⊢ ((𝐴 ≼ ℕ ∧
∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴
≠ ℝ) |