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

Proof

Step Hyp Ref Expression
1 bren Aff:1-1 ontoA
2 simpll Af:1-1 ontoAxA
3 f1of f:1-1 ontoAf:A
4 3 adantl Af:1-1 ontoAf:A
5 4 ffvelrnda Af:1-1 ontoAxfxA
6 2 5 sseldd Af:1-1 ontoAxfx
7 6 leidd Af:1-1 ontoAxfxfx
8 df-br fxfxfxfx
9 7 8 sylib Af:1-1 ontoAxfxfx
10 6 6 opelxpd Af:1-1 ontoAxfxfx2
11 9 10 elind Af:1-1 ontoAxfxfx2
12 df-ov fxIfx=Ifxfx
13 opex fxfxV
14 fvi fxfxVIfxfx=fxfx
15 13 14 ax-mp Ifxfx=fxfx
16 12 15 eqtri fxIfx=fxfx
17 16 mpteq2i xfxIfx=xfxfx
18 11 17 fmptd Af:1-1 ontoAxfxIfx:2
19 nnex V
20 19 a1i Af:1-1 ontoAV
21 6 recnd Af:1-1 ontoAxfx
22 4 feqmptd Af:1-1 ontoAf=xfx
23 20 21 21 22 22 offval2 Af:1-1 ontoAfIff=xfxIfx
24 23 feq1d Af:1-1 ontoAfIff:2xfxIfx:2
25 18 24 mpbird Af:1-1 ontoAfIff:2
26 f1ofo f:1-1 ontoAf:ontoA
27 26 adantl Af:1-1 ontoAf:ontoA
28 forn f:ontoAranf=A
29 27 28 syl Af:1-1 ontoAranf=A
30 29 eleq2d Af:1-1 ontoAyranfyA
31 f1ofn f:1-1 ontoAfFn
32 31 adantl Af:1-1 ontoAfFn
33 fvelrnb fFnyranfxfx=y
34 32 33 syl Af:1-1 ontoAyranfxfx=y
35 30 34 bitr3d Af:1-1 ontoAyAxfx=y
36 23 17 eqtrdi Af:1-1 ontoAfIff=xfxfx
37 36 fveq1d Af:1-1 ontoAfIffx=xfxfxx
38 eqid xfxfx=xfxfx
39 38 fvmpt2 xfxfxVxfxfxx=fxfx
40 13 39 mpan2 xxfxfxx=fxfx
41 37 40 sylan9eq Af:1-1 ontoAxfIffx=fxfx
42 41 fveq2d Af:1-1 ontoAx1stfIffx=1stfxfx
43 fvex fxV
44 43 43 op1st 1stfxfx=fx
45 42 44 eqtrdi Af:1-1 ontoAx1stfIffx=fx
46 45 7 eqbrtrd Af:1-1 ontoAx1stfIffxfx
47 41 fveq2d Af:1-1 ontoAx2ndfIffx=2ndfxfx
48 43 43 op2nd 2ndfxfx=fx
49 47 48 eqtrdi Af:1-1 ontoAx2ndfIffx=fx
50 7 49 breqtrrd Af:1-1 ontoAxfx2ndfIffx
51 46 50 jca Af:1-1 ontoAx1stfIffxfxfx2ndfIffx
52 breq2 fx=y1stfIffxfx1stfIffxy
53 breq1 fx=yfx2ndfIffxy2ndfIffx
54 52 53 anbi12d fx=y1stfIffxfxfx2ndfIffx1stfIffxyy2ndfIffx
55 51 54 syl5ibcom Af:1-1 ontoAxfx=y1stfIffxyy2ndfIffx
56 55 reximdva Af:1-1 ontoAxfx=yx1stfIffxyy2ndfIffx
57 35 56 sylbid Af:1-1 ontoAyAx1stfIffxyy2ndfIffx
58 57 ralrimiv Af:1-1 ontoAyAx1stfIffxyy2ndfIffx
59 ovolficc AfIff:2Aran.fIffyAx1stfIffxyy2ndfIffx
60 25 59 syldan Af:1-1 ontoAAran.fIffyAx1stfIffxyy2ndfIffx
61 58 60 mpbird Af:1-1 ontoAAran.fIff
62 eqid seq1+absfIff=seq1+absfIff
63 62 ovollb2 fIff:2Aran.fIffvol*Asupranseq1+absfIff*<
64 25 61 63 syl2anc Af:1-1 ontoAvol*Asupranseq1+absfIff*<
65 21 21 opelxpd Af:1-1 ontoAxfxfx×
66 absf abs:
67 subf :×
68 fco abs::×abs:×
69 66 67 68 mp2an abs:×
70 69 a1i Af:1-1 ontoAabs:×
71 70 feqmptd Af:1-1 ontoAabs=y×absy
72 fveq2 y=fxfxabsy=absfxfx
73 df-ov fxabsfx=absfxfx
74 72 73 eqtr4di y=fxfxabsy=fxabsfx
75 65 36 71 74 fmptco Af:1-1 ontoAabsfIff=xfxabsfx
76 cnmet absMet
77 met0 absMetfxfxabsfx=0
78 76 21 77 sylancr Af:1-1 ontoAxfxabsfx=0
79 78 mpteq2dva Af:1-1 ontoAxfxabsfx=x0
80 75 79 eqtrd Af:1-1 ontoAabsfIff=x0
81 fconstmpt ×0=x0
82 80 81 eqtr4di Af:1-1 ontoAabsfIff=×0
83 82 seqeq3d Af:1-1 ontoAseq1+absfIff=seq1+×0
84 1z 1
85 nnuz =1
86 85 ser0f 1seq1+×0=×0
87 84 86 ax-mp seq1+×0=×0
88 83 87 eqtrdi Af:1-1 ontoAseq1+absfIff=×0
89 88 rneqd Af:1-1 ontoAranseq1+absfIff=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 Af:1-1 ontoAranseq1+absfIff=0
95 94 supeq1d Af:1-1 ontoAsupranseq1+absfIff*<=sup0*<
96 xrltso <Or*
97 0xr 0*
98 supsn <Or*0*sup0*<=0
99 96 97 98 mp2an sup0*<=0
100 95 99 eqtrdi Af:1-1 ontoAsupranseq1+absfIff*<=0
101 64 100 breqtrd Af:1-1 ontoAvol*A0
102 ovolge0 A0vol*A
103 102 adantr Af:1-1 ontoA0vol*A
104 ovolcl Avol*A*
105 104 adantr Af:1-1 ontoAvol*A*
106 xrletri3 vol*A*0*vol*A=0vol*A00vol*A
107 105 97 106 sylancl Af:1-1 ontoAvol*A=0vol*A00vol*A
108 101 103 107 mpbir2and Af:1-1 ontoAvol*A=0
109 108 ex Af:1-1 ontoAvol*A=0
110 109 exlimdv Aff:1-1 ontoAvol*A=0
111 1 110 syl5bi AAvol*A=0
112 ensym AA
113 111 112 impel AAvol*A=0