Metamath Proof Explorer


Theorem 0ome

Description: The map that assigns 0 to every subset, is an outer measure. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses 0ome.1 φ X V
0ome.2 O = x 𝒫 X 0
Assertion 0ome φ O OutMeas

Proof

Step Hyp Ref Expression
1 0ome.1 φ X V
2 0ome.2 O = x 𝒫 X 0
3 eqid y 𝒫 X 0 = y 𝒫 X 0
4 0e0iccpnf 0 0 +∞
5 4 a1i y 𝒫 X 0 0 +∞
6 3 5 fmpti y 𝒫 X 0 : 𝒫 X 0 +∞
7 eqidd x = y 0 = 0
8 7 cbvmptv x 𝒫 X 0 = y 𝒫 X 0
9 2 8 eqtri O = y 𝒫 X 0
10 9 feq1i O : dom O 0 +∞ y 𝒫 X 0 : dom O 0 +∞
11 9 dmeqi dom O = dom y 𝒫 X 0
12 0re 0
13 12 rgenw y 𝒫 X 0
14 dmmptg y 𝒫 X 0 dom y 𝒫 X 0 = 𝒫 X
15 13 14 ax-mp dom y 𝒫 X 0 = 𝒫 X
16 11 15 eqtri dom O = 𝒫 X
17 16 feq2i y 𝒫 X 0 : dom O 0 +∞ y 𝒫 X 0 : 𝒫 X 0 +∞
18 10 17 bitri O : dom O 0 +∞ y 𝒫 X 0 : 𝒫 X 0 +∞
19 6 18 mpbir O : dom O 0 +∞
20 unipw 𝒫 X = X
21 20 pweqi 𝒫 𝒫 X = 𝒫 X
22 21 eqcomi 𝒫 X = 𝒫 𝒫 X
23 16 eqcomi 𝒫 X = dom O
24 23 unieqi 𝒫 X = dom O
25 24 pweqi 𝒫 𝒫 X = 𝒫 dom O
26 16 22 25 3eqtri dom O = 𝒫 dom O
27 19 26 pm3.2i O : dom O 0 +∞ dom O = 𝒫 dom O
28 0elpw 𝒫 X
29 eqidd y = 0 = 0
30 12 elexi 0 V
31 29 9 30 fvmpt 𝒫 X O = 0
32 28 31 ax-mp O = 0
33 27 32 pm3.2i O : dom O 0 +∞ dom O = 𝒫 dom O O = 0
34 12 leidi 0 0
35 34 a1i y 𝒫 dom O z 𝒫 y 0 0
36 eqidd y = z 0 = 0
37 elpwi z 𝒫 y z y
38 37 adantl y 𝒫 dom O z 𝒫 y z y
39 id y 𝒫 dom O y 𝒫 dom O
40 22 25 eqtr2i 𝒫 dom O = 𝒫 X
41 40 a1i y 𝒫 dom O 𝒫 dom O = 𝒫 X
42 39 41 eleqtrd y 𝒫 dom O y 𝒫 X
43 elpwi y 𝒫 X y X
44 42 43 syl y 𝒫 dom O y X
45 44 adantr y 𝒫 dom O z 𝒫 y y X
46 38 45 sstrd y 𝒫 dom O z 𝒫 y z X
47 simpr y 𝒫 dom O z 𝒫 y z 𝒫 y
48 elpwg z 𝒫 y z 𝒫 X z X
49 47 48 syl y 𝒫 dom O z 𝒫 y z 𝒫 X z X
50 46 49 mpbird y 𝒫 dom O z 𝒫 y z 𝒫 X
51 12 a1i y 𝒫 dom O z 𝒫 y 0
52 9 36 50 51 fvmptd3 y 𝒫 dom O z 𝒫 y O z = 0
53 9 fvmpt2 y 𝒫 X 0 O y = 0
54 42 12 53 sylancl y 𝒫 dom O O y = 0
55 54 adantr y 𝒫 dom O z 𝒫 y O y = 0
56 52 55 breq12d y 𝒫 dom O z 𝒫 y O z O y 0 0
57 35 56 mpbird y 𝒫 dom O z 𝒫 y O z O y
58 57 ralrimiva y 𝒫 dom O z 𝒫 y O z O y
59 58 rgen y 𝒫 dom O z 𝒫 y O z O y
60 33 59 pm3.2i O : dom O 0 +∞ dom O = 𝒫 dom O O = 0 y 𝒫 dom O z 𝒫 y O z O y
61 34 a1i y 𝒫 dom O 0 0
62 36 cbvmptv y 𝒫 X 0 = z 𝒫 X 0
63 9 62 eqtri O = z 𝒫 X 0
64 63 a1i y 𝒫 dom O O = z 𝒫 X 0
65 eqidd y 𝒫 dom O z = y 0 = 0
66 id y 𝒫 dom O y 𝒫 dom O
67 16 pweqi 𝒫 dom O = 𝒫 𝒫 X
68 67 a1i y 𝒫 dom O 𝒫 dom O = 𝒫 𝒫 X
69 66 68 eleqtrd y 𝒫 dom O y 𝒫 𝒫 X
70 elpwi y 𝒫 𝒫 X y 𝒫 X
71 69 70 syl y 𝒫 dom O y 𝒫 X
72 sspwuni y 𝒫 X y X
73 71 72 sylib y 𝒫 dom O y X
74 vuniex y V
75 74 a1i y 𝒫 dom O y V
76 elpwg y V y 𝒫 X y X
77 75 76 syl y 𝒫 dom O y 𝒫 X y X
78 73 77 mpbird y 𝒫 dom O y 𝒫 X
79 12 a1i y 𝒫 dom O 0
80 64 65 78 79 fvmptd y 𝒫 dom O O y = 0
81 64 reseq1d y 𝒫 dom O O y = z 𝒫 X 0 y
82 resmpt y 𝒫 X z 𝒫 X 0 y = z y 0
83 71 82 syl y 𝒫 dom O z 𝒫 X 0 y = z y 0
84 81 83 eqtrd y 𝒫 dom O O y = z y 0
85 84 fveq2d y 𝒫 dom O sum^ O y = sum^ z y 0
86 nfv z y 𝒫 dom O
87 86 66 sge0z y 𝒫 dom O sum^ z y 0 = 0
88 85 87 eqtrd y 𝒫 dom O sum^ O y = 0
89 80 88 breq12d y 𝒫 dom O O y sum^ O y 0 0
90 61 89 mpbird y 𝒫 dom O O y sum^ O y
91 90 a1d y 𝒫 dom O y ω O y sum^ O y
92 91 rgen y 𝒫 dom O y ω O y sum^ O y
93 60 92 pm3.2i O : dom O 0 +∞ dom O = 𝒫 dom O O = 0 y 𝒫 dom O z 𝒫 y O z O y y 𝒫 dom O y ω O y sum^ O y
94 93 a1i φ O : dom O 0 +∞ dom O = 𝒫 dom O O = 0 y 𝒫 dom O z 𝒫 y O z O y y 𝒫 dom O y ω O y sum^ O y
95 9 a1i φ O = y 𝒫 X 0
96 1 pwexd φ 𝒫 X V
97 mptexg 𝒫 X V y 𝒫 X 0 V
98 96 97 syl φ y 𝒫 X 0 V
99 95 98 eqeltrd φ O V
100 isome O V O OutMeas O : dom O 0 +∞ dom O = 𝒫 dom O O = 0 y 𝒫 dom O z 𝒫 y O z O y y 𝒫 dom O y ω O y sum^ O y
101 99 100 syl φ O OutMeas O : dom O 0 +∞ dom O = 𝒫 dom O O = 0 y 𝒫 dom O z 𝒫 y O z O y y 𝒫 dom O y ω O y sum^ O y
102 94 101 mpbird φ O OutMeas