Metamath Proof Explorer

Theorem cntnevol

Description: Counting and Lebesgue measures are different. (Contributed by Thierry Arnoux, 27-Jan-2017)

Ref Expression
Assertion cntnevol ⊢ . ↾ 𝒫 O ≠ vol

Proof

Step Hyp Ref Expression
1 ax-1ne0 ⊢ 1 ≠ 0
2 1 a1i ⊢ 1 ∈ O → 1 ≠ 0
3 snelpwi ⊢ 1 ∈ O → 1 ∈ 𝒫 O
4 fvres ⊢ 1 ∈ 𝒫 O → . ↾ 𝒫 O ⁡ 1 = 1
5 3 4 syl ⊢ 1 ∈ O → . ↾ 𝒫 O ⁡ 1 = 1
6 1re ⊢ 1 ∈ ℝ
7 hashsng ⊢ 1 ∈ ℝ → 1 = 1
8 6 7 ax-mp ⊢ 1 = 1
9 5 8 eqtrdi ⊢ 1 ∈ O → . ↾ 𝒫 O ⁡ 1 = 1
10 snssi ⊢ 1 ∈ ℝ → 1 ⊆ ℝ
11 ovolsn ⊢ 1 ∈ ℝ → vol * ⁡ 1 = 0
12 nulmbl ⊢ 1 ⊆ ℝ ∧ vol * ⁡ 1 = 0 → 1 ∈ dom ⁡ vol
13 10 11 12 syl2anc ⊢ 1 ∈ ℝ → 1 ∈ dom ⁡ vol
14 mblvol ⊢ 1 ∈ dom ⁡ vol → vol ⁡ 1 = vol * ⁡ 1
15 6 11 ax-mp ⊢ vol * ⁡ 1 = 0
16 14 15 eqtrdi ⊢ 1 ∈ dom ⁡ vol → vol ⁡ 1 = 0
17 6 13 16 mp2b ⊢ vol ⁡ 1 = 0
18 17 a1i ⊢ 1 ∈ O → vol ⁡ 1 = 0
19 2 9 18 3netr4d ⊢ 1 ∈ O → . ↾ 𝒫 O ⁡ 1 ≠ vol ⁡ 1
20 fveq1 ⊢ . ↾ 𝒫 O = vol → . ↾ 𝒫 O ⁡ 1 = vol ⁡ 1
21 20 necon3i ⊢ . ↾ 𝒫 O ⁡ 1 ≠ vol ⁡ 1 → . ↾ 𝒫 O ≠ vol
22 19 21 syl ⊢ 1 ∈ O → . ↾ 𝒫 O ≠ vol
23 6 13 ax-mp ⊢ 1 ∈ dom ⁡ vol
24 23 biantrur ⊢ ¬ 1 ∈ dom ⁡ . ↾ 𝒫 O ↔ 1 ∈ dom ⁡ vol ∧ ¬ 1 ∈ dom ⁡ . ↾ 𝒫 O
25 snex ⊢ 1 ∈ V
26 25 elpw ⊢ 1 ∈ 𝒫 O ↔ 1 ⊆ O
27 dmhashres ⊢ dom ⁡ . ↾ 𝒫 O = 𝒫 O
28 27 eleq2i ⊢ 1 ∈ dom ⁡ . ↾ 𝒫 O ↔ 1 ∈ 𝒫 O
29 1ex ⊢ 1 ∈ V
30 29 snss ⊢ 1 ∈ O ↔ 1 ⊆ O
31 26 28 30 3bitr4i ⊢ 1 ∈ dom ⁡ . ↾ 𝒫 O ↔ 1 ∈ O
32 31 notbii ⊢ ¬ 1 ∈ dom ⁡ . ↾ 𝒫 O ↔ ¬ 1 ∈ O
33 24 32 bitr3i ⊢ 1 ∈ dom ⁡ vol ∧ ¬ 1 ∈ dom ⁡ . ↾ 𝒫 O ↔ ¬ 1 ∈ O
34 nelne1 ⊢ 1 ∈ dom ⁡ vol ∧ ¬ 1 ∈ dom ⁡ . ↾ 𝒫 O → dom ⁡ vol ≠ dom ⁡ . ↾ 𝒫 O
35 33 34 sylbir ⊢ ¬ 1 ∈ O → dom ⁡ vol ≠ dom ⁡ . ↾ 𝒫 O
36 35 necomd ⊢ ¬ 1 ∈ O → dom ⁡ . ↾ 𝒫 O ≠ dom ⁡ vol
37 dmeq ⊢ . ↾ 𝒫 O = vol → dom ⁡ . ↾ 𝒫 O = dom ⁡ vol
38 37 necon3i ⊢ dom ⁡ . ↾ 𝒫 O ≠ dom ⁡ vol → . ↾ 𝒫 O ≠ vol
39 36 38 syl ⊢ ¬ 1 ∈ O → . ↾ 𝒫 O ≠ vol
40 22 39 pm2.61i ⊢ . ↾ 𝒫 O ≠ vol