This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ ) → ( 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 )