| Step | Hyp | Ref
| Expression |
| 1 | | retop 24782 |
. . 3
⊢
(topGen‘ran (,)) ∈ Top |
| 2 | | qssre 13001 |
. . 3
⊢ ℚ
⊆ ℝ |
| 3 | | uniretop 24783 |
. . . 4
⊢ ℝ =
∪ (topGen‘ran (,)) |
| 4 | 3 | clsss3 23067 |
. . 3
⊢
(((topGen‘ran (,)) ∈ Top ∧ ℚ ⊆ ℝ)
→ ((cls‘(topGen‘ran (,)))‘ℚ) ⊆
ℝ) |
| 5 | 1, 2, 4 | mp2an 692 |
. 2
⊢
((cls‘(topGen‘ran (,)))‘ℚ) ⊆
ℝ |
| 6 | | ioof 13487 |
. . . . . . 7
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
| 7 | | ffn 6736 |
. . . . . . 7
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
| 8 | | ovelrn 7609 |
. . . . . . 7
⊢ ((,) Fn
(ℝ* × ℝ*) → (𝑦 ∈ ran (,) ↔ ∃𝑧 ∈ ℝ*
∃𝑤 ∈
ℝ* 𝑦 =
(𝑧(,)𝑤))) |
| 9 | 6, 7, 8 | mp2b 10 |
. . . . . 6
⊢ (𝑦 ∈ ran (,) ↔
∃𝑧 ∈
ℝ* ∃𝑤 ∈ ℝ* 𝑦 = (𝑧(,)𝑤)) |
| 10 | | elioo3g 13416 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝑧(,)𝑤) ↔ ((𝑧 ∈ ℝ* ∧ 𝑤 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) ∧ (𝑧 < 𝑥 ∧ 𝑥 < 𝑤))) |
| 11 | 10 | simplbi 497 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑧(,)𝑤) → (𝑧 ∈ ℝ* ∧ 𝑤 ∈ ℝ*
∧ 𝑥 ∈
ℝ*)) |
| 12 | 11 | simp1d 1143 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝑧(,)𝑤) → 𝑧 ∈ ℝ*) |
| 13 | 12 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (𝑧(,)𝑤) ∧ 𝑦 ∈ ℚ) ∧ (𝑧 < 𝑦 ∧ 𝑦 < 𝑤)) → 𝑧 ∈ ℝ*) |
| 14 | 11 | simp2d 1144 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝑧(,)𝑤) → 𝑤 ∈ ℝ*) |
| 15 | 14 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (𝑧(,)𝑤) ∧ 𝑦 ∈ ℚ) ∧ (𝑧 < 𝑦 ∧ 𝑦 < 𝑤)) → 𝑤 ∈ ℝ*) |
| 16 | | qre 12995 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℚ → 𝑦 ∈
ℝ) |
| 17 | 16 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ (𝑧(,)𝑤) ∧ 𝑦 ∈ ℚ) ∧ (𝑧 < 𝑦 ∧ 𝑦 < 𝑤)) → 𝑦 ∈ ℝ) |
| 18 | 17 | rexrd 11311 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ (𝑧(,)𝑤) ∧ 𝑦 ∈ ℚ) ∧ (𝑧 < 𝑦 ∧ 𝑦 < 𝑤)) → 𝑦 ∈ ℝ*) |
| 19 | 13, 15, 18 | 3jca 1129 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ (𝑧(,)𝑤) ∧ 𝑦 ∈ ℚ) ∧ (𝑧 < 𝑦 ∧ 𝑦 < 𝑤)) → (𝑧 ∈ ℝ* ∧ 𝑤 ∈ ℝ*
∧ 𝑦 ∈
ℝ*)) |
| 20 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ (𝑧(,)𝑤) ∧ 𝑦 ∈ ℚ) ∧ (𝑧 < 𝑦 ∧ 𝑦 < 𝑤)) → (𝑧 < 𝑦 ∧ 𝑦 < 𝑤)) |
| 21 | | elioo3g 13416 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝑧(,)𝑤) ↔ ((𝑧 ∈ ℝ* ∧ 𝑤 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ (𝑧 < 𝑦 ∧ 𝑦 < 𝑤))) |
| 22 | 19, 20, 21 | sylanbrc 583 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (𝑧(,)𝑤) ∧ 𝑦 ∈ ℚ) ∧ (𝑧 < 𝑦 ∧ 𝑦 < 𝑤)) → 𝑦 ∈ (𝑧(,)𝑤)) |
| 23 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (𝑧(,)𝑤) ∧ 𝑦 ∈ ℚ) ∧ (𝑧 < 𝑦 ∧ 𝑦 < 𝑤)) → 𝑦 ∈ ℚ) |
| 24 | | inelcm 4465 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ (𝑧(,)𝑤) ∧ 𝑦 ∈ ℚ) → ((𝑧(,)𝑤) ∩ ℚ) ≠
∅) |
| 25 | 22, 23, 24 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (𝑧(,)𝑤) ∧ 𝑦 ∈ ℚ) ∧ (𝑧 < 𝑦 ∧ 𝑦 < 𝑤)) → ((𝑧(,)𝑤) ∩ ℚ) ≠
∅) |
| 26 | 11 | simp3d 1145 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑧(,)𝑤) → 𝑥 ∈ ℝ*) |
| 27 | | eliooord 13446 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑧(,)𝑤) → (𝑧 < 𝑥 ∧ 𝑥 < 𝑤)) |
| 28 | 27 | simpld 494 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑧(,)𝑤) → 𝑧 < 𝑥) |
| 29 | 27 | simprd 495 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑧(,)𝑤) → 𝑥 < 𝑤) |
| 30 | 12, 26, 14, 28, 29 | xrlttrd 13201 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝑧(,)𝑤) → 𝑧 < 𝑤) |
| 31 | | qbtwnxr 13242 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℝ*
∧ 𝑤 ∈
ℝ* ∧ 𝑧
< 𝑤) → ∃𝑦 ∈ ℚ (𝑧 < 𝑦 ∧ 𝑦 < 𝑤)) |
| 32 | 12, 14, 30, 31 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑧(,)𝑤) → ∃𝑦 ∈ ℚ (𝑧 < 𝑦 ∧ 𝑦 < 𝑤)) |
| 33 | 25, 32 | r19.29a 3162 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑧(,)𝑤) → ((𝑧(,)𝑤) ∩ ℚ) ≠
∅) |
| 34 | 33 | a1i 11 |
. . . . . . . . 9
⊢ (𝑦 = (𝑧(,)𝑤) → (𝑥 ∈ (𝑧(,)𝑤) → ((𝑧(,)𝑤) ∩ ℚ) ≠
∅)) |
| 35 | | eleq2 2830 |
. . . . . . . . 9
⊢ (𝑦 = (𝑧(,)𝑤) → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ (𝑧(,)𝑤))) |
| 36 | | ineq1 4213 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑧(,)𝑤) → (𝑦 ∩ ℚ) = ((𝑧(,)𝑤) ∩ ℚ)) |
| 37 | 36 | neeq1d 3000 |
. . . . . . . . 9
⊢ (𝑦 = (𝑧(,)𝑤) → ((𝑦 ∩ ℚ) ≠ ∅ ↔ ((𝑧(,)𝑤) ∩ ℚ) ≠
∅)) |
| 38 | 34, 35, 37 | 3imtr4d 294 |
. . . . . . . 8
⊢ (𝑦 = (𝑧(,)𝑤) → (𝑥 ∈ 𝑦 → (𝑦 ∩ ℚ) ≠
∅)) |
| 39 | 38 | rexlimivw 3151 |
. . . . . . 7
⊢
(∃𝑤 ∈
ℝ* 𝑦 =
(𝑧(,)𝑤) → (𝑥 ∈ 𝑦 → (𝑦 ∩ ℚ) ≠
∅)) |
| 40 | 39 | rexlimivw 3151 |
. . . . . 6
⊢
(∃𝑧 ∈
ℝ* ∃𝑤 ∈ ℝ* 𝑦 = (𝑧(,)𝑤) → (𝑥 ∈ 𝑦 → (𝑦 ∩ ℚ) ≠
∅)) |
| 41 | 9, 40 | sylbi 217 |
. . . . 5
⊢ (𝑦 ∈ ran (,) → (𝑥 ∈ 𝑦 → (𝑦 ∩ ℚ) ≠
∅)) |
| 42 | 41 | rgen 3063 |
. . . 4
⊢
∀𝑦 ∈ ran
(,)(𝑥 ∈ 𝑦 → (𝑦 ∩ ℚ) ≠
∅) |
| 43 | | eqidd 2738 |
. . . . 5
⊢ (𝑥 ∈ ℝ →
(topGen‘ran (,)) = (topGen‘ran (,))) |
| 44 | 3 | a1i 11 |
. . . . 5
⊢ (𝑥 ∈ ℝ → ℝ =
∪ (topGen‘ran (,))) |
| 45 | | retopbas 24781 |
. . . . . 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 23091 |
. . . 4
⊢ (𝑥 ∈ ℝ → (𝑥 ∈
((cls‘(topGen‘ran (,)))‘ℚ) ↔ ∀𝑦 ∈ ran (,)(𝑥 ∈ 𝑦 → (𝑦 ∩ ℚ) ≠
∅))) |
| 50 | 42, 49 | mpbiri 258 |
. . 3
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
((cls‘(topGen‘ran (,)))‘ℚ)) |
| 51 | 50 | ssriv 3987 |
. 2
⊢ ℝ
⊆ ((cls‘(topGen‘ran (,)))‘ℚ) |
| 52 | 5, 51 | eqssi 4000 |
1
⊢
((cls‘(topGen‘ran (,)))‘ℚ) =
ℝ |