Theorem omedm

Description: The domain of an outer measure is a power set. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	omedm	|- ( O e. OutMeas -> dom O = ~P U. dom O )

Proof

Step	Hyp	Ref	Expression
1		isome	|- ( O e. OutMeas -> ( O e. OutMeas <-> ( ( ( ( O : dom O --> ( 0 [,] +oo ) /\ dom O = ~P U. dom O ) /\ ( O ` (/) ) = 0 ) /\ A. x e. ~P U. dom O A. y e. ~P x ( O ` y ) <_ ( O ` x ) ) /\ A. x e. ~P dom O ( x ~<_ _om -> ( O ` U. x ) <_ ( sum^ ` ( O |` x ) ) ) ) ) )
2	1	ibi	|- ( O e. OutMeas -> ( ( ( ( O : dom O --> ( 0 [,] +oo ) /\ dom O = ~P U. dom O ) /\ ( O ` (/) ) = 0 ) /\ A. x e. ~P U. dom O A. y e. ~P x ( O ` y ) <_ ( O ` x ) ) /\ A. x e. ~P dom O ( x ~<_ _om -> ( O ` U. x ) <_ ( sum^ ` ( O |` x ) ) ) ) )
3	2	simplld	|- ( O e. OutMeas -> ( ( O : dom O --> ( 0 [,] +oo ) /\ dom O = ~P U. dom O ) /\ ( O ` (/) ) = 0 ) )
4	3	simplrd	|- ( O e. OutMeas -> dom O = ~P U. dom O )