| 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
|
syl5ib |
⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( ( 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
|
syl5eq |
⊢ ( 𝑚 = 𝑛 → { 𝑡 ∈ ℝ ∣ ( 𝑡 − ( 𝑔 ‘ 𝑚 ) ) ∈ 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 ⊊ 𝒫 ℝ ) |