oms0

Description: A constructed outer measure evaluates to zero for the empty set. (Contributed by Thierry Arnoux, 15-Sep-2019) (Revised by AV, 4-Oct-2020)

	Ref	Expression
Hypotheses	oms.m	$⊢ M = toOMeas (R)$
	oms.o	$⊢ φ \to Q \in V$
	oms.r	$⊢ φ \to R : Q ⟶ [0, +∞]$
	oms.d	$⊢ φ \to \emptyset \in dom R$
	oms.0	$⊢ φ \to R (\emptyset) = 0$
Assertion	oms0	$⊢ φ \to M (\emptyset) = 0$

Proof

Step	Hyp	Ref	Expression
1		oms.m	$⊢ M = toOMeas (R)$
2		oms.o	$⊢ φ \to Q \in V$
3		oms.r	$⊢ φ \to R : Q ⟶ [0, +∞]$
4		oms.d	$⊢ φ \to \emptyset \in dom R$
5		oms.0	$⊢ φ \to R (\emptyset) = 0$
6	1	fveq1i	$⊢ M (\emptyset) = toOMeas (R) (\emptyset)$
7		0ss	$⊢ \emptyset \subseteq ⋃ dom R$
8	3	fdmd	$⊢ φ \to dom R = Q$
9	8	unieqd	$⊢ φ \to ⋃ dom R = ⋃ Q$
10	7 9	sseqtrid	$⊢ φ \to \emptyset \subseteq ⋃ Q$
11		omsfval	$⊢ (Q \in V \land R : Q ⟶ [0, +∞] \land \emptyset \subseteq ⋃ Q) \to toOMeas (R) (\emptyset) = inf (ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y)) [0, +∞] <)$
12	2 3 10 11	syl3anc	$⊢ φ \to toOMeas (R) (\emptyset) = inf (ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y)) [0, +∞] <)$
13		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
14		xrltso	$⊢ < Or ℝ^{*}$
15		soss	$⊢ [0, +∞] \subseteq ℝ^{} \to (< Or ℝ^{} \to < Or [0, +∞])$
16	13 14 15	mp2	$⊢ < Or [0, +∞]$
17	16	a1i	$⊢ φ \to < Or [0, +∞]$
18		0e0iccpnf	$⊢ 0 \in [0, +∞]$
19	18	a1i	$⊢ φ \to 0 \in [0, +∞]$
20	4	snssd	$⊢ φ \to \{\emptyset\} \subseteq dom R$
21		p0ex	$⊢ \{\emptyset\} \in V$
22	21	elpw	$⊢ \{\emptyset\} \in 𝒫 dom R \leftrightarrow \{\emptyset\} \subseteq dom R$
23	20 22	sylibr	$⊢ φ \to \{\emptyset\} \in 𝒫 dom R$
24		0ss	$⊢ \emptyset \subseteq ⋃ \{\emptyset\}$
25		0ex	$⊢ \emptyset \in V$
26		snct	$⊢ \emptyset \in V \to \{\emptyset\} ≼ ω$
27	25 26	ax-mp	$⊢ \{\emptyset\} ≼ ω$
28	24 27	pm3.2i	$⊢ (\emptyset \subseteq ⋃ \{\emptyset\} \land \{\emptyset\} ≼ ω)$
29	23 28	jctir	$⊢ φ \to (\{\emptyset\} \in 𝒫 dom R \land (\emptyset \subseteq ⋃ \{\emptyset\} \land \{\emptyset\} ≼ ω))$
30		unieq	$⊢ z = \{\emptyset\} \to ⋃ z = ⋃ \{\emptyset\}$
31	30	sseq2d	$⊢ z = \{\emptyset\} \to (\emptyset \subseteq ⋃ z \leftrightarrow \emptyset \subseteq ⋃ \{\emptyset\})$
32		breq1	$⊢ z = \{\emptyset\} \to (z ≼ ω \leftrightarrow \{\emptyset\} ≼ ω)$
33	31 32	anbi12d	$⊢ z = \{\emptyset\} \to ((\emptyset \subseteq ⋃ z \land z ≼ ω) \leftrightarrow (\emptyset \subseteq ⋃ \{\emptyset\} \land \{\emptyset\} ≼ ω))$
34	33	elrab	$⊢ \{\emptyset\} \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} \leftrightarrow (\{\emptyset\} \in 𝒫 dom R \land (\emptyset \subseteq ⋃ \{\emptyset\} \land \{\emptyset\} ≼ ω))$
35	29 34	sylibr	$⊢ φ \to \{\emptyset\} \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\}$
36		simpr	$⊢ (φ \land y = \emptyset) \to y = \emptyset$
37	36	fveq2d	$⊢ (φ \land y = \emptyset) \to R (y) = R (\emptyset)$
38	5	adantr	$⊢ (φ \land y = \emptyset) \to R (\emptyset) = 0$
39	37 38	eqtrd	$⊢ (φ \land y = \emptyset) \to R (y) = 0$
40	39 4 19	esumsn	$⊢ φ \to \underset{y \in \{\emptyset\}}{\sum^{*}} R (y) = 0$
41	40	eqcomd	$⊢ φ \to 0 = \underset{y \in \{\emptyset\}}{\sum^{*}} R (y)$
42		esumeq1	$⊢ x = \{\emptyset\} \to \underset{y \in x}{\sum^{}} R (y) = \underset{y \in \{\emptyset\}}{\sum^{}} R (y)$
43	42	rspceeqv	$⊢ (\{\emptyset\} \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} \land 0 = \underset{y \in \{\emptyset\}}{\sum^{}} R (y)) \to \exists x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} 0 = \underset{y \in x}{\sum^{}} R (y)$
44	35 41 43	syl2anc	$⊢ φ \to \exists x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} 0 = \underset{y \in x}{\sum^{*}} R (y)$
45		0xr	$⊢ 0 \in ℝ^{*}$
46		eqid	$⊢ (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y)) = (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))$
47	46	elrnmpt	$⊢ 0 \in ℝ^{} \to (0 \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y)) \leftrightarrow \exists x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} 0 = \underset{y \in x}{\sum^{*}} R (y))$
48	45 47	ax-mp	$⊢ 0 \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y)) \leftrightarrow \exists x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} 0 = \underset{y \in x}{\sum^{}} R (y)$
49	44 48	sylibr	$⊢ φ \to 0 \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y))$
50		nfv	$⊢ Ⅎ x φ$
51		nfmpt1	$⊢ \underline{Ⅎ} x (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y))$
52	51	nfrn	$⊢ \underline{Ⅎ} x ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y))$
53	52	nfcri	$⊢ Ⅎ x a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y))$
54	50 53	nfan	$⊢ Ⅎ x (φ \land a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y)))$
55		simpr	$⊢ (((φ \land a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))) \land x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\}) \land a = \underset{y \in x}{\sum^{}} R (y)) \to a = \underset{y \in x}{\sum^{*}} R (y)$
56		vex	$⊢ x \in V$
57		nfv	$⊢ Ⅎ y φ$
58		nfcv	$⊢ \underline{Ⅎ} y \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\}$
59		nfcv	$⊢ \underline{Ⅎ} y x$
60	59	nfesum1	$⊢ \underline{Ⅎ} y \underset{y \in x}{\sum^{*}} R (y)$
61	58 60	nfmpt	$⊢ \underline{Ⅎ} y (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y))$
62	61	nfrn	$⊢ \underline{Ⅎ} y ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y))$
63	62	nfcri	$⊢ Ⅎ y a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y))$
64	57 63	nfan	$⊢ Ⅎ y (φ \land a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y)))$
65		nfv	$⊢ Ⅎ y x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\}$
66	64 65	nfan	$⊢ Ⅎ y ((φ \land a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y))) \land x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\})$
67	60	nfeq2	$⊢ Ⅎ y a = \underset{y \in x}{\sum^{*}} R (y)$
68	66 67	nfan	$⊢ Ⅎ y (((φ \land a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))) \land x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\}) \land a = \underset{y \in x}{\sum^{}} R (y))$
69	3	ad4antr	$⊢ ((((φ \land a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))) \land x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\}) \land a = \underset{y \in x}{\sum^{}} R (y)) \land y \in x) \to R : Q ⟶ [0, +∞]$
70		ssrab2	$⊢ \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} \subseteq 𝒫 dom R$
71		simpllr	$⊢ ((((φ \land a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))) \land x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\}) \land a = \underset{y \in x}{\sum^{}} R (y)) \land y \in x) \to x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\}$
72	70 71	sselid	$⊢ ((((φ \land a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))) \land x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\}) \land a = \underset{y \in x}{\sum^{}} R (y)) \land y \in x) \to x \in 𝒫 dom R$
73	8	pweqd	$⊢ φ \to 𝒫 dom R = 𝒫 Q$
74	73	ad4antr	$⊢ ((((φ \land a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))) \land x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\}) \land a = \underset{y \in x}{\sum^{}} R (y)) \land y \in x) \to 𝒫 dom R = 𝒫 Q$
75	72 74	eleqtrd	$⊢ ((((φ \land a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))) \land x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\}) \land a = \underset{y \in x}{\sum^{}} R (y)) \land y \in x) \to x \in 𝒫 Q$
76	75	elpwid	$⊢ ((((φ \land a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))) \land x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\}) \land a = \underset{y \in x}{\sum^{}} R (y)) \land y \in x) \to x \subseteq Q$
77		simpr	$⊢ ((((φ \land a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))) \land x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\}) \land a = \underset{y \in x}{\sum^{}} R (y)) \land y \in x) \to y \in x$
78	76 77	sseldd	$⊢ ((((φ \land a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))) \land x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\}) \land a = \underset{y \in x}{\sum^{}} R (y)) \land y \in x) \to y \in Q$
79	69 78	ffvelcdmd	$⊢ ((((φ \land a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))) \land x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\}) \land a = \underset{y \in x}{\sum^{}} R (y)) \land y \in x) \to R (y) \in [0, +∞]$
80	79	ex	$⊢ (((φ \land a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))) \land x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\}) \land a = \underset{y \in x}{\sum^{}} R (y)) \to (y \in x \to R (y) \in [0, +∞])$
81	68 80	ralrimi	$⊢ (((φ \land a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))) \land x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\}) \land a = \underset{y \in x}{\sum^{}} R (y)) \to \forall y \in x R (y) \in [0, +∞]$
82	59	esumcl	$⊢ (x \in V \land \forall y \in x R (y) \in [0, +∞]) \to \underset{y \in x}{\sum^{*}} R (y) \in [0, +∞]$
83	56 81 82	sylancr	$⊢ (((φ \land a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))) \land x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\}) \land a = \underset{y \in x}{\sum^{}} R (y)) \to \underset{y \in x}{\sum^{*}} R (y) \in [0, +∞]$
84	55 83	eqeltrd	$⊢ (((φ \land a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))) \land x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\}) \land a = \underset{y \in x}{\sum^{}} R (y)) \to a \in [0, +∞]$
85		vex	$⊢ a \in V$
86	46	elrnmpt	$⊢ a \in V \to (a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y)) \leftrightarrow \exists x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} a = \underset{y \in x}{\sum^{}} R (y))$
87	85 86	ax-mp	$⊢ a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y)) \leftrightarrow \exists x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} a = \underset{y \in x}{\sum^{}} R (y)$
88	87	bilani	$⊢ (φ \land a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))) \to \exists x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} a = \underset{y \in x}{\sum^{}} R (y)$
89	54 84 88	r19.29af	$⊢ (φ \land a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y))) \to a \in [0, +∞]$
90		pnfxr	$⊢ +∞ \in ℝ^{*}$
91		iccgelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land a \in [0, +∞]) \to 0 \leq a$
92	45 90 91	mp3an12	$⊢ a \in [0, +∞] \to 0 \leq a$
93	89 92	syl	$⊢ (φ \land a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y))) \to 0 \leq a$
94	13 89	sselid	$⊢ (φ \land a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{}} R (y))) \to a \in ℝ^{}$
95		xrlenlt	$⊢ (0 \in ℝ^{} \land a \in ℝ^{}) \to (0 \leq a \leftrightarrow \neg a < 0)$
96	95	bicomd	$⊢ (0 \in ℝ^{} \land a \in ℝ^{}) \to (\neg a < 0 \leftrightarrow 0 \leq a)$
97	45 94 96	sylancr	$⊢ (φ \land a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y))) \to (\neg a < 0 \leftrightarrow 0 \leq a)$
98	93 97	mpbird	$⊢ (φ \land a \in ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y))) \to \neg a < 0$
99	17 19 49 98	infmin	$⊢ φ \to inf (ran (x \in \{z \in 𝒫 dom R \| (\emptyset \subseteq ⋃ z \land z ≼ ω)\} ⟼ \underset{y \in x}{\sum^{*}} R (y)) [0, +∞] <) = 0$
100	12 99	eqtrd	$⊢ φ \to toOMeas (R) (\emptyset) = 0$
101	6 100	eqtrid	$⊢ φ \to M (\emptyset) = 0$

Metamath Proof Explorer

Theorem oms0

Proof