Theorem mbfdm2

Description: The domain of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Aug-2014)

	Ref	Expression
Hypotheses	mbfmptcl.1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
	mbfmptcl.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
Assertion	mbfdm2	⊢ ( 𝜑 → 𝐴 ∈ dom vol )

Proof

Step	Hyp	Ref	Expression
1		mbfmptcl.1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
2		mbfmptcl.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
3	2	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 )
4		dmmptg	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
5	3 4	syl	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
6		mbfdm	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ dom vol )
7	1 6	syl	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ dom vol )
8	5 7	eqeltrrd	⊢ ( 𝜑 → 𝐴 ∈ dom vol )