| 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 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) →
(vol*‘𝑥) =
0) |
| 24 | | nulmbl 25570 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ⊆ ℝ ∧
(vol*‘𝑥) = 0) →
𝑥 ∈ dom
vol) |
| 25 | | mblvol 25565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ dom vol →
(vol‘𝑥) =
(vol*‘𝑥)) |
| 26 | | eqtr 2760 |
. . . . . . . . . . . . . . . . 17
⊢
(((vol‘𝑥) =
(vol*‘𝑥) ∧
(vol*‘𝑥) = 0) →
(vol‘𝑥) =
0) |
| 27 | 26 | expcom 413 |
. . . . . . . . . . . . . . . 16
⊢
((vol*‘𝑥) = 0
→ ((vol‘𝑥) =
(vol*‘𝑥) →
(vol‘𝑥) =
0)) |
| 28 | 25, 27 | syl5 34 |
. . . . . . . . . . . . . . 15
⊢
((vol*‘𝑥) = 0
→ (𝑥 ∈ dom vol
→ (vol‘𝑥) =
0)) |
| 29 | 28 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ⊆ ℝ ∧
(vol*‘𝑥) = 0) →
(𝑥 ∈ dom vol →
(vol‘𝑥) =
0)) |
| 30 | 24, 29 | jcai 516 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ⊆ ℝ ∧
(vol*‘𝑥) = 0) →
(𝑥 ∈ dom vol ∧
(vol‘𝑥) =
0)) |
| 31 | 23, 30 | syldan 591 |
. . . . . . . . . . . 12
⊢ ((𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → (𝑥 ∈ dom vol ∧
(vol‘𝑥) =
0)) |
| 32 | 31 | ralimi 3083 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝐴 (𝑥 ⊆ ℝ ∧ 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) |
| 33 | 22, 32 | sylbi 217 |
. . . . . . . . . 10
⊢ ((∪ 𝐴
⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) |
| 34 | 33 | ancoms 458 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ) → ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) |
| 35 | | fzfi 14013 |
. . . . . . . . . . . . . . 15
⊢
(1...𝑚) ∈
Fin |
| 36 | | fzssuz 13605 |
. . . . . . . . . . . . . . . . 17
⊢
(1...𝑚) ⊆
(ℤ≥‘1) |
| 37 | | nnuz 12921 |
. . . . . . . . . . . . . . . . 17
⊢ ℕ =
(ℤ≥‘1) |
| 38 | 36, 37 | sseqtrri 4033 |
. . . . . . . . . . . . . . . 16
⊢
(1...𝑚) ⊆
ℕ |
| 39 | | fof 6820 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔:ℕ–onto→𝐴 → 𝑔:ℕ⟶𝐴) |
| 40 | 39 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔:ℕ–onto→𝐴 ∧ 𝑙 ∈ ℕ) → (𝑔‘𝑙) ∈ 𝐴) |
| 41 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = (𝑔‘𝑙) → (𝑥 ∈ dom vol ↔ (𝑔‘𝑙) ∈ dom vol)) |
| 42 | | fveqeq2 6915 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = (𝑔‘𝑙) → ((vol‘𝑥) = 0 ↔ (vol‘(𝑔‘𝑙)) = 0)) |
| 43 | 41, 42 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = (𝑔‘𝑙) → ((𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ↔ ((𝑔‘𝑙) ∈ dom vol ∧ (vol‘(𝑔‘𝑙)) = 0))) |
| 44 | 43 | rspccva 3621 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((∀𝑥 ∈
𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔‘𝑙) ∈ 𝐴) → ((𝑔‘𝑙) ∈ dom vol ∧ (vol‘(𝑔‘𝑙)) = 0)) |
| 45 | 44 | simpld 494 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑥 ∈
𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔‘𝑙) ∈ 𝐴) → (𝑔‘𝑙) ∈ dom vol) |
| 46 | 45 | ancoms 458 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑔‘𝑙) ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑔‘𝑙) ∈ dom vol) |
| 47 | 40, 46 | sylan 580 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑔:ℕ–onto→𝐴 ∧ 𝑙 ∈ ℕ) ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑔‘𝑙) ∈ dom vol) |
| 48 | 47 | an32s 652 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (𝑔‘𝑙) ∈ dom vol) |
| 49 | 48 | ralrimiva 3146 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ (𝑔‘𝑙) ∈ dom vol) |
| 50 | | ssralv 4052 |
. . . . . . . . . . . . . . . 16
⊢
((1...𝑚) ⊆
ℕ → (∀𝑙
∈ ℕ (𝑔‘𝑙) ∈ dom vol → ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol)) |
| 51 | 38, 49, 50 | mpsyl 68 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol) |
| 52 | | finiunmbl 25579 |
. . . . . . . . . . . . . . 15
⊢
(((1...𝑚) ∈ Fin
∧ ∀𝑙 ∈
(1...𝑚)(𝑔‘𝑙) ∈ dom vol) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol) |
| 53 | 35, 51, 52 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol) |
| 54 | 53 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol) |
| 55 | 54 | fmpttd 7135 |
. . . . . . . . . . . 12
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol) |
| 56 | | fzssp1 13607 |
. . . . . . . . . . . . . . 15
⊢
(1...𝑛) ⊆
(1...(𝑛 +
1)) |
| 57 | | iunss1 5006 |
. . . . . . . . . . . . . . 15
⊢
((1...𝑛) ⊆
(1...(𝑛 + 1)) →
∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙) ⊆ ∪
𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙)) |
| 58 | 56, 57 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙) ⊆ ∪
𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙) |
| 59 | | oveq2 7439 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛)) |
| 60 | 59 | iuneq1d 5019 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 𝑛 → ∪
𝑙 ∈ (1...𝑚)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙)) |
| 61 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) |
| 62 | | ovex 7464 |
. . . . . . . . . . . . . . . . 17
⊢
(1...𝑛) ∈
V |
| 63 | | fvex 6919 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔‘𝑙) ∈ V |
| 64 | 62, 63 | iunex 7993 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙) ∈ V |
| 65 | 60, 61, 64 | fvmpt 7016 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) = ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙)) |
| 66 | | peano2nn 12278 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℕ) |
| 67 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 = (𝑛 + 1) → (1...𝑚) = (1...(𝑛 + 1))) |
| 68 | 67 | iuneq1d 5019 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = (𝑛 + 1) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) = ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙)) |
| 69 | | ovex 7464 |
. . . . . . . . . . . . . . . . . 18
⊢
(1...(𝑛 + 1)) ∈
V |
| 70 | 69, 63 | iunex 7993 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙) ∈ V |
| 71 | 68, 61, 70 | fvmpt 7016 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 + 1) ∈ ℕ →
((𝑚 ∈ ℕ ↦
∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)) = ∪
𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙)) |
| 72 | 66, 71 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)) = ∪
𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙)) |
| 73 | 65, 72 | sseq12d 4017 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)) ↔ ∪ 𝑙 ∈ (1...𝑛)(𝑔‘𝑙) ⊆ ∪
𝑙 ∈ (1...(𝑛 + 1))(𝑔‘𝑙))) |
| 74 | 58, 73 | mpbiri 258 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1))) |
| 75 | 74 | rgen 3063 |
. . . . . . . . . . . 12
⊢
∀𝑛 ∈
ℕ ((𝑚 ∈ ℕ
↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)) |
| 76 | | nnex 12272 |
. . . . . . . . . . . . . 14
⊢ ℕ
∈ V |
| 77 | 76 | mptex 7243 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈ V |
| 78 | | feq1 6716 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (𝑓:ℕ⟶dom vol ↔ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol)) |
| 79 | | fveq1 6905 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (𝑓‘𝑛) = ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛)) |
| 80 | | fveq1 6905 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (𝑓‘(𝑛 + 1)) = ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1))) |
| 81 | 79, 80 | sseq12d 4017 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ((𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1)) ↔ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)))) |
| 82 | 81 | ralbidv 3178 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (∀𝑛 ∈ ℕ (𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1)) ↔ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1)))) |
| 83 | 78, 82 | anbi12d 632 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ((𝑓:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1))) ↔ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1))))) |
| 84 | | rneq 5947 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ran 𝑓 = ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) |
| 85 | 84 | unieqd 4920 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ∪ ran
𝑓 = ∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) |
| 86 | 85 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (vol‘∪ ran 𝑓) = (vol‘∪
ran (𝑚 ∈ ℕ
↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))) |
| 87 | 84 | imaeq2d 6078 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (vol “ ran 𝑓) = (vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))) |
| 88 | 87 | supeq1d 9486 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → sup((vol “ ran 𝑓), ℝ*, < ) =
sup((vol “ ran (𝑚
∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, <
)) |
| 89 | 86, 88 | eqeq12d 2753 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → ((vol‘∪ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, < ) ↔
(vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, <
))) |
| 90 | 83, 89 | imbi12d 344 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) → (((𝑓:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1))) → (vol‘∪ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, < )) ↔
(((𝑚 ∈ ℕ ↦
∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1))) → (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, <
)))) |
| 91 | | volsupnfl.0 |
. . . . . . . . . . . . 13
⊢ ((𝑓:ℕ⟶dom vol ∧
∀𝑛 ∈ ℕ
(𝑓‘𝑛) ⊆ (𝑓‘(𝑛 + 1))) → (vol‘∪ ran 𝑓) = sup((vol “ ran 𝑓), ℝ*, <
)) |
| 92 | 77, 90, 91 | vtocl 3558 |
. . . . . . . . . . . 12
⊢ (((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘𝑛) ⊆ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))‘(𝑛 + 1))) → (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, <
)) |
| 93 | 55, 75, 92 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = sup((vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, <
)) |
| 94 | | df-iun 4993 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = {𝑛 ∣ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥)} |
| 95 | | eluzfz2 13572 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈
(ℤ≥‘1) → 𝑥 ∈ (1...𝑥)) |
| 96 | 95, 37 | eleq2s 2859 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℕ → 𝑥 ∈ (1...𝑥)) |
| 97 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑙 = 𝑥 → (𝑔‘𝑙) = (𝑔‘𝑥)) |
| 98 | 97 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑙 = 𝑥 → (𝑛 ∈ (𝑔‘𝑙) ↔ 𝑛 ∈ (𝑔‘𝑥))) |
| 99 | 98 | rspcev 3622 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ (1...𝑥) ∧ 𝑛 ∈ (𝑔‘𝑥)) → ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔‘𝑙)) |
| 100 | 96, 99 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℕ ∧ 𝑛 ∈ (𝑔‘𝑥)) → ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔‘𝑙)) |
| 101 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 = 𝑥 → (1...𝑚) = (1...𝑥)) |
| 102 | 101 | rexeqdv 3327 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑥 → (∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙) ↔ ∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔‘𝑙))) |
| 103 | 102 | rspcev 3622 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℕ ∧
∃𝑙 ∈ (1...𝑥)𝑛 ∈ (𝑔‘𝑙)) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙)) |
| 104 | 100, 103 | syldan 591 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℕ ∧ 𝑛 ∈ (𝑔‘𝑥)) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙)) |
| 105 | 104 | rexlimiva 3147 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑥 ∈
ℕ 𝑛 ∈ (𝑔‘𝑥) → ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙)) |
| 106 | | ssrexv 4053 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((1...𝑚) ⊆
ℕ → (∃𝑙
∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙) → ∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔‘𝑙))) |
| 107 | 38, 106 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∃𝑙 ∈
(1...𝑚)𝑛 ∈ (𝑔‘𝑙) → ∃𝑙 ∈ ℕ 𝑛 ∈ (𝑔‘𝑙)) |
| 108 | 98 | cbvrexvw 3238 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∃𝑙 ∈
ℕ 𝑛 ∈ (𝑔‘𝑙) ↔ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥)) |
| 109 | 107, 108 | sylib 218 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑙 ∈
(1...𝑚)𝑛 ∈ (𝑔‘𝑙) → ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥)) |
| 110 | 109 | rexlimivw 3151 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑚 ∈
ℕ ∃𝑙 ∈
(1...𝑚)𝑛 ∈ (𝑔‘𝑙) → ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥)) |
| 111 | 105, 110 | impbii 209 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑥 ∈
ℕ 𝑛 ∈ (𝑔‘𝑥) ↔ ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙)) |
| 112 | | eliun 4995 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ↔ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙)) |
| 113 | 112 | rexbii 3094 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑚 ∈
ℕ 𝑛 ∈ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ↔ ∃𝑚 ∈ ℕ ∃𝑙 ∈ (1...𝑚)𝑛 ∈ (𝑔‘𝑙)) |
| 114 | 111, 113 | bitr4i 278 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑥 ∈
ℕ 𝑛 ∈ (𝑔‘𝑥) ↔ ∃𝑚 ∈ ℕ 𝑛 ∈ ∪
𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) |
| 115 | 114 | abbii 2809 |
. . . . . . . . . . . . . . . 16
⊢ {𝑛 ∣ ∃𝑥 ∈ ℕ 𝑛 ∈ (𝑔‘𝑥)} = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 ∈ ∪
𝑙 ∈ (1...𝑚)(𝑔‘𝑙)} |
| 116 | 94, 115 | eqtri 2765 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 ∈ ∪
𝑙 ∈ (1...𝑚)(𝑔‘𝑙)} |
| 117 | | df-iun 4993 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑚 ∈ ℕ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) = {𝑛 ∣ ∃𝑚 ∈ ℕ 𝑛 ∈ ∪
𝑙 ∈ (1...𝑚)(𝑔‘𝑙)} |
| 118 | | ovex 7464 |
. . . . . . . . . . . . . . . . 17
⊢
(1...𝑚) ∈
V |
| 119 | 118, 63 | iunex 7993 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ V |
| 120 | 119 | dfiun3 5980 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑚 ∈ ℕ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) = ∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) |
| 121 | 116, 117,
120 | 3eqtr2i 2771 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = ∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) |
| 122 | | fofn 6822 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔:ℕ–onto→𝐴 → 𝑔 Fn ℕ) |
| 123 | | fniunfv 7267 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 Fn ℕ → ∪ 𝑥 ∈ ℕ (𝑔‘𝑥) = ∪ ran 𝑔) |
| 124 | 122, 123 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:ℕ–onto→𝐴 → ∪
𝑥 ∈ ℕ (𝑔‘𝑥) = ∪ ran 𝑔) |
| 125 | | forn 6823 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔:ℕ–onto→𝐴 → ran 𝑔 = 𝐴) |
| 126 | 125 | unieqd 4920 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:ℕ–onto→𝐴 → ∪ ran
𝑔 = ∪ 𝐴) |
| 127 | 124, 126 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (𝑔:ℕ–onto→𝐴 → ∪
𝑥 ∈ ℕ (𝑔‘𝑥) = ∪ 𝐴) |
| 128 | 121, 127 | eqtr3id 2791 |
. . . . . . . . . . . . 13
⊢ (𝑔:ℕ–onto→𝐴 → ∪ ran
(𝑚 ∈ ℕ ↦
∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = ∪ 𝐴) |
| 129 | 128 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝑔:ℕ–onto→𝐴 → (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (vol‘∪
𝐴)) |
| 130 | 129 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘∪ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (vol‘∪
𝐴)) |
| 131 | | rnco2 6273 |
. . . . . . . . . . . . . 14
⊢ ran (vol
∘ (𝑚 ∈ ℕ
↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (vol “ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) |
| 132 | | eqidd 2738 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) |
| 133 | | volf 25564 |
. . . . . . . . . . . . . . . . . . 19
⊢ vol:dom
vol⟶(0[,]+∞) |
| 134 | 133 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → vol:dom
vol⟶(0[,]+∞)) |
| 135 | 134 | feqmptd 6977 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → vol = (𝑛 ∈ dom vol ↦
(vol‘𝑛))) |
| 136 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) → (vol‘𝑛) = (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) |
| 137 | 54, 132, 135, 136 | fmptco 7149 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘
(𝑚 ∈ ℕ ↦
∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (𝑚 ∈ ℕ ↦ (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)))) |
| 138 | | mblvol 25565 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ∈ dom vol → (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) |
| 139 | 54, 138 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) |
| 140 | | mblss 25566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 ∈ dom vol → 𝑥 ⊆
ℝ) |
| 141 | 140 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑥 ∈ dom vol ∧
(vol‘𝑥) = 0) →
𝑥 ⊆
ℝ) |
| 142 | 25 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑥 ∈ dom vol →
((vol‘𝑥) = 0 ↔
(vol*‘𝑥) =
0)) |
| 143 | | 0re 11263 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 0 ∈
ℝ |
| 144 | | eleq1a 2836 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (0 ∈
ℝ → ((vol*‘𝑥) = 0 → (vol*‘𝑥) ∈ ℝ)) |
| 145 | 143, 144 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((vol*‘𝑥) = 0
→ (vol*‘𝑥)
∈ ℝ) |
| 146 | 142, 145 | biimtrdi 253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 ∈ dom vol →
((vol‘𝑥) = 0 →
(vol*‘𝑥) ∈
ℝ)) |
| 147 | 146 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑥 ∈ dom vol ∧
(vol‘𝑥) = 0) →
(vol*‘𝑥) ∈
ℝ) |
| 148 | 141, 147 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ dom vol ∧
(vol‘𝑥) = 0) →
(𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) |
| 149 | 148 | ralimi 3083 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∀𝑥 ∈
𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈
ℝ)) |
| 150 | 149 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈
ℝ)) |
| 151 | | ssid 4006 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ℕ
⊆ ℕ |
| 152 | | sseq1 4009 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑥 = (𝑔‘𝑙) → (𝑥 ⊆ ℝ ↔ (𝑔‘𝑙) ⊆ ℝ)) |
| 153 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 = (𝑔‘𝑙) → (vol*‘𝑥) = (vol*‘(𝑔‘𝑙))) |
| 154 | 153 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑥 = (𝑔‘𝑙) → ((vol*‘𝑥) ∈ ℝ ↔ (vol*‘(𝑔‘𝑙)) ∈ ℝ)) |
| 155 | 152, 154 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 = (𝑔‘𝑙) → ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ))) |
| 156 | 155 | ralima 7257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑔 Fn ℕ ∧ ℕ
⊆ ℕ) → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔
∀𝑙 ∈ ℕ
((𝑔‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑙)) ∈
ℝ))) |
| 157 | 122, 151,
156 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔
∀𝑙 ∈ ℕ
((𝑔‘𝑙) ⊆ ℝ ∧
(vol*‘(𝑔‘𝑙)) ∈
ℝ))) |
| 158 | | foima 6825 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑔:ℕ–onto→𝐴 → (𝑔 “ ℕ) = 𝐴) |
| 159 | 158 | raleqdv 3326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ (𝑔 “ ℕ)(𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) ↔
∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈
ℝ))) |
| 160 | 157, 159 | bitr3d 281 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑙 ∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈
ℝ))) |
| 161 | 160 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (∀𝑙 ∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈
ℝ))) |
| 162 | 150, 161 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ)) |
| 163 | | ssralv 4052 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((1...𝑚) ⊆
ℕ → (∀𝑙
∈ ℕ ((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ) → ∀𝑙 ∈ (1...𝑚)((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ))) |
| 164 | 38, 162, 163 | mpsyl 68 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ)) |
| 165 | 164 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∀𝑙 ∈ (1...𝑚)((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ)) |
| 166 | | ovolfiniun 25536 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((1...𝑚) ∈ Fin
∧ ∀𝑙 ∈
(1...𝑚)((𝑔‘𝑙) ⊆ ℝ ∧ (vol*‘(𝑔‘𝑙)) ∈ ℝ)) →
(vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙))) |
| 167 | 35, 165, 166 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙))) |
| 168 | | mblvol 25565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑔‘𝑙) ∈ dom vol → (vol‘(𝑔‘𝑙)) = (vol*‘(𝑔‘𝑙))) |
| 169 | 48, 168 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol‘(𝑔‘𝑙)) = (vol*‘(𝑔‘𝑙))) |
| 170 | 44 | simprd 495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((∀𝑥 ∈
𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔‘𝑙) ∈ 𝐴) → (vol‘(𝑔‘𝑙)) = 0) |
| 171 | 40, 170 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((∀𝑥 ∈
𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) ∧ (𝑔:ℕ–onto→𝐴 ∧ 𝑙 ∈ ℕ)) → (vol‘(𝑔‘𝑙)) = 0) |
| 172 | 171 | ancoms 458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑔:ℕ–onto→𝐴 ∧ 𝑙 ∈ ℕ) ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol‘(𝑔‘𝑙)) = 0) |
| 173 | 172 | an32s 652 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol‘(𝑔‘𝑙)) = 0) |
| 174 | 169, 173 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑙 ∈ ℕ) → (vol*‘(𝑔‘𝑙)) = 0) |
| 175 | 174 | ralrimiva 3146 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ ℕ
(vol*‘(𝑔‘𝑙)) = 0) |
| 176 | | ssralv 4052 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((1...𝑚) ⊆
ℕ → (∀𝑙
∈ ℕ (vol*‘(𝑔‘𝑙)) = 0 → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)) = 0)) |
| 177 | 38, 175, 176 | mpsyl 68 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)) = 0) |
| 178 | 177 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∀𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)) = 0) |
| 179 | 178 | sumeq2d 15737 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)) = Σ𝑙 ∈ (1...𝑚)0) |
| 180 | 35 | olci 867 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((1...𝑚) ⊆
(ℤ≥‘1) ∨ (1...𝑚) ∈ Fin) |
| 181 | | sumz 15758 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((1...𝑚) ⊆
(ℤ≥‘1) ∨ (1...𝑚) ∈ Fin) → Σ𝑙 ∈ (1...𝑚)0 = 0) |
| 182 | 180, 181 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Σ𝑙 ∈
(1...𝑚)0 =
0 |
| 183 | 179, 182 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → Σ𝑙 ∈ (1...𝑚)(vol*‘(𝑔‘𝑙)) = 0) |
| 184 | 167, 183 | breqtrd 5169 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ 0) |
| 185 | | mblss 25566 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑔‘𝑙) ∈ dom vol → (𝑔‘𝑙) ⊆ ℝ) |
| 186 | 185 | ralimi 3083 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∀𝑙 ∈
(1...𝑚)(𝑔‘𝑙) ∈ dom vol → ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ) |
| 187 | 51, 186 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ) |
| 188 | | iunss 5045 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ ↔ ∀𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ) |
| 189 | 187, 188 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ) |
| 190 | 189 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ) |
| 191 | | ovolge0 25516 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ → 0 ≤
(vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) |
| 192 | 190, 191 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → 0 ≤
(vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) |
| 193 | | ovolcl 25513 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙) ⊆ ℝ → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈
ℝ*) |
| 194 | 189, 193 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) →
(vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈
ℝ*) |
| 195 | 194 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈
ℝ*) |
| 196 | | 0xr 11308 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ∈
ℝ* |
| 197 | | xrletri3 13196 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ∈ ℝ* ∧ 0 ∈
ℝ*) → ((vol*‘∪
𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = 0 ↔ ((vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ 0 ∧ 0 ≤ (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))))) |
| 198 | 195, 196,
197 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → ((vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = 0 ↔ ((vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ≤ 0 ∧ 0 ≤ (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))))) |
| 199 | 184, 192,
198 | mpbir2and 713 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol*‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = 0) |
| 200 | 139, 199 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) ∧ 𝑚 ∈ ℕ) → (vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) = 0) |
| 201 | 200 | mpteq2dva 5242 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦
(vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (𝑚 ∈ ℕ ↦ 0)) |
| 202 | | fconstmpt 5747 |
. . . . . . . . . . . . . . . . 17
⊢ (ℕ
× {0}) = (𝑚 ∈
ℕ ↦ 0) |
| 203 | 201, 202 | eqtr4di 2795 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (𝑚 ∈ ℕ ↦
(vol‘∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (ℕ × {0})) |
| 204 | 137, 203 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘
(𝑚 ∈ ℕ ↦
∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (ℕ × {0})) |
| 205 | | frn 6743 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)):ℕ⟶dom vol → ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ⊆ dom vol) |
| 206 | | ffn 6736 |
. . . . . . . . . . . . . . . . . . 19
⊢ (vol:dom
vol⟶(0[,]+∞) → vol Fn dom vol) |
| 207 | 133, 206 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ vol Fn
dom vol |
| 208 | 119, 61 | fnmpti 6711 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) Fn ℕ |
| 209 | | fnco 6686 |
. . . . . . . . . . . . . . . . . 18
⊢ ((vol Fn
dom vol ∧ (𝑚 ∈
ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) Fn ℕ ∧ ran (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ⊆ dom vol) → (vol ∘
(𝑚 ∈ ℕ ↦
∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) Fn ℕ) |
| 210 | 207, 208,
209 | mp3an12 1453 |
. . . . . . . . . . . . . . . . 17
⊢ (ran
(𝑚 ∈ ℕ ↦
∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙)) ⊆ dom vol → (vol ∘ (𝑚 ∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) Fn ℕ) |
| 211 | 55, 205, 210 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol ∘
(𝑚 ∈ ℕ ↦
∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) Fn ℕ) |
| 212 | | 1nn 12277 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℕ |
| 213 | 212 | ne0ii 4344 |
. . . . . . . . . . . . . . . 16
⊢ ℕ
≠ ∅ |
| 214 | | fconst5 7226 |
. . . . . . . . . . . . . . . 16
⊢ (((vol
∘ (𝑚 ∈ ℕ
↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) Fn ℕ ∧ ℕ ≠ ∅)
→ ((vol ∘ (𝑚
∈ ℕ ↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (ℕ × {0}) ↔ ran (vol
∘ (𝑚 ∈ ℕ
↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = {0})) |
| 215 | 211, 213,
214 | sylancl 586 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ((vol ∘
(𝑚 ∈ ℕ ↦
∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = (ℕ × {0}) ↔ ran (vol
∘ (𝑚 ∈ ℕ
↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = {0})) |
| 216 | 204, 215 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → ran (vol ∘
(𝑚 ∈ ℕ ↦
∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = {0}) |
| 217 | 131, 216 | eqtr3id 2791 |
. . . . . . . . . . . . 13
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → (vol “ ran
(𝑚 ∈ ℕ ↦
∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))) = {0}) |
| 218 | 217 | supeq1d 9486 |
. . . . . . . . . . . 12
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → sup((vol “
ran (𝑚 ∈ ℕ
↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, < ) = sup({0},
ℝ*, < )) |
| 219 | | xrltso 13183 |
. . . . . . . . . . . . 13
⊢ < Or
ℝ* |
| 220 | | supsn 9512 |
. . . . . . . . . . . . 13
⊢ (( <
Or ℝ* ∧ 0 ∈ ℝ*) → sup({0},
ℝ*, < ) = 0) |
| 221 | 219, 196,
220 | mp2an 692 |
. . . . . . . . . . . 12
⊢ sup({0},
ℝ*, < ) = 0 |
| 222 | 218, 221 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → sup((vol “
ran (𝑚 ∈ ℕ
↦ ∪ 𝑙 ∈ (1...𝑚)(𝑔‘𝑙))), ℝ*, < ) =
0) |
| 223 | 93, 130, 222 | 3eqtr3rd 2786 |
. . . . . . . . . 10
⊢ ((𝑔:ℕ–onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0)) → 0 =
(vol‘∪ 𝐴)) |
| 224 | 223 | ex 412 |
. . . . . . . . 9
⊢ (𝑔:ℕ–onto→𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 ∈ dom vol ∧ (vol‘𝑥) = 0) → 0 =
(vol‘∪ 𝐴))) |
| 225 | 34, 224 | syl5 34 |
. . . . . . . 8
⊢ (𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ) → 0 = (vol‘∪ 𝐴))) |
| 226 | 225 | exlimiv 1930 |
. . . . . . 7
⊢
(∃𝑔 𝑔:ℕ–onto→𝐴 → ((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ) → 0 = (vol‘∪ 𝐴))) |
| 227 | 18, 226 | syl 17 |
. . . . . 6
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≼ ℕ) →
((∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ) → 0 = (vol‘∪ 𝐴))) |
| 228 | 227 | expimpd 453 |
. . . . 5
⊢ (𝐴 ≠ ∅ → ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol‘∪ 𝐴))) |
| 229 | 11, 228 | pm2.61ine 3025 |
. . . 4
⊢ ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → 0 = (vol‘∪ 𝐴)) |
| 230 | | renepnf 11309 |
. . . . . . 7
⊢ (0 ∈
ℝ → 0 ≠ +∞) |
| 231 | 143, 230 | mp1i 13 |
. . . . . 6
⊢ (∪ 𝐴 =
ℝ → 0 ≠ +∞) |
| 232 | | fveq2 6906 |
. . . . . . 7
⊢ (∪ 𝐴 =
ℝ → (vol‘∪ 𝐴) = (vol‘ℝ)) |
| 233 | | rembl 25575 |
. . . . . . . . 9
⊢ ℝ
∈ dom vol |
| 234 | | mblvol 25565 |
. . . . . . . . 9
⊢ (ℝ
∈ dom vol → (vol‘ℝ) =
(vol*‘ℝ)) |
| 235 | 233, 234 | ax-mp 5 |
. . . . . . . 8
⊢
(vol‘ℝ) = (vol*‘ℝ) |
| 236 | | ovolre 25560 |
. . . . . . . 8
⊢
(vol*‘ℝ) = +∞ |
| 237 | 235, 236 | eqtri 2765 |
. . . . . . 7
⊢
(vol‘ℝ) = +∞ |
| 238 | 232, 237 | eqtrdi 2793 |
. . . . . 6
⊢ (∪ 𝐴 =
ℝ → (vol‘∪ 𝐴) = +∞) |
| 239 | 231, 238 | neeqtrrd 3015 |
. . . . 5
⊢ (∪ 𝐴 =
ℝ → 0 ≠ (vol‘∪ 𝐴)) |
| 240 | 239 | necon2i 2975 |
. . . 4
⊢ (0 =
(vol‘∪ 𝐴) → ∪ 𝐴 ≠ ℝ) |
| 241 | 229, 240 | syl 17 |
. . 3
⊢ ((𝐴 ≼ ℕ ∧
(∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ ∧ ∪ 𝐴
⊆ ℝ)) → ∪ 𝐴 ≠ ℝ) |
| 242 | 241 | expr 456 |
. 2
⊢ ((𝐴 ≼ ℕ ∧
∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → (∪ 𝐴
⊆ ℝ → ∪ 𝐴 ≠ ℝ)) |
| 243 | | eqimss 4042 |
. . 3
⊢ (∪ 𝐴 =
ℝ → ∪ 𝐴 ⊆ ℝ) |
| 244 | 243 | necon3bi 2967 |
. 2
⊢ (¬
∪ 𝐴 ⊆ ℝ → ∪ 𝐴
≠ ℝ) |
| 245 | 242, 244 | pm2.61d1 180 |
1
⊢ ((𝐴 ≼ ℕ ∧
∀𝑥 ∈ 𝐴 𝑥 ≼ ℕ) → ∪ 𝐴
≠ ℝ) |