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 
|- ( ph -> X e. V )
0ome.2 
|- O = ( x e. ~P X |-> 0 )
Assertion 0ome 
|- ( ph -> O e. OutMeas )

Proof

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