Metamath Proof Explorer


Theorem omeiunle

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 omeiunle.nph n φ
omeiunle.ne _ n E
omeiunle.o φ O OutMeas
omeiunle.x X = dom O
omeiunle.z Z = N
omeiunle.e φ E : Z 𝒫 X
Assertion omeiunle φ O n Z E n sum^ n Z O E n

Proof

Step Hyp Ref Expression
1 omeiunle.nph n φ
2 omeiunle.ne _ n E
3 omeiunle.o φ O OutMeas
4 omeiunle.x X = dom O
5 omeiunle.z Z = N
6 omeiunle.e φ E : Z 𝒫 X
7 iccssxr 0 +∞ *
8 6 ffvelrnda φ n Z E n 𝒫 X
9 elpwi E n 𝒫 X E n X
10 8 9 syl φ n Z E n X
11 10 ex φ n Z E n X
12 1 11 ralrimi φ n Z E n X
13 iunss n Z E n X n Z E n X
14 12 13 sylibr φ n Z E n X
15 3 4 14 omecl φ O n Z E n 0 +∞
16 7 15 sseldi φ O n Z E n *
17 6 ffnd φ E Fn Z
18 5 fvexi Z V
19 18 a1i φ Z V
20 fnex E Fn Z Z V E V
21 17 19 20 syl2anc φ E V
22 rnexg E V ran E V
23 21 22 syl φ ran E V
24 3 4 omef φ O : 𝒫 X 0 +∞
25 6 frnd φ ran E 𝒫 X
26 24 25 fssresd φ O ran E : ran E 0 +∞
27 23 26 sge0xrcl φ sum^ O ran E *
28 3 adantr φ n Z O OutMeas
29 28 4 10 omecl φ n Z O E n 0 +∞
30 eqid n Z O E n = n Z O E n
31 1 29 30 fmptdf φ n Z O E n : Z 0 +∞
32 19 31 sge0xrcl φ sum^ n Z O E n *
33 fvex E n V
34 33 rgenw n Z E n V
35 dfiun3g n Z E n V n Z E n = ran n Z E n
36 34 35 ax-mp n Z E n = ran n Z E n
37 36 a1i φ n Z E n = ran n Z E n
38 6 feqmptd φ E = m Z E m
39 nfcv _ n m
40 2 39 nffv _ n E m
41 nfcv _ m E n
42 fveq2 m = n E m = E n
43 40 41 42 cbvmpt m Z E m = n Z E n
44 43 a1i φ m Z E m = n Z E n
45 38 44 eqtrd φ E = n Z E n
46 45 rneqd φ ran E = ran n Z E n
47 46 unieqd φ ran E = ran n Z E n
48 37 47 eqtr4d φ n Z E n = ran E
49 48 fveq2d φ O n Z E n = O ran E
50 fnrndomg Z V E Fn Z ran E Z
51 19 17 50 sylc φ ran E Z
52 5 uzct Z ω
53 52 a1i φ Z ω
54 domtr ran E Z Z ω ran E ω
55 51 53 54 syl2anc φ ran E ω
56 3 4 25 55 omeunile φ O ran E sum^ O ran E
57 49 56 eqbrtrd φ O n Z E n sum^ O ran E
58 ltweuz < We N
59 weeq2 Z = N < We Z < We N
60 5 59 ax-mp < We Z < We N
61 58 60 mpbir < We Z
62 61 a1i φ < We Z
63 19 24 6 62 sge0resrn φ sum^ O ran E sum^ O E
64 fcompt O : 𝒫 X 0 +∞ E : Z 𝒫 X O E = m Z O E m
65 nfcv _ n O
66 65 40 nffv _ n O E m
67 nfcv _ m O E n
68 2fveq3 m = n O E m = O E n
69 66 67 68 cbvmpt m Z O E m = n Z O E n
70 69 a1i O : 𝒫 X 0 +∞ E : Z 𝒫 X m Z O E m = n Z O E n
71 64 70 eqtrd O : 𝒫 X 0 +∞ E : Z 𝒫 X O E = n Z O E n
72 24 6 71 syl2anc φ O E = n Z O E n
73 72 fveq2d φ sum^ O E = sum^ n Z O E n
74 63 73 breqtrd φ sum^ O ran E sum^ n Z O E n
75 16 27 32 57 74 xrletrd φ O n Z E n sum^ n Z O E n