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 A vol * A = 0

Proof

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