Metamath Proof Explorer

Theorem omeiunle

Description: The outer measure of the indexed union of a countable set is less than or equal to the extended sum of the outer measures. The proof uses abrexct rather than fnrndomg , and so does not require ax-ac . (Contributed by Glauco Siliprandi, 17-Aug-2020) (Revised by Vincent Gonzalez, 19-Aug-2026)

Ref Expression
Hypotheses omeiunle.nph 
|- F/ n ph
omeiunle.ne 
|- F/_ n E
omeiunle.o 
|- ( ph -> O e. OutMeas )
omeiunle.x 
|- X = U. dom O
omeiunle.z 
|- Z = ( ZZ>= ` N )
omeiunle.e 
|- ( ph -> E : Z --> ~P X )
Assertion omeiunle 
|- ( ph -> ( O ` U_ n e. Z ( E ` n ) ) <_ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) )

Proof

Step Hyp Ref Expression
1 omeiunle.nph 
 |-  F/ n ph
2 omeiunle.ne 
 |-  F/_ n E
3 omeiunle.o 
 |-  ( ph -> O e. OutMeas )
4 omeiunle.x 
 |-  X = U. dom O
5 omeiunle.z 
 |-  Z = ( ZZ>= ` N )
6 omeiunle.e 
 |-  ( ph -> E : Z --> ~P X )
7 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
8 6 ffvelcdmda 
 |-  ( ( ph /\ n e. Z ) -> ( E ` n ) e. ~P X )
9 elpwi 
 |-  ( ( E ` n ) e. ~P X -> ( E ` n ) C_ X )
10 8 9 syl 
 |-  ( ( ph /\ n e. Z ) -> ( E ` n ) C_ X )
11 10 ex 
 |-  ( ph -> ( n e. Z -> ( E ` n ) C_ X ) )
12 1 11 ralrimi 
 |-  ( ph -> A. n e. Z ( E ` n ) C_ X )
13 iunss 
 |-  ( U_ n e. Z ( E ` n ) C_ X <-> A. n e. Z ( E ` n ) C_ X )
14 12 13 sylibr 
 |-  ( ph -> U_ n e. Z ( E ` n ) C_ X )
15 3 4 14 omecl 
 |-  ( ph -> ( O ` U_ n e. Z ( E ` n ) ) e. ( 0 [,] +oo ) )
16 7 15 sselid 
 |-  ( ph -> ( O ` U_ n e. Z ( E ` n ) ) e. RR* )
17 6 ffnd 
 |-  ( ph -> E Fn Z )
18 5 fvexi 
 |-  Z e. _V
19 18 a1i 
 |-  ( ph -> Z e. _V )
20 fnex 
 |-  ( ( E Fn Z /\ Z e. _V ) -> E e. _V )
21 17 19 20 syl2anc 
 |-  ( ph -> E e. _V )
22 rnexg 
 |-  ( E e. _V -> ran E e. _V )
23 21 22 syl 
 |-  ( ph -> ran E e. _V )
24 3 4 omef 
 |-  ( ph -> O : ~P X --> ( 0 [,] +oo ) )
25 6 frnd 
 |-  ( ph -> ran E C_ ~P X )
26 24 25 fssresd 
 |-  ( ph -> ( O |` ran E ) : ran E --> ( 0 [,] +oo ) )
27 23 26 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( O |` ran E ) ) e. RR* )
28 3 adantr 
 |-  ( ( ph /\ n e. Z ) -> O e. OutMeas )
29 28 4 10 omecl 
 |-  ( ( ph /\ n e. Z ) -> ( O ` ( E ` n ) ) e. ( 0 [,] +oo ) )
30 eqid 
 |-  ( n e. Z |-> ( O ` ( E ` n ) ) ) = ( n e. Z |-> ( O ` ( E ` n ) ) )
31 1 29 30 fmptdf 
 |-  ( ph -> ( n e. Z |-> ( O ` ( E ` n ) ) ) : Z --> ( 0 [,] +oo ) )
32 19 31 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR* )
33 fvex 
 |-  ( E ` n ) e. _V
34 33 rgenw 
 |-  A. n e. Z ( E ` n ) e. _V
35 dfiun3g 
 |-  ( A. n e. Z ( E ` n ) e. _V -> U_ n e. Z ( E ` n ) = U. ran ( n e. Z |-> ( E ` n ) ) )
36 34 35 ax-mp 
 |-  U_ n e. Z ( E ` n ) = U. ran ( n e. Z |-> ( E ` n ) )
37 36 a1i 
 |-  ( ph -> U_ n e. Z ( E ` n ) = U. ran ( n e. Z |-> ( E ` n ) ) )
38 6 feqmptd 
 |-  ( ph -> E = ( m e. Z |-> ( E ` m ) ) )
39 nfcv 
 |-  F/_ n m
40 2 39 nffv 
 |-  F/_ n ( E ` m )
41 nfcv 
 |-  F/_ m ( E ` n )
42 fveq2 
 |-  ( m = n -> ( E ` m ) = ( E ` n ) )
43 40 41 42 cbvmpt 
 |-  ( m e. Z |-> ( E ` m ) ) = ( n e. Z |-> ( E ` n ) )
44 43 a1i 
 |-  ( ph -> ( m e. Z |-> ( E ` m ) ) = ( n e. Z |-> ( E ` n ) ) )
45 38 44 eqtrd 
 |-  ( ph -> E = ( n e. Z |-> ( E ` n ) ) )
46 45 rneqd 
 |-  ( ph -> ran E = ran ( n e. Z |-> ( E ` n ) ) )
47 46 unieqd 
 |-  ( ph -> U. ran E = U. ran ( n e. Z |-> ( E ` n ) ) )
48 37 47 eqtr4d 
 |-  ( ph -> U_ n e. Z ( E ` n ) = U. ran E )
49 48 fveq2d 
 |-  ( ph -> ( O ` U_ n e. Z ( E ` n ) ) = ( O ` U. ran E ) )
50 eqid 
 |-  ( n e. Z |-> ( E ` n ) ) = ( n e. Z |-> ( E ` n ) )
51 50 rnmpt 
 |-  ran ( n e. Z |-> ( E ` n ) ) = { m | E. n e. Z m = ( E ` n ) }
52 46 51 eqtrdi 
 |-  ( ph -> ran E = { m | E. n e. Z m = ( E ` n ) } )
53 5 uzct 
 |-  Z ~<_ _om
54 53 a1i 
 |-  ( ph -> Z ~<_ _om )
55 abrexct 
 |-  ( Z ~<_ _om -> { m | E. n e. Z m = ( E ` n ) } ~<_ _om )
56 54 55 syl 
 |-  ( ph -> { m | E. n e. Z m = ( E ` n ) } ~<_ _om )
57 52 56 eqbrtrd 
 |-  ( ph -> ran E ~<_ _om )
58 3 4 25 57 omeunile 
 |-  ( ph -> ( O ` U. ran E ) <_ ( sum^ ` ( O |` ran E ) ) )
59 49 58 eqbrtrd 
 |-  ( ph -> ( O ` U_ n e. Z ( E ` n ) ) <_ ( sum^ ` ( O |` ran E ) ) )
60 ltweuz 
 |-  < We ( ZZ>= ` N )
61 weeq2 
 |-  ( Z = ( ZZ>= ` N ) -> ( < We Z <-> < We ( ZZ>= ` N ) ) )
62 5 61 ax-mp 
 |-  ( < We Z <-> < We ( ZZ>= ` N ) )
63 60 62 mpbir 
 |-  < We Z
64 63 a1i 
 |-  ( ph -> < We Z )
65 19 24 6 64 sge0resrn 
 |-  ( ph -> ( sum^ ` ( O |` ran E ) ) <_ ( sum^ ` ( O o. E ) ) )
66 fcompt 
 |-  ( ( O : ~P X --> ( 0 [,] +oo ) /\ E : Z --> ~P X ) -> ( O o. E ) = ( m e. Z |-> ( O ` ( E ` m ) ) ) )
67 nfcv 
 |-  F/_ n O
68 67 40 nffv 
 |-  F/_ n ( O ` ( E ` m ) )
69 nfcv 
 |-  F/_ m ( O ` ( E ` n ) )
70 2fveq3 
 |-  ( m = n -> ( O ` ( E ` m ) ) = ( O ` ( E ` n ) ) )
71 68 69 70 cbvmpt 
 |-  ( m e. Z |-> ( O ` ( E ` m ) ) ) = ( n e. Z |-> ( O ` ( E ` n ) ) )
72 71 a1i 
 |-  ( ( O : ~P X --> ( 0 [,] +oo ) /\ E : Z --> ~P X ) -> ( m e. Z |-> ( O ` ( E ` m ) ) ) = ( n e. Z |-> ( O ` ( E ` n ) ) ) )
73 66 72 eqtrd 
 |-  ( ( O : ~P X --> ( 0 [,] +oo ) /\ E : Z --> ~P X ) -> ( O o. E ) = ( n e. Z |-> ( O ` ( E ` n ) ) ) )
74 24 6 73 syl2anc 
 |-  ( ph -> ( O o. E ) = ( n e. Z |-> ( O ` ( E ` n ) ) ) )
75 74 fveq2d 
 |-  ( ph -> ( sum^ ` ( O o. E ) ) = ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) )
76 65 75 breqtrd 
 |-  ( ph -> ( sum^ ` ( O |` ran E ) ) <_ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) )
77 16 27 32 59 76 xrletrd 
 |-  ( ph -> ( O ` U_ n e. Z ( E ` n ) ) <_ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) )