Metamath Proof Explorer

Theorem omeunile

Description: The outer measure of the union of a countable set is the less than or equal to the extended sum of the outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses omeunile.o 
|- ( ph -> O e. OutMeas )
omeunile.x 
|- X = U. dom O
omeunile.y 
|- ( ph -> Y C_ ~P X )
omeunile.ct 
|- ( ph -> Y ~<_ _om )
Assertion omeunile 
|- ( ph -> ( O ` U. Y ) <_ ( sum^ ` ( O |` Y ) ) )

Proof

Step Hyp Ref Expression
1 omeunile.o 
 |-  ( ph -> O e. OutMeas )
2 omeunile.x 
 |-  X = U. dom O
3 omeunile.y 
 |-  ( ph -> Y C_ ~P X )
4 omeunile.ct 
 |-  ( ph -> Y ~<_ _om )
5 1 2 unidmex 
 |-  ( ph -> X e. _V )
6 5 pwexd 
 |-  ( ph -> ~P X e. _V )
7 ssexg 
 |-  ( ( Y C_ ~P X /\ ~P X e. _V ) -> Y e. _V )
8 3 6 7 syl2anc 
 |-  ( ph -> Y e. _V )
9 elpwg 
 |-  ( Y e. _V -> ( Y e. ~P ~P X <-> Y C_ ~P X ) )
10 8 9 syl 
 |-  ( ph -> ( Y e. ~P ~P X <-> Y C_ ~P X ) )
11 3 10 mpbird 
 |-  ( ph -> Y e. ~P ~P X )
12 omedm 
 |-  ( O e. OutMeas -> dom O = ~P U. dom O )
13 1 12 syl 
 |-  ( ph -> dom O = ~P U. dom O )
14 2 pweqi 
 |-  ~P X = ~P U. dom O
15 14 eqcomi 
 |-  ~P U. dom O = ~P X
16 15 a1i 
 |-  ( ph -> ~P U. dom O = ~P X )
17 13 16 eqtr2d 
 |-  ( ph -> ~P X = dom O )
18 17 pweqd 
 |-  ( ph -> ~P ~P X = ~P dom O )
19 11 18 eleqtrd 
 |-  ( ph -> Y e. ~P dom O )
20 isome 
 |-  ( O e. OutMeas -> ( O e. OutMeas <-> ( ( ( ( O : dom O --> ( 0 [,] +oo ) /\ dom O = ~P U. dom O ) /\ ( O ` (/) ) = 0 ) /\ A. y e. ~P U. dom O A. x e. ~P y ( O ` x ) <_ ( O ` y ) ) /\ A. y e. ~P dom O ( y ~<_ _om -> ( O ` U. y ) <_ ( sum^ ` ( O |` y ) ) ) ) ) )
21 1 20 syl 
 |-  ( ph -> ( O e. OutMeas <-> ( ( ( ( O : dom O --> ( 0 [,] +oo ) /\ dom O = ~P U. dom O ) /\ ( O ` (/) ) = 0 ) /\ A. y e. ~P U. dom O A. x e. ~P y ( O ` x ) <_ ( O ` y ) ) /\ A. y e. ~P dom O ( y ~<_ _om -> ( O ` U. y ) <_ ( sum^ ` ( O |` y ) ) ) ) ) )
22 1 21 mpbid 
 |-  ( ph -> ( ( ( ( O : dom O --> ( 0 [,] +oo ) /\ dom O = ~P U. dom O ) /\ ( O ` (/) ) = 0 ) /\ A. y e. ~P U. dom O A. x e. ~P y ( O ` x ) <_ ( O ` y ) ) /\ A. y e. ~P dom O ( y ~<_ _om -> ( O ` U. y ) <_ ( sum^ ` ( O |` y ) ) ) ) )
23 22 simprd 
 |-  ( ph -> A. y e. ~P dom O ( y ~<_ _om -> ( O ` U. y ) <_ ( sum^ ` ( O |` y ) ) ) )
24 breq1 
 |-  ( y = Y -> ( y ~<_ _om <-> Y ~<_ _om ) )
25 unieq 
 |-  ( y = Y -> U. y = U. Y )
26 25 fveq2d 
 |-  ( y = Y -> ( O ` U. y ) = ( O ` U. Y ) )
27 reseq2 
 |-  ( y = Y -> ( O |` y ) = ( O |` Y ) )
28 27 fveq2d 
 |-  ( y = Y -> ( sum^ ` ( O |` y ) ) = ( sum^ ` ( O |` Y ) ) )
29 26 28 breq12d 
 |-  ( y = Y -> ( ( O ` U. y ) <_ ( sum^ ` ( O |` y ) ) <-> ( O ` U. Y ) <_ ( sum^ ` ( O |` Y ) ) ) )
30 24 29 imbi12d 
 |-  ( y = Y -> ( ( y ~<_ _om -> ( O ` U. y ) <_ ( sum^ ` ( O |` y ) ) ) <-> ( Y ~<_ _om -> ( O ` U. Y ) <_ ( sum^ ` ( O |` Y ) ) ) ) )
31 30 rspcva 
 |-  ( ( Y e. ~P dom O /\ A. y e. ~P dom O ( y ~<_ _om -> ( O ` U. y ) <_ ( sum^ ` ( O |` y ) ) ) ) -> ( Y ~<_ _om -> ( O ` U. Y ) <_ ( sum^ ` ( O |` Y ) ) ) )
32 19 23 31 syl2anc 
 |-  ( ph -> ( Y ~<_ _om -> ( O ` U. Y ) <_ ( sum^ ` ( O |` Y ) ) ) )
33 4 32 mpd 
 |-  ( ph -> ( O ` U. Y ) <_ ( sum^ ` ( O |` Y ) ) )