| Step | Hyp | Ref
| Expression |
| 1 | | reex 11246 |
. . . 4
⊢ ℝ
∈ V |
| 2 | 1 | pwex 5380 |
. . 3
⊢ 𝒫
ℝ ∈ V |
| 3 | | weinxp 5770 |
. . . . 5
⊢ ( < We ℝ
↔ ( < ∩ (ℝ ×
ℝ)) We ℝ) |
| 4 | | unipw 5455 |
. . . . . 6
⊢ ∪ 𝒫 ℝ = ℝ |
| 5 | | weeq2 5673 |
. . . . . 6
⊢ (∪ 𝒫 ℝ = ℝ → (( < ∩ (ℝ ×
ℝ)) We ∪ 𝒫 ℝ ↔ ( < ∩
(ℝ × ℝ)) We ℝ)) |
| 6 | 4, 5 | ax-mp 5 |
. . . . 5
⊢ (( < ∩
(ℝ × ℝ)) We ∪ 𝒫 ℝ
↔ ( < ∩ (ℝ ×
ℝ)) We ℝ) |
| 7 | 3, 6 | bitr4i 278 |
. . . 4
⊢ ( < We ℝ
↔ ( < ∩ (ℝ ×
ℝ)) We ∪ 𝒫 ℝ) |
| 8 | 1, 1 | xpex 7773 |
. . . . . 6
⊢ (ℝ
× ℝ) ∈ V |
| 9 | 8 | inex2 5318 |
. . . . 5
⊢ ( < ∩
(ℝ × ℝ)) ∈ V |
| 10 | | weeq1 5672 |
. . . . 5
⊢ (𝑥 = ( < ∩ (ℝ ×
ℝ)) → (𝑥 We
∪ 𝒫 ℝ ↔ ( < ∩ (ℝ ×
ℝ)) We ∪ 𝒫 ℝ)) |
| 11 | 9, 10 | spcev 3606 |
. . . 4
⊢ (( < ∩
(ℝ × ℝ)) We ∪ 𝒫 ℝ
→ ∃𝑥 𝑥 We ∪
𝒫 ℝ) |
| 12 | 7, 11 | sylbi 217 |
. . 3
⊢ ( < We ℝ
→ ∃𝑥 𝑥 We ∪
𝒫 ℝ) |
| 13 | | dfac8c 10073 |
. . 3
⊢
(𝒫 ℝ ∈ V → (∃𝑥 𝑥 We ∪ 𝒫
ℝ → ∃𝑓∀𝑧 ∈ 𝒫 ℝ(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
| 14 | 2, 12, 13 | mpsyl 68 |
. 2
⊢ ( < We ℝ
→ ∃𝑓∀𝑧 ∈ 𝒫 ℝ(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |
| 15 | | qex 13003 |
. . . . . . 7
⊢ ℚ
∈ V |
| 16 | 15 | inex1 5317 |
. . . . . 6
⊢ (ℚ
∩ (-1[,]1)) ∈ V |
| 17 | | nnrecq 13014 |
. . . . . . . 8
⊢ (𝑥 ∈ ℕ → (1 /
𝑥) ∈
ℚ) |
| 18 | | nnrecre 12308 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ → (1 /
𝑥) ∈
ℝ) |
| 19 | | neg1rr 12381 |
. . . . . . . . . . 11
⊢ -1 ∈
ℝ |
| 20 | 19 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → -1 ∈
ℝ) |
| 21 | | 0re 11263 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
| 22 | 21 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → 0 ∈
ℝ) |
| 23 | | neg1lt0 12383 |
. . . . . . . . . . . 12
⊢ -1 <
0 |
| 24 | 19, 21, 23 | ltleii 11384 |
. . . . . . . . . . 11
⊢ -1 ≤
0 |
| 25 | 24 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → -1 ≤
0) |
| 26 | | nnrp 13046 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℝ+) |
| 27 | 26 | rpreccld 13087 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ → (1 /
𝑥) ∈
ℝ+) |
| 28 | 27 | rpge0d 13081 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → 0 ≤ (1
/ 𝑥)) |
| 29 | 20, 22, 18, 25, 28 | letrd 11418 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ → -1 ≤
(1 / 𝑥)) |
| 30 | | nnge1 12294 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ → 1 ≤
𝑥) |
| 31 | | nnre 12273 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℝ) |
| 32 | | nngt0 12297 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℕ → 0 <
𝑥) |
| 33 | | 1re 11261 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
| 34 | | 0lt1 11785 |
. . . . . . . . . . . . 13
⊢ 0 <
1 |
| 35 | | lerec 12151 |
. . . . . . . . . . . . 13
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → (1 ≤ 𝑥 ↔ (1 / 𝑥) ≤ (1 / 1))) |
| 36 | 33, 34, 35 | mpanl12 702 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 0 <
𝑥) → (1 ≤ 𝑥 ↔ (1 / 𝑥) ≤ (1 / 1))) |
| 37 | 31, 32, 36 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ → (1 ≤
𝑥 ↔ (1 / 𝑥) ≤ (1 /
1))) |
| 38 | 30, 37 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → (1 /
𝑥) ≤ (1 /
1)) |
| 39 | | 1div1e1 11958 |
. . . . . . . . . 10
⊢ (1 / 1) =
1 |
| 40 | 38, 39 | breqtrdi 5184 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ → (1 /
𝑥) ≤ 1) |
| 41 | 19, 33 | elicc2i 13453 |
. . . . . . . . 9
⊢ ((1 /
𝑥) ∈ (-1[,]1) ↔
((1 / 𝑥) ∈ ℝ
∧ -1 ≤ (1 / 𝑥) ∧
(1 / 𝑥) ≤
1)) |
| 42 | 18, 29, 40, 41 | syl3anbrc 1344 |
. . . . . . . 8
⊢ (𝑥 ∈ ℕ → (1 /
𝑥) ∈
(-1[,]1)) |
| 43 | 17, 42 | elind 4200 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ → (1 /
𝑥) ∈ (ℚ ∩
(-1[,]1))) |
| 44 | | oveq2 7439 |
. . . . . . . . 9
⊢ ((1 /
𝑥) = (1 / 𝑦) → (1 / (1 / 𝑥)) = (1 / (1 / 𝑦))) |
| 45 | | nncn 12274 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℂ) |
| 46 | | nnne0 12300 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ → 𝑥 ≠ 0) |
| 47 | 45, 46 | recrecd 12040 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → (1 / (1 /
𝑥)) = 𝑥) |
| 48 | | nncn 12274 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
| 49 | | nnne0 12300 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → 𝑦 ≠ 0) |
| 50 | 48, 49 | recrecd 12040 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → (1 / (1 /
𝑦)) = 𝑦) |
| 51 | 47, 50 | eqeqan12d 2751 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((1 / (1
/ 𝑥)) = (1 / (1 / 𝑦)) ↔ 𝑥 = 𝑦)) |
| 52 | 44, 51 | imbitrid 244 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((1 /
𝑥) = (1 / 𝑦) → 𝑥 = 𝑦)) |
| 53 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (1 / 𝑥) = (1 / 𝑦)) |
| 54 | 52, 53 | impbid1 225 |
. . . . . . 7
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((1 /
𝑥) = (1 / 𝑦) ↔ 𝑥 = 𝑦)) |
| 55 | 43, 54 | dom2 9035 |
. . . . . 6
⊢ ((ℚ
∩ (-1[,]1)) ∈ V → ℕ ≼ (ℚ ∩
(-1[,]1))) |
| 56 | 16, 55 | ax-mp 5 |
. . . . 5
⊢ ℕ
≼ (ℚ ∩ (-1[,]1)) |
| 57 | | inss1 4237 |
. . . . . . 7
⊢ (ℚ
∩ (-1[,]1)) ⊆ ℚ |
| 58 | | ssdomg 9040 |
. . . . . . 7
⊢ (ℚ
∈ V → ((ℚ ∩ (-1[,]1)) ⊆ ℚ → (ℚ ∩
(-1[,]1)) ≼ ℚ)) |
| 59 | 15, 57, 58 | mp2 9 |
. . . . . 6
⊢ (ℚ
∩ (-1[,]1)) ≼ ℚ |
| 60 | | qnnen 16249 |
. . . . . 6
⊢ ℚ
≈ ℕ |
| 61 | | domentr 9053 |
. . . . . 6
⊢
(((ℚ ∩ (-1[,]1)) ≼ ℚ ∧ ℚ ≈
ℕ) → (ℚ ∩ (-1[,]1)) ≼ ℕ) |
| 62 | 59, 60, 61 | mp2an 692 |
. . . . 5
⊢ (ℚ
∩ (-1[,]1)) ≼ ℕ |
| 63 | | sbth 9133 |
. . . . 5
⊢ ((ℕ
≼ (ℚ ∩ (-1[,]1)) ∧ (ℚ ∩ (-1[,]1)) ≼
ℕ) → ℕ ≈ (ℚ ∩ (-1[,]1))) |
| 64 | 56, 62, 63 | mp2an 692 |
. . . 4
⊢ ℕ
≈ (ℚ ∩ (-1[,]1)) |
| 65 | | bren 8995 |
. . . 4
⊢ (ℕ
≈ (ℚ ∩ (-1[,]1)) ↔ ∃𝑔 𝑔:ℕ–1-1-onto→(ℚ ∩ (-1[,]1))) |
| 66 | 64, 65 | mpbi 230 |
. . 3
⊢
∃𝑔 𝑔:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) |
| 67 | | eleq1w 2824 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑥 → (𝑎 ∈ (0[,]1) ↔ 𝑥 ∈ (0[,]1))) |
| 68 | | eleq1w 2824 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑦 → (𝑏 ∈ (0[,]1) ↔ 𝑦 ∈ (0[,]1))) |
| 69 | 67, 68 | bi2anan9 638 |
. . . . . . . . . . . 12
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ↔ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)))) |
| 70 | | oveq12 7440 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → (𝑎 − 𝑏) = (𝑥 − 𝑦)) |
| 71 | 70 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → ((𝑎 − 𝑏) ∈ ℚ ↔ (𝑥 − 𝑦) ∈ ℚ)) |
| 72 | 69, 71 | anbi12d 632 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → (((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ) ↔ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ))) |
| 73 | 72 | cbvopabv 5216 |
. . . . . . . . . 10
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)} = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)} |
| 74 | | eqid 2737 |
. . . . . . . . . 10
⊢ ((0[,]1)
/ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) = ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) |
| 75 | | fvex 6919 |
. . . . . . . . . . . 12
⊢ (𝑓‘𝑐) ∈ V |
| 76 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)) = (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)) |
| 77 | 75, 76 | fnmpti 6711 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)) Fn ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) |
| 78 | 77 | a1i 11 |
. . . . . . . . . 10
⊢ ((( < 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 3003 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑤 → (𝑧 ≠ ∅ ↔ 𝑤 ≠ ∅)) |
| 80 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑤 → (𝑓‘𝑧) = (𝑓‘𝑤)) |
| 81 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑤 → 𝑧 = 𝑤) |
| 82 | 80, 81 | eleq12d 2835 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑤 → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘𝑤) ∈ 𝑤)) |
| 83 | 79, 82 | imbi12d 344 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑤 → ((𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ (𝑤 ≠ ∅ → (𝑓‘𝑤) ∈ 𝑤))) |
| 84 | 83 | cbvralvw 3237 |
. . . . . . . . . . . . 13
⊢
(∀𝑧 ∈
𝒫 ℝ(𝑧 ≠
∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∀𝑤 ∈ 𝒫 ℝ(𝑤 ≠ ∅ → (𝑓‘𝑤) ∈ 𝑤)) |
| 85 | 73 | vitalilem1 25643 |
. . . . . . . . . . . . . . . . . 18
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)} Er
(0[,]1) |
| 86 | 85 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (⊤
→ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)} Er
(0[,]1)) |
| 87 | 86 | qsss 8818 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ⊆ 𝒫
(0[,]1)) |
| 88 | 87 | mptru 1547 |
. . . . . . . . . . . . . . 15
⊢ ((0[,]1)
/ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ⊆ 𝒫
(0[,]1) |
| 89 | | unitssre 13539 |
. . . . . . . . . . . . . . . 16
⊢ (0[,]1)
⊆ ℝ |
| 90 | 89 | sspwi 4612 |
. . . . . . . . . . . . . . 15
⊢ 𝒫
(0[,]1) ⊆ 𝒫 ℝ |
| 91 | 88, 90 | sstri 3993 |
. . . . . . . . . . . . . 14
⊢ ((0[,]1)
/ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ⊆ 𝒫
ℝ |
| 92 | | ssralv 4052 |
. . . . . . . . . . . . . 14
⊢ (((0[,]1)
/ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ⊆ 𝒫 ℝ
→ (∀𝑤 ∈
𝒫 ℝ(𝑤 ≠
∅ → (𝑓‘𝑤) ∈ 𝑤) → ∀𝑤 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)})(𝑤 ≠ ∅ → (𝑓‘𝑤) ∈ 𝑤))) |
| 93 | 91, 92 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(∀𝑤 ∈
𝒫 ℝ(𝑤 ≠
∅ → (𝑓‘𝑤) ∈ 𝑤) → ∀𝑤 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)})(𝑤 ≠ ∅ → (𝑓‘𝑤) ∈ 𝑤)) |
| 94 | 84, 93 | sylbi 217 |
. . . . . . . . . . . 12
⊢
(∀𝑧 ∈
𝒫 ℝ(𝑧 ≠
∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑤 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)})(𝑤 ≠ ∅ → (𝑓‘𝑤) ∈ 𝑤)) |
| 95 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = 𝑤 → (𝑓‘𝑐) = (𝑓‘𝑤)) |
| 96 | | fvex 6919 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓‘𝑤) ∈ V |
| 97 | 95, 76, 96 | fvmpt 7016 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) → ((𝑐 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))‘𝑤) = (𝑓‘𝑤)) |
| 98 | 97 | eleq1d 2826 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) → (((𝑐 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))‘𝑤) ∈ 𝑤 ↔ (𝑓‘𝑤) ∈ 𝑤)) |
| 99 | 98 | imbi2d 340 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) → ((𝑤 ≠ ∅ → ((𝑐 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))‘𝑤) ∈ 𝑤) ↔ (𝑤 ≠ ∅ → (𝑓‘𝑤) ∈ 𝑤))) |
| 100 | 99 | ralbiia 3091 |
. . . . . . . . . . . 12
⊢
(∀𝑤 ∈
((0[,]1) / {〈𝑎,
𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)})(𝑤 ≠ ∅ → ((𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))‘𝑤) ∈ 𝑤) ↔ ∀𝑤 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)})(𝑤 ≠ ∅ → (𝑓‘𝑤) ∈ 𝑤)) |
| 101 | 94, 100 | sylibr 234 |
. . . . . . . . . . 11
⊢
(∀𝑧 ∈
𝒫 ℝ(𝑧 ≠
∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑤 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)})(𝑤 ≠ ∅ → ((𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))‘𝑤) ∈ 𝑤)) |
| 102 | 101 | ad2antlr 727 |
. . . . . . . . . 10
⊢ ((( < 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 771 |
. . . . . . . . . 10
⊢ ((( < We ℝ
∧ ∀𝑧 ∈
𝒫 ℝ(𝑧 ≠
∅ → (𝑓‘𝑧) ∈ 𝑧)) ∧ (𝑔:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) ∧ ¬ ran
(𝑐 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)) ∈ (𝒫 ℝ ∖ dom
vol))) → 𝑔:ℕ–1-1-onto→(ℚ ∩ (-1[,]1))) |
| 104 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑠 → (𝑡 − (𝑔‘𝑚)) = (𝑠 − (𝑔‘𝑚))) |
| 105 | 104 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑠 → ((𝑡 − (𝑔‘𝑚)) ∈ ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)) ↔ (𝑠 − (𝑔‘𝑚)) ∈ ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)))) |
| 106 | 105 | cbvrabv 3447 |
. . . . . . . . . . . 12
⊢ {𝑡 ∈ ℝ ∣ (𝑡 − (𝑔‘𝑚)) ∈ ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝑔‘𝑚)) ∈ ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))} |
| 107 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑛 → (𝑔‘𝑚) = (𝑔‘𝑛)) |
| 108 | 107 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (𝑠 − (𝑔‘𝑚)) = (𝑠 − (𝑔‘𝑛))) |
| 109 | 108 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → ((𝑠 − (𝑔‘𝑚)) ∈ ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)) ↔ (𝑠 − (𝑔‘𝑛)) ∈ ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)))) |
| 110 | 109 | rabbidv 3444 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → {𝑠 ∈ ℝ ∣ (𝑠 − (𝑔‘𝑚)) ∈ ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝑔‘𝑛)) ∈ ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))}) |
| 111 | 106, 110 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → {𝑡 ∈ ℝ ∣ (𝑡 − (𝑔‘𝑚)) ∈ ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝑔‘𝑛)) ∈ ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))}) |
| 112 | 111 | cbvmptv 5255 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ ↦ {𝑡 ∈ ℝ ∣ (𝑡 − (𝑔‘𝑚)) ∈ ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))}) = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝑔‘𝑛)) ∈ ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))}) |
| 113 | | simprr 773 |
. . . . . . . . . 10
⊢ ((( < 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 25647 |
. . . . . . . . 9
⊢ ¬ ((
< We
ℝ ∧ ∀𝑧
∈ 𝒫 ℝ(𝑧
≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) ∧ (𝑔:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) ∧ ¬ ran
(𝑐 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)) ∈ (𝒫 ℝ ∖ dom
vol))) |
| 115 | 114 | pm2.21i 119 |
. . . . . . . 8
⊢ ((( < 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 456 |
. . . . . . 7
⊢ ((( < 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 127 |
. . . . . 6
⊢ ((( < We ℝ
∧ ∀𝑧 ∈
𝒫 ℝ(𝑧 ≠
∅ → (𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑔:ℕ–1-1-onto→(ℚ ∩ (-1[,]1))) → ran (𝑐 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)) ∈ (𝒫 ℝ ∖ dom
vol)) |
| 118 | | eldif 3961 |
. . . . . . 7
⊢ (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 25566 |
. . . . . . . . . 10
⊢ (𝑥 ∈ dom vol → 𝑥 ⊆
ℝ) |
| 120 | | velpw 4605 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝒫 ℝ ↔
𝑥 ⊆
ℝ) |
| 121 | 119, 120 | sylibr 234 |
. . . . . . . . 9
⊢ (𝑥 ∈ dom vol → 𝑥 ∈ 𝒫
ℝ) |
| 122 | 121 | ssriv 3987 |
. . . . . . . 8
⊢ dom vol
⊆ 𝒫 ℝ |
| 123 | | ssnelpss 4114 |
. . . . . . . 8
⊢ (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 5 |
. . . . . . 7
⊢ ((ran
(𝑐 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)) ∈ 𝒫 ℝ ∧ ¬ ran
(𝑐 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)) ∈ dom vol) → dom vol ⊊
𝒫 ℝ) |
| 125 | 118, 124 | sylbi 217 |
. . . . . 6
⊢ (ran
(𝑐 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)) ∈ (𝒫 ℝ ∖ dom vol)
→ dom vol ⊊ 𝒫 ℝ) |
| 126 | 117, 125 | syl 17 |
. . . . 5
⊢ ((( < We ℝ
∧ ∀𝑧 ∈
𝒫 ℝ(𝑧 ≠
∅ → (𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑔:ℕ–1-1-onto→(ℚ ∩ (-1[,]1))) → dom vol
⊊ 𝒫 ℝ) |
| 127 | 126 | ex 412 |
. . . 4
⊢ (( < We ℝ
∧ ∀𝑧 ∈
𝒫 ℝ(𝑧 ≠
∅ → (𝑓‘𝑧) ∈ 𝑧)) → (𝑔:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → dom vol
⊊ 𝒫 ℝ)) |
| 128 | 127 | exlimdv 1933 |
. . 3
⊢ (( < We ℝ
∧ ∀𝑧 ∈
𝒫 ℝ(𝑧 ≠
∅ → (𝑓‘𝑧) ∈ 𝑧)) → (∃𝑔 𝑔:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → dom vol
⊊ 𝒫 ℝ)) |
| 129 | 66, 128 | mpi 20 |
. 2
⊢ (( < We ℝ
∧ ∀𝑧 ∈
𝒫 ℝ(𝑧 ≠
∅ → (𝑓‘𝑧) ∈ 𝑧)) → dom vol ⊊ 𝒫
ℝ) |
| 130 | 14, 129 | exlimddv 1935 |
1
⊢ ( < We ℝ
→ dom vol ⊊ 𝒫 ℝ) |