Step | Hyp | Ref
| Expression |
1 | | retop 23364 |
. . 3
⊢
(topGen‘ran (,)) ∈ Top |
2 | | qssre 12352 |
. . 3
⊢ ℚ
⊆ ℝ |
3 | | uniretop 23365 |
. . . 4
⊢ ℝ =
∪ (topGen‘ran (,)) |
4 | 3 | clsss3 21661 |
. . 3
⊢
(((topGen‘ran (,)) ∈ Top ∧ ℚ ⊆ ℝ)
→ ((cls‘(topGen‘ran (,)))‘ℚ) ⊆
ℝ) |
5 | 1, 2, 4 | mp2an 690 |
. 2
⊢
((cls‘(topGen‘ran (,)))‘ℚ) ⊆
ℝ |
6 | | ioof 12829 |
. . . . . . 7
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
7 | | ffn 6509 |
. . . . . . 7
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
8 | | ovelrn 7318 |
. . . . . . 7
⊢ ((,) Fn
(ℝ* × ℝ*) → (𝑦 ∈ ran (,) ↔ ∃𝑧 ∈ ℝ*
∃𝑤 ∈
ℝ* 𝑦 =
(𝑧(,)𝑤))) |
9 | 6, 7, 8 | mp2b 10 |
. . . . . 6
⊢ (𝑦 ∈ ran (,) ↔
∃𝑧 ∈
ℝ* ∃𝑤 ∈ ℝ* 𝑦 = (𝑧(,)𝑤)) |
10 | | elioo3g 12761 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝑧(,)𝑤) ↔ ((𝑧 ∈ ℝ* ∧ 𝑤 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) ∧ (𝑧 < 𝑥 ∧ 𝑥 < 𝑤))) |
11 | 10 | simplbi 500 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑧(,)𝑤) → (𝑧 ∈ ℝ* ∧ 𝑤 ∈ ℝ*
∧ 𝑥 ∈
ℝ*)) |
12 | 11 | simp1d 1138 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝑧(,)𝑤) → 𝑧 ∈ ℝ*) |
13 | 12 | ad2antrr 724 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (𝑧(,)𝑤) ∧ 𝑦 ∈ ℚ) ∧ (𝑧 < 𝑦 ∧ 𝑦 < 𝑤)) → 𝑧 ∈ ℝ*) |
14 | 11 | simp2d 1139 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝑧(,)𝑤) → 𝑤 ∈ ℝ*) |
15 | 14 | ad2antrr 724 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (𝑧(,)𝑤) ∧ 𝑦 ∈ ℚ) ∧ (𝑧 < 𝑦 ∧ 𝑦 < 𝑤)) → 𝑤 ∈ ℝ*) |
16 | | qre 12347 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℚ → 𝑦 ∈
ℝ) |
17 | 16 | ad2antlr 725 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ (𝑧(,)𝑤) ∧ 𝑦 ∈ ℚ) ∧ (𝑧 < 𝑦 ∧ 𝑦 < 𝑤)) → 𝑦 ∈ ℝ) |
18 | 17 | rexrd 10685 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (𝑧(,)𝑤) ∧ 𝑦 ∈ ℚ) ∧ (𝑧 < 𝑦 ∧ 𝑦 < 𝑤)) → 𝑦 ∈ ℝ*) |
19 | 13, 15, 18 | 3jca 1124 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ (𝑧(,)𝑤) ∧ 𝑦 ∈ ℚ) ∧ (𝑧 < 𝑦 ∧ 𝑦 < 𝑤)) → (𝑧 ∈ ℝ* ∧ 𝑤 ∈ ℝ*
∧ 𝑦 ∈
ℝ*)) |
20 | | simpr 487 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ (𝑧(,)𝑤) ∧ 𝑦 ∈ ℚ) ∧ (𝑧 < 𝑦 ∧ 𝑦 < 𝑤)) → (𝑧 < 𝑦 ∧ 𝑦 < 𝑤)) |
21 | | elioo3g 12761 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝑧(,)𝑤) ↔ ((𝑧 ∈ ℝ* ∧ 𝑤 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ (𝑧 < 𝑦 ∧ 𝑦 < 𝑤))) |
22 | 19, 20, 21 | sylanbrc 585 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (𝑧(,)𝑤) ∧ 𝑦 ∈ ℚ) ∧ (𝑧 < 𝑦 ∧ 𝑦 < 𝑤)) → 𝑦 ∈ (𝑧(,)𝑤)) |
23 | | simplr 767 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (𝑧(,)𝑤) ∧ 𝑦 ∈ ℚ) ∧ (𝑧 < 𝑦 ∧ 𝑦 < 𝑤)) → 𝑦 ∈ ℚ) |
24 | | inelcm 4414 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ (𝑧(,)𝑤) ∧ 𝑦 ∈ ℚ) → ((𝑧(,)𝑤) ∩ ℚ) ≠
∅) |
25 | 22, 23, 24 | syl2anc 586 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (𝑧(,)𝑤) ∧ 𝑦 ∈ ℚ) ∧ (𝑧 < 𝑦 ∧ 𝑦 < 𝑤)) → ((𝑧(,)𝑤) ∩ ℚ) ≠
∅) |
26 | 11 | simp3d 1140 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑧(,)𝑤) → 𝑥 ∈ ℝ*) |
27 | | eliooord 12790 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑧(,)𝑤) → (𝑧 < 𝑥 ∧ 𝑥 < 𝑤)) |
28 | 27 | simpld 497 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑧(,)𝑤) → 𝑧 < 𝑥) |
29 | 27 | simprd 498 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑧(,)𝑤) → 𝑥 < 𝑤) |
30 | 12, 26, 14, 28, 29 | xrlttrd 12546 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝑧(,)𝑤) → 𝑧 < 𝑤) |
31 | | qbtwnxr 12587 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℝ*
∧ 𝑤 ∈
ℝ* ∧ 𝑧
< 𝑤) → ∃𝑦 ∈ ℚ (𝑧 < 𝑦 ∧ 𝑦 < 𝑤)) |
32 | 12, 14, 30, 31 | syl3anc 1367 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑧(,)𝑤) → ∃𝑦 ∈ ℚ (𝑧 < 𝑦 ∧ 𝑦 < 𝑤)) |
33 | 25, 32 | r19.29a 3289 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑧(,)𝑤) → ((𝑧(,)𝑤) ∩ ℚ) ≠
∅) |
34 | 33 | a1i 11 |
. . . . . . . . 9
⊢ (𝑦 = (𝑧(,)𝑤) → (𝑥 ∈ (𝑧(,)𝑤) → ((𝑧(,)𝑤) ∩ ℚ) ≠
∅)) |
35 | | eleq2 2901 |
. . . . . . . . 9
⊢ (𝑦 = (𝑧(,)𝑤) → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ (𝑧(,)𝑤))) |
36 | | ineq1 4181 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑧(,)𝑤) → (𝑦 ∩ ℚ) = ((𝑧(,)𝑤) ∩ ℚ)) |
37 | 36 | neeq1d 3075 |
. . . . . . . . 9
⊢ (𝑦 = (𝑧(,)𝑤) → ((𝑦 ∩ ℚ) ≠ ∅ ↔ ((𝑧(,)𝑤) ∩ ℚ) ≠
∅)) |
38 | 34, 35, 37 | 3imtr4d 296 |
. . . . . . . 8
⊢ (𝑦 = (𝑧(,)𝑤) → (𝑥 ∈ 𝑦 → (𝑦 ∩ ℚ) ≠
∅)) |
39 | 38 | rexlimivw 3282 |
. . . . . . 7
⊢
(∃𝑤 ∈
ℝ* 𝑦 =
(𝑧(,)𝑤) → (𝑥 ∈ 𝑦 → (𝑦 ∩ ℚ) ≠
∅)) |
40 | 39 | rexlimivw 3282 |
. . . . . 6
⊢
(∃𝑧 ∈
ℝ* ∃𝑤 ∈ ℝ* 𝑦 = (𝑧(,)𝑤) → (𝑥 ∈ 𝑦 → (𝑦 ∩ ℚ) ≠
∅)) |
41 | 9, 40 | sylbi 219 |
. . . . 5
⊢ (𝑦 ∈ ran (,) → (𝑥 ∈ 𝑦 → (𝑦 ∩ ℚ) ≠
∅)) |
42 | 41 | rgen 3148 |
. . . 4
⊢
∀𝑦 ∈ ran
(,)(𝑥 ∈ 𝑦 → (𝑦 ∩ ℚ) ≠
∅) |
43 | | eqidd 2822 |
. . . . 5
⊢ (𝑥 ∈ ℝ →
(topGen‘ran (,)) = (topGen‘ran (,))) |
44 | 3 | a1i 11 |
. . . . 5
⊢ (𝑥 ∈ ℝ → ℝ =
∪ (topGen‘ran (,))) |
45 | | retopbas 23363 |
. . . . . 6
⊢ ran (,)
∈ TopBases |
46 | 45 | a1i 11 |
. . . . 5
⊢ (𝑥 ∈ ℝ → ran (,)
∈ TopBases) |
47 | 2 | a1i 11 |
. . . . 5
⊢ (𝑥 ∈ ℝ → ℚ
⊆ ℝ) |
48 | | id 22 |
. . . . 5
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ) |
49 | 43, 44, 46, 47, 48 | elcls3 21685 |
. . . 4
⊢ (𝑥 ∈ ℝ → (𝑥 ∈
((cls‘(topGen‘ran (,)))‘ℚ) ↔ ∀𝑦 ∈ ran (,)(𝑥 ∈ 𝑦 → (𝑦 ∩ ℚ) ≠
∅))) |
50 | 42, 49 | mpbiri 260 |
. . 3
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
((cls‘(topGen‘ran (,)))‘ℚ)) |
51 | 50 | ssriv 3971 |
. 2
⊢ ℝ
⊆ ((cls‘(topGen‘ran (,)))‘ℚ) |
52 | 5, 51 | eqssi 3983 |
1
⊢
((cls‘(topGen‘ran (,)))‘ℚ) =
ℝ |