Theorem ovolctb2

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

	Ref	Expression
Assertion	ovolctb2	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ ) → ( vol* ‘ 𝐴 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		ssun1	⊢ 𝐴 ⊆ ( 𝐴 ∪ ℕ )
2		simpl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ ) → 𝐴 ⊆ ℝ )
3		nnssre	⊢ ℕ ⊆ ℝ
4		unss	⊢ ( ( 𝐴 ⊆ ℝ ∧ ℕ ⊆ ℝ ) ↔ ( 𝐴 ∪ ℕ ) ⊆ ℝ )
5	2 3 4	sylanblc	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ ) → ( 𝐴 ∪ ℕ ) ⊆ ℝ )
6		nnenom	⊢ ℕ ≈ ω
7		domentr	⊢ ( ( 𝐴 ≼ ℕ ∧ ℕ ≈ ω ) → 𝐴 ≼ ω )
8	6 7	mpan2	⊢ ( 𝐴 ≼ ℕ → 𝐴 ≼ ω )
9	8	adantl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ ) → 𝐴 ≼ ω )
10		nnct	⊢ ℕ ≼ ω
11		unctb	⊢ ( ( 𝐴 ≼ ω ∧ ℕ ≼ ω ) → ( 𝐴 ∪ ℕ ) ≼ ω )
12	9 10 11	sylancl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ ) → ( 𝐴 ∪ ℕ ) ≼ ω )
13	6	ensymi	⊢ ω ≈ ℕ
14		domentr	⊢ ( ( ( 𝐴 ∪ ℕ ) ≼ ω ∧ ω ≈ ℕ ) → ( 𝐴 ∪ ℕ ) ≼ ℕ )
15	12 13 14	sylancl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ ) → ( 𝐴 ∪ ℕ ) ≼ ℕ )
16		reex	⊢ ℝ ∈ V
17	16	ssex	⊢ ( ( 𝐴 ∪ ℕ ) ⊆ ℝ → ( 𝐴 ∪ ℕ ) ∈ V )
18	5 17	syl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ ) → ( 𝐴 ∪ ℕ ) ∈ V )
19		ssun2	⊢ ℕ ⊆ ( 𝐴 ∪ ℕ )
20		ssdomg	⊢ ( ( 𝐴 ∪ ℕ ) ∈ V → ( ℕ ⊆ ( 𝐴 ∪ ℕ ) → ℕ ≼ ( 𝐴 ∪ ℕ ) ) )
21	18 19 20	mpisyl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ ) → ℕ ≼ ( 𝐴 ∪ ℕ ) )
22		sbth	⊢ ( ( ( 𝐴 ∪ ℕ ) ≼ ℕ ∧ ℕ ≼ ( 𝐴 ∪ ℕ ) ) → ( 𝐴 ∪ ℕ ) ≈ ℕ )
23	15 21 22	syl2anc	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ ) → ( 𝐴 ∪ ℕ ) ≈ ℕ )
24		ovolctb	⊢ ( ( ( 𝐴 ∪ ℕ ) ⊆ ℝ ∧ ( 𝐴 ∪ ℕ ) ≈ ℕ ) → ( vol* ‘ ( 𝐴 ∪ ℕ ) ) = 0 )
25	5 23 24	syl2anc	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ ) → ( vol* ‘ ( 𝐴 ∪ ℕ ) ) = 0 )
26		ovolssnul	⊢ ( ( 𝐴 ⊆ ( 𝐴 ∪ ℕ ) ∧ ( 𝐴 ∪ ℕ ) ⊆ ℝ ∧ ( vol* ‘ ( 𝐴 ∪ ℕ ) ) = 0 ) → ( vol* ‘ 𝐴 ) = 0 )
27	1 5 25 26	mp3an2i	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ ) → ( vol* ‘ 𝐴 ) = 0 )