Step | Hyp | Ref
| Expression |
1 | | unieq 4380 |
. . . . . . . . 9
⊢ (𝐴 = ∅ → ∪ 𝐴 =
∪ ∅) |
2 | | uni0 4401 |
. . . . . . . . 9
⊢ ∪ ∅ = ∅ |
3 | 1, 2 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝐴 = ∅ → ∪ 𝐴 =
∅) |
4 | 3 | fveq2d 6107 |
. . . . . . 7
⊢ (𝐴 = ∅ →
(vol‘∪ 𝐴) = (vol‘∅)) |
5 | | 0mbl 23114 |
. . . . . . . . 9
⊢ ∅
∈ dom vol |
6 | | mblvol 23105 |
. . . . . . . . 9
⊢ (∅
∈ dom vol → (vol‘∅) =
(vol*‘∅)) |
7 | 5, 6 | ax-mp 5 |
. . . . . . . 8
⊢
(vol‘∅) = (vol*‘∅) |
8 | | ovol0 23068 |
. . . . . . . 8
⊢
(vol*‘∅) = 0 |
9 | 7, 8 | eqtri 2632 |
. . . . . . 7
⊢
(vol‘∅) = 0 |
10 | 4, 9 | syl6req 2661 |
. . . . . 6
⊢ (𝐴 = ∅ → 0 =
(vol‘∪ 𝐴)) |
11 | 10 | a1d 25 |
. . . . 5
⊢ (𝐴 = ∅ → ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol‘∪ 𝐴))) |
12 | | reldom 7847 |
. . . . . . . . . . 11
⊢ Rel
≼ |
13 | 12 | brrelexi 5082 |
. . . . . . . . . 10
⊢ (𝐴 ≼ ℕ → 𝐴 ∈ V) |
14 | | 0sdomg 7974 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ≼ ℕ → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
16 | 15 | biimparc 503 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) → ∅
≺ 𝐴) |
17 | | fodomr 7996 |
. . . . . . . 8
⊢ ((∅
≺ 𝐴 ∧ 𝐴 ≼ ℕ) →
∃𝑔 𝑔:ℕ–onto→𝐴) |
18 | 16, 17 | sylancom 698 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) →
∃𝑔 𝑔:ℕ–onto→𝐴) |
19 | | unissb 4405 |
. . . . . . . . . . . . 13
⊢ (∪ 𝐴
⊆ ℝ ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ) |
20 | 19 | anbi1i 727 |
. . . . . . . . . . . 12
⊢ ((∪ 𝐴
⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ)) |
21 | | r19.26 3046 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) ↔ (∀𝑥 ∈ 𝐴 𝑥 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ)) |
22 | 20, 21 | bitr4i 266 |
. . . . . . . . . . 11
⊢ ((∪ 𝐴
⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ)) |
23 | | ovolctb2 23067 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) →
(vol*‘𝑥) =
0) |
24 | | nulmbl 23110 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ⊆ ℝ ∧
(vol*‘𝑥) = 0) →
𝑥 ∈ dom
vol) |
25 | | mblvol 23105 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ dom vol →
(vol‘𝑥) =
(vol*‘𝑥)) |
26 | | eqtr 2629 |
. . . . . . . . . . . . . . . . 17
⊢
(((vol‘𝑥) =
(vol*‘𝑥) ∧
(vol*‘𝑥) = 0) →
(vol‘𝑥) =
0) |
27 | 26 | expcom 450 |
. . . . . . . . . . . . . . . 16
⊢
((vol*‘𝑥) = 0
→ ((vol‘𝑥) =
(vol*‘𝑥) →
(vol‘𝑥) =
0)) |
28 | 25, 27 | syl5 33 |
. . . . . . . . . . . . . . 15
⊢
((vol*‘𝑥) = 0
→ (𝑥 ∈ dom vol
→ (vol‘𝑥) =
0)) |
29 | 28 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ⊆ ℝ ∧
(vol*‘𝑥) = 0) →
(𝑥 ∈ dom vol →
(vol‘𝑥) =
0)) |
30 | 24, 29 | jcai 557 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ⊆ ℝ ∧
(vol*‘𝑥) = 0) →
(𝑥 ∈ dom vol ∧
(vol‘𝑥) =
0)) |
31 | 23, 30 | syldan 486 |
. . . . . . . . . . . 12
⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (𝑥 ∈ dom vol ∧
(vol‘𝑥) =
0)) |
32 | 31 | ralimi 2936 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) |
33 | 22, 32 | sylbi 206 |
. . . . . . . . . 10
⊢ ((∪ 𝐴
⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) |
34 | 33 | ancoms 468 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ) → ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) |
35 | | fzfi 12633 |
. . . . . . . . . . . . . . 15
⊢
(1...𝑚) ∈
Fin |
36 | | fzssuz 12253 |
. . . . . . . . . . . . . . . . 17
⊢
(1...𝑚) ⊆
(ℤ≥‘1) |
37 | | nnuz 11599 |
. . . . . . . . . . . . . . . . 17
⊢ ℕ =
(ℤ≥‘1) |
38 | 36, 37 | sseqtr4i 3601 |
. . . . . . . . . . . . . . . 16
⊢
(1...𝑚) ⊆
ℕ |
39 | | fof 6028 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔:ℕ–onto→𝐴 → 𝑔:ℕ⟶𝐴) |
40 | 39 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔:ℕ–onto→𝐴 ∧ 𝑙 ∈ ℕ) → (𝑔‘𝑙) ∈ 𝐴) |
41 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = (𝑔‘𝑙) → (𝑥 ∈ dom vol ↔ (𝑔‘𝑙) ∈ dom vol)) |
42 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = (𝑔‘𝑙) → (vol‘𝑥) = (vol‘(𝑔‘𝑙))) |
43 | 42 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = (𝑔‘𝑙) → ((vol‘𝑥) = 0 ↔ (vol‘(𝑔‘𝑙)) = 0)) |
44 | 41, 43 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = (𝑔‘𝑙) → ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ↔ ((𝑔‘𝑙) ∈ dom vol ∧ (vol‘(𝑔‘𝑙)) = 0))) |
45 | 44 | rspccva 3281 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((∀𝑥 ∈
𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔‘𝑙) ∈ 𝐴) → ((𝑔‘𝑙) ∈ dom vol ∧ (vol‘(𝑔‘𝑙)) = 0)) |
46 | 45 | simpld 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑥 ∈
𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔‘𝑙) ∈ 𝐴) → (𝑔‘𝑙) ∈ dom vol) |
47 | 46 | ancoms 468 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑔‘𝑙) ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑔‘𝑙) ∈ dom vol) |
48 | 40, 47 | sylan 487 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑔:ℕ–onto→𝐴 ∧ 𝑙 ∈ ℕ) ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑔‘𝑙) ∈ dom vol) |
49 | 48 | an32s 842 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (𝑔‘𝑙) ∈ dom vol) |
50 | 49 | ralrimiva 2949 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ (𝑔‘𝑙) ∈ dom vol) |
51 | | ssralv 3629 |
. . . . . . . . . . . . . . . 16
⊢
((1...𝑚) ⊆
ℕ → (∀𝑙
∈ ℕ (𝑔‘𝑙) ∈ dom vol → ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol)) |
52 | 38, 50, 51 | mpsyl 66 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol) |
53 | | finiunmbl 23119 |
. . . . . . . . . . . . . . 15
⊢
(((1...𝑚) ∈ Fin
∧ ∀𝑙 ∈
(1...𝑚)(𝑔‘𝑙) ∈ dom vol) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol) |
54 | 35, 52, 53 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol) |
55 | 54 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol) |
56 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) |
57 | 55, 56 | fmptd 6292 |
. . . . . . . . . . . 12
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol) |
58 | | fzssp1 12255 |
. . . . . . . . . . . . . . 15
⊢
(1...𝑛) ⊆
(1...(𝑛 +
1)) |
59 | | iunss1 4468 |
. . . . . . . . . . . . . . 15
⊢
((1...𝑛) ⊆
(1...(𝑛 + 1)) →
∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙) ⊆ ∪
𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙)) |
60 | 58, 59 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙) ⊆ ∪
𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙) |
61 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛)) |
62 | 61 | iuneq1d 4481 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 𝑛 → ∪
𝑙 ∈ (1...𝑚)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙)) |
63 | | ovex 6577 |
. . . . . . . . . . . . . . . . 17
⊢
(1...𝑛) ∈
V |
64 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔‘𝑙) ∈ V |
65 | 63, 64 | iunex 7039 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙) ∈ V |
66 | 62, 56, 65 | fvmpt 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) = ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙)) |
67 | | peano2nn 10909 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℕ) |
68 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 = (𝑛 + 1) → (1...𝑚) = (1...(𝑛 + 1))) |
69 | 68 | iuneq1d 4481 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = (𝑛 + 1) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙)) |
70 | | ovex 6577 |
. . . . . . . . . . . . . . . . . 18
⊢
(1...(𝑛 + 1)) ∈
V |
71 | 70, 64 | iunex 7039 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙) ∈ V |
72 | 69, 56, 71 | fvmpt 6191 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 + 1) ∈ ℕ →
((𝑚 ∈ ℕ ↦
∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)) = ∪
𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙)) |
73 | 67, 72 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)) = ∪
𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙)) |
74 | 66, 73 | sseq12d 3597 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)) ↔ ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙) ⊆ ∪
𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙))) |
75 | 60, 74 | mpbiri 247 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1))) |
76 | 75 | rgen 2906 |
. . . . . . . . . . . 12
⊢
∀𝑛 ∈
ℕ ((𝑚 ∈ ℕ
↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)) |
77 | | nnex 10903 |
. . . . . . . . . . . . . 14
⊢ ℕ
∈ V |
78 | 77 | mptex 6390 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈ V |
79 | | feq1 5939 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (𝑓:ℕ⟶dom vol ↔ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol)) |
80 | | fveq1 6102 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (𝑓‘𝑛) = ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛)) |
81 | | fveq1 6102 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (𝑓‘(𝑛 + 1)) = ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1))) |
82 | 80, 81 | sseq12d 3597 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ((𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1)) ↔ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)))) |
83 | 82 | ralbidv 2969 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (∀𝑛 ∈ ℕ (𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1)) ↔ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)))) |
84 | 79, 83 | anbi12d 743 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ((𝑓:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1))) ↔ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1))))) |
85 | | rneq 5272 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ran 𝑓 = ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) |
86 | 85 | unieqd 4382 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ∪ ran
𝑓 = ∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) |
87 | 86 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (vol‘∪ ran 𝑓) = (vol‘∪
ran (𝑚 ∈ ℕ
↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))) |
88 | 85 | imaeq2d 5385 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (vol “ ran 𝑓) = (vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))) |
89 | 88 | supeq1d 8235 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → sup((vol “ ran 𝑓), ℝ*, < ) =
sup((vol “ ran (𝑚
∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, <
)) |
90 | 87, 89 | eqeq12d 2625 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ((vol‘∪ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, < ) ↔
(vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, <
))) |
91 | 84, 90 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (((𝑓:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1))) → (vol‘∪ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, < )) ↔
(((𝑚 ∈ ℕ ↦
∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1))) → (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, <
)))) |
92 | | volsupnfl.0 |
. . . . . . . . . . . . 13
⊢ ((𝑓:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1))) → (vol‘∪ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, <
)) |
93 | 78, 91, 92 | vtocl 3232 |
. . . . . . . . . . . 12
⊢ (((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1))) → (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, <
)) |
94 | 57, 76, 93 | sylancl 693 |
. . . . . . . . . . 11
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, <
)) |
95 | | df-iun 4457 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = {𝑛 ∣ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥)} |
96 | | eluzfz2 12220 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈
(ℤ≥‘1) → 𝑥 ∈ (1...𝑥)) |
97 | 96, 37 | eleq2s 2706 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℕ → 𝑥 ∈ (1...𝑥)) |
98 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑙 = 𝑥 → (𝑔‘𝑙) = (𝑔‘𝑥)) |
99 | 98 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑙 = 𝑥 → (𝑛 ∈ (𝑔‘𝑙) ↔ 𝑛 ∈ (𝑔‘𝑥))) |
100 | 99 | rspcev 3282 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ (1...𝑥) ∧ 𝑛 ∈ (𝑔‘𝑥)) → ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔‘𝑙)) |
101 | 97, 100 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℕ ∧ 𝑛 ∈ (𝑔‘𝑥)) → ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔‘𝑙)) |
102 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 = 𝑥 → (1...𝑚) = (1...𝑥)) |
103 | 102 | rexeqdv 3122 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑥 → (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙) ↔ ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔‘𝑙))) |
104 | 103 | rspcev 3282 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℕ ∧
∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔‘𝑙)) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙)) |
105 | 101, 104 | syldan 486 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℕ ∧ 𝑛 ∈ (𝑔‘𝑥)) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙)) |
106 | 105 | rexlimiva 3010 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑥 ∈
ℕ 𝑛 ∈ (𝑔‘𝑥) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙)) |
107 | | ssrexv 3630 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((1...𝑚) ⊆
ℕ → (∃𝑙
∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙) → ∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔‘𝑙))) |
108 | 38, 107 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∃𝑙 ∈
(1...𝑚)𝑛 ∈ (𝑔‘𝑙) → ∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔‘𝑙)) |
109 | 99 | cbvrexv 3148 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∃𝑙 ∈
ℕ 𝑛 ∈ (𝑔‘𝑙) ↔ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥)) |
110 | 108, 109 | sylib 207 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑙 ∈
(1...𝑚)𝑛 ∈ (𝑔‘𝑙) → ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥)) |
111 | 110 | rexlimivw 3011 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑚 ∈
ℕ ∃𝑙 ∈
(1...𝑚)𝑛 ∈ (𝑔‘𝑙) → ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥)) |
112 | 106, 111 | impbii 198 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑥 ∈
ℕ 𝑛 ∈ (𝑔‘𝑥) ↔ ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙)) |
113 | | eliun 4460 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ↔ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙)) |
114 | 113 | rexbii 3023 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑚 ∈
ℕ 𝑛 ∈ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ↔ ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙)) |
115 | 112, 114 | bitr4i 266 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑥 ∈
ℕ 𝑛 ∈ (𝑔‘𝑥) ↔ ∃𝑚 ∈ ℕ 𝑛 ∈ ∪
𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) |
116 | 115 | abbii 2726 |
. . . . . . . . . . . . . . . 16
⊢ {𝑛 ∣ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥)} = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 ∈ ∪
𝑙 ∈ (1...𝑚)(𝑔‘𝑙)} |
117 | 95, 116 | eqtri 2632 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 ∈ ∪
𝑙 ∈ (1...𝑚)(𝑔‘𝑙)} |
118 | | df-iun 4457 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑚 ∈ ℕ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 ∈ ∪
𝑙 ∈ (1...𝑚)(𝑔‘𝑙)} |
119 | | ovex 6577 |
. . . . . . . . . . . . . . . . 17
⊢
(1...𝑚) ∈
V |
120 | 119, 64 | iunex 7039 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ V |
121 | 120 | dfiun3 5301 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑚 ∈ ℕ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) = ∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) |
122 | 117, 118,
121 | 3eqtr2i 2638 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = ∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) |
123 | | fofn 6030 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔:ℕ–onto→𝐴 → 𝑔 Fn ℕ) |
124 | | fniunfv 6409 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 Fn ℕ → ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = ∪ ran 𝑔) |
125 | 123, 124 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:ℕ–onto→𝐴 → ∪
𝑥 ∈ ℕ (𝑔‘𝑥) = ∪ ran 𝑔) |
126 | | forn 6031 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔:ℕ–onto→𝐴 → ran 𝑔 = 𝐴) |
127 | 126 | unieqd 4382 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:ℕ–onto→𝐴 → ∪ ran
𝑔 = ∪ 𝐴) |
128 | 125, 127 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (𝑔:ℕ–onto→𝐴 → ∪
𝑥 ∈ ℕ (𝑔‘𝑥) = ∪ 𝐴) |
129 | 122, 128 | syl5eqr 2658 |
. . . . . . . . . . . . 13
⊢ (𝑔:ℕ–onto→𝐴 → ∪ ran
(𝑚 ∈ ℕ ↦
∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = ∪ 𝐴) |
130 | 129 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑔:ℕ–onto→𝐴 → (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (vol‘∪
𝐴)) |
131 | 130 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (vol‘∪
𝐴)) |
132 | | rnco2 5559 |
. . . . . . . . . . . . . 14
⊢ ran (vol
∘ (𝑚 ∈ ℕ
↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) |
133 | | eqidd 2611 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) |
134 | | volf 23104 |
. . . . . . . . . . . . . . . . . . 19
⊢ vol:dom
vol⟶(0[,]+∞) |
135 | 134 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → vol:dom
vol⟶(0[,]+∞)) |
136 | 135 | feqmptd 6159 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → vol = (𝑛 ∈ dom vol ↦
(vol‘𝑛))) |
137 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) → (vol‘𝑛) = (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) |
138 | 55, 133, 136, 137 | fmptco 6303 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘
(𝑚 ∈ ℕ ↦
∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (𝑚 ∈ ℕ ↦ (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))) |
139 | | mblvol 23105 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol → (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) |
140 | 55, 139 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) |
141 | | mblss 23106 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 ∈ dom vol → 𝑥 ⊆
ℝ) |
142 | 141 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑥 ∈ dom vol ∧
(vol‘𝑥) = 0) →
𝑥 ⊆
ℝ) |
143 | 25 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑥 ∈ dom vol →
((vol‘𝑥) = 0 ↔
(vol*‘𝑥) =
0)) |
144 | | 0re 9919 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 0 ∈
ℝ |
145 | | eleq1a 2683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (0 ∈
ℝ → ((vol*‘𝑥) = 0 → (vol*‘𝑥) ∈ ℝ)) |
146 | 144, 145 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((vol*‘𝑥) = 0
→ (vol*‘𝑥)
∈ ℝ) |
147 | 143, 146 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 ∈ dom vol →
((vol‘𝑥) = 0 →
(vol*‘𝑥) ∈
ℝ)) |
148 | 147 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑥 ∈ dom vol ∧
(vol‘𝑥) = 0) →
(vol*‘𝑥) ∈
ℝ) |
149 | 142, 148 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ dom vol ∧
(vol‘𝑥) = 0) →
(𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) |
150 | 149 | ralimi 2936 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∀𝑥 ∈
𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈
ℝ)) |
151 | 150 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈
ℝ)) |
152 | | ssid 3587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ℕ
⊆ ℕ |
153 | | sseq1 3589 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑥 = (𝑔‘𝑙) → (𝑥 ⊆ ℝ ↔ (𝑔‘𝑙) ⊆ ℝ)) |
154 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 = (𝑔‘𝑙) → (vol*‘𝑥) = (vol*‘(𝑔‘𝑙))) |
155 | 154 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑥 = (𝑔‘𝑙) → ((vol*‘𝑥) ∈ ℝ ↔ (vol*‘(𝑔‘𝑙)) ∈ ℝ)) |
156 | 153, 155 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 = (𝑔‘𝑙) → ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ))) |
157 | 156 | ralima 6402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑔 Fn ℕ ∧ ℕ
⊆ ℕ) → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔
∀𝑙 ∈ ℕ
((𝑔‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑙)) ∈
ℝ))) |
158 | 123, 152,
157 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔
∀𝑙 ∈ ℕ
((𝑔‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑙)) ∈
ℝ))) |
159 | | foima 6033 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑔:ℕ–onto→𝐴 → (𝑔 “ ℕ) = 𝐴) |
160 | 159 | raleqdv 3121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔
∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈
ℝ))) |
161 | 158, 160 | bitr3d 269 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑙 ∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈
ℝ))) |
162 | 161 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (∀𝑙 ∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈
ℝ))) |
163 | 151, 162 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ)) |
164 | | ssralv 3629 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((1...𝑚) ⊆
ℕ → (∀𝑙
∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ) → ∀𝑙 ∈ (1...𝑚)((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ))) |
165 | 38, 163, 164 | mpsyl 66 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ)) |
166 | 165 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∀𝑙 ∈ (1...𝑚)((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ)) |
167 | | ovolfiniun 23076 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((1...𝑚) ∈ Fin
∧ ∀𝑙 ∈
(1...𝑚)((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ)) →
(vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙))) |
168 | 35, 166, 167 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙))) |
169 | | mblvol 23105 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑔‘𝑙) ∈ dom vol → (vol‘(𝑔‘𝑙)) = (vol*‘(𝑔‘𝑙))) |
170 | 49, 169 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol‘(𝑔‘𝑙)) = (vol*‘(𝑔‘𝑙))) |
171 | 45 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((∀𝑥 ∈
𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔‘𝑙) ∈ 𝐴) → (vol‘(𝑔‘𝑙)) = 0) |
172 | 40, 171 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((∀𝑥 ∈
𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔:ℕ–onto→𝐴 ∧ 𝑙 ∈ ℕ)) → (vol‘(𝑔‘𝑙)) = 0) |
173 | 172 | ancoms 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑔:ℕ–onto→𝐴 ∧ 𝑙 ∈ ℕ) ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘(𝑔‘𝑙)) = 0) |
174 | 173 | an32s 842 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol‘(𝑔‘𝑙)) = 0) |
175 | 170, 174 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol*‘(𝑔‘𝑙)) = 0) |
176 | 175 | ralrimiva 2949 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ
(vol*‘(𝑔‘𝑙)) = 0) |
177 | | ssralv 3629 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((1...𝑚) ⊆
ℕ → (∀𝑙
∈ ℕ (vol*‘(𝑔‘𝑙)) = 0 → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)) = 0)) |
178 | 38, 176, 177 | mpsyl 66 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)) = 0) |
179 | 178 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)) = 0) |
180 | 179 | sumeq2d 14280 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)) = Σ𝑙 ∈ (1...𝑚)0) |
181 | 35 | olci 405 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((1...𝑚) ⊆
(ℤ≥‘1) ∨ (1...𝑚) ∈ Fin) |
182 | | sumz 14300 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((1...𝑚) ⊆
(ℤ≥‘1) ∨ (1...𝑚) ∈ Fin) → Σ𝑙 ∈ (1...𝑚)0 = 0) |
183 | 181, 182 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Σ𝑙 ∈
(1...𝑚)0 =
0 |
184 | 180, 183 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)) = 0) |
185 | 168, 184 | breqtrd 4609 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ 0) |
186 | | mblss 23106 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑔‘𝑙) ∈ dom vol → (𝑔‘𝑙) ⊆ ℝ) |
187 | 186 | ralimi 2936 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∀𝑙 ∈
(1...𝑚)(𝑔‘𝑙) ∈ dom vol → ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ) |
188 | 52, 187 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ) |
189 | | iunss 4497 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ ↔ ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ) |
190 | 188, 189 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ) |
191 | 190 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ) |
192 | | ovolge0 23056 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ → 0 ≤
(vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) |
193 | 191, 192 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → 0 ≤
(vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) |
194 | | ovolcl 23053 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈
ℝ*) |
195 | 190, 194 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) →
(vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈
ℝ*) |
196 | 195 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈
ℝ*) |
197 | | 0xr 9965 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ∈
ℝ* |
198 | | xrletri3 11861 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈ ℝ* ∧ 0 ∈
ℝ*) → ((vol*‘∪
𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = 0 ↔ ((vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ 0 ∧ 0 ≤ (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))))) |
199 | 196, 197,
198 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ((vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = 0 ↔ ((vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ 0 ∧ 0 ≤ (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))))) |
200 | 185, 193,
199 | mpbir2and 959 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = 0) |
201 | 140, 200 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = 0) |
202 | 201 | mpteq2dva 4672 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦
(vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (𝑚 ∈ ℕ ↦ 0)) |
203 | | fconstmpt 5085 |
. . . . . . . . . . . . . . . . 17
⊢ (ℕ
× {0}) = (𝑚 ∈
ℕ ↦ 0) |
204 | 202, 203 | syl6eqr 2662 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦
(vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (ℕ × {0})) |
205 | 138, 204 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘
(𝑚 ∈ ℕ ↦
∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (ℕ × {0})) |
206 | | frn 5966 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol → ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ⊆ dom vol) |
207 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . 19
⊢ (vol:dom
vol⟶(0[,]+∞) → vol Fn dom vol) |
208 | 134, 207 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ vol Fn
dom vol |
209 | 120, 56 | fnmpti 5935 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) Fn ℕ |
210 | | fnco 5913 |
. . . . . . . . . . . . . . . . . 18
⊢ ((vol Fn
dom vol ∧ (𝑚 ∈
ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) Fn ℕ ∧ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ⊆ dom vol) → (vol ∘
(𝑚 ∈ ℕ ↦
∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) Fn ℕ) |
211 | 208, 209,
210 | mp3an12 1406 |
. . . . . . . . . . . . . . . . 17
⊢ (ran
(𝑚 ∈ ℕ ↦
∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ⊆ dom vol → (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) Fn ℕ) |
212 | 57, 206, 211 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘
(𝑚 ∈ ℕ ↦
∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) Fn ℕ) |
213 | | 1nn 10908 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℕ |
214 | 213 | ne0ii 3882 |
. . . . . . . . . . . . . . . 16
⊢ ℕ
≠ ∅ |
215 | | fconst5 6376 |
. . . . . . . . . . . . . . . 16
⊢ (((vol
∘ (𝑚 ∈ ℕ
↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) Fn ℕ ∧ ℕ ≠ ∅)
→ ((vol ∘ (𝑚
∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (ℕ × {0}) ↔ ran (vol
∘ (𝑚 ∈ ℕ
↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = {0})) |
216 | 212, 214,
215 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ((vol ∘
(𝑚 ∈ ℕ ↦
∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (ℕ × {0}) ↔ ran (vol
∘ (𝑚 ∈ ℕ
↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = {0})) |
217 | 205, 216 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ran (vol ∘
(𝑚 ∈ ℕ ↦
∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = {0}) |
218 | 132, 217 | syl5eqr 2658 |
. . . . . . . . . . . . 13
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol “ ran
(𝑚 ∈ ℕ ↦
∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = {0}) |
219 | 218 | supeq1d 8235 |
. . . . . . . . . . . 12
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → sup((vol “
ran (𝑚 ∈ ℕ
↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, < ) = sup({0},
ℝ*, < )) |
220 | | xrltso 11850 |
. . . . . . . . . . . . 13
⊢ < Or
ℝ* |
221 | | supsn 8261 |
. . . . . . . . . . . . 13
⊢ (( <
Or ℝ* ∧ 0 ∈ ℝ*) → sup({0},
ℝ*, < ) = 0) |
222 | 220, 197,
221 | mp2an 704 |
. . . . . . . . . . . 12
⊢ sup({0},
ℝ*, < ) = 0 |
223 | 219, 222 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → sup((vol “
ran (𝑚 ∈ ℕ
↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, < ) =
0) |
224 | 94, 131, 223 | 3eqtr3rd 2653 |
. . . . . . . . . 10
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → 0 =
(vol‘∪ 𝐴)) |
225 | 224 | ex 449 |
. . . . . . . . 9
⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → 0 =
(vol‘∪ 𝐴))) |
226 | 34, 225 | syl5 33 |
. . . . . . . 8
⊢ (𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ) → 0 = (vol‘∪ 𝐴))) |
227 | 226 | exlimiv 1845 |
. . . . . . 7
⊢
(∃𝑔 𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ) → 0 = (vol‘∪ 𝐴))) |
228 | 18, 227 | syl 17 |
. . . . . 6
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) →
((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ) → 0 = (vol‘∪ 𝐴))) |
229 | 228 | expimpd 627 |
. . . . 5
⊢ (𝐴 ≠ ∅ → ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol‘∪ 𝐴))) |
230 | 11, 229 | pm2.61ine 2865 |
. . . 4
⊢ ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol‘∪ 𝐴)) |
231 | | renepnf 9966 |
. . . . . . 7
⊢ (0 ∈
ℝ → 0 ≠ +∞) |
232 | 144, 231 | mp1i 13 |
. . . . . 6
⊢ (∪ 𝐴 =
ℝ → 0 ≠ +∞) |
233 | | fveq2 6103 |
. . . . . . 7
⊢ (∪ 𝐴 =
ℝ → (vol‘∪ 𝐴) = (vol‘ℝ)) |
234 | | rembl 23115 |
. . . . . . . . 9
⊢ ℝ
∈ dom vol |
235 | | mblvol 23105 |
. . . . . . . . 9
⊢ (ℝ
∈ dom vol → (vol‘ℝ) =
(vol*‘ℝ)) |
236 | 234, 235 | ax-mp 5 |
. . . . . . . 8
⊢
(vol‘ℝ) = (vol*‘ℝ) |
237 | | ovolre 23100 |
. . . . . . . 8
⊢
(vol*‘ℝ) = +∞ |
238 | 236, 237 | eqtri 2632 |
. . . . . . 7
⊢
(vol‘ℝ) = +∞ |
239 | 233, 238 | syl6eq 2660 |
. . . . . 6
⊢ (∪ 𝐴 =
ℝ → (vol‘∪ 𝐴) = +∞) |
240 | 232, 239 | neeqtrrd 2856 |
. . . . 5
⊢ (∪ 𝐴 =
ℝ → 0 ≠ (vol‘∪ 𝐴)) |
241 | 240 | necon2i 2816 |
. . . 4
⊢ (0 =
(vol‘∪ 𝐴) → ∪ 𝐴 ≠ ℝ) |
242 | 230, 241 | syl 17 |
. . 3
⊢ ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → ∪ 𝐴 ≠ ℝ) |
243 | 242 | expr 641 |
. 2
⊢ ((𝐴 ≼ ℕ ∧
∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → (∪ 𝐴
⊆ ℝ → ∪ 𝐴 ≠ ℝ)) |
244 | | eqimss 3620 |
. . 3
⊢ (∪ 𝐴 =
ℝ → ∪ 𝐴 ⊆ ℝ) |
245 | 244 | necon3bi 2808 |
. 2
⊢ (¬
∪ 𝐴 ⊆ ℝ → ∪ 𝐴
≠ ℝ) |
246 | 243, 245 | pm2.61d1 170 |
1
⊢ ((𝐴 ≼ ℕ ∧
∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴
≠ ℝ) |