Metamath Proof Explorer

Theorem measval

Description: The value of the measures function applied on a sigma-algebra. (Contributed by Thierry Arnoux, 17-Oct-2016)

		Ref	Expression
	Assertion	measval	$⊢ S \in ⋃ ran sigAlgebra \to measures (S) = \{m \| (m : S ⟶ [0, +∞] \land m (\emptyset) = 0 \land \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{*}} m (y)))\}$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (m : S ⟶ [0, +∞] \land m (\emptyset) = 0 \land \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{*}} m (y))) \to m : S ⟶ [0, +∞]$
2	1	ss2abi	$⊢ \{m \| (m : S ⟶ [0, +∞] \land m (\emptyset) = 0 \land \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{*}} m (y)))\} \subseteq \{m \| m : S ⟶ [0, +∞]\}$
3		ovex	$⊢ [0, +∞] \in V$
4		mapex	$⊢ (S \in ⋃ ran sigAlgebra \land [0, +∞] \in V) \to \{m \| m : S ⟶ [0, +∞]\} \in V$
5	3 4	mpan2	$⊢ S \in ⋃ ran sigAlgebra \to \{m \| m : S ⟶ [0, +∞]\} \in V$
6		ssexg	$⊢ (\{m \| (m : S ⟶ [0, +∞] \land m (\emptyset) = 0 \land \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{}} m (y)))\} \subseteq \{m \| m : S ⟶ [0, +∞]\} \land \{m \| m : S ⟶ [0, +∞]\} \in V) \to \{m \| (m : S ⟶ [0, +∞] \land m (\emptyset) = 0 \land \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{}} m (y)))\} \in V$
7	2 5 6	sylancr	$⊢ S \in ⋃ ran sigAlgebra \to \{m \| (m : S ⟶ [0, +∞] \land m (\emptyset) = 0 \land \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{*}} m (y)))\} \in V$
8		feq2	$⊢ s = S \to (m : s ⟶ [0, +∞] \leftrightarrow m : S ⟶ [0, +∞])$
9		pweq	$⊢ s = S \to 𝒫 s = 𝒫 S$
10	9	raleqdv	$⊢ s = S \to (\forall x \in 𝒫 s ((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{}} m (y)) \leftrightarrow \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{}} m (y)))$
11	8 10	3anbi13d	$⊢ s = S \to ((m : s ⟶ [0, +∞] \land m (\emptyset) = 0 \land \forall x \in 𝒫 s ((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{}} m (y))) \leftrightarrow (m : S ⟶ [0, +∞] \land m (\emptyset) = 0 \land \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{}} m (y))))$
12	11	abbidv	$⊢ s = S \to \{m \| (m : s ⟶ [0, +∞] \land m (\emptyset) = 0 \land \forall x \in 𝒫 s ((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{}} m (y)))\} = \{m \| (m : S ⟶ [0, +∞] \land m (\emptyset) = 0 \land \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{}} m (y)))\}$
13		df-meas	$⊢ measures = (s \in ⋃ ran sigAlgebra ⟼ \{m \| (m : s ⟶ [0, +∞] \land m (\emptyset) = 0 \land \forall x \in 𝒫 s ((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{*}} m (y)))\})$
14	12 13	fvmptg	$⊢ (S \in ⋃ ran sigAlgebra \land \{m \| (m : S ⟶ [0, +∞] \land m (\emptyset) = 0 \land \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{}} m (y)))\} \in V) \to measures (S) = \{m \| (m : S ⟶ [0, +∞] \land m (\emptyset) = 0 \land \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{}} m (y)))\}$
15	7 14	mpdan	$⊢ S \in ⋃ ran sigAlgebra \to measures (S) = \{m \| (m : S ⟶ [0, +∞] \land m (\emptyset) = 0 \land \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{*}} m (y)))\}$