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 \in dom area \land A \in ℝ) \to (S [\{A\}] \in dom vol \land vol (S [\{A\}]) \in ℝ)$

Step	Hyp	Ref	Expression
1		dmarea	$⊢ S \in dom area \leftrightarrow (S \subseteq ℝ^{2} \land \forall x \in ℝ S [\{x\}] \in {vol}^{-1} [ℝ] \land (x \in ℝ ⟼ vol (S [\{x\}])) \in 𝐿^{1})$
2	1	simp2bi	$⊢ S \in dom area \to \forall x \in ℝ S [\{x\}] \in {vol}^{-1} [ℝ]$
3		sneq	$⊢ x = A \to \{x\} = \{A\}$
4	3	imaeq2d	$⊢ x = A \to S [\{x\}] = S [\{A\}]$
5	4	eleq1d	$⊢ x = A \to (S [\{x\}] \in {vol}^{-1} [ℝ] \leftrightarrow S [\{A\}] \in {vol}^{-1} [ℝ])$
6	5	rspccva	$⊢ (\forall x \in ℝ S [\{x\}] \in {vol}^{-1} [ℝ] \land A \in ℝ) \to S [\{A\}] \in {vol}^{-1} [ℝ]$
7	2 6	sylan	$⊢ (S \in dom area \land A \in ℝ) \to S [\{A\}] \in {vol}^{-1} [ℝ]$
8		volf	$⊢ vol : dom vol ⟶ [0, +∞]$
9		ffn	$⊢ vol : dom vol ⟶ [0, +∞] \to vol Fn dom vol$
10		elpreima	$⊢ vol Fn dom vol \to (S [\{A\}] \in {vol}^{-1} [ℝ] \leftrightarrow (S [\{A\}] \in dom vol \land vol (S [\{A\}]) \in ℝ))$
11	8 9 10	mp2b	$⊢ S [\{A\}] \in {vol}^{-1} [ℝ] \leftrightarrow (S [\{A\}] \in dom vol \land vol (S [\{A\}]) \in ℝ)$
12	7 11	sylib	$⊢ (S \in dom area \land A \in ℝ) \to (S [\{A\}] \in dom vol \land vol (S [\{A\}]) \in ℝ)$

Metamath Proof Explorer