Step | Hyp | Ref
| Expression |
1 | | i1fd.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
2 | 1 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → 𝐹:ℝ⟶ℝ) |
3 | | ffun 6048 |
. . . . . . . 8
⊢ (𝐹:ℝ⟶ℝ →
Fun 𝐹) |
4 | | funcnvcnv 5956 |
. . . . . . . 8
⊢ (Fun
𝐹 → Fun ◡◡𝐹) |
5 | | imadif 5973 |
. . . . . . . 8
⊢ (Fun
◡◡𝐹 → (◡𝐹 “ (ℝ ∖ (ℝ ∖
𝑥))) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥)))) |
6 | 2, 3, 4, 5 | 4syl 19 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ (ℝ ∖ (ℝ ∖
𝑥))) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥)))) |
7 | | ioof 12271 |
. . . . . . . . . . . . 13
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
8 | | frn 6053 |
. . . . . . . . . . . . 13
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → ran (,) ⊆ 𝒫 ℝ) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ran (,)
⊆ 𝒫 ℝ |
10 | 9 | sseli 3599 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ran (,) → 𝑥 ∈ 𝒫
ℝ) |
11 | 10 | elpwid 4170 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ran (,) → 𝑥 ⊆
ℝ) |
12 | 11 | ad2antlr 763 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → 𝑥 ⊆ ℝ) |
13 | | dfss4 3858 |
. . . . . . . . 9
⊢ (𝑥 ⊆ ℝ ↔ (ℝ
∖ (ℝ ∖ 𝑥)) = 𝑥) |
14 | 12, 13 | sylib 208 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (ℝ ∖
(ℝ ∖ 𝑥)) =
𝑥) |
15 | 14 | imaeq2d 5466 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ (ℝ ∖ (ℝ ∖
𝑥))) = (◡𝐹 “ 𝑥)) |
16 | 6, 15 | eqtr3d 2658 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))) = (◡𝐹 “ 𝑥)) |
17 | | fimacnv 6347 |
. . . . . . . . 9
⊢ (𝐹:ℝ⟶ℝ →
(◡𝐹 “ ℝ) =
ℝ) |
18 | 2, 17 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ ℝ) =
ℝ) |
19 | | rembl 23308 |
. . . . . . . 8
⊢ ℝ
∈ dom vol |
20 | 18, 19 | syl6eqel 2709 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ ℝ) ∈ dom
vol) |
21 | 1 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → 𝐹:ℝ⟶ℝ) |
22 | | inpreima 6342 |
. . . . . . . . . . . . . 14
⊢ (Fun
𝐹 → (◡𝐹 “ (𝑦 ∩ ran 𝐹)) = ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ ran 𝐹))) |
23 | | iunid 4575 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹){𝑥} = (𝑦 ∩ ran 𝐹) |
24 | 23 | imaeq2i 5464 |
. . . . . . . . . . . . . . 15
⊢ (◡𝐹 “ ∪
𝑥 ∈ (𝑦 ∩ ran 𝐹){𝑥}) = (◡𝐹 “ (𝑦 ∩ ran 𝐹)) |
25 | | imaiun 6503 |
. . . . . . . . . . . . . . 15
⊢ (◡𝐹 “ ∪
𝑥 ∈ (𝑦 ∩ ran 𝐹){𝑥}) = ∪
𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) |
26 | 24, 25 | eqtr3i 2646 |
. . . . . . . . . . . . . 14
⊢ (◡𝐹 “ (𝑦 ∩ ran 𝐹)) = ∪
𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) |
27 | | cnvimass 5485 |
. . . . . . . . . . . . . . . 16
⊢ (◡𝐹 “ 𝑦) ⊆ dom 𝐹 |
28 | | cnvimarndm 5486 |
. . . . . . . . . . . . . . . 16
⊢ (◡𝐹 “ ran 𝐹) = dom 𝐹 |
29 | 27, 28 | sseqtr4i 3638 |
. . . . . . . . . . . . . . 15
⊢ (◡𝐹 “ 𝑦) ⊆ (◡𝐹 “ ran 𝐹) |
30 | | df-ss 3588 |
. . . . . . . . . . . . . . 15
⊢ ((◡𝐹 “ 𝑦) ⊆ (◡𝐹 “ ran 𝐹) ↔ ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ ran 𝐹)) = (◡𝐹 “ 𝑦)) |
31 | 29, 30 | mpbi 220 |
. . . . . . . . . . . . . 14
⊢ ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ ran 𝐹)) = (◡𝐹 “ 𝑦) |
32 | 22, 26, 31 | 3eqtr3g 2679 |
. . . . . . . . . . . . 13
⊢ (Fun
𝐹 → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) = (◡𝐹 “ 𝑦)) |
33 | 21, 3, 32 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) = (◡𝐹 “ 𝑦)) |
34 | | i1fd.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ran 𝐹 ∈ Fin) |
35 | 34 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ran 𝐹 ∈ Fin) |
36 | | inss2 3834 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∩ ran 𝐹) ⊆ ran 𝐹 |
37 | | ssfi 8180 |
. . . . . . . . . . . . . 14
⊢ ((ran
𝐹 ∈ Fin ∧ (𝑦 ∩ ran 𝐹) ⊆ ran 𝐹) → (𝑦 ∩ ran 𝐹) ∈ Fin) |
38 | 35, 36, 37 | sylancl 694 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (𝑦 ∩ ran 𝐹) ∈ Fin) |
39 | | simpll 790 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → 𝜑) |
40 | | inss1 3833 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∩ ran 𝐹) ⊆ 𝑦 |
41 | 40 | sseli 3599 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
(𝑦 ∩ ran 𝐹) → 0 ∈ 𝑦) |
42 | 41 | con3i 150 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬ 0
∈ 𝑦 → ¬ 0
∈ (𝑦 ∩ ran 𝐹)) |
43 | 42 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ¬ 0 ∈ (𝑦 ∩ ran 𝐹)) |
44 | | disjsn 4246 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ ¬ 0 ∈
(𝑦 ∩ ran 𝐹)) |
45 | 43, 44 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅) |
46 | | reldisj 4020 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∩ ran 𝐹) ⊆ ran 𝐹 → (((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ (𝑦 ∩ ran 𝐹) ⊆ (ran 𝐹 ∖ {0}))) |
47 | 36, 46 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ (𝑦 ∩ ran 𝐹) ⊆ (ran 𝐹 ∖ {0})) |
48 | 45, 47 | sylib 208 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (𝑦 ∩ ran 𝐹) ⊆ (ran 𝐹 ∖ {0})) |
49 | 48 | sselda 3603 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → 𝑥 ∈ (ran 𝐹 ∖ {0})) |
50 | | i1fd.3 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → (◡𝐹 “ {𝑥}) ∈ dom vol) |
51 | 39, 49, 50 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (◡𝐹 “ {𝑥}) ∈ dom vol) |
52 | 51 | ralrimiva 2966 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol) |
53 | | finiunmbl 23312 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∩ ran 𝐹) ∈ Fin ∧ ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol) → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol) |
54 | 38, 52, 53 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol) |
55 | 33, 54 | eqeltrrd 2702 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (◡𝐹 “ 𝑦) ∈ dom vol) |
56 | 55 | ex 450 |
. . . . . . . . . 10
⊢ (𝜑 → (¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol)) |
57 | 56 | alrimiv 1855 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑦(¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol)) |
58 | 57 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ∀𝑦(¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol)) |
59 | | elndif 3734 |
. . . . . . . . 9
⊢ (0 ∈
𝑥 → ¬ 0 ∈
(ℝ ∖ 𝑥)) |
60 | 59 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ¬ 0 ∈ (ℝ
∖ 𝑥)) |
61 | | reex 10027 |
. . . . . . . . . 10
⊢ ℝ
∈ V |
62 | | difexg 4808 |
. . . . . . . . . 10
⊢ (ℝ
∈ V → (ℝ ∖ 𝑥) ∈ V) |
63 | 61, 62 | ax-mp 5 |
. . . . . . . . 9
⊢ (ℝ
∖ 𝑥) ∈
V |
64 | | eleq2 2690 |
. . . . . . . . . . 11
⊢ (𝑦 = (ℝ ∖ 𝑥) → (0 ∈ 𝑦 ↔ 0 ∈ (ℝ
∖ 𝑥))) |
65 | 64 | notbid 308 |
. . . . . . . . . 10
⊢ (𝑦 = (ℝ ∖ 𝑥) → (¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ (ℝ
∖ 𝑥))) |
66 | | imaeq2 5462 |
. . . . . . . . . . 11
⊢ (𝑦 = (ℝ ∖ 𝑥) → (◡𝐹 “ 𝑦) = (◡𝐹 “ (ℝ ∖ 𝑥))) |
67 | 66 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (𝑦 = (ℝ ∖ 𝑥) → ((◡𝐹 “ 𝑦) ∈ dom vol ↔ (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol)) |
68 | 65, 67 | imbi12d 334 |
. . . . . . . . 9
⊢ (𝑦 = (ℝ ∖ 𝑥) → ((¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) ↔ (¬ 0 ∈
(ℝ ∖ 𝑥) →
(◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol))) |
69 | 63, 68 | spcv 3299 |
. . . . . . . 8
⊢
(∀𝑦(¬ 0
∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) → (¬ 0 ∈
(ℝ ∖ 𝑥) →
(◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol)) |
70 | 58, 60, 69 | sylc 65 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol) |
71 | | difmbl 23311 |
. . . . . . 7
⊢ (((◡𝐹 “ ℝ) ∈ dom vol ∧
(◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))) ∈ dom vol) |
72 | 20, 70, 71 | syl2anc 693 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))) ∈ dom vol) |
73 | 16, 72 | eqeltrrd 2702 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ 𝑥) ∈ dom vol) |
74 | | eleq2 2690 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (0 ∈ 𝑦 ↔ 0 ∈ 𝑥)) |
75 | 74 | notbid 308 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ 𝑥)) |
76 | | imaeq2 5462 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (◡𝐹 “ 𝑦) = (◡𝐹 “ 𝑥)) |
77 | 76 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → ((◡𝐹 “ 𝑦) ∈ dom vol ↔ (◡𝐹 “ 𝑥) ∈ dom vol)) |
78 | 75, 77 | imbi12d 334 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) ↔ (¬ 0 ∈
𝑥 → (◡𝐹 “ 𝑥) ∈ dom vol))) |
79 | 78 | spv 2260 |
. . . . . . . 8
⊢
(∀𝑦(¬ 0
∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) → (¬ 0 ∈
𝑥 → (◡𝐹 “ 𝑥) ∈ dom vol)) |
80 | 57, 79 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (¬ 0 ∈ 𝑥 → (◡𝐹 “ 𝑥) ∈ dom vol)) |
81 | 80 | imp 445 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑥) → (◡𝐹 “ 𝑥) ∈ dom vol) |
82 | 81 | adantlr 751 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ ¬ 0 ∈ 𝑥) → (◡𝐹 “ 𝑥) ∈ dom vol) |
83 | 73, 82 | pm2.61dan 832 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ran (,)) → (◡𝐹 “ 𝑥) ∈ dom vol) |
84 | 83 | ralrimiva 2966 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol) |
85 | | ismbf 23397 |
. . . 4
⊢ (𝐹:ℝ⟶ℝ →
(𝐹 ∈ MblFn ↔
∀𝑥 ∈ ran
(,)(◡𝐹 “ 𝑥) ∈ dom vol)) |
86 | 1, 85 | syl 17 |
. . 3
⊢ (𝜑 → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol)) |
87 | 84, 86 | mpbird 247 |
. 2
⊢ (𝜑 → 𝐹 ∈ MblFn) |
88 | | mblvol 23298 |
. . . . . . . 8
⊢ ((◡𝐹 “ 𝑦) ∈ dom vol → (vol‘(◡𝐹 “ 𝑦)) = (vol*‘(◡𝐹 “ 𝑦))) |
89 | 55, 88 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol‘(◡𝐹 “ 𝑦)) = (vol*‘(◡𝐹 “ 𝑦))) |
90 | | mblss 23299 |
. . . . . . . . 9
⊢ ((◡𝐹 “ 𝑦) ∈ dom vol → (◡𝐹 “ 𝑦) ⊆ ℝ) |
91 | 55, 90 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (◡𝐹 “ 𝑦) ⊆ ℝ) |
92 | | mblvol 23298 |
. . . . . . . . . . 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 693 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (vol‘(◡𝐹 “ {𝑥})) ∈ ℝ) |
96 | 93, 95 | eqeltrrd 2702 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ) |
97 | 38, 96 | fsumrecl 14465 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ) |
98 | 33 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})) = (vol*‘(◡𝐹 “ 𝑦))) |
99 | | mblss 23299 |
. . . . . . . . . . . . 13
⊢ ((◡𝐹 “ {𝑥}) ∈ dom vol → (◡𝐹 “ {𝑥}) ⊆ ℝ) |
100 | 51, 99 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (◡𝐹 “ {𝑥}) ⊆ ℝ) |
101 | 100, 96 | jca 554 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → ((◡𝐹 “ {𝑥}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ)) |
102 | 101 | ralrimiva 2966 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)((◡𝐹 “ {𝑥}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ)) |
103 | | ovolfiniun 23269 |
. . . . . . . . . 10
⊢ (((𝑦 ∩ ran 𝐹) ∈ Fin ∧ ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)((◡𝐹 “ {𝑥}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ)) →
(vol*‘∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥}))) |
104 | 38, 102, 103 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥}))) |
105 | 98, 104 | eqbrtrrd 4677 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘(◡𝐹 “ 𝑦)) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥}))) |
106 | | ovollecl 23251 |
. . . . . . . 8
⊢ (((◡𝐹 “ 𝑦) ⊆ ℝ ∧ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ ∧ (vol*‘(◡𝐹 “ 𝑦)) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥}))) → (vol*‘(◡𝐹 “ 𝑦)) ∈ ℝ) |
107 | 91, 97, 105, 106 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘(◡𝐹 “ 𝑦)) ∈ ℝ) |
108 | 89, 107 | eqeltrd 2701 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ) |
109 | 108 | ex 450 |
. . . . 5
⊢ (𝜑 → (¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ)) |
110 | 109 | alrimiv 1855 |
. . . 4
⊢ (𝜑 → ∀𝑦(¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ)) |
111 | | neldifsn 4321 |
. . . 4
⊢ ¬ 0
∈ (ℝ ∖ {0}) |
112 | | difexg 4808 |
. . . . . 6
⊢ (ℝ
∈ V → (ℝ ∖ {0}) ∈ V) |
113 | 61, 112 | ax-mp 5 |
. . . . 5
⊢ (ℝ
∖ {0}) ∈ V |
114 | | eleq2 2690 |
. . . . . . 7
⊢ (𝑦 = (ℝ ∖ {0}) →
(0 ∈ 𝑦 ↔ 0 ∈
(ℝ ∖ {0}))) |
115 | 114 | notbid 308 |
. . . . . 6
⊢ (𝑦 = (ℝ ∖ {0}) →
(¬ 0 ∈ 𝑦 ↔
¬ 0 ∈ (ℝ ∖ {0}))) |
116 | | imaeq2 5462 |
. . . . . . . 8
⊢ (𝑦 = (ℝ ∖ {0}) →
(◡𝐹 “ 𝑦) = (◡𝐹 “ (ℝ ∖
{0}))) |
117 | 116 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑦 = (ℝ ∖ {0}) →
(vol‘(◡𝐹 “ 𝑦)) = (vol‘(◡𝐹 “ (ℝ ∖
{0})))) |
118 | 117 | eleq1d 2686 |
. . . . . 6
⊢ (𝑦 = (ℝ ∖ {0}) →
((vol‘(◡𝐹 “ 𝑦)) ∈ ℝ ↔ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ)) |
119 | 115, 118 | imbi12d 334 |
. . . . 5
⊢ (𝑦 = (ℝ ∖ {0}) →
((¬ 0 ∈ 𝑦 →
(vol‘(◡𝐹 “ 𝑦)) ∈ ℝ) ↔ (¬ 0 ∈
(ℝ ∖ {0}) → (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ))) |
120 | 113, 119 | spcv 3299 |
. . . 4
⊢
(∀𝑦(¬ 0
∈ 𝑦 →
(vol‘(◡𝐹 “ 𝑦)) ∈ ℝ) → (¬ 0 ∈
(ℝ ∖ {0}) → (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ)) |
121 | 110, 111,
120 | mpisyl 21 |
. . 3
⊢ (𝜑 → (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ) |
122 | 1, 34, 121 | 3jca 1242 |
. 2
⊢ (𝜑 → (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧
(vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ)) |
123 | | isi1f 23441 |
. 2
⊢ (𝐹 ∈ dom ∫1
↔ (𝐹 ∈ MblFn
∧ (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧
(vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ))) |
124 | 87, 122, 123 | sylanbrc 698 |
1
⊢ (𝜑 → 𝐹 ∈ dom
∫1) |