# Metamath Proof Explorer

## Theorem ovolctb2

Description: The volume of a countable set is 0. (Contributed by Mario Carneiro, 17-Mar-2014)

Ref Expression
Assertion ovolctb2 ${⊢}\left({A}\subseteq ℝ\wedge {A}\preccurlyeq ℕ\right)\to {vol}^{*}\left({A}\right)=0$

### Proof

Step Hyp Ref Expression
1 ssun1 ${⊢}{A}\subseteq {A}\cup ℕ$
2 simpl ${⊢}\left({A}\subseteq ℝ\wedge {A}\preccurlyeq ℕ\right)\to {A}\subseteq ℝ$
3 nnssre ${⊢}ℕ\subseteq ℝ$
4 unss ${⊢}\left({A}\subseteq ℝ\wedge ℕ\subseteq ℝ\right)↔{A}\cup ℕ\subseteq ℝ$
5 2 3 4 sylanblc ${⊢}\left({A}\subseteq ℝ\wedge {A}\preccurlyeq ℕ\right)\to {A}\cup ℕ\subseteq ℝ$
6 nnenom ${⊢}ℕ\approx \mathrm{\omega }$
7 domentr ${⊢}\left({A}\preccurlyeq ℕ\wedge ℕ\approx \mathrm{\omega }\right)\to {A}\preccurlyeq \mathrm{\omega }$
8 6 7 mpan2 ${⊢}{A}\preccurlyeq ℕ\to {A}\preccurlyeq \mathrm{\omega }$
9 8 adantl ${⊢}\left({A}\subseteq ℝ\wedge {A}\preccurlyeq ℕ\right)\to {A}\preccurlyeq \mathrm{\omega }$
10 nnct ${⊢}ℕ\preccurlyeq \mathrm{\omega }$
11 unctb ${⊢}\left({A}\preccurlyeq \mathrm{\omega }\wedge ℕ\preccurlyeq \mathrm{\omega }\right)\to \left({A}\cup ℕ\right)\preccurlyeq \mathrm{\omega }$
12 9 10 11 sylancl ${⊢}\left({A}\subseteq ℝ\wedge {A}\preccurlyeq ℕ\right)\to \left({A}\cup ℕ\right)\preccurlyeq \mathrm{\omega }$
13 6 ensymi ${⊢}\mathrm{\omega }\approx ℕ$
14 domentr ${⊢}\left(\left({A}\cup ℕ\right)\preccurlyeq \mathrm{\omega }\wedge \mathrm{\omega }\approx ℕ\right)\to \left({A}\cup ℕ\right)\preccurlyeq ℕ$
15 12 13 14 sylancl ${⊢}\left({A}\subseteq ℝ\wedge {A}\preccurlyeq ℕ\right)\to \left({A}\cup ℕ\right)\preccurlyeq ℕ$
16 reex ${⊢}ℝ\in \mathrm{V}$
17 16 ssex ${⊢}{A}\cup ℕ\subseteq ℝ\to {A}\cup ℕ\in \mathrm{V}$
18 5 17 syl ${⊢}\left({A}\subseteq ℝ\wedge {A}\preccurlyeq ℕ\right)\to {A}\cup ℕ\in \mathrm{V}$
19 ssun2 ${⊢}ℕ\subseteq {A}\cup ℕ$
20 ssdomg ${⊢}{A}\cup ℕ\in \mathrm{V}\to \left(ℕ\subseteq {A}\cup ℕ\to ℕ\preccurlyeq \left({A}\cup ℕ\right)\right)$
21 18 19 20 mpisyl ${⊢}\left({A}\subseteq ℝ\wedge {A}\preccurlyeq ℕ\right)\to ℕ\preccurlyeq \left({A}\cup ℕ\right)$
22 sbth ${⊢}\left(\left({A}\cup ℕ\right)\preccurlyeq ℕ\wedge ℕ\preccurlyeq \left({A}\cup ℕ\right)\right)\to \left({A}\cup ℕ\right)\approx ℕ$
23 15 21 22 syl2anc ${⊢}\left({A}\subseteq ℝ\wedge {A}\preccurlyeq ℕ\right)\to \left({A}\cup ℕ\right)\approx ℕ$
24 ovolctb ${⊢}\left({A}\cup ℕ\subseteq ℝ\wedge \left({A}\cup ℕ\right)\approx ℕ\right)\to {vol}^{*}\left({A}\cup ℕ\right)=0$
25 5 23 24 syl2anc ${⊢}\left({A}\subseteq ℝ\wedge {A}\preccurlyeq ℕ\right)\to {vol}^{*}\left({A}\cup ℕ\right)=0$
26 ovolssnul ${⊢}\left({A}\subseteq {A}\cup ℕ\wedge {A}\cup ℕ\subseteq ℝ\wedge {vol}^{*}\left({A}\cup ℕ\right)=0\right)\to {vol}^{*}\left({A}\right)=0$
27 1 5 25 26 mp3an2i ${⊢}\left({A}\subseteq ℝ\wedge {A}\preccurlyeq ℕ\right)\to {vol}^{*}\left({A}\right)=0$