measvunilem0

		Ref	Expression
	Hypothesis	measvunilem.0.1	$⊢ \underline{Ⅎ} x A$
	Assertion	measvunilem0	$⊢ (M \in measures (S) \land \forall x \in A B \in \{\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.0.1	$⊢ \underline{Ⅎ} x A$
2		simp3l	$⊢ (M \in measures (S) \land \forall x \in A B \in \{\emptyset\} \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to A ≼ ω$
3		ctex	$⊢ A ≼ ω \to A \in V$
4	1	esum0	$⊢ A \in V \to \underset{x \in A}{\sum^{*}} 0 = 0$
5	2 3 4	3syl	$⊢ (M \in measures (S) \land \forall x \in A B \in \{\emptyset\} \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to \underset{x \in A}{\sum^{*}} 0 = 0$
6		nfv	$⊢ Ⅎ x M \in measures (S)$
7		nfra1	$⊢ Ⅎ x \forall x \in A B \in \{\emptyset\}$
8		nfcv	$⊢ \underline{Ⅎ} x ≼$
9		nfcv	$⊢ \underline{Ⅎ} x ω$
10	1 8 9	nfbr	$⊢ Ⅎ x A ≼ ω$
11		nfdisj1	$⊢ Ⅎ x \underset{x \in A}{Disj} B$
12	10 11	nfan	$⊢ Ⅎ x (A ≼ ω \land \underset{x \in A}{Disj} B)$
13	6 7 12	nf3an	$⊢ Ⅎ x (M \in measures (S) \land \forall x \in A B \in \{\emptyset\} \land (A ≼ ω \land \underset{x \in A}{Disj} B))$
14		eqidd	$⊢ (M \in measures (S) \land \forall x \in A B \in \{\emptyset\} \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to A = A$
15		simp2	$⊢ (M \in measures (S) \land \forall x \in A B \in \{\emptyset\} \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to \forall x \in A B \in \{\emptyset\}$
16	15	r19.21bi	$⊢ ((M \in measures (S) \land \forall x \in A B \in \{\emptyset\} \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \land x \in A) \to B \in \{\emptyset\}$
17		elsni	$⊢ B \in \{\emptyset\} \to B = \emptyset$
18	16 17	syl	$⊢ ((M \in measures (S) \land \forall x \in A B \in \{\emptyset\} \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \land x \in A) \to B = \emptyset$
19	18	fveq2d	$⊢ ((M \in measures (S) \land \forall x \in A B \in \{\emptyset\} \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \land x \in A) \to M (B) = M (\emptyset)$
20		measvnul	$⊢ M \in measures (S) \to M (\emptyset) = 0$
21	20	3ad2ant1	$⊢ (M \in measures (S) \land \forall x \in A B \in \{\emptyset\} \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to M (\emptyset) = 0$
22	21	adantr	$⊢ ((M \in measures (S) \land \forall x \in A B \in \{\emptyset\} \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \land x \in A) \to M (\emptyset) = 0$
23	19 22	eqtrd	$⊢ ((M \in measures (S) \land \forall x \in A B \in \{\emptyset\} \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \land x \in A) \to M (B) = 0$
24	13 14 23	esumeq12dvaf	$⊢ (M \in measures (S) \land \forall x \in A B \in \{\emptyset\} \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to \underset{x \in A}{\sum^{}} M (B) = \underset{x \in A}{\sum^{}} 0$
25	13 1 1 14 18	iuneq12daf	$⊢ (M \in measures (S) \land \forall x \in A B \in \{\emptyset\} \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to ⋃_{x \in A} B = ⋃_{x \in A} \emptyset$
26		iun0	$⊢ ⋃_{x \in A} \emptyset = \emptyset$
27	25 26	eqtrdi	$⊢ (M \in measures (S) \land \forall x \in A B \in \{\emptyset\} \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to ⋃_{x \in A} B = \emptyset$
28	27	fveq2d	$⊢ (M \in measures (S) \land \forall x \in A B \in \{\emptyset\} \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to M (⋃_{x \in A} B) = M (\emptyset)$
29	28 21	eqtrd	$⊢ (M \in measures (S) \land \forall x \in A B \in \{\emptyset\} \land (A ≼ ω \land \underset{x \in A}{Disj} B)) \to M (⋃_{x \in A} B) = 0$
30	5 24 29	3eqtr4rd	$⊢ (M \in measures (S) \land \forall x \in A B \in \{\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 measvunilem0

Proof