Metamath Proof Explorer


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 φ O OutMeas
omelesplit.2 X = dom O
omelesplit.3 φ A X
Assertion omelesplit φ O A O A E + 𝑒 O A E

Proof

Step Hyp Ref Expression
1 omelesplit.1 φ O OutMeas
2 omelesplit.2 X = dom O
3 omelesplit.3 φ A X
4 inundif A E A E = A
5 4 eqcomi A = A E A E
6 5 a1i φ A = A E A E
7 6 fveq2d φ O A = O A E A E
8 ssinss1 A X A E X
9 3 8 syl φ A E X
10 3 ssdifssd φ A E X
11 1 2 9 10 omeunle φ O A E A E O A E + 𝑒 O A E
12 7 11 eqbrtrd φ O A O A E + 𝑒 O A E