| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | i1fd.1 | . . . . . . . . 9
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) | 
| 2 | 1 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → 𝐹:ℝ⟶ℝ) | 
| 3 |  | ffun 6739 | . . . . . . . 8
⊢ (𝐹:ℝ⟶ℝ →
Fun 𝐹) | 
| 4 |  | funcnvcnv 6633 | . . . . . . . 8
⊢ (Fun
𝐹 → Fun ◡◡𝐹) | 
| 5 |  | imadif 6650 | . . . . . . . 8
⊢ (Fun
◡◡𝐹 → (◡𝐹 “ (ℝ ∖ (ℝ ∖
𝑥))) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥)))) | 
| 6 | 2, 3, 4, 5 | 4syl 19 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ (ℝ ∖ (ℝ ∖
𝑥))) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥)))) | 
| 7 |  | ioof 13487 | . . . . . . . . . . . . 13
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ | 
| 8 |  | frn 6743 | . . . . . . . . . . . . 13
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → ran (,) ⊆ 𝒫 ℝ) | 
| 9 | 7, 8 | ax-mp 5 | . . . . . . . . . . . 12
⊢ ran (,)
⊆ 𝒫 ℝ | 
| 10 | 9 | sseli 3979 | . . . . . . . . . . 11
⊢ (𝑥 ∈ ran (,) → 𝑥 ∈ 𝒫
ℝ) | 
| 11 | 10 | elpwid 4609 | . . . . . . . . . 10
⊢ (𝑥 ∈ ran (,) → 𝑥 ⊆
ℝ) | 
| 12 | 11 | ad2antlr 727 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → 𝑥 ⊆ ℝ) | 
| 13 |  | dfss4 4269 | . . . . . . . . 9
⊢ (𝑥 ⊆ ℝ ↔ (ℝ
∖ (ℝ ∖ 𝑥)) = 𝑥) | 
| 14 | 12, 13 | sylib 218 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (ℝ ∖
(ℝ ∖ 𝑥)) =
𝑥) | 
| 15 | 14 | imaeq2d 6078 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ (ℝ ∖ (ℝ ∖
𝑥))) = (◡𝐹 “ 𝑥)) | 
| 16 | 6, 15 | eqtr3d 2779 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))) = (◡𝐹 “ 𝑥)) | 
| 17 |  | fimacnv 6758 | . . . . . . . . 9
⊢ (𝐹:ℝ⟶ℝ →
(◡𝐹 “ ℝ) =
ℝ) | 
| 18 | 2, 17 | syl 17 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ ℝ) =
ℝ) | 
| 19 |  | rembl 25575 | . . . . . . . 8
⊢ ℝ
∈ dom vol | 
| 20 | 18, 19 | eqeltrdi 2849 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ ℝ) ∈ dom
vol) | 
| 21 | 1 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → 𝐹:ℝ⟶ℝ) | 
| 22 |  | inpreima 7084 | . . . . . . . . . . . . . 14
⊢ (Fun
𝐹 → (◡𝐹 “ (𝑦 ∩ ran 𝐹)) = ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ ran 𝐹))) | 
| 23 |  | iunid 5060 | . . . . . . . . . . . . . . . 16
⊢ ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹){𝑥} = (𝑦 ∩ ran 𝐹) | 
| 24 | 23 | imaeq2i 6076 | . . . . . . . . . . . . . . 15
⊢ (◡𝐹 “ ∪
𝑥 ∈ (𝑦 ∩ ran 𝐹){𝑥}) = (◡𝐹 “ (𝑦 ∩ ran 𝐹)) | 
| 25 |  | imaiun 7265 | . . . . . . . . . . . . . . 15
⊢ (◡𝐹 “ ∪
𝑥 ∈ (𝑦 ∩ ran 𝐹){𝑥}) = ∪
𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) | 
| 26 | 24, 25 | eqtr3i 2767 | . . . . . . . . . . . . . 14
⊢ (◡𝐹 “ (𝑦 ∩ ran 𝐹)) = ∪
𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) | 
| 27 |  | cnvimass 6100 | . . . . . . . . . . . . . . . 16
⊢ (◡𝐹 “ 𝑦) ⊆ dom 𝐹 | 
| 28 |  | cnvimarndm 6101 | . . . . . . . . . . . . . . . 16
⊢ (◡𝐹 “ ran 𝐹) = dom 𝐹 | 
| 29 | 27, 28 | sseqtrri 4033 | . . . . . . . . . . . . . . 15
⊢ (◡𝐹 “ 𝑦) ⊆ (◡𝐹 “ ran 𝐹) | 
| 30 |  | dfss2 3969 | . . . . . . . . . . . . . . 15
⊢ ((◡𝐹 “ 𝑦) ⊆ (◡𝐹 “ ran 𝐹) ↔ ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ ran 𝐹)) = (◡𝐹 “ 𝑦)) | 
| 31 | 29, 30 | mpbi 230 | . . . . . . . . . . . . . 14
⊢ ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ ran 𝐹)) = (◡𝐹 “ 𝑦) | 
| 32 | 22, 26, 31 | 3eqtr3g 2800 | . . . . . . . . . . . . 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 4238 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∩ ran 𝐹) ⊆ ran 𝐹 | 
| 37 |  | ssfi 9213 | . . . . . . . . . . . . . 14
⊢ ((ran
𝐹 ∈ Fin ∧ (𝑦 ∩ ran 𝐹) ⊆ ran 𝐹) → (𝑦 ∩ ran 𝐹) ∈ Fin) | 
| 38 | 35, 36, 37 | sylancl 586 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (𝑦 ∩ ran 𝐹) ∈ Fin) | 
| 39 |  | simpll 767 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → 𝜑) | 
| 40 |  | elinel1 4201 | . . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
(𝑦 ∩ ran 𝐹) → 0 ∈ 𝑦) | 
| 41 | 40 | con3i 154 | . . . . . . . . . . . . . . . . . . 19
⊢ (¬ 0
∈ 𝑦 → ¬ 0
∈ (𝑦 ∩ ran 𝐹)) | 
| 42 | 41 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ¬ 0 ∈ (𝑦 ∩ ran 𝐹)) | 
| 43 |  | disjsn 4711 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ ¬ 0 ∈
(𝑦 ∩ ran 𝐹)) | 
| 44 | 42, 43 | sylibr 234 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅) | 
| 45 |  | reldisj 4453 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∩ ran 𝐹) ⊆ ran 𝐹 → (((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ (𝑦 ∩ ran 𝐹) ⊆ (ran 𝐹 ∖ {0}))) | 
| 46 | 36, 45 | ax-mp 5 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ (𝑦 ∩ ran 𝐹) ⊆ (ran 𝐹 ∖ {0})) | 
| 47 | 44, 46 | sylib 218 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (𝑦 ∩ ran 𝐹) ⊆ (ran 𝐹 ∖ {0})) | 
| 48 | 47 | sselda 3983 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → 𝑥 ∈ (ran 𝐹 ∖ {0})) | 
| 49 |  | i1fd.3 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → (◡𝐹 “ {𝑥}) ∈ dom vol) | 
| 50 | 39, 48, 49 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (◡𝐹 “ {𝑥}) ∈ dom vol) | 
| 51 | 50 | ralrimiva 3146 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol) | 
| 52 |  | finiunmbl 25579 | . . . . . . . . . . . . 13
⊢ (((𝑦 ∩ ran 𝐹) ∈ Fin ∧ ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol) → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol) | 
| 53 | 38, 51, 52 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol) | 
| 54 | 33, 53 | eqeltrrd 2842 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (◡𝐹 “ 𝑦) ∈ dom vol) | 
| 55 | 54 | ex 412 | . . . . . . . . . 10
⊢ (𝜑 → (¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol)) | 
| 56 | 55 | alrimiv 1927 | . . . . . . . . 9
⊢ (𝜑 → ∀𝑦(¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol)) | 
| 57 | 56 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ∀𝑦(¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol)) | 
| 58 |  | elndif 4133 | . . . . . . . . 9
⊢ (0 ∈
𝑥 → ¬ 0 ∈
(ℝ ∖ 𝑥)) | 
| 59 | 58 | adantl 481 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ¬ 0 ∈ (ℝ
∖ 𝑥)) | 
| 60 |  | reex 11246 | . . . . . . . . . 10
⊢ ℝ
∈ V | 
| 61 | 60 | difexi 5330 | . . . . . . . . 9
⊢ (ℝ
∖ 𝑥) ∈
V | 
| 62 |  | eleq2 2830 | . . . . . . . . . . 11
⊢ (𝑦 = (ℝ ∖ 𝑥) → (0 ∈ 𝑦 ↔ 0 ∈ (ℝ
∖ 𝑥))) | 
| 63 | 62 | notbid 318 | . . . . . . . . . 10
⊢ (𝑦 = (ℝ ∖ 𝑥) → (¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ (ℝ
∖ 𝑥))) | 
| 64 |  | imaeq2 6074 | . . . . . . . . . . 11
⊢ (𝑦 = (ℝ ∖ 𝑥) → (◡𝐹 “ 𝑦) = (◡𝐹 “ (ℝ ∖ 𝑥))) | 
| 65 | 64 | eleq1d 2826 | . . . . . . . . . 10
⊢ (𝑦 = (ℝ ∖ 𝑥) → ((◡𝐹 “ 𝑦) ∈ dom vol ↔ (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol)) | 
| 66 | 63, 65 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑦 = (ℝ ∖ 𝑥) → ((¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) ↔ (¬ 0 ∈
(ℝ ∖ 𝑥) →
(◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol))) | 
| 67 | 61, 66 | spcv 3605 | . . . . . . . 8
⊢
(∀𝑦(¬ 0
∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) → (¬ 0 ∈
(ℝ ∖ 𝑥) →
(◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol)) | 
| 68 | 57, 59, 67 | sylc 65 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol) | 
| 69 |  | difmbl 25578 | . . . . . . 7
⊢ (((◡𝐹 “ ℝ) ∈ dom vol ∧
(◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))) ∈ dom vol) | 
| 70 | 20, 68, 69 | syl2anc 584 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))) ∈ dom vol) | 
| 71 | 16, 70 | eqeltrrd 2842 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ 𝑥) ∈ dom vol) | 
| 72 |  | eleq2 2830 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (0 ∈ 𝑦 ↔ 0 ∈ 𝑥)) | 
| 73 | 72 | notbid 318 | . . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ 𝑥)) | 
| 74 |  | imaeq2 6074 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (◡𝐹 “ 𝑦) = (◡𝐹 “ 𝑥)) | 
| 75 | 74 | eleq1d 2826 | . . . . . . . . . 10
⊢ (𝑦 = 𝑥 → ((◡𝐹 “ 𝑦) ∈ dom vol ↔ (◡𝐹 “ 𝑥) ∈ dom vol)) | 
| 76 | 73, 75 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) ↔ (¬ 0 ∈
𝑥 → (◡𝐹 “ 𝑥) ∈ dom vol))) | 
| 77 | 76 | spvv 1996 | . . . . . . . 8
⊢
(∀𝑦(¬ 0
∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) → (¬ 0 ∈
𝑥 → (◡𝐹 “ 𝑥) ∈ dom vol)) | 
| 78 | 56, 77 | syl 17 | . . . . . . 7
⊢ (𝜑 → (¬ 0 ∈ 𝑥 → (◡𝐹 “ 𝑥) ∈ dom vol)) | 
| 79 | 78 | imp 406 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑥) → (◡𝐹 “ 𝑥) ∈ dom vol) | 
| 80 | 79 | adantlr 715 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ ¬ 0 ∈ 𝑥) → (◡𝐹 “ 𝑥) ∈ dom vol) | 
| 81 | 71, 80 | pm2.61dan 813 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ran (,)) → (◡𝐹 “ 𝑥) ∈ dom vol) | 
| 82 | 81 | ralrimiva 3146 | . . 3
⊢ (𝜑 → ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol) | 
| 83 |  | ismbf 25663 | . . . 4
⊢ (𝐹:ℝ⟶ℝ →
(𝐹 ∈ MblFn ↔
∀𝑥 ∈ ran
(,)(◡𝐹 “ 𝑥) ∈ dom vol)) | 
| 84 | 1, 83 | syl 17 | . . 3
⊢ (𝜑 → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol)) | 
| 85 | 82, 84 | mpbird 257 | . 2
⊢ (𝜑 → 𝐹 ∈ MblFn) | 
| 86 |  | mblvol 25565 | . . . . . . . 8
⊢ ((◡𝐹 “ 𝑦) ∈ dom vol → (vol‘(◡𝐹 “ 𝑦)) = (vol*‘(◡𝐹 “ 𝑦))) | 
| 87 | 54, 86 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol‘(◡𝐹 “ 𝑦)) = (vol*‘(◡𝐹 “ 𝑦))) | 
| 88 |  | mblss 25566 | . . . . . . . . 9
⊢ ((◡𝐹 “ 𝑦) ∈ dom vol → (◡𝐹 “ 𝑦) ⊆ ℝ) | 
| 89 | 54, 88 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (◡𝐹 “ 𝑦) ⊆ ℝ) | 
| 90 |  | mblvol 25565 | . . . . . . . . . . 11
⊢ ((◡𝐹 “ {𝑥}) ∈ dom vol → (vol‘(◡𝐹 “ {𝑥})) = (vol*‘(◡𝐹 “ {𝑥}))) | 
| 91 | 50, 90 | syl 17 | . . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (vol‘(◡𝐹 “ {𝑥})) = (vol*‘(◡𝐹 “ {𝑥}))) | 
| 92 |  | i1fd.4 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → (vol‘(◡𝐹 “ {𝑥})) ∈ ℝ) | 
| 93 | 39, 48, 92 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (vol‘(◡𝐹 “ {𝑥})) ∈ ℝ) | 
| 94 | 91, 93 | eqeltrrd 2842 | . . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ) | 
| 95 | 38, 94 | fsumrecl 15770 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ) | 
| 96 | 33 | fveq2d 6910 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})) = (vol*‘(◡𝐹 “ 𝑦))) | 
| 97 |  | mblss 25566 | . . . . . . . . . . . . 13
⊢ ((◡𝐹 “ {𝑥}) ∈ dom vol → (◡𝐹 “ {𝑥}) ⊆ ℝ) | 
| 98 | 50, 97 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (◡𝐹 “ {𝑥}) ⊆ ℝ) | 
| 99 | 98, 94 | jca 511 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → ((◡𝐹 “ {𝑥}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ)) | 
| 100 | 99 | ralrimiva 3146 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)((◡𝐹 “ {𝑥}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ)) | 
| 101 |  | ovolfiniun 25536 | . . . . . . . . . 10
⊢ (((𝑦 ∩ ran 𝐹) ∈ Fin ∧ ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)((◡𝐹 “ {𝑥}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ)) →
(vol*‘∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥}))) | 
| 102 | 38, 100, 101 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥}))) | 
| 103 | 96, 102 | eqbrtrrd 5167 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘(◡𝐹 “ 𝑦)) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥}))) | 
| 104 |  | ovollecl 25518 | . . . . . . . 8
⊢ (((◡𝐹 “ 𝑦) ⊆ ℝ ∧ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ ∧ (vol*‘(◡𝐹 “ 𝑦)) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥}))) → (vol*‘(◡𝐹 “ 𝑦)) ∈ ℝ) | 
| 105 | 89, 95, 103, 104 | syl3anc 1373 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘(◡𝐹 “ 𝑦)) ∈ ℝ) | 
| 106 | 87, 105 | eqeltrd 2841 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ) | 
| 107 | 106 | ex 412 | . . . . 5
⊢ (𝜑 → (¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ)) | 
| 108 | 107 | alrimiv 1927 | . . . 4
⊢ (𝜑 → ∀𝑦(¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ)) | 
| 109 |  | neldifsn 4792 | . . . 4
⊢  ¬ 0
∈ (ℝ ∖ {0}) | 
| 110 | 60 | difexi 5330 | . . . . 5
⊢ (ℝ
∖ {0}) ∈ V | 
| 111 |  | eleq2 2830 | . . . . . . 7
⊢ (𝑦 = (ℝ ∖ {0}) →
(0 ∈ 𝑦 ↔ 0 ∈
(ℝ ∖ {0}))) | 
| 112 | 111 | notbid 318 | . . . . . 6
⊢ (𝑦 = (ℝ ∖ {0}) →
(¬ 0 ∈ 𝑦 ↔
¬ 0 ∈ (ℝ ∖ {0}))) | 
| 113 |  | imaeq2 6074 | . . . . . . . 8
⊢ (𝑦 = (ℝ ∖ {0}) →
(◡𝐹 “ 𝑦) = (◡𝐹 “ (ℝ ∖
{0}))) | 
| 114 | 113 | fveq2d 6910 | . . . . . . 7
⊢ (𝑦 = (ℝ ∖ {0}) →
(vol‘(◡𝐹 “ 𝑦)) = (vol‘(◡𝐹 “ (ℝ ∖
{0})))) | 
| 115 | 114 | eleq1d 2826 | . . . . . 6
⊢ (𝑦 = (ℝ ∖ {0}) →
((vol‘(◡𝐹 “ 𝑦)) ∈ ℝ ↔ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ)) | 
| 116 | 112, 115 | imbi12d 344 | . . . . 5
⊢ (𝑦 = (ℝ ∖ {0}) →
((¬ 0 ∈ 𝑦 →
(vol‘(◡𝐹 “ 𝑦)) ∈ ℝ) ↔ (¬ 0 ∈
(ℝ ∖ {0}) → (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ))) | 
| 117 | 110, 116 | spcv 3605 | . . . 4
⊢
(∀𝑦(¬ 0
∈ 𝑦 →
(vol‘(◡𝐹 “ 𝑦)) ∈ ℝ) → (¬ 0 ∈
(ℝ ∖ {0}) → (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ)) | 
| 118 | 108, 109,
117 | mpisyl 21 | . . 3
⊢ (𝜑 → (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ) | 
| 119 | 1, 34, 118 | 3jca 1129 | . 2
⊢ (𝜑 → (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧
(vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ)) | 
| 120 |  | isi1f 25709 | . 2
⊢ (𝐹 ∈ dom ∫1
↔ (𝐹 ∈ MblFn
∧ (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧
(vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈
ℝ))) | 
| 121 | 85, 119, 120 | sylanbrc 583 | 1
⊢ (𝜑 → 𝐹 ∈ dom
∫1) |