Metamath Proof Explorer

Theorem omeiunlempt

Description: The outer measure of the indexed 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 omeiunlempt.nph 
|- F/ n ph
omeiunlempt.o 
|- ( ph -> O e. OutMeas )
omeiunlempt.x 
|- X = U. dom O
omeiunlempt.z 
|- Z = ( ZZ>= ` N )
omeiunlempt.e 
|- ( ( ph /\ n e. Z ) -> E C_ X )
Assertion omeiunlempt 
|- ( ph -> ( O ` U_ n e. Z E ) <_ ( sum^ ` ( n e. Z |-> ( O ` E ) ) ) )

Proof

Step Hyp Ref Expression
1 omeiunlempt.nph 
 |-  F/ n ph
2 omeiunlempt.o 
 |-  ( ph -> O e. OutMeas )
3 omeiunlempt.x 
 |-  X = U. dom O
4 omeiunlempt.z 
 |-  Z = ( ZZ>= ` N )
5 omeiunlempt.e 
 |-  ( ( ph /\ n e. Z ) -> E C_ X )
6 nfmpt1 
 |-  F/_ n ( n e. Z |-> E )
7 2 3 unidmex 
 |-  ( ph -> X e. _V )
8 7 adantr 
 |-  ( ( ph /\ n e. Z ) -> X e. _V )
9 ssexg 
 |-  ( ( E C_ X /\ X e. _V ) -> E e. _V )
10 5 8 9 syl2anc 
 |-  ( ( ph /\ n e. Z ) -> E e. _V )
11 elpwg 
 |-  ( E e. _V -> ( E e. ~P X <-> E C_ X ) )
12 10 11 syl 
 |-  ( ( ph /\ n e. Z ) -> ( E e. ~P X <-> E C_ X ) )
13 5 12 mpbird 
 |-  ( ( ph /\ n e. Z ) -> E e. ~P X )
14 eqid 
 |-  ( n e. Z |-> E ) = ( n e. Z |-> E )
15 1 13 14 fmptdf 
 |-  ( ph -> ( n e. Z |-> E ) : Z --> ~P X )
16 1 6 2 3 4 15 omeiunle 
 |-  ( ph -> ( O ` U_ n e. Z ( ( n e. Z |-> E ) ` n ) ) <_ ( sum^ ` ( n e. Z |-> ( O ` ( ( n e. Z |-> E ) ` n ) ) ) ) )
17 simpr 
 |-  ( ( ph /\ n e. Z ) -> n e. Z )
18 14 fvmpt2 
 |-  ( ( n e. Z /\ E e. _V ) -> ( ( n e. Z |-> E ) ` n ) = E )
19 17 10 18 syl2anc 
 |-  ( ( ph /\ n e. Z ) -> ( ( n e. Z |-> E ) ` n ) = E )
20 19 eqcomd 
 |-  ( ( ph /\ n e. Z ) -> E = ( ( n e. Z |-> E ) ` n ) )
21 1 20 iuneq2df 
 |-  ( ph -> U_ n e. Z E = U_ n e. Z ( ( n e. Z |-> E ) ` n ) )
22 21 fveq2d 
 |-  ( ph -> ( O ` U_ n e. Z E ) = ( O ` U_ n e. Z ( ( n e. Z |-> E ) ` n ) ) )
23 20 fveq2d 
 |-  ( ( ph /\ n e. Z ) -> ( O ` E ) = ( O ` ( ( n e. Z |-> E ) ` n ) ) )
24 1 23 mpteq2da 
 |-  ( ph -> ( n e. Z |-> ( O ` E ) ) = ( n e. Z |-> ( O ` ( ( n e. Z |-> E ) ` n ) ) ) )
25 24 fveq2d 
 |-  ( ph -> ( sum^ ` ( n e. Z |-> ( O ` E ) ) ) = ( sum^ ` ( n e. Z |-> ( O ` ( ( n e. Z |-> E ) ` n ) ) ) ) )
26 22 25 breq12d 
 |-  ( ph -> ( ( O ` U_ n e. Z E ) <_ ( sum^ ` ( n e. Z |-> ( O ` E ) ) ) <-> ( O ` U_ n e. Z ( ( n e. Z |-> E ) ` n ) ) <_ ( sum^ ` ( n e. Z |-> ( O ` ( ( n e. Z |-> E ) ` n ) ) ) ) ) )
27 16 26 mpbird 
 |-  ( ph -> ( O ` U_ n e. Z E ) <_ ( sum^ ` ( n e. Z |-> ( O ` E ) ) ) )