Metamath Proof Explorer

Theorem nulmbl2

Description: A set of outer measure zero is measurable. The term "outer measure zero" here is slightly different from "nullset/negligible set"; a nullset has vol* ( A ) = 0 while "outer measure zero" means that for any x there is a y containing A with volume less than x . Assuming AC, these notions are equivalent (because the intersection of all such y is a nullset) but in ZF this is a strictly weaker notion. Proposition 563Gb of Fremlin5 p. 193. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Assertion nulmbl2 
|- ( A. x e. RR+ E. y e. dom vol ( A C_ y /\ ( vol* ` y ) <_ x ) -> A e. dom vol )

Proof

Step Hyp Ref Expression
1 1rp 
 |-  1 e. RR+
2 1 ne0ii 
 |-  RR+ =/= (/)
3 r19.2z 
 |-  ( ( RR+ =/= (/) /\ A. x e. RR+ E. y e. dom vol ( A C_ y /\ ( vol* ` y ) <_ x ) ) -> E. x e. RR+ E. y e. dom vol ( A C_ y /\ ( vol* ` y ) <_ x ) )
4 2 3 mpan 
 |-  ( A. x e. RR+ E. y e. dom vol ( A C_ y /\ ( vol* ` y ) <_ x ) -> E. x e. RR+ E. y e. dom vol ( A C_ y /\ ( vol* ` y ) <_ x ) )
5 simprl 
 |-  ( ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) -> A C_ y )
6 mblss 
 |-  ( y e. dom vol -> y C_ RR )
7 6 adantr 
 |-  ( ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) -> y C_ RR )
8 5 7 sstrd 
 |-  ( ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) -> A C_ RR )
9 8 rexlimiva 
 |-  ( E. y e. dom vol ( A C_ y /\ ( vol* ` y ) <_ x ) -> A C_ RR )
10 9 rexlimivw 
 |-  ( E. x e. RR+ E. y e. dom vol ( A C_ y /\ ( vol* ` y ) <_ x ) -> A C_ RR )
11 4 10 syl 
 |-  ( A. x e. RR+ E. y e. dom vol ( A C_ y /\ ( vol* ` y ) <_ x ) -> A C_ RR )
12 inss1 
 |-  ( z i^i A ) C_ z
13 elpwi 
 |-  ( z e. ~P RR -> z C_ RR )
14 13 adantr 
 |-  ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) -> z C_ RR )
15 simpr 
 |-  ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) -> ( vol* ` z ) e. RR )
16 ovolsscl 
 |-  ( ( ( z i^i A ) C_ z /\ z C_ RR /\ ( vol* ` z ) e. RR ) -> ( vol* ` ( z i^i A ) ) e. RR )
17 12 14 15 16 mp3an2i 
 |-  ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) -> ( vol* ` ( z i^i A ) ) e. RR )
18 difssd 
 |-  ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) -> ( z \ A ) C_ z )
19 ovolsscl 
 |-  ( ( ( z \ A ) C_ z /\ z C_ RR /\ ( vol* ` z ) e. RR ) -> ( vol* ` ( z \ A ) ) e. RR )
20 18 14 15 19 syl3anc 
 |-  ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) -> ( vol* ` ( z \ A ) ) e. RR )
21 17 20 readdcld 
 |-  ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) -> ( ( vol* ` ( z i^i A ) ) + ( vol* ` ( z \ A ) ) ) e. RR )
22 21 ad2antrr 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( ( vol* ` ( z i^i A ) ) + ( vol* ` ( z \ A ) ) ) e. RR )
23 15 ad2antrr 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( vol* ` z ) e. RR )
24 difssd 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( y \ A ) C_ y )
25 7 adantl 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> y C_ RR )
26 rpre 
 |-  ( x e. RR+ -> x e. RR )
27 26 ad2antlr 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> x e. RR )
28 simprrr 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( vol* ` y ) <_ x )
29 ovollecl 
 |-  ( ( y C_ RR /\ x e. RR /\ ( vol* ` y ) <_ x ) -> ( vol* ` y ) e. RR )
30 25 27 28 29 syl3anc 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( vol* ` y ) e. RR )
31 ovolsscl 
 |-  ( ( ( y \ A ) C_ y /\ y C_ RR /\ ( vol* ` y ) e. RR ) -> ( vol* ` ( y \ A ) ) e. RR )
32 24 25 30 31 syl3anc 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( vol* ` ( y \ A ) ) e. RR )
33 23 32 readdcld 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( ( vol* ` z ) + ( vol* ` ( y \ A ) ) ) e. RR )
34 23 27 readdcld 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( ( vol* ` z ) + x ) e. RR )
35 17 ad2antrr 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( vol* ` ( z i^i A ) ) e. RR )
36 20 ad2antrr 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( vol* ` ( z \ A ) ) e. RR )
37 inss1 
 |-  ( z i^i y ) C_ z
38 14 ad2antrr 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> z C_ RR )
39 ovolsscl 
 |-  ( ( ( z i^i y ) C_ z /\ z C_ RR /\ ( vol* ` z ) e. RR ) -> ( vol* ` ( z i^i y ) ) e. RR )
40 37 38 23 39 mp3an2i 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( vol* ` ( z i^i y ) ) e. RR )
41 difssd 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( z \ y ) C_ z )
42 ovolsscl 
 |-  ( ( ( z \ y ) C_ z /\ z C_ RR /\ ( vol* ` z ) e. RR ) -> ( vol* ` ( z \ y ) ) e. RR )
43 41 38 23 42 syl3anc 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( vol* ` ( z \ y ) ) e. RR )
44 43 32 readdcld 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( ( vol* ` ( z \ y ) ) + ( vol* ` ( y \ A ) ) ) e. RR )
45 simprrl 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> A C_ y )
46 sslin 
 |-  ( A C_ y -> ( z i^i A ) C_ ( z i^i y ) )
47 45 46 syl 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( z i^i A ) C_ ( z i^i y ) )
48 37 38 sstrid 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( z i^i y ) C_ RR )
49 ovolss 
 |-  ( ( ( z i^i A ) C_ ( z i^i y ) /\ ( z i^i y ) C_ RR ) -> ( vol* ` ( z i^i A ) ) <_ ( vol* ` ( z i^i y ) ) )
50 47 48 49 syl2anc 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( vol* ` ( z i^i A ) ) <_ ( vol* ` ( z i^i y ) ) )
51 38 ssdifssd 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( z \ y ) C_ RR )
52 25 ssdifssd 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( y \ A ) C_ RR )
53 51 52 unssd 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( ( z \ y ) u. ( y \ A ) ) C_ RR )
54 ovolun 
 |-  ( ( ( ( z \ y ) C_ RR /\ ( vol* ` ( z \ y ) ) e. RR ) /\ ( ( y \ A ) C_ RR /\ ( vol* ` ( y \ A ) ) e. RR ) ) -> ( vol* ` ( ( z \ y ) u. ( y \ A ) ) ) <_ ( ( vol* ` ( z \ y ) ) + ( vol* ` ( y \ A ) ) ) )
55 51 43 52 32 54 syl22anc 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( vol* ` ( ( z \ y ) u. ( y \ A ) ) ) <_ ( ( vol* ` ( z \ y ) ) + ( vol* ` ( y \ A ) ) ) )
56 ovollecl 
 |-  ( ( ( ( z \ y ) u. ( y \ A ) ) C_ RR /\ ( ( vol* ` ( z \ y ) ) + ( vol* ` ( y \ A ) ) ) e. RR /\ ( vol* ` ( ( z \ y ) u. ( y \ A ) ) ) <_ ( ( vol* ` ( z \ y ) ) + ( vol* ` ( y \ A ) ) ) ) -> ( vol* ` ( ( z \ y ) u. ( y \ A ) ) ) e. RR )
57 53 44 55 56 syl3anc 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( vol* ` ( ( z \ y ) u. ( y \ A ) ) ) e. RR )
58 ssun1 
 |-  z C_ ( z u. y )
59 undif1 
 |-  ( ( z \ y ) u. y ) = ( z u. y )
60 58 59 sseqtrri 
 |-  z C_ ( ( z \ y ) u. y )
61 ssdif 
 |-  ( z C_ ( ( z \ y ) u. y ) -> ( z \ A ) C_ ( ( ( z \ y ) u. y ) \ A ) )
62 60 61 ax-mp 
 |-  ( z \ A ) C_ ( ( ( z \ y ) u. y ) \ A )
63 difundir 
 |-  ( ( ( z \ y ) u. y ) \ A ) = ( ( ( z \ y ) \ A ) u. ( y \ A ) )
64 62 63 sseqtri 
 |-  ( z \ A ) C_ ( ( ( z \ y ) \ A ) u. ( y \ A ) )
65 difun1 
 |-  ( z \ ( y u. A ) ) = ( ( z \ y ) \ A )
66 ssequn2 
 |-  ( A C_ y <-> ( y u. A ) = y )
67 45 66 sylib 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( y u. A ) = y )
68 67 difeq2d 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( z \ ( y u. A ) ) = ( z \ y ) )
69 65 68 eqtr3id 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( ( z \ y ) \ A ) = ( z \ y ) )
70 69 uneq1d 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( ( ( z \ y ) \ A ) u. ( y \ A ) ) = ( ( z \ y ) u. ( y \ A ) ) )
71 64 70 sseqtrid 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( z \ A ) C_ ( ( z \ y ) u. ( y \ A ) ) )
72 ovolss 
 |-  ( ( ( z \ A ) C_ ( ( z \ y ) u. ( y \ A ) ) /\ ( ( z \ y ) u. ( y \ A ) ) C_ RR ) -> ( vol* ` ( z \ A ) ) <_ ( vol* ` ( ( z \ y ) u. ( y \ A ) ) ) )
73 71 53 72 syl2anc 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( vol* ` ( z \ A ) ) <_ ( vol* ` ( ( z \ y ) u. ( y \ A ) ) ) )
74 36 57 44 73 55 letrd 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( vol* ` ( z \ A ) ) <_ ( ( vol* ` ( z \ y ) ) + ( vol* ` ( y \ A ) ) ) )
75 35 36 40 44 50 74 le2addd 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( ( vol* ` ( z i^i A ) ) + ( vol* ` ( z \ A ) ) ) <_ ( ( vol* ` ( z i^i y ) ) + ( ( vol* ` ( z \ y ) ) + ( vol* ` ( y \ A ) ) ) ) )
76 simprl 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> y e. dom vol )
77 mblsplit 
 |-  ( ( y e. dom vol /\ z C_ RR /\ ( vol* ` z ) e. RR ) -> ( vol* ` z ) = ( ( vol* ` ( z i^i y ) ) + ( vol* ` ( z \ y ) ) ) )
78 76 38 23 77 syl3anc 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( vol* ` z ) = ( ( vol* ` ( z i^i y ) ) + ( vol* ` ( z \ y ) ) ) )
79 78 oveq1d 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( ( vol* ` z ) + ( vol* ` ( y \ A ) ) ) = ( ( ( vol* ` ( z i^i y ) ) + ( vol* ` ( z \ y ) ) ) + ( vol* ` ( y \ A ) ) ) )
80 40 recnd 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( vol* ` ( z i^i y ) ) e. CC )
81 43 recnd 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( vol* ` ( z \ y ) ) e. CC )
82 32 recnd 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( vol* ` ( y \ A ) ) e. CC )
83 80 81 82 addassd 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( ( ( vol* ` ( z i^i y ) ) + ( vol* ` ( z \ y ) ) ) + ( vol* ` ( y \ A ) ) ) = ( ( vol* ` ( z i^i y ) ) + ( ( vol* ` ( z \ y ) ) + ( vol* ` ( y \ A ) ) ) ) )
84 79 83 eqtrd 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( ( vol* ` z ) + ( vol* ` ( y \ A ) ) ) = ( ( vol* ` ( z i^i y ) ) + ( ( vol* ` ( z \ y ) ) + ( vol* ` ( y \ A ) ) ) ) )
85 75 84 breqtrrd 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( ( vol* ` ( z i^i A ) ) + ( vol* ` ( z \ A ) ) ) <_ ( ( vol* ` z ) + ( vol* ` ( y \ A ) ) ) )
86 difss 
 |-  ( y \ A ) C_ y
87 ovolss 
 |-  ( ( ( y \ A ) C_ y /\ y C_ RR ) -> ( vol* ` ( y \ A ) ) <_ ( vol* ` y ) )
88 86 25 87 sylancr 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( vol* ` ( y \ A ) ) <_ ( vol* ` y ) )
89 32 30 27 88 28 letrd 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( vol* ` ( y \ A ) ) <_ x )
90 32 27 23 89 leadd2dd 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( ( vol* ` z ) + ( vol* ` ( y \ A ) ) ) <_ ( ( vol* ` z ) + x ) )
91 22 33 34 85 90 letrd 
 |-  ( ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) /\ ( y e. dom vol /\ ( A C_ y /\ ( vol* ` y ) <_ x ) ) ) -> ( ( vol* ` ( z i^i A ) ) + ( vol* ` ( z \ A ) ) ) <_ ( ( vol* ` z ) + x ) )
92 91 rexlimdvaa 
 |-  ( ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) /\ x e. RR+ ) -> ( E. y e. dom vol ( A C_ y /\ ( vol* ` y ) <_ x ) -> ( ( vol* ` ( z i^i A ) ) + ( vol* ` ( z \ A ) ) ) <_ ( ( vol* ` z ) + x ) ) )
93 92 ralimdva 
 |-  ( ( z e. ~P RR /\ ( vol* ` z ) e. RR ) -> ( A. x e. RR+ E. y e. dom vol ( A C_ y /\ ( vol* ` y ) <_ x ) -> A. x e. RR+ ( ( vol* ` ( z i^i A ) ) + ( vol* ` ( z \ A ) ) ) <_ ( ( vol* ` z ) + x ) ) )
94 93 impcom 
 |-  ( ( A. x e. RR+ E. y e. dom vol ( A C_ y /\ ( vol* ` y ) <_ x ) /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) -> A. x e. RR+ ( ( vol* ` ( z i^i A ) ) + ( vol* ` ( z \ A ) ) ) <_ ( ( vol* ` z ) + x ) )
95 21 adantl 
 |-  ( ( A. x e. RR+ E. y e. dom vol ( A C_ y /\ ( vol* ` y ) <_ x ) /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) -> ( ( vol* ` ( z i^i A ) ) + ( vol* ` ( z \ A ) ) ) e. RR )
96 95 rexrd 
 |-  ( ( A. x e. RR+ E. y e. dom vol ( A C_ y /\ ( vol* ` y ) <_ x ) /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) -> ( ( vol* ` ( z i^i A ) ) + ( vol* ` ( z \ A ) ) ) e. RR* )
97 simprr 
 |-  ( ( A. x e. RR+ E. y e. dom vol ( A C_ y /\ ( vol* ` y ) <_ x ) /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) -> ( vol* ` z ) e. RR )
98 xralrple 
 |-  ( ( ( ( vol* ` ( z i^i A ) ) + ( vol* ` ( z \ A ) ) ) e. RR* /\ ( vol* ` z ) e. RR ) -> ( ( ( vol* ` ( z i^i A ) ) + ( vol* ` ( z \ A ) ) ) <_ ( vol* ` z ) <-> A. x e. RR+ ( ( vol* ` ( z i^i A ) ) + ( vol* ` ( z \ A ) ) ) <_ ( ( vol* ` z ) + x ) ) )
99 96 97 98 syl2anc 
 |-  ( ( A. x e. RR+ E. y e. dom vol ( A C_ y /\ ( vol* ` y ) <_ x ) /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) -> ( ( ( vol* ` ( z i^i A ) ) + ( vol* ` ( z \ A ) ) ) <_ ( vol* ` z ) <-> A. x e. RR+ ( ( vol* ` ( z i^i A ) ) + ( vol* ` ( z \ A ) ) ) <_ ( ( vol* ` z ) + x ) ) )
100 94 99 mpbird 
 |-  ( ( A. x e. RR+ E. y e. dom vol ( A C_ y /\ ( vol* ` y ) <_ x ) /\ ( z e. ~P RR /\ ( vol* ` z ) e. RR ) ) -> ( ( vol* ` ( z i^i A ) ) + ( vol* ` ( z \ A ) ) ) <_ ( vol* ` z ) )
101 100 expr 
 |-  ( ( A. x e. RR+ E. y e. dom vol ( A C_ y /\ ( vol* ` y ) <_ x ) /\ z e. ~P RR ) -> ( ( vol* ` z ) e. RR -> ( ( vol* ` ( z i^i A ) ) + ( vol* ` ( z \ A ) ) ) <_ ( vol* ` z ) ) )
102 101 ralrimiva 
 |-  ( A. x e. RR+ E. y e. dom vol ( A C_ y /\ ( vol* ` y ) <_ x ) -> A. z e. ~P RR ( ( vol* ` z ) e. RR -> ( ( vol* ` ( z i^i A ) ) + ( vol* ` ( z \ A ) ) ) <_ ( vol* ` z ) ) )
103 ismbl2 
 |-  ( A e. dom vol <-> ( A C_ RR /\ A. z e. ~P RR ( ( vol* ` z ) e. RR -> ( ( vol* ` ( z i^i A ) ) + ( vol* ` ( z \ A ) ) ) <_ ( vol* ` z ) ) ) )
104 11 102 103 sylanbrc 
 |-  ( A. x e. RR+ E. y e. dom vol ( A C_ y /\ ( vol* ` y ) <_ x ) -> A e. dom vol )