Metamath Proof Explorer

Theorem cntnevol

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

Ref Expression
Assertion cntnevol 
|- ( # |` ~P O ) =/= vol

Proof

Step Hyp Ref Expression
1 ax-1ne0 
 |-  1 =/= 0
2 1 a1i 
 |-  ( 1 e. O -> 1 =/= 0 )
3 snelpwi 
 |-  ( 1 e. O -> { 1 } e. ~P O )
4 fvres 
 |-  ( { 1 } e. ~P O -> ( ( # |` ~P O ) ` { 1 } ) = ( # ` { 1 } ) )
5 3 4 syl 
 |-  ( 1 e. O -> ( ( # |` ~P O ) ` { 1 } ) = ( # ` { 1 } ) )
6 1re 
 |-  1 e. RR
7 hashsng 
 |-  ( 1 e. RR -> ( # ` { 1 } ) = 1 )
8 6 7 ax-mp 
 |-  ( # ` { 1 } ) = 1
9 5 8 eqtrdi 
 |-  ( 1 e. O -> ( ( # |` ~P O ) ` { 1 } ) = 1 )
10 snssi 
 |-  ( 1 e. RR -> { 1 } C_ RR )
11 ovolsn 
 |-  ( 1 e. RR -> ( vol* ` { 1 } ) = 0 )
12 nulmbl 
 |-  ( ( { 1 } C_ RR /\ ( vol* ` { 1 } ) = 0 ) -> { 1 } e. dom vol )
13 10 11 12 syl2anc 
 |-  ( 1 e. RR -> { 1 } e. dom vol )
14 mblvol 
 |-  ( { 1 } e. dom vol -> ( vol ` { 1 } ) = ( vol* ` { 1 } ) )
15 6 11 ax-mp 
 |-  ( vol* ` { 1 } ) = 0
16 14 15 eqtrdi 
 |-  ( { 1 } e. dom vol -> ( vol ` { 1 } ) = 0 )
17 6 13 16 mp2b 
 |-  ( vol ` { 1 } ) = 0
18 17 a1i 
 |-  ( 1 e. O -> ( vol ` { 1 } ) = 0 )
19 2 9 18 3netr4d 
 |-  ( 1 e. O -> ( ( # |` ~P O ) ` { 1 } ) =/= ( vol ` { 1 } ) )
20 fveq1 
 |-  ( ( # |` ~P O ) = vol -> ( ( # |` ~P O ) ` { 1 } ) = ( vol ` { 1 } ) )
21 20 necon3i 
 |-  ( ( ( # |` ~P O ) ` { 1 } ) =/= ( vol ` { 1 } ) -> ( # |` ~P O ) =/= vol )
22 19 21 syl 
 |-  ( 1 e. O -> ( # |` ~P O ) =/= vol )
23 6 13 ax-mp 
 |-  { 1 } e. dom vol
24 23 biantrur 
 |-  ( -. { 1 } e. dom ( # |` ~P O ) <-> ( { 1 } e. dom vol /\ -. { 1 } e. dom ( # |` ~P O ) ) )
25 snex 
 |-  { 1 } e. _V
26 25 elpw 
 |-  ( { 1 } e. ~P O <-> { 1 } C_ O )
27 dmhashres 
 |-  dom ( # |` ~P O ) = ~P O
28 27 eleq2i 
 |-  ( { 1 } e. dom ( # |` ~P O ) <-> { 1 } e. ~P O )
29 1ex 
 |-  1 e. _V
30 29 snss 
 |-  ( 1 e. O <-> { 1 } C_ O )
31 26 28 30 3bitr4i 
 |-  ( { 1 } e. dom ( # |` ~P O ) <-> 1 e. O )
32 31 notbii 
 |-  ( -. { 1 } e. dom ( # |` ~P O ) <-> -. 1 e. O )
33 24 32 bitr3i 
 |-  ( ( { 1 } e. dom vol /\ -. { 1 } e. dom ( # |` ~P O ) ) <-> -. 1 e. O )
34 nelne1 
 |-  ( ( { 1 } e. dom vol /\ -. { 1 } e. dom ( # |` ~P O ) ) -> dom vol =/= dom ( # |` ~P O ) )
35 33 34 sylbir 
 |-  ( -. 1 e. O -> dom vol =/= dom ( # |` ~P O ) )
36 35 necomd 
 |-  ( -. 1 e. O -> dom ( # |` ~P O ) =/= dom vol )
37 dmeq 
 |-  ( ( # |` ~P O ) = vol -> dom ( # |` ~P O ) = dom vol )
38 37 necon3i 
 |-  ( dom ( # |` ~P O ) =/= dom vol -> ( # |` ~P O ) =/= vol )
39 36 38 syl 
 |-  ( -. 1 e. O -> ( # |` ~P O ) =/= vol )
40 22 39 pm2.61i 
 |-  ( # |` ~P O ) =/= vol