measbasedom

Description: The base set of a measure is its domain. (Contributed by Thierry Arnoux, 25-Dec-2016)

		Ref	Expression
	Assertion	measbasedom	$⊢ M \in ⋃ ran measures \leftrightarrow M \in measures (dom M)$

Step	Hyp	Ref	Expression
1		isrnmeas	$⊢ M \in ⋃ ran measures \to (dom M \in ⋃ ran sigAlgebra \land (M : dom M ⟶ [0, +∞] \land M (\emptyset) = 0 \land \forall x \in 𝒫 dom M ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = \underset{y \in x}{\sum^{*}} M (y))))$
2	1	simprd	$⊢ M \in ⋃ ran measures \to (M : dom M ⟶ [0, +∞] \land M (\emptyset) = 0 \land \forall x \in 𝒫 dom M ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = \underset{y \in x}{\sum^{*}} M (y)))$
3		dmmeas	$⊢ M \in ⋃ ran measures \to dom M \in ⋃ ran sigAlgebra$
4		ismeas	$⊢ dom M \in ⋃ ran sigAlgebra \to (M \in measures (dom M) \leftrightarrow (M : dom M ⟶ [0, +∞] \land M (\emptyset) = 0 \land \forall x \in 𝒫 dom M ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = \underset{y \in x}{\sum^{*}} M (y))))$
5	3 4	syl	$⊢ M \in ⋃ ran measures \to (M \in measures (dom M) \leftrightarrow (M : dom M ⟶ [0, +∞] \land M (\emptyset) = 0 \land \forall x \in 𝒫 dom M ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = \underset{y \in x}{\sum^{*}} M (y))))$
6	2 5	mpbird	$⊢ M \in ⋃ ran measures \to M \in measures (dom M)$
7		elfvunirn	$⊢ M \in measures (dom M) \to M \in ⋃ ran measures$
8	6 7	impbii	$⊢ M \in ⋃ ran measures \leftrightarrow M \in measures (dom M)$

Metamath Proof Explorer