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 syl6eq 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 syl6eq 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