Theorem voncmpl

Description: The Lebesgue measure is complete. See Definition 112Df of Fremlin1 p. 19. This is an observation written after Definition 115E of Fremlin1 p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	voncmpl.x	$$⊢\phi \to X\in \mathrm{Fin}$$
	voncmpl.s	$$⊢S=\mathrm{dom}\mathrm{voln}\left(X\right)$$
	voncmpl.e	$$⊢\phi \to E\in \mathrm{dom}\mathrm{voln}\left(X\right)$$
	voncmpl.z	$$⊢\phi \to \mathrm{voln}\left(X\right)\left(E\right)=0$$
	voncmpl.f	$$⊢\phi \to F\subseteq E$$
Assertion	voncmpl	$$⊢\phi \to F\in S$$

Proof

Step	Hyp	Ref	Expression
1		voncmpl.x	$$⊢\phi \to X\in \mathrm{Fin}$$
2		voncmpl.s	$$⊢S=\mathrm{dom}\mathrm{voln}\left(X\right)$$
3		voncmpl.e	$$⊢\phi \to E\in \mathrm{dom}\mathrm{voln}\left(X\right)$$
4		voncmpl.z	$$⊢\phi \to \mathrm{voln}\left(X\right)\left(E\right)=0$$
5		voncmpl.f	$$⊢\phi \to F\subseteq E$$
6	1	ovnome	$$⊢\phi \to \mathrm{voln*}\left(X\right)\in \mathrm{OutMeas}$$
7		eqid	$$⊢\bigcup \mathrm{dom}\mathrm{voln*}\left(X\right)=\bigcup \mathrm{dom}\mathrm{voln*}\left(X\right)$$
8	1	dmvon	$$⊢\phi \to \mathrm{dom}\mathrm{voln}\left(X\right)=\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)$$
9		eqid	$$⊢\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)=\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)$$
10	9	caragenss	$$⊢\mathrm{voln*}\left(X\right)\in \mathrm{OutMeas}\to \mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)\subseteq \mathrm{dom}\mathrm{voln*}\left(X\right)$$
11	6 10	syl	$$⊢\phi \to \mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)\subseteq \mathrm{dom}\mathrm{voln*}\left(X\right)$$
12	8 11	eqsstrd	$$⊢\phi \to \mathrm{dom}\mathrm{voln}\left(X\right)\subseteq \mathrm{dom}\mathrm{voln*}\left(X\right)$$
13	12 3	sseldd	$$⊢\phi \to E\in \mathrm{dom}\mathrm{voln*}\left(X\right)$$
14		elssuni	$$⊢E\in \mathrm{dom}\mathrm{voln*}\left(X\right)\to E\subseteq \bigcup \mathrm{dom}\mathrm{voln*}\left(X\right)$$
15	13 14	syl	$$⊢\phi \to E\subseteq \bigcup \mathrm{dom}\mathrm{voln*}\left(X\right)$$
16	5 15	sstrd	$$⊢\phi \to F\subseteq \bigcup \mathrm{dom}\mathrm{voln*}\left(X\right)$$
17	4	eqcomd	$$⊢\phi \to 0=\mathrm{voln}\left(X\right)\left(E\right)$$
18	1	vonval	$$⊢\phi \to \mathrm{voln}\left(X\right)={\mathrm{voln*}\left(X\right)\upharpoonright }_{\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)}$$
19	18	fveq1d	$$⊢\phi \to \mathrm{voln}\left(X\right)\left(E\right)=\left({\mathrm{voln*}\left(X\right)\upharpoonright }_{\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)}\right)\left(E\right)$$
20	17 19	eqtrd	$$⊢\phi \to 0=\left({\mathrm{voln*}\left(X\right)\upharpoonright }_{\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)}\right)\left(E\right)$$
21	2	a1i	$$⊢\phi \to S=\mathrm{dom}\mathrm{voln}\left(X\right)$$
22	21 8	eqtr2d	$$⊢\phi \to \mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)=S$$
23	22	reseq2d	$$⊢\phi \to {\mathrm{voln*}\left(X\right)\upharpoonright }_{\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)}={\mathrm{voln*}\left(X\right)\upharpoonright }_S$$
24	23	fveq1d	$$⊢\phi \to \left({\mathrm{voln*}\left(X\right)\upharpoonright }_{\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)}\right)\left(E\right)=\left({\mathrm{voln*}\left(X\right)\upharpoonright }_S\right)\left(E\right)$$
25	3 2	eleqtrrdi	$$⊢\phi \to E\in S$$
26		fvres	$$⊢E\in S\to \left({\mathrm{voln*}\left(X\right)\upharpoonright }_S\right)\left(E\right)=\mathrm{voln*}\left(X\right)\left(E\right)$$
27	25 26	syl	$$⊢\phi \to \left({\mathrm{voln*}\left(X\right)\upharpoonright }_S\right)\left(E\right)=\mathrm{voln*}\left(X\right)\left(E\right)$$
28	20 24 27	3eqtrrd	$$⊢\phi \to \mathrm{voln*}\left(X\right)\left(E\right)=0$$
29	6 7 15 28 5	omess0	$$⊢\phi \to \mathrm{voln*}\left(X\right)\left(F\right)=0$$
30	6 7 16 29 9	caragencmpl	$$⊢\phi \to F\in \mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)$$
31	30 22	eleqtrd	$$⊢\phi \to F\in S$$