Metamath Proof Explorer


Theorem volsup2

Description: The volume of A is the supremum of the sequence vol*( A i^i ( -u n , n ) ) of volumes of bounded sets. (Contributed by Mario Carneiro, 30-Aug-2014)

Ref Expression
Assertion volsup2 A dom vol B B < vol A n B < vol A n n

Proof

Step Hyp Ref Expression
1 simp3 A dom vol B B < vol A B < vol A
2 rexr B B *
3 2 3ad2ant2 A dom vol B B < vol A B *
4 iccssxr 0 +∞ *
5 volf vol : dom vol 0 +∞
6 5 ffvelrni A dom vol vol A 0 +∞
7 4 6 sseldi A dom vol vol A *
8 7 3ad2ant1 A dom vol B B < vol A vol A *
9 xrltnle B * vol A * B < vol A ¬ vol A B
10 3 8 9 syl2anc A dom vol B B < vol A B < vol A ¬ vol A B
11 1 10 mpbid A dom vol B B < vol A ¬ vol A B
12 negeq m = n m = n
13 id m = n m = n
14 12 13 oveq12d m = n m m = n n
15 14 ineq2d m = n A m m = A n n
16 eqid m A m m = m A m m
17 ovex n n V
18 17 inex2 A n n V
19 15 16 18 fvmpt n m A m m n = A n n
20 19 iuneq2i n m A m m n = n A n n
21 iunin2 n A n n = A n n n
22 20 21 eqtri n m A m m n = A n n n
23 simpl1 A dom vol B B < vol A n A dom vol
24 nnre n n
25 24 adantl A dom vol B B < vol A n n
26 25 renegcld A dom vol B B < vol A n n
27 iccmbl n n n n dom vol
28 26 25 27 syl2anc A dom vol B B < vol A n n n dom vol
29 inmbl A dom vol n n dom vol A n n dom vol
30 23 28 29 syl2anc A dom vol B B < vol A n A n n dom vol
31 15 cbvmptv m A m m = n A n n
32 30 31 fmptd A dom vol B B < vol A m A m m : dom vol
33 32 ffnd A dom vol B B < vol A m A m m Fn
34 fniunfv m A m m Fn n m A m m n = ran m A m m
35 33 34 syl A dom vol B B < vol A n m A m m n = ran m A m m
36 mblss A dom vol A
37 36 3ad2ant1 A dom vol B B < vol A A
38 37 sselda A dom vol B B < vol A x A x
39 recn x x
40 39 abscld x x
41 arch x n x < n
42 40 41 syl x n x < n
43 ltle x n x < n x n
44 40 24 43 syl2an x n x < n x n
45 id x n x x n x n x x n
46 45 3expib x n x x n x n x x n
47 46 adantr x n n x x n x n x x n
48 absle x n x n n x x n
49 24 48 sylan2 x n x n n x x n
50 24 adantl x n n
51 50 renegcld x n n
52 elicc2 n n x n n x n x x n
53 51 50 52 syl2anc x n x n n x n x x n
54 47 49 53 3imtr4d x n x n x n n
55 44 54 syld x n x < n x n n
56 55 reximdva x n x < n n x n n
57 42 56 mpd x n x n n
58 38 57 syl A dom vol B B < vol A x A n x n n
59 58 ex A dom vol B B < vol A x A n x n n
60 eliun x n n n n x n n
61 59 60 syl6ibr A dom vol B B < vol A x A x n n n
62 61 ssrdv A dom vol B B < vol A A n n n
63 df-ss A n n n A n n n = A
64 62 63 sylib A dom vol B B < vol A A n n n = A
65 22 35 64 3eqtr3a A dom vol B B < vol A ran m A m m = A
66 65 fveq2d A dom vol B B < vol A vol ran m A m m = vol A
67 peano2re n n + 1
68 25 67 syl A dom vol B B < vol A n n + 1
69 68 renegcld A dom vol B B < vol A n n + 1
70 25 lep1d A dom vol B B < vol A n n n + 1
71 25 68 lenegd A dom vol B B < vol A n n n + 1 n + 1 n
72 70 71 mpbid A dom vol B B < vol A n n + 1 n
73 iccss n + 1 n + 1 n + 1 n n n + 1 n n n + 1 n + 1
74 69 68 72 70 73 syl22anc A dom vol B B < vol A n n n n + 1 n + 1
75 sslin n n n + 1 n + 1 A n n A n + 1 n + 1
76 74 75 syl A dom vol B B < vol A n A n n A n + 1 n + 1
77 19 adantl A dom vol B B < vol A n m A m m n = A n n
78 peano2nn n n + 1
79 78 adantl A dom vol B B < vol A n n + 1
80 negeq m = n + 1 m = n + 1
81 id m = n + 1 m = n + 1
82 80 81 oveq12d m = n + 1 m m = n + 1 n + 1
83 82 ineq2d m = n + 1 A m m = A n + 1 n + 1
84 ovex n + 1 n + 1 V
85 84 inex2 A n + 1 n + 1 V
86 83 16 85 fvmpt n + 1 m A m m n + 1 = A n + 1 n + 1
87 79 86 syl A dom vol B B < vol A n m A m m n + 1 = A n + 1 n + 1
88 76 77 87 3sstr4d A dom vol B B < vol A n m A m m n m A m m n + 1
89 88 ralrimiva A dom vol B B < vol A n m A m m n m A m m n + 1
90 volsup m A m m : dom vol n m A m m n m A m m n + 1 vol ran m A m m = sup vol ran m A m m * <
91 32 89 90 syl2anc A dom vol B B < vol A vol ran m A m m = sup vol ran m A m m * <
92 66 91 eqtr3d A dom vol B B < vol A vol A = sup vol ran m A m m * <
93 92 breq1d A dom vol B B < vol A vol A B sup vol ran m A m m * < B
94 imassrn vol ran m A m m ran vol
95 frn vol : dom vol 0 +∞ ran vol 0 +∞
96 5 95 ax-mp ran vol 0 +∞
97 96 4 sstri ran vol *
98 94 97 sstri vol ran m A m m *
99 supxrleub vol ran m A m m * B * sup vol ran m A m m * < B n vol ran m A m m n B
100 98 3 99 sylancr A dom vol B B < vol A sup vol ran m A m m * < B n vol ran m A m m n B
101 ffn vol : dom vol 0 +∞ vol Fn dom vol
102 5 101 ax-mp vol Fn dom vol
103 32 frnd A dom vol B B < vol A ran m A m m dom vol
104 breq1 n = vol z n B vol z B
105 104 ralima vol Fn dom vol ran m A m m dom vol n vol ran m A m m n B z ran m A m m vol z B
106 102 103 105 sylancr A dom vol B B < vol A n vol ran m A m m n B z ran m A m m vol z B
107 fveq2 z = m A m m n vol z = vol m A m m n
108 107 breq1d z = m A m m n vol z B vol m A m m n B
109 108 ralrn m A m m Fn z ran m A m m vol z B n vol m A m m n B
110 33 109 syl A dom vol B B < vol A z ran m A m m vol z B n vol m A m m n B
111 19 fveq2d n vol m A m m n = vol A n n
112 111 breq1d n vol m A m m n B vol A n n B
113 112 ralbiia n vol m A m m n B n vol A n n B
114 110 113 bitrdi A dom vol B B < vol A z ran m A m m vol z B n vol A n n B
115 106 114 bitrd A dom vol B B < vol A n vol ran m A m m n B n vol A n n B
116 93 100 115 3bitrd A dom vol B B < vol A vol A B n vol A n n B
117 11 116 mtbid A dom vol B B < vol A ¬ n vol A n n B
118 rexnal n ¬ vol A n n B ¬ n vol A n n B
119 117 118 sylibr A dom vol B B < vol A n ¬ vol A n n B
120 3 adantr A dom vol B B < vol A n B *
121 5 ffvelrni A n n dom vol vol A n n 0 +∞
122 4 121 sseldi A n n dom vol vol A n n *
123 30 122 syl A dom vol B B < vol A n vol A n n *
124 xrltnle B * vol A n n * B < vol A n n ¬ vol A n n B
125 120 123 124 syl2anc A dom vol B B < vol A n B < vol A n n ¬ vol A n n B
126 125 rexbidva A dom vol B B < vol A n B < vol A n n n ¬ vol A n n B
127 119 126 mpbird A dom vol B B < vol A n B < vol A n n