Step | Hyp | Ref
| Expression |
1 | | unissb 4853 |
. . 3
⊢ (∪ ran 𝑅 ⊆ (ℝ × ℝ) ↔
∀𝑑 ∈ ran 𝑅 𝑑 ⊆ (ℝ ×
ℝ)) |
2 | | dya2ioc.2 |
. . . . 5
⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣)) |
3 | | vex 3412 |
. . . . . 6
⊢ 𝑢 ∈ V |
4 | | vex 3412 |
. . . . . 6
⊢ 𝑣 ∈ V |
5 | 3, 4 | xpex 7538 |
. . . . 5
⊢ (𝑢 × 𝑣) ∈ V |
6 | 2, 5 | elrnmpo 7346 |
. . . 4
⊢ (𝑑 ∈ ran 𝑅 ↔ ∃𝑢 ∈ ran 𝐼∃𝑣 ∈ ran 𝐼 𝑑 = (𝑢 × 𝑣)) |
7 | | simpr 488 |
. . . . . . 7
⊢ (((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) ∧ 𝑑 = (𝑢 × 𝑣)) → 𝑑 = (𝑢 × 𝑣)) |
8 | | pwssb 5009 |
. . . . . . . . . . . 12
⊢ (ran
𝐼 ⊆ 𝒫 ℝ
↔ ∀𝑑 ∈ ran
𝐼 𝑑 ⊆ ℝ) |
9 | | dya2ioc.1 |
. . . . . . . . . . . . . 14
⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) |
10 | | ovex 7246 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) ∈ V |
11 | 9, 10 | elrnmpo 7346 |
. . . . . . . . . . . . 13
⊢ (𝑑 ∈ ran 𝐼 ↔ ∃𝑥 ∈ ℤ ∃𝑛 ∈ ℤ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) |
12 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) |
13 | | simpll 767 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → 𝑥 ∈ ℤ) |
14 | 13 | zred 12282 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → 𝑥 ∈ ℝ) |
15 | | 2re 11904 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℝ |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → 2 ∈
ℝ) |
17 | | 2ne0 11934 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ≠
0 |
18 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → 2 ≠ 0) |
19 | | simplr 769 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → 𝑛 ∈ ℤ) |
20 | 16, 18, 19 | reexpclzd 13816 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → (2↑𝑛) ∈ ℝ) |
21 | | 2cnd 11908 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → 2 ∈
ℂ) |
22 | 21, 18, 19 | expne0d 13722 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → (2↑𝑛) ≠ 0) |
23 | 14, 20, 22 | redivcld 11660 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → (𝑥 / (2↑𝑛)) ∈ ℝ) |
24 | | 1red 10834 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → 1 ∈
ℝ) |
25 | 14, 24 | readdcld 10862 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → (𝑥 + 1) ∈ ℝ) |
26 | 25, 20, 22 | redivcld 11660 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → ((𝑥 + 1) / (2↑𝑛)) ∈ ℝ) |
27 | 26 | rexrd 10883 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → ((𝑥 + 1) / (2↑𝑛)) ∈
ℝ*) |
28 | | icossre 13016 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 / (2↑𝑛)) ∈ ℝ ∧ ((𝑥 + 1) / (2↑𝑛)) ∈ ℝ*) → ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) ⊆ ℝ) |
29 | 23, 27, 28 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) ⊆ ℝ) |
30 | 12, 29 | eqsstrd 3939 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → 𝑑 ⊆ ℝ) |
31 | 30 | ex 416 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) → 𝑑 ⊆ ℝ)) |
32 | 31 | rexlimivv 3211 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
ℤ ∃𝑛 ∈
ℤ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) → 𝑑 ⊆ ℝ) |
33 | 11, 32 | sylbi 220 |
. . . . . . . . . . . 12
⊢ (𝑑 ∈ ran 𝐼 → 𝑑 ⊆ ℝ) |
34 | 8, 33 | mprgbir 3076 |
. . . . . . . . . . 11
⊢ ran 𝐼 ⊆ 𝒫
ℝ |
35 | 34 | sseli 3896 |
. . . . . . . . . 10
⊢ (𝑢 ∈ ran 𝐼 → 𝑢 ∈ 𝒫 ℝ) |
36 | 35 | elpwid 4524 |
. . . . . . . . 9
⊢ (𝑢 ∈ ran 𝐼 → 𝑢 ⊆ ℝ) |
37 | 34 | sseli 3896 |
. . . . . . . . . 10
⊢ (𝑣 ∈ ran 𝐼 → 𝑣 ∈ 𝒫 ℝ) |
38 | 37 | elpwid 4524 |
. . . . . . . . 9
⊢ (𝑣 ∈ ran 𝐼 → 𝑣 ⊆ ℝ) |
39 | | xpss12 5566 |
. . . . . . . . 9
⊢ ((𝑢 ⊆ ℝ ∧ 𝑣 ⊆ ℝ) → (𝑢 × 𝑣) ⊆ (ℝ ×
ℝ)) |
40 | 36, 38, 39 | syl2an 599 |
. . . . . . . 8
⊢ ((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) → (𝑢 × 𝑣) ⊆ (ℝ ×
ℝ)) |
41 | 40 | adantr 484 |
. . . . . . 7
⊢ (((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) ∧ 𝑑 = (𝑢 × 𝑣)) → (𝑢 × 𝑣) ⊆ (ℝ ×
ℝ)) |
42 | 7, 41 | eqsstrd 3939 |
. . . . . 6
⊢ (((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) ∧ 𝑑 = (𝑢 × 𝑣)) → 𝑑 ⊆ (ℝ ×
ℝ)) |
43 | 42 | ex 416 |
. . . . 5
⊢ ((𝑢 ∈ ran 𝐼 ∧ 𝑣 ∈ ran 𝐼) → (𝑑 = (𝑢 × 𝑣) → 𝑑 ⊆ (ℝ ×
ℝ))) |
44 | 43 | rexlimivv 3211 |
. . . 4
⊢
(∃𝑢 ∈ ran
𝐼∃𝑣 ∈ ran 𝐼 𝑑 = (𝑢 × 𝑣) → 𝑑 ⊆ (ℝ ×
ℝ)) |
45 | 6, 44 | sylbi 220 |
. . 3
⊢ (𝑑 ∈ ran 𝑅 → 𝑑 ⊆ (ℝ ×
ℝ)) |
46 | 1, 45 | mprgbir 3076 |
. 2
⊢ ∪ ran 𝑅 ⊆ (ℝ ×
ℝ) |
47 | | sxbrsiga.0 |
. . . . . 6
⊢ 𝐽 = (topGen‘ran
(,)) |
48 | | retop 23659 |
. . . . . 6
⊢
(topGen‘ran (,)) ∈ Top |
49 | 47, 48 | eqeltri 2834 |
. . . . 5
⊢ 𝐽 ∈ Top |
50 | 49, 49 | txtopi 22487 |
. . . 4
⊢ (𝐽 ×t 𝐽) ∈ Top |
51 | | uniretop 23660 |
. . . . . . 7
⊢ ℝ =
∪ (topGen‘ran (,)) |
52 | 47 | unieqi 4832 |
. . . . . . 7
⊢ ∪ 𝐽 =
∪ (topGen‘ran (,)) |
53 | 51, 52 | eqtr4i 2768 |
. . . . . 6
⊢ ℝ =
∪ 𝐽 |
54 | 49, 49, 53, 53 | txunii 22490 |
. . . . 5
⊢ (ℝ
× ℝ) = ∪ (𝐽 ×t 𝐽) |
55 | 54 | topopn 21803 |
. . . 4
⊢ ((𝐽 ×t 𝐽) ∈ Top → (ℝ
× ℝ) ∈ (𝐽
×t 𝐽)) |
56 | 47, 9, 2 | dya2iocuni 31962 |
. . . 4
⊢ ((ℝ
× ℝ) ∈ (𝐽
×t 𝐽)
→ ∃𝑐 ∈
𝒫 ran 𝑅∪ 𝑐 =
(ℝ × ℝ)) |
57 | 50, 55, 56 | mp2b 10 |
. . 3
⊢
∃𝑐 ∈
𝒫 ran 𝑅∪ 𝑐 =
(ℝ × ℝ) |
58 | | simpr 488 |
. . . . 5
⊢ ((𝑐 ∈ 𝒫 ran 𝑅 ∧ ∪ 𝑐 =
(ℝ × ℝ)) → ∪ 𝑐 = (ℝ ×
ℝ)) |
59 | | elpwi 4522 |
. . . . . . 7
⊢ (𝑐 ∈ 𝒫 ran 𝑅 → 𝑐 ⊆ ran 𝑅) |
60 | 59 | adantr 484 |
. . . . . 6
⊢ ((𝑐 ∈ 𝒫 ran 𝑅 ∧ ∪ 𝑐 =
(ℝ × ℝ)) → 𝑐 ⊆ ran 𝑅) |
61 | 60 | unissd 4829 |
. . . . 5
⊢ ((𝑐 ∈ 𝒫 ran 𝑅 ∧ ∪ 𝑐 =
(ℝ × ℝ)) → ∪ 𝑐 ⊆ ∪ ran 𝑅) |
62 | 58, 61 | eqsstrrd 3940 |
. . . 4
⊢ ((𝑐 ∈ 𝒫 ran 𝑅 ∧ ∪ 𝑐 =
(ℝ × ℝ)) → (ℝ × ℝ) ⊆ ∪ ran 𝑅) |
63 | 62 | rexlimiva 3200 |
. . 3
⊢
(∃𝑐 ∈
𝒫 ran 𝑅∪ 𝑐 =
(ℝ × ℝ) → (ℝ × ℝ) ⊆ ∪ ran 𝑅) |
64 | 57, 63 | ax-mp 5 |
. 2
⊢ (ℝ
× ℝ) ⊆ ∪ ran 𝑅 |
65 | 46, 64 | eqssi 3917 |
1
⊢ ∪ ran 𝑅 = (ℝ ×
ℝ) |