# Metamath Proof Explorer

## Theorem cntnevol

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

Ref Expression
Assertion cntnevol ${⊢}{\left|.\right|↾}_{𝒫{O}}\ne vol$

### Proof

Step Hyp Ref Expression
1 ax-1ne0 ${⊢}1\ne 0$
2 1 a1i ${⊢}1\in {O}\to 1\ne 0$
3 snelpwi ${⊢}1\in {O}\to \left\{1\right\}\in 𝒫{O}$
4 fvres ${⊢}\left\{1\right\}\in 𝒫{O}\to \left({\left|.\right|↾}_{𝒫{O}}\right)\left(\left\{1\right\}\right)=\left|\left\{1\right\}\right|$
5 3 4 syl ${⊢}1\in {O}\to \left({\left|.\right|↾}_{𝒫{O}}\right)\left(\left\{1\right\}\right)=\left|\left\{1\right\}\right|$
6 1re ${⊢}1\in ℝ$
7 hashsng ${⊢}1\in ℝ\to \left|\left\{1\right\}\right|=1$
8 6 7 ax-mp ${⊢}\left|\left\{1\right\}\right|=1$
9 5 8 syl6eq ${⊢}1\in {O}\to \left({\left|.\right|↾}_{𝒫{O}}\right)\left(\left\{1\right\}\right)=1$
10 snssi ${⊢}1\in ℝ\to \left\{1\right\}\subseteq ℝ$
11 ovolsn ${⊢}1\in ℝ\to {vol}^{*}\left(\left\{1\right\}\right)=0$
12 nulmbl ${⊢}\left(\left\{1\right\}\subseteq ℝ\wedge {vol}^{*}\left(\left\{1\right\}\right)=0\right)\to \left\{1\right\}\in \mathrm{dom}vol$
13 10 11 12 syl2anc ${⊢}1\in ℝ\to \left\{1\right\}\in \mathrm{dom}vol$
14 mblvol ${⊢}\left\{1\right\}\in \mathrm{dom}vol\to vol\left(\left\{1\right\}\right)={vol}^{*}\left(\left\{1\right\}\right)$
15 6 11 ax-mp ${⊢}{vol}^{*}\left(\left\{1\right\}\right)=0$
16 14 15 syl6eq ${⊢}\left\{1\right\}\in \mathrm{dom}vol\to vol\left(\left\{1\right\}\right)=0$
17 6 13 16 mp2b ${⊢}vol\left(\left\{1\right\}\right)=0$
18 17 a1i ${⊢}1\in {O}\to vol\left(\left\{1\right\}\right)=0$
19 2 9 18 3netr4d ${⊢}1\in {O}\to \left({\left|.\right|↾}_{𝒫{O}}\right)\left(\left\{1\right\}\right)\ne vol\left(\left\{1\right\}\right)$
20 fveq1 ${⊢}{\left|.\right|↾}_{𝒫{O}}=vol\to \left({\left|.\right|↾}_{𝒫{O}}\right)\left(\left\{1\right\}\right)=vol\left(\left\{1\right\}\right)$
21 20 necon3i ${⊢}\left({\left|.\right|↾}_{𝒫{O}}\right)\left(\left\{1\right\}\right)\ne vol\left(\left\{1\right\}\right)\to {\left|.\right|↾}_{𝒫{O}}\ne vol$
22 19 21 syl ${⊢}1\in {O}\to {\left|.\right|↾}_{𝒫{O}}\ne vol$
23 6 13 ax-mp ${⊢}\left\{1\right\}\in \mathrm{dom}vol$
24 23 biantrur ${⊢}¬\left\{1\right\}\in \mathrm{dom}\left({\left|.\right|↾}_{𝒫{O}}\right)↔\left(\left\{1\right\}\in \mathrm{dom}vol\wedge ¬\left\{1\right\}\in \mathrm{dom}\left({\left|.\right|↾}_{𝒫{O}}\right)\right)$
25 snex ${⊢}\left\{1\right\}\in \mathrm{V}$
26 25 elpw ${⊢}\left\{1\right\}\in 𝒫{O}↔\left\{1\right\}\subseteq {O}$
27 dmhashres ${⊢}\mathrm{dom}\left({\left|.\right|↾}_{𝒫{O}}\right)=𝒫{O}$
28 27 eleq2i ${⊢}\left\{1\right\}\in \mathrm{dom}\left({\left|.\right|↾}_{𝒫{O}}\right)↔\left\{1\right\}\in 𝒫{O}$
29 1ex ${⊢}1\in \mathrm{V}$
30 29 snss ${⊢}1\in {O}↔\left\{1\right\}\subseteq {O}$
31 26 28 30 3bitr4i ${⊢}\left\{1\right\}\in \mathrm{dom}\left({\left|.\right|↾}_{𝒫{O}}\right)↔1\in {O}$
32 31 notbii ${⊢}¬\left\{1\right\}\in \mathrm{dom}\left({\left|.\right|↾}_{𝒫{O}}\right)↔¬1\in {O}$
33 24 32 bitr3i ${⊢}\left(\left\{1\right\}\in \mathrm{dom}vol\wedge ¬\left\{1\right\}\in \mathrm{dom}\left({\left|.\right|↾}_{𝒫{O}}\right)\right)↔¬1\in {O}$
34 nelne1 ${⊢}\left(\left\{1\right\}\in \mathrm{dom}vol\wedge ¬\left\{1\right\}\in \mathrm{dom}\left({\left|.\right|↾}_{𝒫{O}}\right)\right)\to \mathrm{dom}vol\ne \mathrm{dom}\left({\left|.\right|↾}_{𝒫{O}}\right)$
35 33 34 sylbir ${⊢}¬1\in {O}\to \mathrm{dom}vol\ne \mathrm{dom}\left({\left|.\right|↾}_{𝒫{O}}\right)$
36 35 necomd ${⊢}¬1\in {O}\to \mathrm{dom}\left({\left|.\right|↾}_{𝒫{O}}\right)\ne \mathrm{dom}vol$
37 dmeq ${⊢}{\left|.\right|↾}_{𝒫{O}}=vol\to \mathrm{dom}\left({\left|.\right|↾}_{𝒫{O}}\right)=\mathrm{dom}vol$
38 37 necon3i ${⊢}\mathrm{dom}\left({\left|.\right|↾}_{𝒫{O}}\right)\ne \mathrm{dom}vol\to {\left|.\right|↾}_{𝒫{O}}\ne vol$
39 36 38 syl ${⊢}¬1\in {O}\to {\left|.\right|↾}_{𝒫{O}}\ne vol$
40 22 39 pm2.61i ${⊢}{\left|.\right|↾}_{𝒫{O}}\ne vol$