# 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$