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	⊢ ( ( 𝑆 ∈ dom area ∧ 𝐴 ∈ ℝ ) → ( ( 𝑆 “ { 𝐴 } ) ∈ dom vol ∧ ( vol ‘ ( 𝑆 “ { 𝐴 } ) ) ∈ ℝ ) )

Proof

Step	Hyp	Ref	Expression
1		dmarea	⊢ ( 𝑆 ∈ dom area ↔ ( 𝑆 ⊆ ( ℝ × ℝ ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑆 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) )
2	1	simp2bi	⊢ ( 𝑆 ∈ dom area → ∀ 𝑥 ∈ ℝ ( 𝑆 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) )
3		sneq	⊢ ( 𝑥 = 𝐴 → { 𝑥 } = { 𝐴 } )
4	3	imaeq2d	⊢ ( 𝑥 = 𝐴 → ( 𝑆 “ { 𝑥 } ) = ( 𝑆 “ { 𝐴 } ) )
5	4	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑆 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ↔ ( 𝑆 “ { 𝐴 } ) ∈ ( ◡ vol “ ℝ ) ) )
6	5	rspccva	⊢ ( ( ∀ 𝑥 ∈ ℝ ( 𝑆 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ 𝐴 ∈ ℝ ) → ( 𝑆 “ { 𝐴 } ) ∈ ( ◡ vol “ ℝ ) )
7	2 6	sylan	⊢ ( ( 𝑆 ∈ dom area ∧ 𝐴 ∈ ℝ ) → ( 𝑆 “ { 𝐴 } ) ∈ ( ◡ vol “ ℝ ) )
8		volf	⊢ vol : dom vol ⟶ ( 0 [,] +∞ )
9		ffn	⊢ ( vol : dom vol ⟶ ( 0 [,] +∞ ) → vol Fn dom vol )
10		elpreima	⊢ ( vol Fn dom vol → ( ( 𝑆 “ { 𝐴 } ) ∈ ( ◡ vol “ ℝ ) ↔ ( ( 𝑆 “ { 𝐴 } ) ∈ dom vol ∧ ( vol ‘ ( 𝑆 “ { 𝐴 } ) ) ∈ ℝ ) ) )
11	8 9 10	mp2b	⊢ ( ( 𝑆 “ { 𝐴 } ) ∈ ( ◡ vol “ ℝ ) ↔ ( ( 𝑆 “ { 𝐴 } ) ∈ dom vol ∧ ( vol ‘ ( 𝑆 “ { 𝐴 } ) ) ∈ ℝ ) )
12	7 11	sylib	⊢ ( ( 𝑆 ∈ dom area ∧ 𝐴 ∈ ℝ ) → ( ( 𝑆 “ { 𝐴 } ) ∈ dom vol ∧ ( vol ‘ ( 𝑆 “ { 𝐴 } ) ) ∈ ℝ ) )