measvunilem

		Ref	Expression
	Hypothesis	measvunilem.1	$⊢ \underline{Ⅎ} x A$
	Assertion	measvunilem	$⊢ (M \in measures (S) \land \forall x \in A B \in (S ∖ \{\emptyset\}) \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to M (⋃_{x \in A} B) = \underset{x \in A}{\sum^{*}} M (B)$

Proof

Step	Hyp	Ref	Expression
1		measvunilem.1	$⊢ \underline{Ⅎ} x A$
2		simp1	$⊢ (M \in measures (S) \land \forall x \in A B \in (S ∖ \{\emptyset\}) \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to M \in measures (S)$
3		simp3l	$⊢ (M \in measures (S) \land \forall x \in A B \in (S ∖ \{\emptyset\}) \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to A ≼ ω$
4	1	abrexctf	$⊢ A ≼ ω \to \{y \| \exists x \in A y = B\} ≼ ω$
5	3 4	syl	$⊢ (M \in measures (S) \land \forall x \in A B \in (S ∖ \{\emptyset\}) \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to \{y \| \exists x \in A y = B\} ≼ ω$
6		ctex	$⊢ \{y \| \exists x \in A y = B\} ≼ ω \to \{y \| \exists x \in A y = B\} \in V$
7	5 6	syl	$⊢ (M \in measures (S) \land \forall x \in A B \in (S ∖ \{\emptyset\}) \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to \{y \| \exists x \in A y = B\} \in V$
8		simp2	$⊢ (M \in measures (S) \land \forall x \in A B \in (S ∖ \{\emptyset\}) \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to \forall x \in A B \in (S ∖ \{\emptyset\})$
9		eldifi	$⊢ B \in (S ∖ \{\emptyset\}) \to B \in S$
10	9	ralimi	$⊢ \forall x \in A B \in (S ∖ \{\emptyset\}) \to \forall x \in A B \in S$
11		nfcv	$⊢ \underline{Ⅎ} x S$
12	11	abrexss	$⊢ \forall x \in A B \in S \to \{y \| \exists x \in A y = B\} \subseteq S$
13	10 12	syl	$⊢ \forall x \in A B \in (S ∖ \{\emptyset\}) \to \{y \| \exists x \in A y = B\} \subseteq S$
14	8 13	syl	$⊢ (M \in measures (S) \land \forall x \in A B \in (S ∖ \{\emptyset\}) \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to \{y \| \exists x \in A y = B\} \subseteq S$
15		elpwg	$⊢ \{y \| \exists x \in A y = B\} \in V \to (\{y \| \exists x \in A y = B\} \in 𝒫 S \leftrightarrow \{y \| \exists x \in A y = B\} \subseteq S)$
16	15	biimpar	$⊢ (\{y \| \exists x \in A y = B\} \in V \land \{y \| \exists x \in A y = B\} \subseteq S) \to \{y \| \exists x \in A y = B\} \in 𝒫 S$
17	7 14 16	syl2anc	$⊢ (M \in measures (S) \land \forall x \in A B \in (S ∖ \{\emptyset\}) \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to \{y \| \exists x \in A y = B\} \in 𝒫 S$
18		simp3r	$⊢ (M \in measures (S) \land \forall x \in A B \in (S ∖ \{\emptyset\}) \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to \underset{x \in A}{Disj} B$
19	1	disjabrexf	$⊢ \underset{x \in A}{Disj} B \to \underset{z \in \{y \| \exists x \in A y = B\}}{Disj} z$
20	18 19	syl	$⊢ (M \in measures (S) \land \forall x \in A B \in (S ∖ \{\emptyset\}) \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to \underset{z \in \{y \| \exists x \in A y = B\}}{Disj} z$
21		measvun	$⊢ (M \in measures (S) \land \{y \| \exists x \in A y = B\} \in 𝒫 S \land (\{y \| \exists x \in A y = B\} ≼ ω \land \underset{z \in \{y \| \exists x \in A y = B\}}{Disj} z)) \to M (⋃ \{y \| \exists x \in A y = B\}) = \underset{z \in \{y \| \exists x \in A y = B\}}{\sum^{*}} M (z)$
22	2 17 5 20 21	syl112anc	$⊢ (M \in measures (S) \land \forall x \in A B \in (S ∖ \{\emptyset\}) \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to M (⋃ \{y \| \exists x \in A y = B\}) = \underset{z \in \{y \| \exists x \in A y = B\}}{\sum^{*}} M (z)$
23		dfiun2g	$⊢ \forall x \in A B \in (S ∖ \{\emptyset\}) \to ⋃_{x \in A} B = ⋃ \{y \| \exists x \in A y = B\}$
24	23	fveq2d	$⊢ \forall x \in A B \in (S ∖ \{\emptyset\}) \to M (⋃_{x \in A} B) = M (⋃ \{y \| \exists x \in A y = B\})$
25	8 24	syl	$⊢ (M \in measures (S) \land \forall x \in A B \in (S ∖ \{\emptyset\}) \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to M (⋃_{x \in A} B) = M (⋃ \{y \| \exists x \in A y = B\})$
26		nfcv	$⊢ \underline{Ⅎ} x M (z)$
27		nfv	$⊢ Ⅎ x M \in measures (S)$
28		nfra1	$⊢ Ⅎ x \forall x \in A B \in (S ∖ \{\emptyset\})$
29		nfcv	$⊢ \underline{Ⅎ} x ≼$
30		nfcv	$⊢ \underline{Ⅎ} x ω$
31	1 29 30	nfbr	$⊢ Ⅎ x A ≼ ω$
32		nfdisj1	$⊢ Ⅎ x \underset{x \in A}{Disj} B$
33	31 32	nfan	$⊢ Ⅎ x (A ≼ ω \land \underset{x \in A}{Disj} B)$
34	27 28 33	nf3an	$⊢ Ⅎ x (M \in measures (S) \land \forall x \in A B \in (S ∖ \{\emptyset\}) \land (A ≼ ω \land \underset{x \in A}{Disj} B))$
35		fveq2	$⊢ z = B \to M (z) = M (B)$
36		ctex	$⊢ A ≼ ω \to A \in V$
37	3 36	syl	$⊢ (M \in measures (S) \land \forall x \in A B \in (S ∖ \{\emptyset\}) \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to A \in V$
38	8	r19.21bi	$⊢ ((M \in measures (S) \land \forall x \in A B \in (S ∖ \{\emptyset\}) \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \land x \in A) \to B \in (S ∖ \{\emptyset\})$
39	34 1 38 18	disjdsct	$⊢ (M \in measures (S) \land \forall x \in A B \in (S ∖ \{\emptyset\}) \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to Fun {(x \in A ⟼ B)}^{-1}$
40		simpl1	$⊢ ((M \in measures (S) \land \forall x \in A B \in (S ∖ \{\emptyset\}) \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \land x \in A) \to M \in measures (S)$
41		measvxrge0	$⊢ (M \in measures (S) \land B \in S) \to M (B) \in [0, +∞]$
42	9 41	sylan2	$⊢ (M \in measures (S) \land B \in (S ∖ \{\emptyset\})) \to M (B) \in [0, +∞]$
43	40 38 42	syl2anc	$⊢ ((M \in measures (S) \land \forall x \in A B \in (S ∖ \{\emptyset\}) \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \land x \in A) \to M (B) \in [0, +∞]$
44	26 34 1 35 37 39 43 38	esumc	$⊢ (M \in measures (S) \land \forall x \in A B \in (S ∖ \{\emptyset\}) \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to \underset{x \in A}{\sum^{}} M (B) = \underset{z \in \{y \| \exists x \in A y = B\}}{\sum^{}} M (z)$
45	22 25 44	3eqtr4d	$⊢ (M \in measures (S) \land \forall x \in A B \in (S ∖ \{\emptyset\}) \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to M (⋃_{x \in A} B) = \underset{x \in A}{\sum^{*}} M (B)$

Metamath Proof Explorer

Theorem measvunilem

Proof