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 \mathbb{N}\right)\to {vol}^{*}\left(A\right)=0$$

Proof

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