This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ℝ ↔ ( < ∩ ( ℝ × ℝ ) ) We ℝ )
4 unipw ⊢ ∪ 𝒫 ℝ = ℝ
5 weeq2 ⊢ ( ∪ 𝒫 ℝ = ℝ → ( ( < ∩ ( ℝ × ℝ ) ) We ∪ 𝒫 ℝ ↔ ( < ∩ ( ℝ × ℝ ) ) We ℝ ) )
6 4 5 ax-mp ⊢ ( ( < ∩ ( ℝ × ℝ ) ) We ∪ 𝒫 ℝ ↔ ( < ∩ ( ℝ × ℝ ) ) We ℝ )
7 3 6 bitr4i ⊢ ( < We ℝ ↔ ( < ∩ ( ℝ × ℝ ) ) We ∪ 𝒫 ℝ )
8 1 1 xpex ⊢ ( ℝ × ℝ ) ∈ V
9 8 inex2 ⊢ ( < ∩ ( ℝ × ℝ ) ) ∈ V
10 weeq1 ⊢ ( 𝑥 = ( < ∩ ( ℝ × ℝ ) ) → ( 𝑥 We ∪ 𝒫 ℝ ↔ ( < ∩ ( ℝ × ℝ ) ) We ∪ 𝒫 ℝ ) )
11 9 10 spcev ⊢ ( ( < ∩ ( ℝ × ℝ ) ) We ∪ 𝒫 ℝ → ∃ 𝑥 𝑥 We ∪ 𝒫 ℝ )
12 7 11 sylbi ⊢ ( < We ℝ → ∃ 𝑥 𝑥 We ∪ 𝒫 ℝ )
13 dfac8c ⊢ ( 𝒫 ℝ ∈ V → ( ∃ 𝑥 𝑥 We ∪ 𝒫 ℝ → ∃ 𝑓 ∀ 𝑧 ∈ 𝒫 ℝ ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
14 2 12 13 mpsyl ⊢ ( < We ℝ → ∃ 𝑓 ∀ 𝑧 ∈ 𝒫 ℝ ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
15 qex ⊢ ℚ ∈ V
16 15 inex1 ⊢ ( ℚ ∩ ( - 1 [,] 1 ) ) ∈ V
17 nnrecq ⊢ ( 𝑥 ∈ ℕ → ( 1 / 𝑥 ) ∈ ℚ )
18 nnrecre ⊢ ( 𝑥 ∈ ℕ → ( 1 / 𝑥 ) ∈ ℝ )
19 neg1rr ⊢ - 1 ∈ ℝ
20 19 a1i ⊢ ( 𝑥 ∈ ℕ → - 1 ∈ ℝ )
21 0re ⊢ 0 ∈ ℝ
22 21 a1i ⊢ ( 𝑥 ∈ ℕ → 0 ∈ ℝ )
23 neg1lt0 ⊢ - 1 < 0
24 19 21 23 ltleii ⊢ - 1 ≤ 0
25 24 a1i ⊢ ( 𝑥 ∈ ℕ → - 1 ≤ 0 )
26 nnrp ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℝ+ )
27 26 rpreccld ⊢ ( 𝑥 ∈ ℕ → ( 1 / 𝑥 ) ∈ ℝ+ )
28 27 rpge0d ⊢ ( 𝑥 ∈ ℕ → 0 ≤ ( 1 / 𝑥 ) )
29 20 22 18 25 28 letrd ⊢ ( 𝑥 ∈ ℕ → - 1 ≤ ( 1 / 𝑥 ) )
30 nnge1 ⊢ ( 𝑥 ∈ ℕ → 1 ≤ 𝑥 )
31 nnre ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℝ )
32 nngt0 ⊢ ( 𝑥 ∈ ℕ → 0 < 𝑥 )
33 1re ⊢ 1 ∈ ℝ
34 0lt1 ⊢ 0 < 1
35 lerec ⊢ ( ( ( 1 ∈ ℝ ∧ 0 < 1 ) ∧ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ) → ( 1 ≤ 𝑥 ↔ ( 1 / 𝑥 ) ≤ ( 1 / 1 ) ) )
36 33 34 35 mpanl12 ⊢ ( ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) → ( 1 ≤ 𝑥 ↔ ( 1 / 𝑥 ) ≤ ( 1 / 1 ) ) )
37 31 32 36 syl2anc ⊢ ( 𝑥 ∈ ℕ → ( 1 ≤ 𝑥 ↔ ( 1 / 𝑥 ) ≤ ( 1 / 1 ) ) )
38 30 37 mpbid ⊢ ( 𝑥 ∈ ℕ → ( 1 / 𝑥 ) ≤ ( 1 / 1 ) )
39 1div1e1 ⊢ ( 1 / 1 ) = 1
40 38 39 breqtrdi ⊢ ( 𝑥 ∈ ℕ → ( 1 / 𝑥 ) ≤ 1 )
41 19 33 elicc2i ⊢ ( ( 1 / 𝑥 ) ∈ ( - 1 [,] 1 ) ↔ ( ( 1 / 𝑥 ) ∈ ℝ ∧ - 1 ≤ ( 1 / 𝑥 ) ∧ ( 1 / 𝑥 ) ≤ 1 ) )
42 18 29 40 41 syl3anbrc ⊢ ( 𝑥 ∈ ℕ → ( 1 / 𝑥 ) ∈ ( - 1 [,] 1 ) )
43 17 42 elind ⊢ ( 𝑥 ∈ ℕ → ( 1 / 𝑥 ) ∈ ( ℚ ∩ ( - 1 [,] 1 ) ) )
44 oveq2 ⊢ ( ( 1 / 𝑥 ) = ( 1 / 𝑦 ) → ( 1 / ( 1 / 𝑥 ) ) = ( 1 / ( 1 / 𝑦 ) ) )
45 nncn ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℂ )
46 nnne0 ⊢ ( 𝑥 ∈ ℕ → 𝑥 ≠ 0 )
47 45 46 recrecd ⊢ ( 𝑥 ∈ ℕ → ( 1 / ( 1 / 𝑥 ) ) = 𝑥 )
48 nncn ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℂ )
49 nnne0 ⊢ ( 𝑦 ∈ ℕ → 𝑦 ≠ 0 )
50 48 49 recrecd ⊢ ( 𝑦 ∈ ℕ → ( 1 / ( 1 / 𝑦 ) ) = 𝑦 )
51 47 50 eqeqan12d ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( ( 1 / ( 1 / 𝑥 ) ) = ( 1 / ( 1 / 𝑦 ) ) ↔ 𝑥 = 𝑦 ) )
52 44 51 imbitrid ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( ( 1 / 𝑥 ) = ( 1 / 𝑦 ) → 𝑥 = 𝑦 ) )
53 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 1 / 𝑥 ) = ( 1 / 𝑦 ) )
54 52 53 impbid1 ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( ( 1 / 𝑥 ) = ( 1 / 𝑦 ) ↔ 𝑥 = 𝑦 ) )
55 43 54 dom2 ⊢ ( ( ℚ ∩ ( - 1 [,] 1 ) ) ∈ V → ℕ ≼ ( ℚ ∩ ( - 1 [,] 1 ) ) )
56 16 55 ax-mp ⊢ ℕ ≼ ( ℚ ∩ ( - 1 [,] 1 ) )
57 inss1 ⊢ ( ℚ ∩ ( - 1 [,] 1 ) ) ⊆ ℚ
58 ssdomg ⊢ ( ℚ ∈ V → ( ( ℚ ∩ ( - 1 [,] 1 ) ) ⊆ ℚ → ( ℚ ∩ ( - 1 [,] 1 ) ) ≼ ℚ ) )
59 15 57 58 mp2 ⊢ ( ℚ ∩ ( - 1 [,] 1 ) ) ≼ ℚ
60 qnnen ⊢ ℚ ≈ ℕ
61 domentr ⊢ ( ( ( ℚ ∩ ( - 1 [,] 1 ) ) ≼ ℚ ∧ ℚ ≈ ℕ ) → ( ℚ ∩ ( - 1 [,] 1 ) ) ≼ ℕ )
62 59 60 61 mp2an ⊢ ( ℚ ∩ ( - 1 [,] 1 ) ) ≼ ℕ
63 sbth ⊢ ( ( ℕ ≼ ( ℚ ∩ ( - 1 [,] 1 ) ) ∧ ( ℚ ∩ ( - 1 [,] 1 ) ) ≼ ℕ ) → ℕ ≈ ( ℚ ∩ ( - 1 [,] 1 ) ) )
64 56 62 63 mp2an ⊢ ℕ ≈ ( ℚ ∩ ( - 1 [,] 1 ) )
65 bren ⊢ ( ℕ ≈ ( ℚ ∩ ( - 1 [,] 1 ) ) ↔ ∃ 𝑔 𝑔 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) )
66 64 65 mpbi ⊢ ∃ 𝑔 𝑔 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) )
67 eleq1w ⊢ ( 𝑎 = 𝑥 → ( 𝑎 ∈ ( 0 [,] 1 ) ↔ 𝑥 ∈ ( 0 [,] 1 ) ) )
68 eleq1w ⊢ ( 𝑏 = 𝑦 → ( 𝑏 ∈ ( 0 [,] 1 ) ↔ 𝑦 ∈ ( 0 [,] 1 ) ) )
69 67 68 bi2anan9 ⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ↔ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) )
70 oveq12 ⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ( 𝑎 − 𝑏 ) = ( 𝑥 − 𝑦 ) )
71 70 eleq1d ⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ( ( 𝑎 − 𝑏 ) ∈ ℚ ↔ ( 𝑥 − 𝑦 ) ∈ ℚ ) )
72 69 71 anbi12d ⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ( ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) ↔ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑥 − 𝑦 ) ∈ ℚ ) ) )
73 72 cbvopabv ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑥 − 𝑦 ) ∈ ℚ ) }
74 eqid ⊢ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) = ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } )
75 fvex ⊢ ( 𝑓 ‘ 𝑐 ) ∈ V
76 eqid ⊢ ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) = ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) )
77 75 76 fnmpti ⊢ ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) Fn ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } )
78 77 a1i ⊢ ( ( ( < We ℝ ∧ ∀ 𝑧 ∈ 𝒫 ℝ ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) ∧ ( 𝑔 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) ∧ ¬ ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ∈ ( 𝒫 ℝ ∖ dom vol ) ) ) → ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) Fn ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) )
79 neeq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 ≠ ∅ ↔ 𝑤 ≠ ∅ ) )
80 fveq2 ⊢ ( 𝑧 = 𝑤 → ( 𝑓 ‘ 𝑧 ) = ( 𝑓 ‘ 𝑤 ) )
81 id ⊢ ( 𝑧 = 𝑤 → 𝑧 = 𝑤 )
82 80 81 eleq12d ⊢ ( 𝑧 = 𝑤 → ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ↔ ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ) )
83 79 82 imbi12d ⊢ ( 𝑧 = 𝑤 → ( ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( 𝑤 ≠ ∅ → ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ) ) )
84 83 cbvralvw ⊢ ( ∀ 𝑧 ∈ 𝒫 ℝ ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ∀ 𝑤 ∈ 𝒫 ℝ ( 𝑤 ≠ ∅ → ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ) )
85 73 vitalilem1 ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } Er ( 0 [,] 1 )
86 85 a1i ⊢ ( ⊤ → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } Er ( 0 [,] 1 ) )
87 86 qsss ⊢ ( ⊤ → ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ⊆ 𝒫 ( 0 [,] 1 ) )
88 87 mptru ⊢ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ⊆ 𝒫 ( 0 [,] 1 )
89 unitssre ⊢ ( 0 [,] 1 ) ⊆ ℝ
90 89 sspwi ⊢ 𝒫 ( 0 [,] 1 ) ⊆ 𝒫 ℝ
91 88 90 sstri ⊢ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ⊆ 𝒫 ℝ
92 ssralv ⊢ ( ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ⊆ 𝒫 ℝ → ( ∀ 𝑤 ∈ 𝒫 ℝ ( 𝑤 ≠ ∅ → ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ) → ∀ 𝑤 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ( 𝑤 ≠ ∅ → ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ) ) )
93 91 92 ax-mp ⊢ ( ∀ 𝑤 ∈ 𝒫 ℝ ( 𝑤 ≠ ∅ → ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ) → ∀ 𝑤 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ( 𝑤 ≠ ∅ → ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ) )
94 84 93 sylbi ⊢ ( ∀ 𝑧 ∈ 𝒫 ℝ ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∀ 𝑤 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ( 𝑤 ≠ ∅ → ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ) )
95 fveq2 ⊢ ( 𝑐 = 𝑤 → ( 𝑓 ‘ 𝑐 ) = ( 𝑓 ‘ 𝑤 ) )
96 fvex ⊢ ( 𝑓 ‘ 𝑤 ) ∈ V
97 95 76 96 fvmpt ⊢ ( 𝑤 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) → ( ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ‘ 𝑤 ) = ( 𝑓 ‘ 𝑤 ) )
98 97 eleq1d ⊢ ( 𝑤 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) → ( ( ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ‘ 𝑤 ) ∈ 𝑤 ↔ ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ) )
99 98 imbi2d ⊢ ( 𝑤 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) → ( ( 𝑤 ≠ ∅ → ( ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ‘ 𝑤 ) ∈ 𝑤 ) ↔ ( 𝑤 ≠ ∅ → ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ) ) )
100 99 ralbiia ⊢ ( ∀ 𝑤 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ( 𝑤 ≠ ∅ → ( ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ‘ 𝑤 ) ∈ 𝑤 ) ↔ ∀ 𝑤 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ( 𝑤 ≠ ∅ → ( 𝑓 ‘ 𝑤 ) ∈ 𝑤 ) )
101 94 100 sylibr ⊢ ( ∀ 𝑧 ∈ 𝒫 ℝ ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∀ 𝑤 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ( 𝑤 ≠ ∅ → ( ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ‘ 𝑤 ) ∈ 𝑤 ) )
102 101 ad2antlr ⊢ ( ( ( < We ℝ ∧ ∀ 𝑧 ∈ 𝒫 ℝ ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) ∧ ( 𝑔 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) ∧ ¬ ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ∈ ( 𝒫 ℝ ∖ dom vol ) ) ) → ∀ 𝑤 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ( 𝑤 ≠ ∅ → ( ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ‘ 𝑤 ) ∈ 𝑤 ) )
103 simprl ⊢ ( ( ( < We ℝ ∧ ∀ 𝑧 ∈ 𝒫 ℝ ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) ∧ ( 𝑔 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) ∧ ¬ ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ∈ ( 𝒫 ℝ ∖ dom vol ) ) ) → 𝑔 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) )
104 oveq1 ⊢ ( 𝑡 = 𝑠 → ( 𝑡 − ( 𝑔 ‘ 𝑚 ) ) = ( 𝑠 − ( 𝑔 ‘ 𝑚 ) ) )
105 104 eleq1d ⊢ ( 𝑡 = 𝑠 → ( ( 𝑡 − ( 𝑔 ‘ 𝑚 ) ) ∈ ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ↔ ( 𝑠 − ( 𝑔 ‘ 𝑚 ) ) ∈ ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ) )
106 105 cbvrabv ⊢ { 𝑡 ∈ ℝ ∣ ( 𝑡 − ( 𝑔 ‘ 𝑚 ) ) ∈ ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) } = { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝑔 ‘ 𝑚 ) ) ∈ ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) }
107 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝑔 ‘ 𝑚 ) = ( 𝑔 ‘ 𝑛 ) )
108 107 oveq2d ⊢ ( 𝑚 = 𝑛 → ( 𝑠 − ( 𝑔 ‘ 𝑚 ) ) = ( 𝑠 − ( 𝑔 ‘ 𝑛 ) ) )
109 108 eleq1d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑠 − ( 𝑔 ‘ 𝑚 ) ) ∈ ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ↔ ( 𝑠 − ( 𝑔 ‘ 𝑛 ) ) ∈ ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ) )
110 109 rabbidv ⊢ ( 𝑚 = 𝑛 → { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝑔 ‘ 𝑚 ) ) ∈ ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) } = { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝑔 ‘ 𝑛 ) ) ∈ ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) } )
111 106 110 eqtrid ⊢ ( 𝑚 = 𝑛 → { 𝑡 ∈ ℝ ∣ ( 𝑡 − ( 𝑔 ‘ 𝑚 ) ) ∈ ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) } = { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝑔 ‘ 𝑛 ) ) ∈ ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) } )
112 111 cbvmptv ⊢ ( 𝑚 ∈ ℕ ↦ { 𝑡 ∈ ℝ ∣ ( 𝑡 − ( 𝑔 ‘ 𝑚 ) ) ∈ ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) } ) = ( 𝑛 ∈ ℕ ↦ { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝑔 ‘ 𝑛 ) ) ∈ ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) } )
113 simprr ⊢ ( ( ( < We ℝ ∧ ∀ 𝑧 ∈ 𝒫 ℝ ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) ∧ ( 𝑔 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) ∧ ¬ ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ∈ ( 𝒫 ℝ ∖ dom vol ) ) ) → ¬ ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ∈ ( 𝒫 ℝ ∖ dom vol ) )
114 73 74 78 102 103 112 113 vitalilem5 ⊢ ¬ ( ( < We ℝ ∧ ∀ 𝑧 ∈ 𝒫 ℝ ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) ∧ ( 𝑔 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) ∧ ¬ ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ∈ ( 𝒫 ℝ ∖ dom vol ) ) )
115 114 pm2.21i ⊢ ( ( ( < We ℝ ∧ ∀ 𝑧 ∈ 𝒫 ℝ ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) ∧ ( 𝑔 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) ∧ ¬ ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ∈ ( 𝒫 ℝ ∖ dom vol ) ) ) → ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ∈ ( 𝒫 ℝ ∖ dom vol ) )
116 115 expr ⊢ ( ( ( < We ℝ ∧ ∀ 𝑧 ∈ 𝒫 ℝ ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) ∧ 𝑔 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) ) → ( ¬ ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ∈ ( 𝒫 ℝ ∖ dom vol ) → ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ∈ ( 𝒫 ℝ ∖ dom vol ) ) )
117 116 pm2.18d ⊢ ( ( ( < We ℝ ∧ ∀ 𝑧 ∈ 𝒫 ℝ ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) ∧ 𝑔 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) ) → ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ∈ ( 𝒫 ℝ ∖ dom vol ) )
118 eldif ⊢ ( ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ∈ ( 𝒫 ℝ ∖ dom vol ) ↔ ( ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ∈ 𝒫 ℝ ∧ ¬ ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ∈ dom vol ) )
119 mblss ⊢ ( 𝑥 ∈ dom vol → 𝑥 ⊆ ℝ )
120 velpw ⊢ ( 𝑥 ∈ 𝒫 ℝ ↔ 𝑥 ⊆ ℝ )
121 119 120 sylibr ⊢ ( 𝑥 ∈ dom vol → 𝑥 ∈ 𝒫 ℝ )
122 121 ssriv ⊢ dom vol ⊆ 𝒫 ℝ
123 ssnelpss ⊢ ( dom vol ⊆ 𝒫 ℝ → ( ( ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ∈ 𝒫 ℝ ∧ ¬ ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ∈ dom vol ) → dom vol ⊊ 𝒫 ℝ ) )
124 122 123 ax-mp ⊢ ( ( ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ∈ 𝒫 ℝ ∧ ¬ ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ∈ dom vol ) → dom vol ⊊ 𝒫 ℝ )
125 118 124 sylbi ⊢ ( ran ( 𝑐 ∈ ( ( 0 [,] 1 ) / { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 0 [,] 1 ) ∧ 𝑏 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑎 − 𝑏 ) ∈ ℚ ) } ) ↦ ( 𝑓 ‘ 𝑐 ) ) ∈ ( 𝒫 ℝ ∖ dom vol ) → dom vol ⊊ 𝒫 ℝ )
126 117 125 syl ⊢ ( ( ( < We ℝ ∧ ∀ 𝑧 ∈ 𝒫 ℝ ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) ∧ 𝑔 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) ) → dom vol ⊊ 𝒫 ℝ )
127 126 ex ⊢ ( ( < We ℝ ∧ ∀ 𝑧 ∈ 𝒫 ℝ ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) → ( 𝑔 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) → dom vol ⊊ 𝒫 ℝ ) )
128 127 exlimdv ⊢ ( ( < We ℝ ∧ ∀ 𝑧 ∈ 𝒫 ℝ ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) → ( ∃ 𝑔 𝑔 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) → dom vol ⊊ 𝒫 ℝ ) )
129 66 128 mpi ⊢ ( ( < We ℝ ∧ ∀ 𝑧 ∈ 𝒫 ℝ ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) → dom vol ⊊ 𝒫 ℝ )
130 14 129 exlimddv ⊢ ( < We ℝ → dom vol ⊊ 𝒫 ℝ )