Metamath Proof Explorer

Theorem ovolctb

Description: The volume of a denumerable set is 0. (Contributed by Mario Carneiro, 17-Mar-2014) (Proof shortened by Mario Carneiro, 25-Mar-2015)

Ref Expression
Assertion ovolctb 
|- ( ( A C_ RR /\ A ~~ NN ) -> ( vol* ` A ) = 0 )

Proof

Step Hyp Ref Expression
1 bren 
 |-  ( NN ~~ A <-> E. f f : NN -1-1-onto-> A )
2 simpll 
 |-  ( ( ( A C_ RR /\ f : NN -1-1-onto-> A ) /\ x e. NN ) -> A C_ RR )
3 f1of 
 |-  ( f : NN -1-1-onto-> A -> f : NN --> A )
4 3 adantl 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> f : NN --> A )
5 4 ffvelrnda 
 |-  ( ( ( A C_ RR /\ f : NN -1-1-onto-> A ) /\ x e. NN ) -> ( f ` x ) e. A )
6 2 5 sseldd 
 |-  ( ( ( A C_ RR /\ f : NN -1-1-onto-> A ) /\ x e. NN ) -> ( f ` x ) e. RR )
7 6 leidd 
 |-  ( ( ( A C_ RR /\ f : NN -1-1-onto-> A ) /\ x e. NN ) -> ( f ` x ) <_ ( f ` x ) )
8 df-br 
 |-  ( ( f ` x ) <_ ( f ` x ) <-> <. ( f ` x ) , ( f ` x ) >. e. <_ )
9 7 8 sylib 
 |-  ( ( ( A C_ RR /\ f : NN -1-1-onto-> A ) /\ x e. NN ) -> <. ( f ` x ) , ( f ` x ) >. e. <_ )
10 6 6 opelxpd 
 |-  ( ( ( A C_ RR /\ f : NN -1-1-onto-> A ) /\ x e. NN ) -> <. ( f ` x ) , ( f ` x ) >. e. ( RR X. RR ) )
11 9 10 elind 
 |-  ( ( ( A C_ RR /\ f : NN -1-1-onto-> A ) /\ x e. NN ) -> <. ( f ` x ) , ( f ` x ) >. e. ( <_ i^i ( RR X. RR ) ) )
12 df-ov 
 |-  ( ( f ` x ) _I ( f ` x ) ) = ( _I ` <. ( f ` x ) , ( f ` x ) >. )
13 opex 
 |-  <. ( f ` x ) , ( f ` x ) >. e. _V
14 fvi 
 |-  ( <. ( f ` x ) , ( f ` x ) >. e. _V -> ( _I ` <. ( f ` x ) , ( f ` x ) >. ) = <. ( f ` x ) , ( f ` x ) >. )
15 13 14 ax-mp 
 |-  ( _I ` <. ( f ` x ) , ( f ` x ) >. ) = <. ( f ` x ) , ( f ` x ) >.
16 12 15 eqtri 
 |-  ( ( f ` x ) _I ( f ` x ) ) = <. ( f ` x ) , ( f ` x ) >.
17 16 mpteq2i 
 |-  ( x e. NN |-> ( ( f ` x ) _I ( f ` x ) ) ) = ( x e. NN |-> <. ( f ` x ) , ( f ` x ) >. )
18 11 17 fmptd 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ( x e. NN |-> ( ( f ` x ) _I ( f ` x ) ) ) : NN --> ( <_ i^i ( RR X. RR ) ) )
19 nnex 
 |-  NN e. _V
20 19 a1i 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> NN e. _V )
21 6 recnd 
 |-  ( ( ( A C_ RR /\ f : NN -1-1-onto-> A ) /\ x e. NN ) -> ( f ` x ) e. CC )
22 4 feqmptd 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> f = ( x e. NN |-> ( f ` x ) ) )
23 20 21 21 22 22 offval2 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ( f oF _I f ) = ( x e. NN |-> ( ( f ` x ) _I ( f ` x ) ) ) )
24 23 feq1d 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ( ( f oF _I f ) : NN --> ( <_ i^i ( RR X. RR ) ) <-> ( x e. NN |-> ( ( f ` x ) _I ( f ` x ) ) ) : NN --> ( <_ i^i ( RR X. RR ) ) ) )
25 18 24 mpbird 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ( f oF _I f ) : NN --> ( <_ i^i ( RR X. RR ) ) )
26 f1ofo 
 |-  ( f : NN -1-1-onto-> A -> f : NN -onto-> A )
27 26 adantl 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> f : NN -onto-> A )
28 forn 
 |-  ( f : NN -onto-> A -> ran f = A )
29 27 28 syl 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ran f = A )
30 29 eleq2d 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ( y e. ran f <-> y e. A ) )
31 f1ofn 
 |-  ( f : NN -1-1-onto-> A -> f Fn NN )
32 31 adantl 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> f Fn NN )
33 fvelrnb 
 |-  ( f Fn NN -> ( y e. ran f <-> E. x e. NN ( f ` x ) = y ) )
34 32 33 syl 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ( y e. ran f <-> E. x e. NN ( f ` x ) = y ) )
35 30 34 bitr3d 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ( y e. A <-> E. x e. NN ( f ` x ) = y ) )
36 23 17 eqtrdi 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ( f oF _I f ) = ( x e. NN |-> <. ( f ` x ) , ( f ` x ) >. ) )
37 36 fveq1d 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ( ( f oF _I f ) ` x ) = ( ( x e. NN |-> <. ( f ` x ) , ( f ` x ) >. ) ` x ) )
38 eqid 
 |-  ( x e. NN |-> <. ( f ` x ) , ( f ` x ) >. ) = ( x e. NN |-> <. ( f ` x ) , ( f ` x ) >. )
39 38 fvmpt2 
 |-  ( ( x e. NN /\ <. ( f ` x ) , ( f ` x ) >. e. _V ) -> ( ( x e. NN |-> <. ( f ` x ) , ( f ` x ) >. ) ` x ) = <. ( f ` x ) , ( f ` x ) >. )
40 13 39 mpan2 
 |-  ( x e. NN -> ( ( x e. NN |-> <. ( f ` x ) , ( f ` x ) >. ) ` x ) = <. ( f ` x ) , ( f ` x ) >. )
41 37 40 sylan9eq 
 |-  ( ( ( A C_ RR /\ f : NN -1-1-onto-> A ) /\ x e. NN ) -> ( ( f oF _I f ) ` x ) = <. ( f ` x ) , ( f ` x ) >. )
42 41 fveq2d 
 |-  ( ( ( A C_ RR /\ f : NN -1-1-onto-> A ) /\ x e. NN ) -> ( 1st ` ( ( f oF _I f ) ` x ) ) = ( 1st ` <. ( f ` x ) , ( f ` x ) >. ) )
43 fvex 
 |-  ( f ` x ) e. _V
44 43 43 op1st 
 |-  ( 1st ` <. ( f ` x ) , ( f ` x ) >. ) = ( f ` x )
45 42 44 eqtrdi 
 |-  ( ( ( A C_ RR /\ f : NN -1-1-onto-> A ) /\ x e. NN ) -> ( 1st ` ( ( f oF _I f ) ` x ) ) = ( f ` x ) )
46 45 7 eqbrtrd 
 |-  ( ( ( A C_ RR /\ f : NN -1-1-onto-> A ) /\ x e. NN ) -> ( 1st ` ( ( f oF _I f ) ` x ) ) <_ ( f ` x ) )
47 41 fveq2d 
 |-  ( ( ( A C_ RR /\ f : NN -1-1-onto-> A ) /\ x e. NN ) -> ( 2nd ` ( ( f oF _I f ) ` x ) ) = ( 2nd ` <. ( f ` x ) , ( f ` x ) >. ) )
48 43 43 op2nd 
 |-  ( 2nd ` <. ( f ` x ) , ( f ` x ) >. ) = ( f ` x )
49 47 48 eqtrdi 
 |-  ( ( ( A C_ RR /\ f : NN -1-1-onto-> A ) /\ x e. NN ) -> ( 2nd ` ( ( f oF _I f ) ` x ) ) = ( f ` x ) )
50 7 49 breqtrrd 
 |-  ( ( ( A C_ RR /\ f : NN -1-1-onto-> A ) /\ x e. NN ) -> ( f ` x ) <_ ( 2nd ` ( ( f oF _I f ) ` x ) ) )
51 46 50 jca 
 |-  ( ( ( A C_ RR /\ f : NN -1-1-onto-> A ) /\ x e. NN ) -> ( ( 1st ` ( ( f oF _I f ) ` x ) ) <_ ( f ` x ) /\ ( f ` x ) <_ ( 2nd ` ( ( f oF _I f ) ` x ) ) ) )
52 breq2 
 |-  ( ( f ` x ) = y -> ( ( 1st ` ( ( f oF _I f ) ` x ) ) <_ ( f ` x ) <-> ( 1st ` ( ( f oF _I f ) ` x ) ) <_ y ) )
53 breq1 
 |-  ( ( f ` x ) = y -> ( ( f ` x ) <_ ( 2nd ` ( ( f oF _I f ) ` x ) ) <-> y <_ ( 2nd ` ( ( f oF _I f ) ` x ) ) ) )
54 52 53 anbi12d 
 |-  ( ( f ` x ) = y -> ( ( ( 1st ` ( ( f oF _I f ) ` x ) ) <_ ( f ` x ) /\ ( f ` x ) <_ ( 2nd ` ( ( f oF _I f ) ` x ) ) ) <-> ( ( 1st ` ( ( f oF _I f ) ` x ) ) <_ y /\ y <_ ( 2nd ` ( ( f oF _I f ) ` x ) ) ) ) )
55 51 54 syl5ibcom 
 |-  ( ( ( A C_ RR /\ f : NN -1-1-onto-> A ) /\ x e. NN ) -> ( ( f ` x ) = y -> ( ( 1st ` ( ( f oF _I f ) ` x ) ) <_ y /\ y <_ ( 2nd ` ( ( f oF _I f ) ` x ) ) ) ) )
56 55 reximdva 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ( E. x e. NN ( f ` x ) = y -> E. x e. NN ( ( 1st ` ( ( f oF _I f ) ` x ) ) <_ y /\ y <_ ( 2nd ` ( ( f oF _I f ) ` x ) ) ) ) )
57 35 56 sylbid 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ( y e. A -> E. x e. NN ( ( 1st ` ( ( f oF _I f ) ` x ) ) <_ y /\ y <_ ( 2nd ` ( ( f oF _I f ) ` x ) ) ) ) )
58 57 ralrimiv 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> A. y e. A E. x e. NN ( ( 1st ` ( ( f oF _I f ) ` x ) ) <_ y /\ y <_ ( 2nd ` ( ( f oF _I f ) ` x ) ) ) )
59 ovolficc 
 |-  ( ( A C_ RR /\ ( f oF _I f ) : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( A C_ U. ran ( [,] o. ( f oF _I f ) ) <-> A. y e. A E. x e. NN ( ( 1st ` ( ( f oF _I f ) ` x ) ) <_ y /\ y <_ ( 2nd ` ( ( f oF _I f ) ` x ) ) ) ) )
60 25 59 syldan 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ( A C_ U. ran ( [,] o. ( f oF _I f ) ) <-> A. y e. A E. x e. NN ( ( 1st ` ( ( f oF _I f ) ` x ) ) <_ y /\ y <_ ( 2nd ` ( ( f oF _I f ) ` x ) ) ) ) )
61 58 60 mpbird 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> A C_ U. ran ( [,] o. ( f oF _I f ) ) )
62 eqid 
 |-  seq 1 ( + , ( ( abs o. - ) o. ( f oF _I f ) ) ) = seq 1 ( + , ( ( abs o. - ) o. ( f oF _I f ) ) )
63 62 ovollb2 
 |-  ( ( ( f oF _I f ) : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( [,] o. ( f oF _I f ) ) ) -> ( vol* ` A ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( f oF _I f ) ) ) , RR* , < ) )
64 25 61 63 syl2anc 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ( vol* ` A ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( f oF _I f ) ) ) , RR* , < ) )
65 21 21 opelxpd 
 |-  ( ( ( A C_ RR /\ f : NN -1-1-onto-> A ) /\ x e. NN ) -> <. ( f ` x ) , ( f ` x ) >. e. ( CC X. CC ) )
66 absf 
 |-  abs : CC --> RR
67 subf 
 |-  - : ( CC X. CC ) --> CC
68 fco 
 |-  ( ( abs : CC --> RR /\ - : ( CC X. CC ) --> CC ) -> ( abs o. - ) : ( CC X. CC ) --> RR )
69 66 67 68 mp2an 
 |-  ( abs o. - ) : ( CC X. CC ) --> RR
70 69 a1i 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ( abs o. - ) : ( CC X. CC ) --> RR )
71 70 feqmptd 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ( abs o. - ) = ( y e. ( CC X. CC ) |-> ( ( abs o. - ) ` y ) ) )
72 fveq2 
 |-  ( y = <. ( f ` x ) , ( f ` x ) >. -> ( ( abs o. - ) ` y ) = ( ( abs o. - ) ` <. ( f ` x ) , ( f ` x ) >. ) )
73 df-ov 
 |-  ( ( f ` x ) ( abs o. - ) ( f ` x ) ) = ( ( abs o. - ) ` <. ( f ` x ) , ( f ` x ) >. )
74 72 73 eqtr4di 
 |-  ( y = <. ( f ` x ) , ( f ` x ) >. -> ( ( abs o. - ) ` y ) = ( ( f ` x ) ( abs o. - ) ( f ` x ) ) )
75 65 36 71 74 fmptco 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ( ( abs o. - ) o. ( f oF _I f ) ) = ( x e. NN |-> ( ( f ` x ) ( abs o. - ) ( f ` x ) ) ) )
76 cnmet 
 |-  ( abs o. - ) e. ( Met ` CC )
77 met0 
 |-  ( ( ( abs o. - ) e. ( Met ` CC ) /\ ( f ` x ) e. CC ) -> ( ( f ` x ) ( abs o. - ) ( f ` x ) ) = 0 )
78 76 21 77 sylancr 
 |-  ( ( ( A C_ RR /\ f : NN -1-1-onto-> A ) /\ x e. NN ) -> ( ( f ` x ) ( abs o. - ) ( f ` x ) ) = 0 )
79 78 mpteq2dva 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ( x e. NN |-> ( ( f ` x ) ( abs o. - ) ( f ` x ) ) ) = ( x e. NN |-> 0 ) )
80 75 79 eqtrd 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ( ( abs o. - ) o. ( f oF _I f ) ) = ( x e. NN |-> 0 ) )
81 fconstmpt 
 |-  ( NN X. { 0 } ) = ( x e. NN |-> 0 )
82 80 81 eqtr4di 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ( ( abs o. - ) o. ( f oF _I f ) ) = ( NN X. { 0 } ) )
83 82 seqeq3d 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> seq 1 ( + , ( ( abs o. - ) o. ( f oF _I f ) ) ) = seq 1 ( + , ( NN X. { 0 } ) ) )
84 1z 
 |-  1 e. ZZ
85 nnuz 
 |-  NN = ( ZZ>= ` 1 )
86 85 ser0f 
 |-  ( 1 e. ZZ -> seq 1 ( + , ( NN X. { 0 } ) ) = ( NN X. { 0 } ) )
87 84 86 ax-mp 
 |-  seq 1 ( + , ( NN X. { 0 } ) ) = ( NN X. { 0 } )
88 83 87 eqtrdi 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> seq 1 ( + , ( ( abs o. - ) o. ( f oF _I f ) ) ) = ( NN X. { 0 } ) )
89 88 rneqd 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ran seq 1 ( + , ( ( abs o. - ) o. ( f oF _I f ) ) ) = ran ( NN X. { 0 } ) )
90 1nn 
 |-  1 e. NN
91 ne0i 
 |-  ( 1 e. NN -> NN =/= (/) )
92 rnxp 
 |-  ( NN =/= (/) -> ran ( NN X. { 0 } ) = { 0 } )
93 90 91 92 mp2b 
 |-  ran ( NN X. { 0 } ) = { 0 }
94 89 93 eqtrdi 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ran seq 1 ( + , ( ( abs o. - ) o. ( f oF _I f ) ) ) = { 0 } )
95 94 supeq1d 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( f oF _I f ) ) ) , RR* , < ) = sup ( { 0 } , RR* , < ) )
96 xrltso 
 |-  < Or RR*
97 0xr 
 |-  0 e. RR*
98 supsn 
 |-  ( ( < Or RR* /\ 0 e. RR* ) -> sup ( { 0 } , RR* , < ) = 0 )
99 96 97 98 mp2an 
 |-  sup ( { 0 } , RR* , < ) = 0
100 95 99 eqtrdi 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( f oF _I f ) ) ) , RR* , < ) = 0 )
101 64 100 breqtrd 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ( vol* ` A ) <_ 0 )
102 ovolge0 
 |-  ( A C_ RR -> 0 <_ ( vol* ` A ) )
103 102 adantr 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> 0 <_ ( vol* ` A ) )
104 ovolcl 
 |-  ( A C_ RR -> ( vol* ` A ) e. RR* )
105 104 adantr 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ( vol* ` A ) e. RR* )
106 xrletri3 
 |-  ( ( ( vol* ` A ) e. RR* /\ 0 e. RR* ) -> ( ( vol* ` A ) = 0 <-> ( ( vol* ` A ) <_ 0 /\ 0 <_ ( vol* ` A ) ) ) )
107 105 97 106 sylancl 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ( ( vol* ` A ) = 0 <-> ( ( vol* ` A ) <_ 0 /\ 0 <_ ( vol* ` A ) ) ) )
108 101 103 107 mpbir2and 
 |-  ( ( A C_ RR /\ f : NN -1-1-onto-> A ) -> ( vol* ` A ) = 0 )
109 108 ex 
 |-  ( A C_ RR -> ( f : NN -1-1-onto-> A -> ( vol* ` A ) = 0 ) )
110 109 exlimdv 
 |-  ( A C_ RR -> ( E. f f : NN -1-1-onto-> A -> ( vol* ` A ) = 0 ) )
111 1 110 syl5bi 
 |-  ( A C_ RR -> ( NN ~~ A -> ( vol* ` A ) = 0 ) )
112 ensym 
 |-  ( A ~~ NN -> NN ~~ A )
113 111 112 impel 
 |-  ( ( A C_ RR /\ A ~~ NN ) -> ( vol* ` A ) = 0 )