Metamath Proof Explorer

Theorem areambl

Description: The fibers of a measurable region are finitely measurable subsets of RR . (Contributed by Mario Carneiro, 21-Jun-2015)

Ref Expression
Assertion areambl ⊢ S ∈ dom ⁡ area ∧ A ∈ ℝ → S A ∈ dom ⁡ vol ∧ vol ⁡ S A ∈ ℝ

Proof

Step Hyp Ref Expression
1 dmarea ⊢ S ∈ dom ⁡ area ↔ S ⊆ ℝ 2 ∧ ∀ x ∈ ℝ S x ∈ vol -1 ℝ ∧ x ∈ ℝ ⟼ vol ⁡ S x ∈ 𝐿 1
2 1 simp2bi ⊢ S ∈ dom ⁡ area → ∀ x ∈ ℝ S x ∈ vol -1 ℝ
3 sneq ⊢ x = A → x = A
4 3 imaeq2d ⊢ x = A → S x = S A
5 4 eleq1d ⊢ x = A → S x ∈ vol -1 ℝ ↔ S A ∈ vol -1 ℝ
6 5 rspccva ⊢ ∀ x ∈ ℝ S x ∈ vol -1 ℝ ∧ A ∈ ℝ → S A ∈ vol -1 ℝ
7 2 6 sylan ⊢ S ∈ dom ⁡ area ∧ A ∈ ℝ → S A ∈ vol -1 ℝ
8 volf ⊢ vol : dom ⁡ vol ⟶ 0 +∞
9 ffn ⊢ vol : dom ⁡ vol ⟶ 0 +∞ → vol Fn dom ⁡ vol
10 elpreima ⊢ vol Fn dom ⁡ vol → S A ∈ vol -1 ℝ ↔ S A ∈ dom ⁡ vol ∧ vol ⁡ S A ∈ ℝ
11 8 9 10 mp2b ⊢ S A ∈ vol -1 ℝ ↔ S A ∈ dom ⁡ vol ∧ vol ⁡ S A ∈ ℝ
12 7 11 sylib ⊢ S ∈ dom ⁡ area ∧ A ∈ ℝ → S A ∈ dom ⁡ vol ∧ vol ⁡ S A ∈ ℝ