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 | | 0mbl 23307 |
. . . . . . . . 9
⊢ ∅
∈ dom vol |
6 | | mblvol 23298 |
. . . . . . . . 9
⊢ (∅
∈ dom vol → (vol‘∅) =
(vol*‘∅)) |
7 | 5, 6 | ax-mp 5 |
. . . . . . . 8
⊢
(vol‘∅) = (vol*‘∅) |
8 | | ovol0 23261 |
. . . . . . . 8
⊢
(vol*‘∅) = 0 |
9 | 7, 8 | eqtri 2644 |
. . . . . . 7
⊢
(vol‘∅) = 0 |
10 | 4, 9 | syl6req 2673 |
. . . . . 6
⊢ (𝐴 = ∅ → 0 =
(vol‘∪ 𝐴)) |
11 | 10 | a1d 25 |
. . . . 5
⊢ (𝐴 = ∅ → ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol‘∪ 𝐴))) |
12 | | reldom 7961 |
. . . . . . . . . . 11
⊢ Rel
≼ |
13 | 12 | brrelexi 5158 |
. . . . . . . . . 10
⊢ (𝐴 ≼ ℕ → 𝐴 ∈ V) |
14 | | 0sdomg 8089 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ≼ ℕ → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
16 | 15 | biimparc 504 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∅
≺ 𝐴) |
17 | | fodomr 8111 |
. . . . . . . 8
⊢ ((∅
≺ 𝐴 ∧ 𝐴 ≼ ℕ) →
∃𝑔 𝑔:ℕ–onto→𝐴) |
18 | 16, 17 | sylancom 701 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) →
∃𝑔 𝑔:ℕ–onto→𝐴) |
19 | | unissb 4469 |
. . . . . . . . . . . . 13
⊢ (∪ 𝐴
⊆ ℝ ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ) |
20 | 19 | anbi1i 731 |
. . . . . . . . . . . 12
⊢ ((∪ 𝐴
⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ)) |
21 | | r19.26 3064 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ)) |
22 | 20, 21 | bitr4i 267 |
. . . . . . . . . . 11
⊢ ((∪ 𝐴
⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ)) |
23 | | ovolctb2 23260 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) →
(vol*‘𝑥) =
0) |
24 | 23 | ex 450 |
. . . . . . . . . . . . 13
⊢ (𝑥 ⊆ ℝ → (𝑥 ≼ ℕ →
(vol*‘𝑥) =
0)) |
25 | 24 | imdistani 726 |
. . . . . . . . . . . 12
⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) =
0)) |
26 | 25 | ralimi 2952 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)) |
27 | 22, 26 | sylbi 207 |
. . . . . . . . . 10
⊢ ((∪ 𝐴
⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)) |
28 | 27 | ancoms 469 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0)) |
29 | | foima 6120 |
. . . . . . . . . . . 12
⊢ (𝑔:ℕ–onto→𝐴 → (𝑔 “ ℕ) = 𝐴) |
30 | 29 | raleqdv 3144 |
. . . . . . . . . . 11
⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0))) |
31 | | fofn 6117 |
. . . . . . . . . . . 12
⊢ (𝑔:ℕ–onto→𝐴 → 𝑔 Fn ℕ) |
32 | | ssid 3624 |
. . . . . . . . . . . 12
⊢ ℕ
⊆ ℕ |
33 | | sseq1 3626 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑔‘𝑚) → (𝑥 ⊆ ℝ ↔ (𝑔‘𝑚) ⊆ ℝ)) |
34 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑔‘𝑚) → (vol*‘𝑥) = (vol*‘(𝑔‘𝑚))) |
35 | 34 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑔‘𝑚) → ((vol*‘𝑥) = 0 ↔ (vol*‘(𝑔‘𝑚)) = 0)) |
36 | 33, 35 | anbi12d 747 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑔‘𝑚) → ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0))) |
37 | 36 | ralima 6498 |
. . . . . . . . . . . 12
⊢ ((𝑔 Fn ℕ ∧ ℕ
⊆ ℕ) → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0))) |
38 | 31, 32, 37 | sylancl 694 |
. . . . . . . . . . 11
⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0))) |
39 | 30, 38 | bitr3d 270 |
. . . . . . . . . 10
⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) ↔ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0))) |
40 | | difss 3737 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ (𝑔‘𝑚) |
41 | | ovolssnul 23255 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ (𝑔‘𝑚) ∧ (𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) |
42 | 40, 41 | mp3an1 1411 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) |
43 | | ssdifss 3741 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔‘𝑚) ⊆ ℝ → ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ) |
44 | | nulmbl 23303 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol) |
45 | | mblvol 23298 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))) |
46 | 45 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → ((vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0 ↔ (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0)) |
47 | 46 | biimpar 502 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) |
48 | | 0re 10040 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
ℝ |
49 | 47, 48 | syl6eqel 2709 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ) |
50 | 49 | expcom 451 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0 → (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)) |
51 | 50 | ancld 576 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0 → (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))) |
52 | 51 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol → (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))) |
53 | 44, 52 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)) |
54 | 43, 53 | sylan 488 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = 0) → (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)) |
55 | 42, 54 | syldan 487 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)) |
56 | 55 | ralimi 2952 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) → ∀𝑚 ∈ ℕ (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)) |
57 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → (𝑔‘𝑚) = (𝑔‘𝑛)) |
58 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑛 → (1..^𝑚) = (1..^𝑛)) |
59 | 58 | iuneq1d 4545 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) |
60 | 57, 59 | difeq12d 3729 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑛 → ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) = ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) |
61 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) |
62 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔‘𝑛) ∈ V |
63 | | difexg 4808 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑔‘𝑛) ∈ V → ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ V) |
64 | 62, 63 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ V |
65 | 60, 61, 64 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) = ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) |
66 | 65 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ↔ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol)) |
67 | 65 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ →
(vol‘((𝑚 ∈
ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) |
68 | 67 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ →
((vol‘((𝑚 ∈
ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ ↔ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ)) |
69 | 66, 68 | anbi12d 747 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → ((((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ↔ (((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ))) |
70 | 69 | ralbiia 2979 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
ℕ (((𝑚 ∈ ℕ
↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ↔ ∀𝑛 ∈ ℕ (((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ)) |
71 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑚 → (𝑔‘𝑛) = (𝑔‘𝑚)) |
72 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑚 → (1..^𝑛) = (1..^𝑚)) |
73 | 72 | iuneq1d 4545 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑚 → ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) |
74 | 71, 73 | difeq12d 3729 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑚 → ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) = ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) |
75 | 74 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑚 → (((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ↔ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol)) |
76 | 74 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑚 → (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))) |
77 | 76 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑚 → ((vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ ↔ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)) |
78 | 75, 77 | anbi12d 747 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑚 → ((((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ) ↔ (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ))) |
79 | 78 | cbvralv 3171 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
ℕ (((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) ∈ ℝ) ↔ ∀𝑚 ∈ ℕ (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)) |
80 | 70, 79 | bitri 264 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑛 ∈
ℕ (((𝑚 ∈ ℕ
↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ↔ ∀𝑚 ∈ ℕ (((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)) ∈ dom vol ∧ (vol‘((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ ℝ)) |
81 | 56, 80 | sylibr 224 |
. . . . . . . . . . . . . 14
⊢
(∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) → ∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ)) |
82 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑙 → (𝑔‘𝑛) = (𝑔‘𝑙)) |
83 | 82 | iundisj2 23317 |
. . . . . . . . . . . . . . 15
⊢
Disj 𝑛 ∈
ℕ ((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) |
84 | | disjeq2 4624 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
ℕ ((𝑚 ∈ ℕ
↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) = ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) → (Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) |
85 | 84, 65 | mprg 2926 |
. . . . . . . . . . . . . . 15
⊢
(Disj 𝑛
∈ ℕ ((𝑚 ∈
ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) |
86 | 83, 85 | mpbir 221 |
. . . . . . . . . . . . . 14
⊢
Disj 𝑛 ∈
ℕ ((𝑚 ∈ ℕ
↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) |
87 | | nnex 11026 |
. . . . . . . . . . . . . . . . 17
⊢ ℕ
∈ V |
88 | 87 | mptex 6486 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∈ V |
89 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (𝑓‘𝑛) = ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) |
90 | 89 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((𝑓‘𝑛) ∈ dom vol ↔ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol)) |
91 | 89 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (vol‘(𝑓‘𝑛)) = (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))) |
92 | 91 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((vol‘(𝑓‘𝑛)) ∈ ℝ ↔ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ)) |
93 | 90, 92 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ↔ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ))) |
94 | 93 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ↔ ∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ))) |
95 | 89 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) = ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) |
96 | 95 | disjeq2dv 4625 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (Disj 𝑛 ∈ ℕ (𝑓‘𝑛) ↔ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))) |
97 | 94, 96 | anbi12d 747 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)) ↔ (∀𝑛 ∈ ℕ (((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))) |
98 | 89 | iuneq2d 4547 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ∪ 𝑛 ∈ ℕ (𝑓‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) |
99 | 98 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))) |
100 | | voliunnfl.1 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑆 = seq1( + , 𝐺) |
101 | | voliunnfl.2 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))) |
102 | | seqeq3 12806 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))) → seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))))) |
103 | 101, 102 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ seq1( + ,
𝐺) = seq1( + , (𝑛 ∈ ℕ ↦
(vol‘(𝑓‘𝑛)))) |
104 | 100, 103 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑆 = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))) |
105 | 104 | rneqi 5352 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ran 𝑆 = ran seq1( + , (𝑛 ∈ ℕ ↦
(vol‘(𝑓‘𝑛)))) |
106 | 105 | supeq1i 8353 |
. . . . . . . . . . . . . . . . . . 19
⊢ sup(ran
𝑆, ℝ*,
< ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))), ℝ*, <
) |
107 | 91 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))) |
108 | 107 | seqeq3d 12809 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))))) |
109 | 108 | rneqd 5353 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘(𝑓‘𝑛)))) = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))))) |
110 | 109 | supeq1d 8352 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦
(vol‘(𝑓‘𝑛)))), ℝ*, <
) = sup(ran seq1( + , (𝑛
∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, <
)) |
111 | 106, 110 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → sup(ran 𝑆, ℝ*, < ) = sup(ran
seq1( + , (𝑛 ∈ ℕ
↦ (vol‘((𝑚
∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, <
)) |
112 | 99, 111 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → ((vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = sup(ran 𝑆, ℝ*, < ) ↔
(vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, <
))) |
113 | 97, 112 | imbi12d 334 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙))) → (((∀𝑛 ∈ ℕ ((𝑓‘𝑛) ∈ dom vol ∧ (vol‘(𝑓‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = sup(ran 𝑆, ℝ*, < )) ↔
((∀𝑛 ∈ ℕ
(((𝑚 ∈ ℕ ↦
((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, <
)))) |
114 | | voliunnfl.3 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑛 ∈
ℕ ((𝑓‘𝑛) ∈ dom vol ∧
(vol‘(𝑓‘𝑛)) ∈ ℝ) ∧
Disj 𝑛 ∈
ℕ (𝑓‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ (𝑓‘𝑛)) = sup(ran 𝑆, ℝ*, <
)) |
115 | 88, 113, 114 | vtocl 3259 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑛 ∈
ℕ (((𝑚 ∈ ℕ
↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, <
)) |
116 | 65 | iuneq2i 4539 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) |
117 | 116 | fveq2i 6194 |
. . . . . . . . . . . . . . 15
⊢
(vol‘∪ 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) = (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) |
118 | 67 | mpteq2ia 4740 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ ↦
(vol‘((𝑚 ∈
ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) |
119 | | seqeq3 12806 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℕ ↦
(vol‘((𝑚 ∈
ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) → seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))))) |
120 | 118, 119 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ seq1( + ,
(𝑛 ∈ ℕ ↦
(vol‘((𝑚 ∈
ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))) |
121 | 120 | rneqi 5352 |
. . . . . . . . . . . . . . . 16
⊢ ran seq1(
+ , (𝑛 ∈ ℕ
↦ (vol‘((𝑚
∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))) = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))) |
122 | 121 | supeq1i 8353 |
. . . . . . . . . . . . . . 15
⊢ sup(ran
seq1( + , (𝑛 ∈ ℕ
↦ (vol‘((𝑚
∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)))), ℝ*, < ) = sup(ran
seq1( + , (𝑛 ∈ ℕ
↦ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, <
) |
123 | 115, 117,
122 | 3eqtr3g 2679 |
. . . . . . . . . . . . . 14
⊢
((∀𝑛 ∈
ℕ (((𝑚 ∈ ℕ
↦ ((𝑔‘𝑚) ∖ ∪ 𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛) ∈ dom vol ∧ (vol‘((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ((𝑔‘𝑚) ∖ ∪
𝑙 ∈ (1..^𝑚)(𝑔‘𝑙)))‘𝑛)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, <
)) |
124 | 81, 86, 123 | sylancl 694 |
. . . . . . . . . . . . 13
⊢
(∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) →
(vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, <
)) |
125 | 124 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, <
)) |
126 | 82 | iundisj 23316 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) |
127 | | fofun 6116 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔:ℕ–onto→𝐴 → Fun 𝑔) |
128 | | funiunfv 6506 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
𝑔 → ∪ 𝑛 ∈ ℕ (𝑔‘𝑛) = ∪ (𝑔 “
ℕ)) |
129 | 127, 128 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔:ℕ–onto→𝐴 → ∪
𝑛 ∈ ℕ (𝑔‘𝑛) = ∪ (𝑔 “
ℕ)) |
130 | 126, 129 | syl5eqr 2670 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:ℕ–onto→𝐴 → ∪
𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) = ∪ (𝑔 “
ℕ)) |
131 | 29 | unieqd 4446 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:ℕ–onto→𝐴 → ∪ (𝑔 “ ℕ) = ∪ 𝐴) |
132 | 130, 131 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ (𝑔:ℕ–onto→𝐴 → ∪
𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) = ∪ 𝐴) |
133 | 132 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑔:ℕ–onto→𝐴 → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol‘∪
𝐴)) |
134 | 133 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → (vol‘∪ 𝑛 ∈ ℕ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol‘∪
𝐴)) |
135 | 57 | sseq1d 3632 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → ((𝑔‘𝑚) ⊆ ℝ ↔ (𝑔‘𝑛) ⊆ ℝ)) |
136 | 57 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑛 → (vol*‘(𝑔‘𝑚)) = (vol*‘(𝑔‘𝑛))) |
137 | 136 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → ((vol*‘(𝑔‘𝑚)) = 0 ↔ (vol*‘(𝑔‘𝑛)) = 0)) |
138 | 135, 137 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑛 → (((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) ↔ ((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0))) |
139 | 138 | rspccva 3308 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) ∧ 𝑛 ∈ ℕ) → ((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0)) |
140 | | ssdifss 3741 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔‘𝑛) ⊆ ℝ → ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ) |
141 | 140 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ) |
142 | | difss 3737 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ (𝑔‘𝑛) |
143 | | ovolssnul 23255 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol*‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0) |
144 | 142, 143 | mp3an1 1411 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol*‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0) |
145 | 141, 144 | jca 554 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0)) |
146 | | nulmbl 23303 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ⊆ ℝ ∧ (vol*‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0) → ((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol) |
147 | | mblvol 23298 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)) ∈ dom vol → (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol*‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) |
148 | 145, 146,
147 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = (vol*‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) |
149 | 148, 144 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑔‘𝑛) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑛)) = 0) → (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0) |
150 | 139, 149 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) ∧ 𝑛 ∈ ℕ) → (vol‘((𝑔‘𝑛) ∖ ∪
𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))) = 0) |
151 | 150 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) → (𝑛 ∈ ℕ ↦
(vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙)))) = (𝑛 ∈ ℕ ↦ 0)) |
152 | 151 | seqeq3d 12809 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) → seq1( + , (𝑛 ∈ ℕ ↦
(vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))) = seq1( + , (𝑛 ∈ ℕ ↦ 0))) |
153 | 152 | rneqd 5353 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) → ran seq1( + ,
(𝑛 ∈ ℕ ↦
(vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))) = ran seq1( + , (𝑛 ∈ ℕ ↦ 0))) |
154 | 153 | supeq1d 8352 |
. . . . . . . . . . . . . 14
⊢
(∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) → sup(ran seq1( + ,
(𝑛 ∈ ℕ ↦
(vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ) = sup(ran
seq1( + , (𝑛 ∈ ℕ
↦ 0)), ℝ*, < )) |
155 | | 0cn 10032 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
ℂ |
156 | | ser1const 12857 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((0
∈ ℂ ∧ 𝑚
∈ ℕ) → (seq1( + , (ℕ × {0}))‘𝑚) = (𝑚 · 0)) |
157 | 155, 156 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ ℕ → (seq1( +
, (ℕ × {0}))‘𝑚) = (𝑚 · 0)) |
158 | | nncn 11028 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℂ) |
159 | 158 | mul01d 10235 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ ℕ → (𝑚 · 0) =
0) |
160 | 157, 159 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ ℕ → (seq1( +
, (ℕ × {0}))‘𝑚) = 0) |
161 | 160 | mpteq2ia 4740 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ ℕ ↦ (seq1( +
, (ℕ × {0}))‘𝑚)) = (𝑚 ∈ ℕ ↦ 0) |
162 | | fconstmpt 5163 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℕ
× {0}) = (𝑛 ∈
ℕ ↦ 0) |
163 | | seqeq3 12806 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((ℕ
× {0}) = (𝑛 ∈
ℕ ↦ 0) → seq1( + , (ℕ × {0})) = seq1( + , (𝑛 ∈ ℕ ↦
0))) |
164 | 162, 163 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ seq1( + ,
(ℕ × {0})) = seq1( + , (𝑛 ∈ ℕ ↦ 0)) |
165 | | 1z 11407 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
ℤ |
166 | | seqfn 12813 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1 ∈
ℤ → seq1( + , (ℕ × {0})) Fn
(ℤ≥‘1)) |
167 | 165, 166 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ seq1( + ,
(ℕ × {0})) Fn (ℤ≥‘1) |
168 | | nnuz 11723 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ℕ =
(ℤ≥‘1) |
169 | 168 | fneq2i 5986 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (seq1( +
, (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) Fn
(ℤ≥‘1)) |
170 | | dffn5 6241 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (seq1( +
, (ℕ × {0})) Fn ℕ ↔ seq1( + , (ℕ × {0})) =
(𝑚 ∈ ℕ ↦
(seq1( + , (ℕ × {0}))‘𝑚))) |
171 | 169, 170 | bitr3i 266 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (seq1( +
, (ℕ × {0})) Fn (ℤ≥‘1) ↔ seq1( + ,
(ℕ × {0})) = (𝑚
∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚))) |
172 | 167, 171 | mpbi 220 |
. . . . . . . . . . . . . . . . . . . 20
⊢ seq1( + ,
(ℕ × {0})) = (𝑚
∈ ℕ ↦ (seq1( + , (ℕ × {0}))‘𝑚)) |
173 | 164, 172 | eqtr3i 2646 |
. . . . . . . . . . . . . . . . . . 19
⊢ seq1( + ,
(𝑛 ∈ ℕ ↦
0)) = (𝑚 ∈ ℕ
↦ (seq1( + , (ℕ × {0}))‘𝑚)) |
174 | | fconstmpt 5163 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℕ
× {0}) = (𝑚 ∈
ℕ ↦ 0) |
175 | 161, 173,
174 | 3eqtr4i 2654 |
. . . . . . . . . . . . . . . . . 18
⊢ seq1( + ,
(𝑛 ∈ ℕ ↦
0)) = (ℕ × {0}) |
176 | 175 | rneqi 5352 |
. . . . . . . . . . . . . . . . 17
⊢ ran seq1(
+ , (𝑛 ∈ ℕ
↦ 0)) = ran (ℕ × {0}) |
177 | | 1nn 11031 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℕ |
178 | | ne0i 3921 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
ℕ → ℕ ≠ ∅) |
179 | | rnxp 5564 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℕ
≠ ∅ → ran (ℕ × {0}) = {0}) |
180 | 177, 178,
179 | mp2b 10 |
. . . . . . . . . . . . . . . . 17
⊢ ran
(ℕ × {0}) = {0} |
181 | 176, 180 | eqtri 2644 |
. . . . . . . . . . . . . . . 16
⊢ ran seq1(
+ , (𝑛 ∈ ℕ
↦ 0)) = {0} |
182 | 181 | supeq1i 8353 |
. . . . . . . . . . . . . . 15
⊢ sup(ran
seq1( + , (𝑛 ∈ ℕ
↦ 0)), ℝ*, < ) = sup({0}, ℝ*, <
) |
183 | | xrltso 11974 |
. . . . . . . . . . . . . . . 16
⊢ < Or
ℝ* |
184 | | 0xr 10086 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ* |
185 | | supsn 8378 |
. . . . . . . . . . . . . . . 16
⊢ (( <
Or ℝ* ∧ 0 ∈ ℝ*) → sup({0},
ℝ*, < ) = 0) |
186 | 183, 184,
185 | mp2an 708 |
. . . . . . . . . . . . . . 15
⊢ sup({0},
ℝ*, < ) = 0 |
187 | 182, 186 | eqtri 2644 |
. . . . . . . . . . . . . 14
⊢ sup(ran
seq1( + , (𝑛 ∈ ℕ
↦ 0)), ℝ*, < ) = 0 |
188 | 154, 187 | syl6eq 2672 |
. . . . . . . . . . . . 13
⊢
(∀𝑚 ∈
ℕ ((𝑔‘𝑚) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑚)) = 0) → sup(ran seq1( + ,
(𝑛 ∈ ℕ ↦
(vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ) =
0) |
189 | 188 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → sup(ran seq1( + , (𝑛 ∈ ℕ ↦
(vol‘((𝑔‘𝑛) ∖ ∪ 𝑙 ∈ (1..^𝑛)(𝑔‘𝑙))))), ℝ*, < ) =
0) |
190 | 125, 134,
189 | 3eqtr3rd 2665 |
. . . . . . . . . . 11
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0)) → 0 = (vol‘∪ 𝐴)) |
191 | 190 | ex 450 |
. . . . . . . . . 10
⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑚 ∈ ℕ ((𝑔‘𝑚) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑚)) = 0) → 0 = (vol‘∪ 𝐴))) |
192 | 39, 191 | sylbid 230 |
. . . . . . . . 9
⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) = 0) → 0 =
(vol‘∪ 𝐴))) |
193 | 28, 192 | syl5 34 |
. . . . . . . 8
⊢ (𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ) → 0 = (vol‘∪ 𝐴))) |
194 | 193 | exlimiv 1858 |
. . . . . . 7
⊢
(∃𝑔 𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ) → 0 = (vol‘∪ 𝐴))) |
195 | 18, 194 | syl 17 |
. . . . . 6
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) →
((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ) → 0 = (vol‘∪ 𝐴))) |
196 | 195 | expimpd 629 |
. . . . 5
⊢ (𝐴 ≠ ∅ → ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol‘∪ 𝐴))) |
197 | 11, 196 | pm2.61ine 2877 |
. . . 4
⊢ ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol‘∪ 𝐴)) |
198 | | renepnf 10087 |
. . . . . . 7
⊢ (0 ∈
ℝ → 0 ≠ +∞) |
199 | 48, 198 | mp1i 13 |
. . . . . 6
⊢ (∪ 𝐴 =
ℝ → 0 ≠ +∞) |
200 | | fveq2 6191 |
. . . . . . 7
⊢ (∪ 𝐴 =
ℝ → (vol‘∪ 𝐴) = (vol‘ℝ)) |
201 | | rembl 23308 |
. . . . . . . . 9
⊢ ℝ
∈ dom vol |
202 | | mblvol 23298 |
. . . . . . . . 9
⊢ (ℝ
∈ dom vol → (vol‘ℝ) =
(vol*‘ℝ)) |
203 | 201, 202 | ax-mp 5 |
. . . . . . . 8
⊢
(vol‘ℝ) = (vol*‘ℝ) |
204 | | ovolre 23293 |
. . . . . . . 8
⊢
(vol*‘ℝ) = +∞ |
205 | 203, 204 | eqtri 2644 |
. . . . . . 7
⊢
(vol‘ℝ) = +∞ |
206 | 200, 205 | syl6eq 2672 |
. . . . . 6
⊢ (∪ 𝐴 =
ℝ → (vol‘∪ 𝐴) = +∞) |
207 | 199, 206 | neeqtrrd 2868 |
. . . . 5
⊢ (∪ 𝐴 =
ℝ → 0 ≠ (vol‘∪ 𝐴)) |
208 | 207 | necon2i 2828 |
. . . 4
⊢ (0 =
(vol‘∪ 𝐴) → ∪ 𝐴 ≠ ℝ) |
209 | 197, 208 | syl 17 |
. . 3
⊢ ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → ∪ 𝐴 ≠ ℝ) |
210 | 209 | expr 643 |
. 2
⊢ ((𝐴 ≼ ℕ ∧
∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → (∪ 𝐴
⊆ ℝ → ∪ 𝐴 ≠ ℝ)) |
211 | | eqimss 3657 |
. . 3
⊢ (∪ 𝐴 =
ℝ → ∪ 𝐴 ⊆ ℝ) |
212 | 211 | necon3bi 2820 |
. 2
⊢ (¬
∪ 𝐴 ⊆ ℝ → ∪ 𝐴
≠ ℝ) |
213 | 210, 212 | pm2.61d1 171 |
1
⊢ ((𝐴 ≼ ℕ ∧
∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴
≠ ℝ) |