Theorem omecl

Description: The outer measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	omecl.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
	omecl.x	$$⊢X=\bigcup \mathrm{dom}O$$
	omecl.ss	$$⊢\phi \to A\subseteq X$$
Assertion	omecl	$$⊢\phi \to O\left(A\right)\in \left[0,\mathrm{+\infty }\right]$$

Proof

Step	Hyp	Ref	Expression
1		omecl.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
2		omecl.x	$$⊢X=\bigcup \mathrm{dom}O$$
3		omecl.ss	$$⊢\phi \to A\subseteq X$$
4	1 2	omef	$$⊢\phi \to O:𝒫X⟶\left[0,\mathrm{+\infty }\right]$$
5	2	a1i	$$⊢\phi \to X=\bigcup \mathrm{dom}O$$
6	1	dmexd	$$⊢\phi \to \mathrm{dom}O\in \mathrm{V}$$
7	6	uniexd	$$⊢\phi \to \bigcup \mathrm{dom}O\in \mathrm{V}$$
8	5 7	eqeltrd	$$⊢\phi \to X\in \mathrm{V}$$
9	8 3	ssexd	$$⊢\phi \to A\in \mathrm{V}$$
10		elpwg	$$⊢A\in \mathrm{V}\to \left(A\in 𝒫X\leftrightarrow A\subseteq X\right)$$
11	9 10	syl	$$⊢\phi \to \left(A\in 𝒫X\leftrightarrow A\subseteq X\right)$$
12	3 11	mpbird	$$⊢\phi \to A\in 𝒫X$$
13	4 12	ffvelcdmd	$$⊢\phi \to O\left(A\right)\in \left[0,\mathrm{+\infty }\right]$$