Step | Hyp | Ref
| Expression |
1 | | i1fd.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
2 | 1 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → 𝐹:ℝ⟶ℝ) |
3 | | ffun 5961 |
. . . . . . . 8
⊢ (𝐹:ℝ⟶ℝ →
Fun 𝐹) |
4 | | funcnvcnv 5870 |
. . . . . . . 8
⊢ (Fun
𝐹 → Fun ◡◡𝐹) |
5 | | imadif 5887 |
. . . . . . . 8
⊢ (Fun
◡◡𝐹 → (◡𝐹 “ (ℝ ∖ (ℝ ∖
𝑥))) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥)))) |
6 | 2, 3, 4, 5 | 4syl 19 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ (ℝ ∖ (ℝ ∖
𝑥))) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥)))) |
7 | | ioof 12142 |
. . . . . . . . . . . . 13
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
8 | | frn 5966 |
. . . . . . . . . . . . 13
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → ran (,) ⊆ 𝒫 ℝ) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ran (,)
⊆ 𝒫 ℝ |
10 | 9 | sseli 3564 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ran (,) → 𝑥 ∈ 𝒫
ℝ) |
11 | 10 | elpwid 4118 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ran (,) → 𝑥 ⊆
ℝ) |
12 | 11 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → 𝑥 ⊆ ℝ) |
13 | | dfss4 3820 |
. . . . . . . . 9
⊢ (𝑥 ⊆ ℝ ↔ (ℝ
∖ (ℝ ∖ 𝑥)) = 𝑥) |
14 | 12, 13 | sylib 207 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (ℝ ∖
(ℝ ∖ 𝑥)) =
𝑥) |
15 | 14 | imaeq2d 5385 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ (ℝ ∖ (ℝ ∖
𝑥))) = (◡𝐹 “ 𝑥)) |
16 | 6, 15 | eqtr3d 2646 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))) = (◡𝐹 “ 𝑥)) |
17 | | fimacnv 6255 |
. . . . . . . . 9
⊢ (𝐹:ℝ⟶ℝ →
(◡𝐹 “ ℝ) =
ℝ) |
18 | 2, 17 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ ℝ) =
ℝ) |
19 | | rembl 23115 |
. . . . . . . 8
⊢ ℝ
∈ dom vol |
20 | 18, 19 | syl6eqel 2696 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ ℝ) ∈ dom
vol) |
21 | 1 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → 𝐹:ℝ⟶ℝ) |
22 | | inpreima 6250 |
. . . . . . . . . . . . . 14
⊢ (Fun
𝐹 → (◡𝐹 “ (𝑦 ∩ ran 𝐹)) = ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ ran 𝐹))) |
23 | | iunid 4511 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹){𝑥} = (𝑦 ∩ ran 𝐹) |
24 | 23 | imaeq2i 5383 |
. . . . . . . . . . . . . . 15
⊢ (◡𝐹 “ ∪
𝑥 ∈ (𝑦 ∩ ran 𝐹){𝑥}) = (◡𝐹 “ (𝑦 ∩ ran 𝐹)) |
25 | | imaiun 6407 |
. . . . . . . . . . . . . . 15
⊢ (◡𝐹 “ ∪
𝑥 ∈ (𝑦 ∩ ran 𝐹){𝑥}) = ∪
𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) |
26 | 24, 25 | eqtr3i 2634 |
. . . . . . . . . . . . . 14
⊢ (◡𝐹 “ (𝑦 ∩ ran 𝐹)) = ∪
𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) |
27 | | cnvimass 5404 |
. . . . . . . . . . . . . . . 16
⊢ (◡𝐹 “ 𝑦) ⊆ dom 𝐹 |
28 | | cnvimarndm 5405 |
. . . . . . . . . . . . . . . 16
⊢ (◡𝐹 “ ran 𝐹) = dom 𝐹 |
29 | 27, 28 | sseqtr4i 3601 |
. . . . . . . . . . . . . . 15
⊢ (◡𝐹 “ 𝑦) ⊆ (◡𝐹 “ ran 𝐹) |
30 | | df-ss 3554 |
. . . . . . . . . . . . . . 15
⊢ ((◡𝐹 “ 𝑦) ⊆ (◡𝐹 “ ran 𝐹) ↔ ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ ran 𝐹)) = (◡𝐹 “ 𝑦)) |
31 | 29, 30 | mpbi 219 |
. . . . . . . . . . . . . 14
⊢ ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ ran 𝐹)) = (◡𝐹 “ 𝑦) |
32 | 22, 26, 31 | 3eqtr3g 2667 |
. . . . . . . . . . . . 13
⊢ (Fun
𝐹 → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) = (◡𝐹 “ 𝑦)) |
33 | 21, 3, 32 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) = (◡𝐹 “ 𝑦)) |
34 | | i1fd.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ran 𝐹 ∈ Fin) |
35 | 34 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ran 𝐹 ∈ Fin) |
36 | | inss2 3796 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∩ ran 𝐹) ⊆ ran 𝐹 |
37 | | ssfi 8065 |
. . . . . . . . . . . . . 14
⊢ ((ran
𝐹 ∈ Fin ∧ (𝑦 ∩ ran 𝐹) ⊆ ran 𝐹) → (𝑦 ∩ ran 𝐹) ∈ Fin) |
38 | 35, 36, 37 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (𝑦 ∩ ran 𝐹) ∈ Fin) |
39 | | simpll 786 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → 𝜑) |
40 | | inss1 3795 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∩ ran 𝐹) ⊆ 𝑦 |
41 | 40 | sseli 3564 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
(𝑦 ∩ ran 𝐹) → 0 ∈ 𝑦) |
42 | 41 | con3i 149 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬ 0
∈ 𝑦 → ¬ 0
∈ (𝑦 ∩ ran 𝐹)) |
43 | 42 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ¬ 0 ∈ (𝑦 ∩ ran 𝐹)) |
44 | | disjsn 4192 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ ¬ 0 ∈
(𝑦 ∩ ran 𝐹)) |
45 | 43, 44 | sylibr 223 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅) |
46 | | reldisj 3972 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∩ ran 𝐹) ⊆ ran 𝐹 → (((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ (𝑦 ∩ ran 𝐹) ⊆ (ran 𝐹 ∖ {0}))) |
47 | 36, 46 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ (𝑦 ∩ ran 𝐹) ⊆ (ran 𝐹 ∖ {0})) |
48 | 45, 47 | sylib 207 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (𝑦 ∩ ran 𝐹) ⊆ (ran 𝐹 ∖ {0})) |
49 | 48 | sselda 3568 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → 𝑥 ∈ (ran 𝐹 ∖ {0})) |
50 | | i1fd.3 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → (◡𝐹 “ {𝑥}) ∈ dom vol) |
51 | 39, 49, 50 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (◡𝐹 “ {𝑥}) ∈ dom vol) |
52 | 51 | ralrimiva 2949 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol) |
53 | | finiunmbl 23119 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∩ ran 𝐹) ∈ Fin ∧ ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol) → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol) |
54 | 38, 52, 53 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol) |
55 | 33, 54 | eqeltrrd 2689 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (◡𝐹 “ 𝑦) ∈ dom vol) |
56 | 55 | ex 449 |
. . . . . . . . . 10
⊢ (𝜑 → (¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol)) |
57 | 56 | alrimiv 1842 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑦(¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol)) |
58 | 57 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ∀𝑦(¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol)) |
59 | | elndif 3696 |
. . . . . . . . 9
⊢ (0 ∈
𝑥 → ¬ 0 ∈
(ℝ ∖ 𝑥)) |
60 | 59 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ¬ 0 ∈ (ℝ
∖ 𝑥)) |
61 | | reex 9906 |
. . . . . . . . . 10
⊢ ℝ
∈ V |
62 | | difexg 4735 |
. . . . . . . . . 10
⊢ (ℝ
∈ V → (ℝ ∖ 𝑥) ∈ V) |
63 | 61, 62 | ax-mp 5 |
. . . . . . . . 9
⊢ (ℝ
∖ 𝑥) ∈
V |
64 | | eleq2 2677 |
. . . . . . . . . . 11
⊢ (𝑦 = (ℝ ∖ 𝑥) → (0 ∈ 𝑦 ↔ 0 ∈ (ℝ
∖ 𝑥))) |
65 | 64 | notbid 307 |
. . . . . . . . . 10
⊢ (𝑦 = (ℝ ∖ 𝑥) → (¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ (ℝ
∖ 𝑥))) |
66 | | imaeq2 5381 |
. . . . . . . . . . 11
⊢ (𝑦 = (ℝ ∖ 𝑥) → (◡𝐹 “ 𝑦) = (◡𝐹 “ (ℝ ∖ 𝑥))) |
67 | 66 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑦 = (ℝ ∖ 𝑥) → ((◡𝐹 “ 𝑦) ∈ dom vol ↔ (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol)) |
68 | 65, 67 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑦 = (ℝ ∖ 𝑥) → ((¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) ↔ (¬ 0 ∈
(ℝ ∖ 𝑥) →
(◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol))) |
69 | 63, 68 | spcv 3272 |
. . . . . . . 8
⊢
(∀𝑦(¬ 0
∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) → (¬ 0 ∈
(ℝ ∖ 𝑥) →
(◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol)) |
70 | 58, 60, 69 | sylc 63 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol) |
71 | | difmbl 23118 |
. . . . . . 7
⊢ (((◡𝐹 “ ℝ) ∈ dom vol ∧
(◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))) ∈ dom vol) |
72 | 20, 70, 71 | syl2anc 691 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))) ∈ dom vol) |
73 | 16, 72 | eqeltrrd 2689 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ 𝑥) ∈ dom vol) |
74 | | eleq2 2677 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (0 ∈ 𝑦 ↔ 0 ∈ 𝑥)) |
75 | 74 | notbid 307 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ 𝑥)) |
76 | | imaeq2 5381 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (◡𝐹 “ 𝑦) = (◡𝐹 “ 𝑥)) |
77 | 76 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → ((◡𝐹 “ 𝑦) ∈ dom vol ↔ (◡𝐹 “ 𝑥) ∈ dom vol)) |
78 | 75, 77 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) ↔ (¬ 0 ∈
𝑥 → (◡𝐹 “ 𝑥) ∈ dom vol))) |
79 | 78 | spv 2248 |
. . . . . . . 8
⊢
(∀𝑦(¬ 0
∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) → (¬ 0 ∈
𝑥 → (◡𝐹 “ 𝑥) ∈ dom vol)) |
80 | 57, 79 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (¬ 0 ∈ 𝑥 → (◡𝐹 “ 𝑥) ∈ dom vol)) |
81 | 80 | imp 444 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑥) → (◡𝐹 “ 𝑥) ∈ dom vol) |
82 | 81 | adantlr 747 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ ¬ 0 ∈ 𝑥) → (◡𝐹 “ 𝑥) ∈ dom vol) |
83 | 73, 82 | pm2.61dan 828 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ran (,)) → (◡𝐹 “ 𝑥) ∈ dom vol) |
84 | 83 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol) |
85 | | ismbf 23203 |
. . . 4
⊢ (𝐹:ℝ⟶ℝ →
(𝐹 ∈ MblFn ↔
∀𝑥 ∈ ran
(,)(◡𝐹 “ 𝑥) ∈ dom vol)) |
86 | 1, 85 | syl 17 |
. . 3
⊢ (𝜑 → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol)) |
87 | 84, 86 | mpbird 246 |
. 2
⊢ (𝜑 → 𝐹 ∈ MblFn) |
88 | | mblvol 23105 |
. . . . . . . 8
⊢ ((◡𝐹 “ 𝑦) ∈ dom vol → (vol‘(◡𝐹 “ 𝑦)) = (vol*‘(◡𝐹 “ 𝑦))) |
89 | 55, 88 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol‘(◡𝐹 “ 𝑦)) = (vol*‘(◡𝐹 “ 𝑦))) |
90 | | mblss 23106 |
. . . . . . . . 9
⊢ ((◡𝐹 “ 𝑦) ∈ dom vol → (◡𝐹 “ 𝑦) ⊆ ℝ) |
91 | 55, 90 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (◡𝐹 “ 𝑦) ⊆ ℝ) |
92 | | mblvol 23105 |
. . . . . . . . . . 11
⊢ ((◡𝐹 “ {𝑥}) ∈ dom vol → (vol‘(◡𝐹 “ {𝑥})) = (vol*‘(◡𝐹 “ {𝑥}))) |
93 | 51, 92 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (vol‘(◡𝐹 “ {𝑥})) = (vol*‘(◡𝐹 “ {𝑥}))) |
94 | | i1fd.4 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → (vol‘(◡𝐹 “ {𝑥})) ∈ ℝ) |
95 | 39, 49, 94 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (vol‘(◡𝐹 “ {𝑥})) ∈ ℝ) |
96 | 93, 95 | eqeltrrd 2689 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ) |
97 | 38, 96 | fsumrecl 14312 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ) |
98 | 33 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})) = (vol*‘(◡𝐹 “ 𝑦))) |
99 | | mblss 23106 |
. . . . . . . . . . . . 13
⊢ ((◡𝐹 “ {𝑥}) ∈ dom vol → (◡𝐹 “ {𝑥}) ⊆ ℝ) |
100 | 51, 99 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (◡𝐹 “ {𝑥}) ⊆ ℝ) |
101 | 100, 96 | jca 553 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → ((◡𝐹 “ {𝑥}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ)) |
102 | 101 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)((◡𝐹 “ {𝑥}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ)) |
103 | | ovolfiniun 23076 |
. . . . . . . . . 10
⊢ (((𝑦 ∩ ran 𝐹) ∈ Fin ∧ ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)((◡𝐹 “ {𝑥}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ)) →
(vol*‘∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥}))) |
104 | 38, 102, 103 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥}))) |
105 | 98, 104 | eqbrtrrd 4607 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘(◡𝐹 “ 𝑦)) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥}))) |
106 | | ovollecl 23058 |
. . . . . . . 8
⊢ (((◡𝐹 “ 𝑦) ⊆ ℝ ∧ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ ∧ (vol*‘(◡𝐹 “ 𝑦)) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥}))) → (vol*‘(◡𝐹 “ 𝑦)) ∈ ℝ) |
107 | 91, 97, 105, 106 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘(◡𝐹 “ 𝑦)) ∈ ℝ) |
108 | 89, 107 | eqeltrd 2688 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ) |
109 | 108 | ex 449 |
. . . . 5
⊢ (𝜑 → (¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ)) |
110 | 109 | alrimiv 1842 |
. . . 4
⊢ (𝜑 → ∀𝑦(¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ)) |
111 | | neldifsn 4262 |
. . . 4
⊢ ¬ 0
∈ (ℝ ∖ {0}) |
112 | | difexg 4735 |
. . . . . 6
⊢ (ℝ
∈ V → (ℝ ∖ {0}) ∈ V) |
113 | 61, 112 | ax-mp 5 |
. . . . 5
⊢ (ℝ
∖ {0}) ∈ V |
114 | | eleq2 2677 |
. . . . . . 7
⊢ (𝑦 = (ℝ ∖ {0}) →
(0 ∈ 𝑦 ↔ 0 ∈
(ℝ ∖ {0}))) |
115 | 114 | notbid 307 |
. . . . . 6
⊢ (𝑦 = (ℝ ∖ {0}) →
(¬ 0 ∈ 𝑦 ↔
¬ 0 ∈ (ℝ ∖ {0}))) |
116 | | imaeq2 5381 |
. . . . . . . 8
⊢ (𝑦 = (ℝ ∖ {0}) →
(◡𝐹 “ 𝑦) = (◡𝐹 “ (ℝ ∖
{0}))) |
117 | 116 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑦 = (ℝ ∖ {0}) →
(vol‘(◡𝐹 “ 𝑦)) = (vol‘(◡𝐹 “ (ℝ ∖
{0})))) |
118 | 117 | eleq1d 2672 |
. . . . . 6
⊢ (𝑦 = (ℝ ∖ {0}) →
((vol‘(◡𝐹 “ 𝑦)) ∈ ℝ ↔ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ)) |
119 | 115, 118 | imbi12d 333 |
. . . . 5
⊢ (𝑦 = (ℝ ∖ {0}) →
((¬ 0 ∈ 𝑦 →
(vol‘(◡𝐹 “ 𝑦)) ∈ ℝ) ↔ (¬ 0 ∈
(ℝ ∖ {0}) → (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ))) |
120 | 113, 119 | spcv 3272 |
. . . 4
⊢
(∀𝑦(¬ 0
∈ 𝑦 →
(vol‘(◡𝐹 “ 𝑦)) ∈ ℝ) → (¬ 0 ∈
(ℝ ∖ {0}) → (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ)) |
121 | 110, 111,
120 | mpisyl 21 |
. . 3
⊢ (𝜑 → (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ) |
122 | 1, 34, 121 | 3jca 1235 |
. 2
⊢ (𝜑 → (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧
(vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ)) |
123 | | isi1f 23247 |
. 2
⊢ (𝐹 ∈ dom ∫1
↔ (𝐹 ∈ MblFn
∧ (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧
(vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ))) |
124 | 87, 122, 123 | sylanbrc 695 |
1
⊢ (𝜑 → 𝐹 ∈ dom
∫1) |