Theorem omelesplit

Description: The outer measure of a set A is less than or equal to the extended addition of the outer measures of the decomposition induced on A by any E . Step (a) in the proof of Caratheodory's Method, Theorem 113C of Fremlin1 p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	omelesplit.1	|- ( ph -> O e. OutMeas )
	omelesplit.2	|- X = U. dom O
	omelesplit.3	|- ( ph -> A C_ X )
Assertion	omelesplit	|- ( ph -> ( O ` A ) <_ ( ( O ` ( A i^i E ) ) +e ( O ` ( A \ E ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		omelesplit.1	|- ( ph -> O e. OutMeas )
2		omelesplit.2	|- X = U. dom O
3		omelesplit.3	|- ( ph -> A C_ X )
4		inundif	|- ( ( A i^i E ) u. ( A \ E ) ) = A
5	4	eqcomi	|- A = ( ( A i^i E ) u. ( A \ E ) )
6	5	a1i	|- ( ph -> A = ( ( A i^i E ) u. ( A \ E ) ) )
7	6	fveq2d	|- ( ph -> ( O ` A ) = ( O ` ( ( A i^i E ) u. ( A \ E ) ) ) )
8		ssinss1	|- ( A C_ X -> ( A i^i E ) C_ X )
9	3 8	syl	|- ( ph -> ( A i^i E ) C_ X )
10	3	ssdifssd	|- ( ph -> ( A \ E ) C_ X )
11	1 2 9 10	omeunle	|- ( ph -> ( O ` ( ( A i^i E ) u. ( A \ E ) ) ) <_ ( ( O ` ( A i^i E ) ) +e ( O ` ( A \ E ) ) ) )
12	7 11	eqbrtrd	|- ( ph -> ( O ` A ) <_ ( ( O ` ( A i^i E ) ) +e ( O ` ( A \ E ) ) ) )