This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mbfdm2

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

Ref Expression
Hypotheses mbfmptcl.1 ⊢ φ → x ∈ A ⟼ B ∈ MblFn
mbfmptcl.2 ⊢ φ ∧ x ∈ A → B ∈ V
Assertion mbfdm2 ⊢ φ → A ∈ dom ⁡ vol

Proof

Step Hyp Ref Expression
1 mbfmptcl.1 ⊢ φ → x ∈ A ⟼ B ∈ MblFn
2 mbfmptcl.2 ⊢ φ ∧ x ∈ A → B ∈ V
3 2 ralrimiva ⊢ φ → ∀ x ∈ A B ∈ V
4 dmmptg ⊢ ∀ x ∈ A B ∈ V → dom ⁡ x ∈ A ⟼ B = A
5 3 4 syl ⊢ φ → dom ⁡ x ∈ A ⟼ B = A
6 mbfdm ⊢ x ∈ A ⟼ B ∈ MblFn → dom ⁡ x ∈ A ⟼ B ∈ dom ⁡ vol
7 1 6 syl ⊢ φ → dom ⁡ x ∈ A ⟼ B ∈ dom ⁡ vol
8 5 7 eqeltrrd ⊢ φ → A ∈ dom ⁡ vol