Metamath Proof Explorer

Theorem cntnevol

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

Ref Expression
Assertion cntnevol ( ♯ ↾ 𝒫 𝑂 ) ≠ vol

Proof

Step Hyp Ref Expression
1 ax-1ne0 ⊢ 1 ≠ 0
2 1 a1i ⊢ ( 1 ∈ 𝑂 → 1 ≠ 0 )
3 snelpwi ⊢ ( 1 ∈ 𝑂 → { 1 } ∈ 𝒫 𝑂 )
4 fvres ⊢ ( { 1 } ∈ 𝒫 𝑂 → ( ( ♯ ↾ 𝒫 𝑂 ) ‘ { 1 } ) = ( ♯ ‘ { 1 } ) )
5 3 4 syl ⊢ ( 1 ∈ 𝑂 → ( ( ♯ ↾ 𝒫 𝑂 ) ‘ { 1 } ) = ( ♯ ‘ { 1 } ) )
6 1re ⊢ 1 ∈ ℝ
7 hashsng ⊢ ( 1 ∈ ℝ → ( ♯ ‘ { 1 } ) = 1 )
8 6 7 ax-mp ⊢ ( ♯ ‘ { 1 } ) = 1
9 5 8 eqtrdi ⊢ ( 1 ∈ 𝑂 → ( ( ♯ ↾ 𝒫 𝑂 ) ‘ { 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 ∈ 𝑂 → ( vol ‘ { 1 } ) = 0 )
19 2 9 18 3netr4d ⊢ ( 1 ∈ 𝑂 → ( ( ♯ ↾ 𝒫 𝑂 ) ‘ { 1 } ) ≠ ( vol ‘ { 1 } ) )
20 fveq1 ⊢ ( ( ♯ ↾ 𝒫 𝑂 ) = vol → ( ( ♯ ↾ 𝒫 𝑂 ) ‘ { 1 } ) = ( vol ‘ { 1 } ) )
21 20 necon3i ⊢ ( ( ( ♯ ↾ 𝒫 𝑂 ) ‘ { 1 } ) ≠ ( vol ‘ { 1 } ) → ( ♯ ↾ 𝒫 𝑂 ) ≠ vol )
22 19 21 syl ⊢ ( 1 ∈ 𝑂 → ( ♯ ↾ 𝒫 𝑂 ) ≠ vol )
23 6 13 ax-mp ⊢ { 1 } ∈ dom vol
24 23 biantrur ⊢ ( ¬ { 1 } ∈ dom ( ♯ ↾ 𝒫 𝑂 ) ↔ ( { 1 } ∈ dom vol ∧ ¬ { 1 } ∈ dom ( ♯ ↾ 𝒫 𝑂 ) ) )
25 snex ⊢ { 1 } ∈ V
26 25 elpw ⊢ ( { 1 } ∈ 𝒫 𝑂 ↔ { 1 } ⊆ 𝑂 )
27 dmhashres ⊢ dom ( ♯ ↾ 𝒫 𝑂 ) = 𝒫 𝑂
28 27 eleq2i ⊢ ( { 1 } ∈ dom ( ♯ ↾ 𝒫 𝑂 ) ↔ { 1 } ∈ 𝒫 𝑂 )
29 1ex ⊢ 1 ∈ V
30 29 snss ⊢ ( 1 ∈ 𝑂 ↔ { 1 } ⊆ 𝑂 )
31 26 28 30 3bitr4i ⊢ ( { 1 } ∈ dom ( ♯ ↾ 𝒫 𝑂 ) ↔ 1 ∈ 𝑂 )
32 31 notbii ⊢ ( ¬ { 1 } ∈ dom ( ♯ ↾ 𝒫 𝑂 ) ↔ ¬ 1 ∈ 𝑂 )
33 24 32 bitr3i ⊢ ( ( { 1 } ∈ dom vol ∧ ¬ { 1 } ∈ dom ( ♯ ↾ 𝒫 𝑂 ) ) ↔ ¬ 1 ∈ 𝑂 )
34 nelne1 ⊢ ( ( { 1 } ∈ dom vol ∧ ¬ { 1 } ∈ dom ( ♯ ↾ 𝒫 𝑂 ) ) → dom vol ≠ dom ( ♯ ↾ 𝒫 𝑂 ) )
35 33 34 sylbir ⊢ ( ¬ 1 ∈ 𝑂 → dom vol ≠ dom ( ♯ ↾ 𝒫 𝑂 ) )
36 35 necomd ⊢ ( ¬ 1 ∈ 𝑂 → dom ( ♯ ↾ 𝒫 𝑂 ) ≠ dom vol )
37 dmeq ⊢ ( ( ♯ ↾ 𝒫 𝑂 ) = vol → dom ( ♯ ↾ 𝒫 𝑂 ) = dom vol )
38 37 necon3i ⊢ ( dom ( ♯ ↾ 𝒫 𝑂 ) ≠ dom vol → ( ♯ ↾ 𝒫 𝑂 ) ≠ vol )
39 36 38 syl ⊢ ( ¬ 1 ∈ 𝑂 → ( ♯ ↾ 𝒫 𝑂 ) ≠ vol )
40 22 39 pm2.61i ⊢ ( ♯ ↾ 𝒫 𝑂 ) ≠ vol