Metamath Proof Explorer

Theorem vitali

Description: If the reals can be well-ordered, then there are non-measurable sets. The proof uses "Vitali sets", named for Giuseppe Vitali (1905). (Contributed by Mario Carneiro, 16-Jun-2014)

Ref Expression
Assertion vitali ⊢<˙Weℝ→dom⁡vol⊂𝒫ℝ

Proof

Step Hyp Ref Expression
1 reex ⊢ℝ∈V
2 1 pwex ⊢𝒫ℝ∈V
3 weinxp ⊢<˙Weℝ↔<˙∩ℝ2Weℝ
4 unipw ⊢⋃𝒫ℝ=ℝ
5 weeq2 ⊢⋃𝒫ℝ=ℝ→<˙∩ℝ2We⋃𝒫ℝ↔<˙∩ℝ2Weℝ
6 4 5 ax-mp ⊢<˙∩ℝ2We⋃𝒫ℝ↔<˙∩ℝ2Weℝ
7 3 6 bitr4i ⊢<˙Weℝ↔<˙∩ℝ2We⋃𝒫ℝ
8 1 1 xpex ⊢ℝ2∈V
9 8 inex2 ⊢<˙∩ℝ2∈V
10 weeq1 ⊢x=<˙∩ℝ2→xWe⋃𝒫ℝ↔<˙∩ℝ2We⋃𝒫ℝ
11 9 10 spcev ⊢<˙∩ℝ2We⋃𝒫ℝ→∃xxWe⋃𝒫ℝ
12 7 11 sylbi ⊢<˙Weℝ→∃xxWe⋃𝒫ℝ
13 dfac8c ⊢𝒫ℝ∈V→∃xxWe⋃𝒫ℝ→∃f∀z∈𝒫ℝz≠∅→f⁡z∈z
14 2 12 13 mpsyl ⊢<˙Weℝ→∃f∀z∈𝒫ℝz≠∅→f⁡z∈z
15 qex ⊢ℚ∈V
16 15 inex1 ⊢ℚ∩−11∈V
17 nnrecq ⊢x∈ℕ→1x∈ℚ
18 nnrecre ⊢x∈ℕ→1x∈ℝ
19 neg1rr ⊢−1∈ℝ
20 19 a1i ⊢x∈ℕ→−1∈ℝ
21 0re ⊢0∈ℝ
22 21 a1i ⊢x∈ℕ→0∈ℝ
23 neg1lt0 ⊢−1<0
24 19 21 23 ltleii ⊢−1≤0
25 24 a1i ⊢x∈ℕ→−1≤0
26 nnrp ⊢x∈ℕ→x∈ℝ+
27 26 rpreccld ⊢x∈ℕ→1x∈ℝ+
28 27 rpge0d ⊢x∈ℕ→0≤1x
29 20 22 18 25 28 letrd ⊢x∈ℕ→−1≤1x
30 nnge1 ⊢x∈ℕ→1≤x
31 nnre ⊢x∈ℕ→x∈ℝ
32 nngt0 ⊢x∈ℕ→0<x
33 1re ⊢1∈ℝ
34 0lt1 ⊢0<1
35 lerec ⊢1∈ℝ∧0<1∧x∈ℝ∧0<x→1≤x↔1x≤11
36 33 34 35 mpanl12 ⊢x∈ℝ∧0<x→1≤x↔1x≤11
37 31 32 36 syl2anc ⊢x∈ℕ→1≤x↔1x≤11
38 30 37 mpbid ⊢x∈ℕ→1x≤11
39 1div1e1 ⊢11=1
40 38 39 breqtrdi ⊢x∈ℕ→1x≤1
41 19 33 elicc2i ⊢1x∈−11↔1x∈ℝ∧−1≤1x∧1x≤1
42 18 29 40 41 syl3anbrc ⊢x∈ℕ→1x∈−11
43 17 42 elind ⊢x∈ℕ→1x∈ℚ∩−11
44 oveq2 ⊢1x=1y→11x=11y
45 nncn ⊢x∈ℕ→x∈ℂ
46 nnne0 ⊢x∈ℕ→x≠0
47 45 46 recrecd ⊢x∈ℕ→11x=x
48 nncn ⊢y∈ℕ→y∈ℂ
49 nnne0 ⊢y∈ℕ→y≠0
50 48 49 recrecd ⊢y∈ℕ→11y=y
51 47 50 eqeqan12d ⊢x∈ℕ∧y∈ℕ→11x=11y↔x=y
52 44 51 imbitrid ⊢x∈ℕ∧y∈ℕ→1x=1y→x=y
53 oveq2 ⊢x=y→1x=1y
54 52 53 impbid1 ⊢x∈ℕ∧y∈ℕ→1x=1y↔x=y
55 43 54 dom2 ⊢ℚ∩−11∈V→ℕ≼ℚ∩−11
56 16 55 ax-mp ⊢ℕ≼ℚ∩−11
57 inss1 ⊢ℚ∩−11⊆ℚ
58 ssdomg ⊢ℚ∈V→ℚ∩−11⊆ℚ→ℚ∩−11≼ℚ
59 15 57 58 mp2 ⊢ℚ∩−11≼ℚ
60 qnnen ⊢ℚ≈ℕ
61 domentr ⊢ℚ∩−11≼ℚ∧ℚ≈ℕ→ℚ∩−11≼ℕ
62 59 60 61 mp2an ⊢ℚ∩−11≼ℕ
63 sbth ⊢ℕ≼ℚ∩−11∧ℚ∩−11≼ℕ→ℕ≈ℚ∩−11
64 56 62 63 mp2an ⊢ℕ≈ℚ∩−11
65 bren ⊢ℕ≈ℚ∩−11↔∃gg:ℕ⟶1-1 ontoℚ∩−11
66 64 65 mpbi ⊢∃gg:ℕ⟶1-1 ontoℚ∩−11
67 eleq1w ⊢a=x→a∈01↔x∈01
68 eleq1w ⊢b=y→b∈01↔y∈01
69 67 68 bi2anan9 ⊢a=x∧b=y→a∈01∧b∈01↔x∈01∧y∈01
70 oveq12 ⊢a=x∧b=y→a−b=x−y
71 70 eleq1d ⊢a=x∧b=y→a−b∈ℚ↔x−y∈ℚ
72 69 71 anbi12d ⊢a=x∧b=y→a∈01∧b∈01∧a−b∈ℚ↔x∈01∧y∈01∧x−y∈ℚ
73 72 cbvopabv ⊢ab|a∈01∧b∈01∧a−b∈ℚ=xy|x∈01∧y∈01∧x−y∈ℚ
74 eqid ⊢01/ab|a∈01∧b∈01∧a−b∈ℚ=01/ab|a∈01∧b∈01∧a−b∈ℚ
75 fvex ⊢f⁡c∈V
76 eqid ⊢c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c=c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c
77 75 76 fnmpti ⊢c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡cFn01/ab|a∈01∧b∈01∧a−b∈ℚ
78 77 a1i ⊢<˙Weℝ∧∀z∈𝒫ℝz≠∅→f⁡z∈z∧g:ℕ⟶1-1 ontoℚ∩−11∧¬ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c∈𝒫ℝ∖dom⁡vol→c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡cFn01/ab|a∈01∧b∈01∧a−b∈ℚ
79 neeq1 ⊢z=w→z≠∅↔w≠∅
80 fveq2 ⊢z=w→f⁡z=f⁡w
81 id ⊢z=w→z=w
82 80 81 eleq12d ⊢z=w→f⁡z∈z↔f⁡w∈w
83 79 82 imbi12d ⊢z=w→z≠∅→f⁡z∈z↔w≠∅→f⁡w∈w
84 83 cbvralvw ⊢∀z∈𝒫ℝz≠∅→f⁡z∈z↔∀w∈𝒫ℝw≠∅→f⁡w∈w
85 73 vitalilem1 ⊢ab|a∈01∧b∈01∧a−b∈ℚEr01
86 85 a1i ⊢⊤→ab|a∈01∧b∈01∧a−b∈ℚEr01
87 86 qsss ⊢⊤→01/ab|a∈01∧b∈01∧a−b∈ℚ⊆𝒫01
88 87 mptru ⊢01/ab|a∈01∧b∈01∧a−b∈ℚ⊆𝒫01
89 unitssre ⊢01⊆ℝ
90 89 sspwi ⊢𝒫01⊆𝒫ℝ
91 88 90 sstri ⊢01/ab|a∈01∧b∈01∧a−b∈ℚ⊆𝒫ℝ
92 ssralv ⊢01/ab|a∈01∧b∈01∧a−b∈ℚ⊆𝒫ℝ→∀w∈𝒫ℝw≠∅→f⁡w∈w→∀w∈01/ab|a∈01∧b∈01∧a−b∈ℚw≠∅→f⁡w∈w
93 91 92 ax-mp ⊢∀w∈𝒫ℝw≠∅→f⁡w∈w→∀w∈01/ab|a∈01∧b∈01∧a−b∈ℚw≠∅→f⁡w∈w
94 84 93 sylbi ⊢∀z∈𝒫ℝz≠∅→f⁡z∈z→∀w∈01/ab|a∈01∧b∈01∧a−b∈ℚw≠∅→f⁡w∈w
95 fveq2 ⊢c=w→f⁡c=f⁡w
96 fvex ⊢f⁡w∈V
97 95 76 96 fvmpt ⊢w∈01/ab|a∈01∧b∈01∧a−b∈ℚ→c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c⁡w=f⁡w
98 97 eleq1d ⊢w∈01/ab|a∈01∧b∈01∧a−b∈ℚ→c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c⁡w∈w↔f⁡w∈w
99 98 imbi2d ⊢w∈01/ab|a∈01∧b∈01∧a−b∈ℚ→w≠∅→c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c⁡w∈w↔w≠∅→f⁡w∈w
100 99 ralbiia ⊢∀w∈01/ab|a∈01∧b∈01∧a−b∈ℚw≠∅→c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c⁡w∈w↔∀w∈01/ab|a∈01∧b∈01∧a−b∈ℚw≠∅→f⁡w∈w
101 94 100 sylibr ⊢∀z∈𝒫ℝz≠∅→f⁡z∈z→∀w∈01/ab|a∈01∧b∈01∧a−b∈ℚw≠∅→c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c⁡w∈w
102 101 ad2antlr ⊢<˙Weℝ∧∀z∈𝒫ℝz≠∅→f⁡z∈z∧g:ℕ⟶1-1 ontoℚ∩−11∧¬ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c∈𝒫ℝ∖dom⁡vol→∀w∈01/ab|a∈01∧b∈01∧a−b∈ℚw≠∅→c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c⁡w∈w
103 simprl ⊢<˙Weℝ∧∀z∈𝒫ℝz≠∅→f⁡z∈z∧g:ℕ⟶1-1 ontoℚ∩−11∧¬ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c∈𝒫ℝ∖dom⁡vol→g:ℕ⟶1-1 ontoℚ∩−11
104 oveq1 ⊢t=s→t−g⁡m=s−g⁡m
105 104 eleq1d ⊢t=s→t−g⁡m∈ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c↔s−g⁡m∈ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c
106 105 cbvrabv ⊢t∈ℝ|t−g⁡m∈ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c=s∈ℝ|s−g⁡m∈ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c
107 fveq2 ⊢m=n→g⁡m=g⁡n
108 107 oveq2d ⊢m=n→s−g⁡m=s−g⁡n
109 108 eleq1d ⊢m=n→s−g⁡m∈ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c↔s−g⁡n∈ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c
110 109 rabbidv ⊢m=n→s∈ℝ|s−g⁡m∈ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c=s∈ℝ|s−g⁡n∈ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c
111 106 110 eqtrid ⊢m=n→t∈ℝ|t−g⁡m∈ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c=s∈ℝ|s−g⁡n∈ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c
112 111 cbvmptv ⊢m∈ℕ⟼t∈ℝ|t−g⁡m∈ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c=n∈ℕ⟼s∈ℝ|s−g⁡n∈ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c
113 simprr ⊢<˙Weℝ∧∀z∈𝒫ℝz≠∅→f⁡z∈z∧g:ℕ⟶1-1 ontoℚ∩−11∧¬ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c∈𝒫ℝ∖dom⁡vol→¬ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c∈𝒫ℝ∖dom⁡vol
114 73 74 78 102 103 112 113 vitalilem5 ⊢¬<˙Weℝ∧∀z∈𝒫ℝz≠∅→f⁡z∈z∧g:ℕ⟶1-1 ontoℚ∩−11∧¬ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c∈𝒫ℝ∖dom⁡vol
115 114 pm2.21i ⊢<˙Weℝ∧∀z∈𝒫ℝz≠∅→f⁡z∈z∧g:ℕ⟶1-1 ontoℚ∩−11∧¬ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c∈𝒫ℝ∖dom⁡vol→ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c∈𝒫ℝ∖dom⁡vol
116 115 expr ⊢<˙Weℝ∧∀z∈𝒫ℝz≠∅→f⁡z∈z∧g:ℕ⟶1-1 ontoℚ∩−11→¬ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c∈𝒫ℝ∖dom⁡vol→ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c∈𝒫ℝ∖dom⁡vol
117 116 pm2.18d ⊢<˙Weℝ∧∀z∈𝒫ℝz≠∅→f⁡z∈z∧g:ℕ⟶1-1 ontoℚ∩−11→ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c∈𝒫ℝ∖dom⁡vol
118 eldif ⊢ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c∈𝒫ℝ∖dom⁡vol↔ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c∈𝒫ℝ∧¬ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c∈dom⁡vol
119 mblss ⊢x∈dom⁡vol→x⊆ℝ
120 velpw ⊢x∈𝒫ℝ↔x⊆ℝ
121 119 120 sylibr ⊢x∈dom⁡vol→x∈𝒫ℝ
122 121 ssriv ⊢dom⁡vol⊆𝒫ℝ
123 ssnelpss ⊢dom⁡vol⊆𝒫ℝ→ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c∈𝒫ℝ∧¬ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c∈dom⁡vol→dom⁡vol⊂𝒫ℝ
124 122 123 ax-mp ⊢ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c∈𝒫ℝ∧¬ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c∈dom⁡vol→dom⁡vol⊂𝒫ℝ
125 118 124 sylbi ⊢ran⁡c∈01/ab|a∈01∧b∈01∧a−b∈ℚ⟼f⁡c∈𝒫ℝ∖dom⁡vol→dom⁡vol⊂𝒫ℝ
126 117 125 syl ⊢<˙Weℝ∧∀z∈𝒫ℝz≠∅→f⁡z∈z∧g:ℕ⟶1-1 ontoℚ∩−11→dom⁡vol⊂𝒫ℝ
127 126 ex ⊢<˙Weℝ∧∀z∈𝒫ℝz≠∅→f⁡z∈z→g:ℕ⟶1-1 ontoℚ∩−11→dom⁡vol⊂𝒫ℝ
128 127 exlimdv ⊢<˙Weℝ∧∀z∈𝒫ℝz≠∅→f⁡z∈z→∃gg:ℕ⟶1-1 ontoℚ∩−11→dom⁡vol⊂𝒫ℝ
129 66 128 mpi ⊢<˙Weℝ∧∀z∈𝒫ℝz≠∅→f⁡z∈z→dom⁡vol⊂𝒫ℝ
130 14 129 exlimddv ⊢<˙Weℝ→dom⁡vol⊂𝒫ℝ