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