Metamath Proof Explorer

Theorem omeunle

Description: The outer measure of the union of two sets is less than or equal to the sum of the measures, Remark 113B (c) of Fremlin1 p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses omeunle.o 
|- ( ph -> O e. OutMeas )
omeunle.x 
|- X = U. dom O
omeunle.a 
|- ( ph -> A C_ X )
omeunle.b 
|- ( ph -> B C_ X )
Assertion omeunle 
|- ( ph -> ( O ` ( A u. B ) ) <_ ( ( O ` A ) +e ( O ` B ) ) )

Proof

Step Hyp Ref Expression
1 omeunle.o 
 |-  ( ph -> O e. OutMeas )
2 omeunle.x 
 |-  X = U. dom O
3 omeunle.a 
 |-  ( ph -> A C_ X )
4 omeunle.b 
 |-  ( ph -> B C_ X )
5 1 2 unidmex 
 |-  ( ph -> X e. _V )
6 ssexg 
 |-  ( ( A C_ X /\ X e. _V ) -> A e. _V )
7 3 5 6 syl2anc 
 |-  ( ph -> A e. _V )
8 ssexg 
 |-  ( ( B C_ X /\ X e. _V ) -> B e. _V )
9 4 5 8 syl2anc 
 |-  ( ph -> B e. _V )
10 uniprg 
 |-  ( ( A e. _V /\ B e. _V ) -> U. { A , B } = ( A u. B ) )
11 7 9 10 syl2anc 
 |-  ( ph -> U. { A , B } = ( A u. B ) )
12 11 eqcomd 
 |-  ( ph -> ( A u. B ) = U. { A , B } )
13 12 fveq2d 
 |-  ( ph -> ( O ` ( A u. B ) ) = ( O ` U. { A , B } ) )
14 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
15 3 4 unssd 
 |-  ( ph -> ( A u. B ) C_ X )
16 11 15 eqsstrd 
 |-  ( ph -> U. { A , B } C_ X )
17 1 2 16 omecl 
 |-  ( ph -> ( O ` U. { A , B } ) e. ( 0 [,] +oo ) )
18 14 17 sselid 
 |-  ( ph -> ( O ` U. { A , B } ) e. RR* )
19 prfi 
 |-  { A , B } e. Fin
20 19 elexi 
 |-  { A , B } e. _V
21 20 a1i 
 |-  ( ph -> { A , B } e. _V )
22 1 2 omef 
 |-  ( ph -> O : ~P X --> ( 0 [,] +oo ) )
23 elpwg 
 |-  ( A e. _V -> ( A e. ~P X <-> A C_ X ) )
24 7 23 syl 
 |-  ( ph -> ( A e. ~P X <-> A C_ X ) )
25 3 24 mpbird 
 |-  ( ph -> A e. ~P X )
26 elpwg 
 |-  ( B e. _V -> ( B e. ~P X <-> B C_ X ) )
27 9 26 syl 
 |-  ( ph -> ( B e. ~P X <-> B C_ X ) )
28 4 27 mpbird 
 |-  ( ph -> B e. ~P X )
29 25 28 jca 
 |-  ( ph -> ( A e. ~P X /\ B e. ~P X ) )
30 prssg 
 |-  ( ( A e. _V /\ B e. _V ) -> ( ( A e. ~P X /\ B e. ~P X ) <-> { A , B } C_ ~P X ) )
31 7 9 30 syl2anc 
 |-  ( ph -> ( ( A e. ~P X /\ B e. ~P X ) <-> { A , B } C_ ~P X ) )
32 29 31 mpbid 
 |-  ( ph -> { A , B } C_ ~P X )
33 22 32 fssresd 
 |-  ( ph -> ( O |` { A , B } ) : { A , B } --> ( 0 [,] +oo ) )
34 21 33 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( O |` { A , B } ) ) e. RR* )
35 1 2 3 omecl 
 |-  ( ph -> ( O ` A ) e. ( 0 [,] +oo ) )
36 14 35 sselid 
 |-  ( ph -> ( O ` A ) e. RR* )
37 1 2 4 omecl 
 |-  ( ph -> ( O ` B ) e. ( 0 [,] +oo ) )
38 14 37 sselid 
 |-  ( ph -> ( O ` B ) e. RR* )
39 36 38 xaddcld 
 |-  ( ph -> ( ( O ` A ) +e ( O ` B ) ) e. RR* )
40 isfinite 
 |-  ( { A , B } e. Fin <-> { A , B } ~< _om )
41 40 biimpi 
 |-  ( { A , B } e. Fin -> { A , B } ~< _om )
42 sdomdom 
 |-  ( { A , B } ~< _om -> { A , B } ~<_ _om )
43 41 42 syl 
 |-  ( { A , B } e. Fin -> { A , B } ~<_ _om )
44 19 43 ax-mp 
 |-  { A , B } ~<_ _om
45 44 a1i 
 |-  ( ph -> { A , B } ~<_ _om )
46 1 2 32 45 omeunile 
 |-  ( ph -> ( O ` U. { A , B } ) <_ ( sum^ ` ( O |` { A , B } ) ) )
47 22 32 feqresmpt 
 |-  ( ph -> ( O |` { A , B } ) = ( k e. { A , B } |-> ( O ` k ) ) )
48 47 fveq2d 
 |-  ( ph -> ( sum^ ` ( O |` { A , B } ) ) = ( sum^ ` ( k e. { A , B } |-> ( O ` k ) ) ) )
49 fveq2 
 |-  ( k = A -> ( O ` k ) = ( O ` A ) )
50 fveq2 
 |-  ( k = B -> ( O ` k ) = ( O ` B ) )
51 7 9 35 37 49 50 sge0prle 
 |-  ( ph -> ( sum^ ` ( k e. { A , B } |-> ( O ` k ) ) ) <_ ( ( O ` A ) +e ( O ` B ) ) )
52 48 51 eqbrtrd 
 |-  ( ph -> ( sum^ ` ( O |` { A , B } ) ) <_ ( ( O ` A ) +e ( O ` B ) ) )
53 18 34 39 46 52 xrletrd 
 |-  ( ph -> ( O ` U. { A , B } ) <_ ( ( O ` A ) +e ( O ` B ) ) )
54 13 53 eqbrtrd 
 |-  ( ph -> ( O ` ( A u. B ) ) <_ ( ( O ` A ) +e ( O ` B ) ) )