isrnmeas

Description: The property of being a measure on an undefined base sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016)

		Ref	Expression
	Assertion	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))))$

Proof

Step	Hyp	Ref	Expression
1		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)))\})$
2		vex	$⊢ s \in V$
3		ovex	$⊢ [0, +∞] \in V$
4		mapex	$⊢ (s \in V \land [0, +∞] \in V) \to \{m \| m : s ⟶ [0, +∞]\} \in V$
5	2 3 4	mp2an	$⊢ \{m \| m : s ⟶ [0, +∞]\} \in V$
6		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, +∞]$
7	6	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, +∞]\}$
8	5 7	ssexi	$⊢ \{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$
9		feq1	$⊢ m = M \to (m : s ⟶ [0, +∞] \leftrightarrow M : s ⟶ [0, +∞])$
10		fveq1	$⊢ m = M \to m (\emptyset) = M (\emptyset)$
11	10	eqeq1d	$⊢ m = M \to (m (\emptyset) = 0 \leftrightarrow M (\emptyset) = 0)$
12		fveq1	$⊢ m = M \to m (⋃ x) = M (⋃ x)$
13		fveq1	$⊢ m = M \to m (y) = M (y)$
14	13	esumeq2sdv	$⊢ m = M \to \underset{y \in x}{\sum^{}} m (y) = \underset{y \in x}{\sum^{}} M (y)$
15	12 14	eqeq12d	$⊢ m = M \to (m (⋃ x) = \underset{y \in x}{\sum^{}} m (y) \leftrightarrow M (⋃ x) = \underset{y \in x}{\sum^{}} M (y))$
16	15	imbi2d	$⊢ m = M \to (((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{}} m (y)) \leftrightarrow ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = \underset{y \in x}{\sum^{}} M (y)))$
17	16	ralbidv	$⊢ m = M \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)))$
18	9 11 17	3anbi123d	$⊢ m = M \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))))$
19	1 8 18	abfmpunirn	$⊢ M \in ⋃ ran measures \leftrightarrow (M \in V \land \exists s \in ⋃ ran sigAlgebra (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))))$
20	19	simprbi	$⊢ M \in ⋃ ran measures \to \exists s \in ⋃ ran sigAlgebra (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)))$
21		fdm	$⊢ M : s ⟶ [0, +∞] \to dom M = s$
22	21	3ad2ant1	$⊢ (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 dom M = s$
23	22	adantl	$⊢ (s \in ⋃ ran sigAlgebra \land (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 dom M = s$
24		simpl	$⊢ (s \in ⋃ ran sigAlgebra \land (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 s \in ⋃ ran sigAlgebra$
25	23 24	eqeltrd	$⊢ (s \in ⋃ ran sigAlgebra \land (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 dom M \in ⋃ ran sigAlgebra$
26		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, +∞]$
27		feq2	$⊢ dom M = s \to (M : dom M ⟶ [0, +∞] \leftrightarrow M : s ⟶ [0, +∞])$
28	27	biimpar	$⊢ (dom M = s \land M : s ⟶ [0, +∞]) \to M : dom M ⟶ [0, +∞]$
29	22 26 28	syl2anc	$⊢ (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 : dom M ⟶ [0, +∞]$
30		simp2	$⊢ (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 (\emptyset) = 0$
31		simp3	$⊢ (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 \forall x \in 𝒫 s ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = \underset{y \in x}{\sum^{}} M (y))$
32		pweq	$⊢ dom M = s \to 𝒫 dom M = 𝒫 s$
33	32	raleqdv	$⊢ dom M = s \to (\forall x \in 𝒫 dom M ((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)))$
34	33	biimpar	$⊢ (dom M = s \land \forall x \in 𝒫 s ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = \underset{y \in x}{\sum^{}} M (y))) \to \forall x \in 𝒫 dom M ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = \underset{y \in x}{\sum^{}} M (y))$
35	22 31 34	syl2anc	$⊢ (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 \forall x \in 𝒫 dom M ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = \underset{y \in x}{\sum^{}} M (y))$
36	29 30 35	3jca	$⊢ (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 : 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)))$
37	36	adantl	$⊢ (s \in ⋃ ran sigAlgebra \land (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 : 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)))$
38	25 37	jca	$⊢ (s \in ⋃ ran sigAlgebra \land (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 (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))))$
39	38	rexlimiva	$⊢ \exists s \in ⋃ ran sigAlgebra (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 (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))))$
40	20 39	syl	$⊢ 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))))$

Metamath Proof Explorer

Theorem isrnmeas

Proof