Step | Hyp | Ref
| Expression |
1 | | reex 9906 |
. . . 4
⊢ ℝ
∈ V |
2 | 1 | pwex 4774 |
. . 3
⊢ 𝒫
ℝ ∈ V |
3 | | weinxp 5109 |
. . . . 5
⊢ ( < We ℝ
↔ ( < ∩ (ℝ ×
ℝ)) We ℝ) |
4 | | unipw 4845 |
. . . . . 6
⊢ ∪ 𝒫 ℝ = ℝ |
5 | | weeq2 5027 |
. . . . . 6
⊢ (∪ 𝒫 ℝ = ℝ → (( < ∩ (ℝ ×
ℝ)) We ∪ 𝒫 ℝ ↔ ( < ∩
(ℝ × ℝ)) We ℝ)) |
6 | 4, 5 | ax-mp 5 |
. . . . 5
⊢ (( < ∩
(ℝ × ℝ)) We ∪ 𝒫 ℝ
↔ ( < ∩ (ℝ ×
ℝ)) We ℝ) |
7 | 3, 6 | bitr4i 266 |
. . . 4
⊢ ( < We ℝ
↔ ( < ∩ (ℝ ×
ℝ)) We ∪ 𝒫 ℝ) |
8 | 1, 1 | xpex 6860 |
. . . . . 6
⊢ (ℝ
× ℝ) ∈ V |
9 | 8 | inex2 4728 |
. . . . 5
⊢ ( < ∩
(ℝ × ℝ)) ∈ V |
10 | | weeq1 5026 |
. . . . 5
⊢ (𝑥 = ( < ∩ (ℝ ×
ℝ)) → (𝑥 We
∪ 𝒫 ℝ ↔ ( < ∩ (ℝ ×
ℝ)) We ∪ 𝒫 ℝ)) |
11 | 9, 10 | spcev 3273 |
. . . 4
⊢ (( < ∩
(ℝ × ℝ)) We ∪ 𝒫 ℝ
→ ∃𝑥 𝑥 We ∪
𝒫 ℝ) |
12 | 7, 11 | sylbi 206 |
. . 3
⊢ ( < We ℝ
→ ∃𝑥 𝑥 We ∪
𝒫 ℝ) |
13 | | dfac8c 8739 |
. . 3
⊢
(𝒫 ℝ ∈ V → (∃𝑥 𝑥 We ∪ 𝒫
ℝ → ∃𝑓∀𝑧 ∈ 𝒫 ℝ(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) |
14 | 2, 12, 13 | mpsyl 66 |
. 2
⊢ ( < We ℝ
→ ∃𝑓∀𝑧 ∈ 𝒫 ℝ(𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) |
15 | | qex 11676 |
. . . . . . 7
⊢ ℚ
∈ V |
16 | 15 | inex1 4727 |
. . . . . 6
⊢ (ℚ
∩ (-1[,]1)) ∈ V |
17 | | nnrecq 11687 |
. . . . . . . 8
⊢ (𝑥 ∈ ℕ → (1 /
𝑥) ∈
ℚ) |
18 | | nnrecre 10934 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ → (1 /
𝑥) ∈
ℝ) |
19 | | neg1rr 11002 |
. . . . . . . . . . 11
⊢ -1 ∈
ℝ |
20 | 19 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → -1 ∈
ℝ) |
21 | | 0re 9919 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
22 | 21 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → 0 ∈
ℝ) |
23 | | neg1lt0 11004 |
. . . . . . . . . . . 12
⊢ -1 <
0 |
24 | 19, 21, 23 | ltleii 10039 |
. . . . . . . . . . 11
⊢ -1 ≤
0 |
25 | 24 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → -1 ≤
0) |
26 | | nnrp 11718 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℝ+) |
27 | 26 | rpreccld 11758 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ → (1 /
𝑥) ∈
ℝ+) |
28 | 27 | rpge0d 11752 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → 0 ≤ (1
/ 𝑥)) |
29 | 20, 22, 18, 25, 28 | letrd 10073 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ → -1 ≤
(1 / 𝑥)) |
30 | | nnge1 10923 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ → 1 ≤
𝑥) |
31 | | nnre 10904 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℝ) |
32 | | nngt0 10926 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℕ → 0 <
𝑥) |
33 | | 1re 9918 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
34 | | 0lt1 10429 |
. . . . . . . . . . . . 13
⊢ 0 <
1 |
35 | | lerec 10785 |
. . . . . . . . . . . . 13
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → (1 ≤ 𝑥 ↔ (1 / 𝑥) ≤ (1 / 1))) |
36 | 33, 34, 35 | mpanl12 714 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 0 <
𝑥) → (1 ≤ 𝑥 ↔ (1 / 𝑥) ≤ (1 / 1))) |
37 | 31, 32, 36 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ → (1 ≤
𝑥 ↔ (1 / 𝑥) ≤ (1 /
1))) |
38 | 30, 37 | mpbid 221 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → (1 /
𝑥) ≤ (1 /
1)) |
39 | | 1div1e1 10596 |
. . . . . . . . . 10
⊢ (1 / 1) =
1 |
40 | 38, 39 | syl6breq 4624 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ → (1 /
𝑥) ≤ 1) |
41 | 19, 33 | elicc2i 12110 |
. . . . . . . . 9
⊢ ((1 /
𝑥) ∈ (-1[,]1) ↔
((1 / 𝑥) ∈ ℝ
∧ -1 ≤ (1 / 𝑥) ∧
(1 / 𝑥) ≤
1)) |
42 | 18, 29, 40, 41 | syl3anbrc 1239 |
. . . . . . . 8
⊢ (𝑥 ∈ ℕ → (1 /
𝑥) ∈
(-1[,]1)) |
43 | 17, 42 | elind 3760 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ → (1 /
𝑥) ∈ (ℚ ∩
(-1[,]1))) |
44 | | oveq2 6557 |
. . . . . . . . 9
⊢ ((1 /
𝑥) = (1 / 𝑦) → (1 / (1 / 𝑥)) = (1 / (1 / 𝑦))) |
45 | | nncn 10905 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℂ) |
46 | | nnne0 10930 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ → 𝑥 ≠ 0) |
47 | 45, 46 | recrecd 10677 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → (1 / (1 /
𝑥)) = 𝑥) |
48 | | nncn 10905 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
49 | | nnne0 10930 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → 𝑦 ≠ 0) |
50 | 48, 49 | recrecd 10677 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → (1 / (1 /
𝑦)) = 𝑦) |
51 | 47, 50 | eqeqan12d 2626 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((1 / (1
/ 𝑥)) = (1 / (1 / 𝑦)) ↔ 𝑥 = 𝑦)) |
52 | 44, 51 | syl5ib 233 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((1 /
𝑥) = (1 / 𝑦) → 𝑥 = 𝑦)) |
53 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (1 / 𝑥) = (1 / 𝑦)) |
54 | 52, 53 | impbid1 214 |
. . . . . . 7
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((1 /
𝑥) = (1 / 𝑦) ↔ 𝑥 = 𝑦)) |
55 | 43, 54 | dom2 7884 |
. . . . . 6
⊢ ((ℚ
∩ (-1[,]1)) ∈ V → ℕ ≼ (ℚ ∩
(-1[,]1))) |
56 | 16, 55 | ax-mp 5 |
. . . . 5
⊢ ℕ
≼ (ℚ ∩ (-1[,]1)) |
57 | | inss1 3795 |
. . . . . . 7
⊢ (ℚ
∩ (-1[,]1)) ⊆ ℚ |
58 | | ssdomg 7887 |
. . . . . . 7
⊢ (ℚ
∈ V → ((ℚ ∩ (-1[,]1)) ⊆ ℚ → (ℚ ∩
(-1[,]1)) ≼ ℚ)) |
59 | 15, 57, 58 | mp2 9 |
. . . . . 6
⊢ (ℚ
∩ (-1[,]1)) ≼ ℚ |
60 | | qnnen 14781 |
. . . . . 6
⊢ ℚ
≈ ℕ |
61 | | domentr 7901 |
. . . . . 6
⊢
(((ℚ ∩ (-1[,]1)) ≼ ℚ ∧ ℚ ≈
ℕ) → (ℚ ∩ (-1[,]1)) ≼ ℕ) |
62 | 59, 60, 61 | mp2an 704 |
. . . . 5
⊢ (ℚ
∩ (-1[,]1)) ≼ ℕ |
63 | | sbth 7965 |
. . . . 5
⊢ ((ℕ
≼ (ℚ ∩ (-1[,]1)) ∧ (ℚ ∩ (-1[,]1)) ≼
ℕ) → ℕ ≈ (ℚ ∩ (-1[,]1))) |
64 | 56, 62, 63 | mp2an 704 |
. . . 4
⊢ ℕ
≈ (ℚ ∩ (-1[,]1)) |
65 | | bren 7850 |
. . . 4
⊢ (ℕ
≈ (ℚ ∩ (-1[,]1)) ↔ ∃𝑔 𝑔:ℕ–1-1-onto→(ℚ ∩ (-1[,]1))) |
66 | 64, 65 | mpbi 219 |
. . 3
⊢
∃𝑔 𝑔:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) |
67 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑥 → (𝑎 ∈ (0[,]1) ↔ 𝑥 ∈ (0[,]1))) |
68 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑦 → (𝑏 ∈ (0[,]1) ↔ 𝑦 ∈ (0[,]1))) |
69 | 67, 68 | bi2anan9 913 |
. . . . . . . . . . . 12
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ↔ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)))) |
70 | | oveq12 6558 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → (𝑎 − 𝑏) = (𝑥 − 𝑦)) |
71 | 70 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → ((𝑎 − 𝑏) ∈ ℚ ↔ (𝑥 − 𝑦) ∈ ℚ)) |
72 | 69, 71 | anbi12d 743 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → (((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ) ↔ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ))) |
73 | 72 | cbvopabv 4654 |
. . . . . . . . . 10
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)} = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)} |
74 | | eqid 2610 |
. . . . . . . . . 10
⊢ ((0[,]1)
/ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) = ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) |
75 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ (𝑓‘𝑐) ∈ V |
76 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)) = (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)) |
77 | 75, 76 | fnmpti 5935 |
. . . . . . . . . . 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 2844 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑤 → (𝑧 ≠ ∅ ↔ 𝑤 ≠ ∅)) |
80 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑤 → (𝑓‘𝑧) = (𝑓‘𝑤)) |
81 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑤 → 𝑧 = 𝑤) |
82 | 80, 81 | eleq12d 2682 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑤 → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘𝑤) ∈ 𝑤)) |
83 | 79, 82 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑤 → ((𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ (𝑤 ≠ ∅ → (𝑓‘𝑤) ∈ 𝑤))) |
84 | 83 | cbvralv 3147 |
. . . . . . . . . . . . 13
⊢
(∀𝑧 ∈
𝒫 ℝ(𝑧 ≠
∅ → (𝑓‘𝑧) ∈ 𝑧) ↔ ∀𝑤 ∈ 𝒫 ℝ(𝑤 ≠ ∅ → (𝑓‘𝑤) ∈ 𝑤)) |
85 | 73 | vitalilem1 23182 |
. . . . . . . . . . . . . . . . . 18
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)} Er
(0[,]1) |
86 | 85 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (⊤
→ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)} Er
(0[,]1)) |
87 | 86 | qsss 7695 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ⊆ 𝒫
(0[,]1)) |
88 | 87 | trud 1484 |
. . . . . . . . . . . . . . 15
⊢ ((0[,]1)
/ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ⊆ 𝒫
(0[,]1) |
89 | | unitssre 12190 |
. . . . . . . . . . . . . . . 16
⊢ (0[,]1)
⊆ ℝ |
90 | | sspwb 4844 |
. . . . . . . . . . . . . . . 16
⊢ ((0[,]1)
⊆ ℝ ↔ 𝒫 (0[,]1) ⊆ 𝒫
ℝ) |
91 | 89, 90 | mpbi 219 |
. . . . . . . . . . . . . . 15
⊢ 𝒫
(0[,]1) ⊆ 𝒫 ℝ |
92 | 88, 91 | sstri 3577 |
. . . . . . . . . . . . . 14
⊢ ((0[,]1)
/ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ⊆ 𝒫
ℝ |
93 | | ssralv 3629 |
. . . . . . . . . . . . . 14
⊢ (((0[,]1)
/ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ⊆ 𝒫 ℝ
→ (∀𝑤 ∈
𝒫 ℝ(𝑤 ≠
∅ → (𝑓‘𝑤) ∈ 𝑤) → ∀𝑤 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)})(𝑤 ≠ ∅ → (𝑓‘𝑤) ∈ 𝑤))) |
94 | 92, 93 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(∀𝑤 ∈
𝒫 ℝ(𝑤 ≠
∅ → (𝑓‘𝑤) ∈ 𝑤) → ∀𝑤 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)})(𝑤 ≠ ∅ → (𝑓‘𝑤) ∈ 𝑤)) |
95 | 84, 94 | sylbi 206 |
. . . . . . . . . . . 12
⊢
(∀𝑧 ∈
𝒫 ℝ(𝑧 ≠
∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑤 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)})(𝑤 ≠ ∅ → (𝑓‘𝑤) ∈ 𝑤)) |
96 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = 𝑤 → (𝑓‘𝑐) = (𝑓‘𝑤)) |
97 | | fvex 6113 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓‘𝑤) ∈ V |
98 | 96, 76, 97 | fvmpt 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) → ((𝑐 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))‘𝑤) = (𝑓‘𝑤)) |
99 | 98 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) → (((𝑐 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))‘𝑤) ∈ 𝑤 ↔ (𝑓‘𝑤) ∈ 𝑤)) |
100 | 99 | imbi2d 329 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) → ((𝑤 ≠ ∅ → ((𝑐 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))‘𝑤) ∈ 𝑤) ↔ (𝑤 ≠ ∅ → (𝑓‘𝑤) ∈ 𝑤))) |
101 | 100 | ralbiia 2962 |
. . . . . . . . . . . 12
⊢
(∀𝑤 ∈
((0[,]1) / {〈𝑎,
𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)})(𝑤 ≠ ∅ → ((𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))‘𝑤) ∈ 𝑤) ↔ ∀𝑤 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)})(𝑤 ≠ ∅ → (𝑓‘𝑤) ∈ 𝑤)) |
102 | 95, 101 | sylibr 223 |
. . . . . . . . . . 11
⊢
(∀𝑧 ∈
𝒫 ℝ(𝑧 ≠
∅ → (𝑓‘𝑧) ∈ 𝑧) → ∀𝑤 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)})(𝑤 ≠ ∅ → ((𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))‘𝑤) ∈ 𝑤)) |
103 | 102 | ad2antlr 759 |
. . . . . . . . . 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)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))‘𝑤) ∈ 𝑤)) |
104 | | simprl 790 |
. . . . . . . . . 10
⊢ ((( < We ℝ
∧ ∀𝑧 ∈
𝒫 ℝ(𝑧 ≠
∅ → (𝑓‘𝑧) ∈ 𝑧)) ∧ (𝑔:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) ∧ ¬ ran
(𝑐 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)) ∈ (𝒫 ℝ ∖ dom
vol))) → 𝑔:ℕ–1-1-onto→(ℚ ∩ (-1[,]1))) |
105 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑠 → (𝑡 − (𝑔‘𝑚)) = (𝑠 − (𝑔‘𝑚))) |
106 | 105 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑠 → ((𝑡 − (𝑔‘𝑚)) ∈ ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)) ↔ (𝑠 − (𝑔‘𝑚)) ∈ ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)))) |
107 | 106 | cbvrabv 3172 |
. . . . . . . . . . . 12
⊢ {𝑡 ∈ ℝ ∣ (𝑡 − (𝑔‘𝑚)) ∈ ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝑔‘𝑚)) ∈ ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))} |
108 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑛 → (𝑔‘𝑚) = (𝑔‘𝑛)) |
109 | 108 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (𝑠 − (𝑔‘𝑚)) = (𝑠 − (𝑔‘𝑛))) |
110 | 109 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → ((𝑠 − (𝑔‘𝑚)) ∈ ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)) ↔ (𝑠 − (𝑔‘𝑛)) ∈ ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)))) |
111 | 110 | rabbidv 3164 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → {𝑠 ∈ ℝ ∣ (𝑠 − (𝑔‘𝑚)) ∈ ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝑔‘𝑛)) ∈ ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))}) |
112 | 107, 111 | syl5eq 2656 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → {𝑡 ∈ ℝ ∣ (𝑡 − (𝑔‘𝑚)) ∈ ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝑔‘𝑛)) ∈ ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))}) |
113 | 112 | cbvmptv 4678 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ ↦ {𝑡 ∈ ℝ ∣ (𝑡 − (𝑔‘𝑚)) ∈ ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))}) = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝑔‘𝑛)) ∈ ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐))}) |
114 | | simprr 792 |
. . . . . . . . . 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)) |
115 | 73, 74, 78, 103, 104, 113, 114 | vitalilem5 23187 |
. . . . . . . . 9
⊢ ¬ ((
< We
ℝ ∧ ∀𝑧
∈ 𝒫 ℝ(𝑧
≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) ∧ (𝑔:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) ∧ ¬ ran
(𝑐 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)) ∈ (𝒫 ℝ ∖ dom
vol))) |
116 | 115 | pm2.21i 115 |
. . . . . . . 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)) |
117 | 116 | expr 641 |
. . . . . . 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))) |
118 | 117 | pm2.18d 123 |
. . . . . 6
⊢ ((( < We ℝ
∧ ∀𝑧 ∈
𝒫 ℝ(𝑧 ≠
∅ → (𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑔:ℕ–1-1-onto→(ℚ ∩ (-1[,]1))) → ran (𝑐 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)) ∈ (𝒫 ℝ ∖ dom
vol)) |
119 | | eldif 3550 |
. . . . . . 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)) |
120 | | mblss 23106 |
. . . . . . . . . 10
⊢ (𝑥 ∈ dom vol → 𝑥 ⊆
ℝ) |
121 | | selpw 4115 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝒫 ℝ ↔
𝑥 ⊆
ℝ) |
122 | 120, 121 | sylibr 223 |
. . . . . . . . 9
⊢ (𝑥 ∈ dom vol → 𝑥 ∈ 𝒫
ℝ) |
123 | 122 | ssriv 3572 |
. . . . . . . 8
⊢ dom vol
⊆ 𝒫 ℝ |
124 | | ssnelpss 3680 |
. . . . . . . 8
⊢ (dom vol
⊆ 𝒫 ℝ → ((ran (𝑐 ∈ ((0[,]1) / {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)) ∈ 𝒫 ℝ ∧ ¬ ran
(𝑐 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)) ∈ dom vol) → dom vol ⊊
𝒫 ℝ)) |
125 | 123, 124 | ax-mp 5 |
. . . . . . 7
⊢ ((ran
(𝑐 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)) ∈ 𝒫 ℝ ∧ ¬ ran
(𝑐 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)) ∈ dom vol) → dom vol ⊊
𝒫 ℝ) |
126 | 119, 125 | sylbi 206 |
. . . . . 6
⊢ (ran
(𝑐 ∈ ((0[,]1) /
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (0[,]1) ∧ 𝑏 ∈ (0[,]1)) ∧ (𝑎 − 𝑏) ∈ ℚ)}) ↦ (𝑓‘𝑐)) ∈ (𝒫 ℝ ∖ dom vol)
→ dom vol ⊊ 𝒫 ℝ) |
127 | 118, 126 | syl 17 |
. . . . 5
⊢ ((( < We ℝ
∧ ∀𝑧 ∈
𝒫 ℝ(𝑧 ≠
∅ → (𝑓‘𝑧) ∈ 𝑧)) ∧ 𝑔:ℕ–1-1-onto→(ℚ ∩ (-1[,]1))) → dom vol
⊊ 𝒫 ℝ) |
128 | 127 | ex 449 |
. . . 4
⊢ (( < We ℝ
∧ ∀𝑧 ∈
𝒫 ℝ(𝑧 ≠
∅ → (𝑓‘𝑧) ∈ 𝑧)) → (𝑔:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → dom vol
⊊ 𝒫 ℝ)) |
129 | 128 | exlimdv 1848 |
. . 3
⊢ (( < We ℝ
∧ ∀𝑧 ∈
𝒫 ℝ(𝑧 ≠
∅ → (𝑓‘𝑧) ∈ 𝑧)) → (∃𝑔 𝑔:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → dom vol
⊊ 𝒫 ℝ)) |
130 | 66, 129 | mpi 20 |
. 2
⊢ (( < We ℝ
∧ ∀𝑧 ∈
𝒫 ℝ(𝑧 ≠
∅ → (𝑓‘𝑧) ∈ 𝑧)) → dom vol ⊊ 𝒫
ℝ) |
131 | 14, 130 | exlimddv 1850 |
1
⊢ ( < We ℝ
→ dom vol ⊊ 𝒫 ℝ) |