Step | Hyp | Ref
| Expression |
1 | | uniretop 23660 |
. . 3
⊢ ℝ =
∪ (topGen‘ran (,)) |
2 | | rehaus 23696 |
. . . 4
⊢
(topGen‘ran (,)) ∈ Haus |
3 | 2 | a1i 11 |
. . 3
⊢ (⊤
→ (topGen‘ran (,)) ∈ Haus) |
4 | | rerrext 31671 |
. . . 4
⊢
ℝfld ∈ ℝExt |
5 | | eqid 2737 |
. . . . 5
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
6 | | retopn 24276 |
. . . . 5
⊢
(topGen‘ran (,)) =
(TopOpen‘ℝfld) |
7 | 5, 6 | rrhcne 31675 |
. . . 4
⊢
(ℝfld ∈ ℝExt →
(ℝHom‘ℝfld) ∈ ((topGen‘ran (,)) Cn
(topGen‘ran (,)))) |
8 | 4, 7 | mp1i 13 |
. . 3
⊢ (⊤
→ (ℝHom‘ℝfld) ∈ ((topGen‘ran (,))
Cn (topGen‘ran (,)))) |
9 | | retop 23659 |
. . . . . 6
⊢
(topGen‘ran (,)) ∈ Top |
10 | 1 | toptopon 21814 |
. . . . . 6
⊢
((topGen‘ran (,)) ∈ Top ↔ (topGen‘ran (,)) ∈
(TopOn‘ℝ)) |
11 | 9, 10 | mpbi 233 |
. . . . 5
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
12 | | idcn 22154 |
. . . . 5
⊢
((topGen‘ran (,)) ∈ (TopOn‘ℝ) → ( I ↾
ℝ) ∈ ((topGen‘ran (,)) Cn (topGen‘ran
(,)))) |
13 | 11, 12 | ax-mp 5 |
. . . 4
⊢ ( I
↾ ℝ) ∈ ((topGen‘ran (,)) Cn (topGen‘ran
(,))) |
14 | 13 | a1i 11 |
. . 3
⊢ (⊤
→ ( I ↾ ℝ) ∈ ((topGen‘ran (,)) Cn (topGen‘ran
(,)))) |
15 | 9 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ (topGen‘ran (,)) ∈ Top) |
16 | | f1oi 6698 |
. . . . . . . . . 10
⊢ ( I
↾ ℚ):ℚ–1-1-onto→ℚ |
17 | | f1of 6661 |
. . . . . . . . . 10
⊢ (( I
↾ ℚ):ℚ–1-1-onto→ℚ → ( I ↾
ℚ):ℚ⟶ℚ) |
18 | 16, 17 | ax-mp 5 |
. . . . . . . . 9
⊢ ( I
↾ ℚ):ℚ⟶ℚ |
19 | | qssre 12555 |
. . . . . . . . 9
⊢ ℚ
⊆ ℝ |
20 | | fss 6562 |
. . . . . . . . 9
⊢ ((( I
↾ ℚ):ℚ⟶ℚ ∧ ℚ ⊆ ℝ) → (
I ↾ ℚ):ℚ⟶ℝ) |
21 | 18, 19, 20 | mp2an 692 |
. . . . . . . 8
⊢ ( I
↾ ℚ):ℚ⟶ℝ |
22 | 21 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ ( I ↾ ℚ):ℚ⟶ℝ) |
23 | 19 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ ℚ ⊆ ℝ) |
24 | | qdensere 23667 |
. . . . . . . 8
⊢
((cls‘(topGen‘ran (,)))‘ℚ) =
ℝ |
25 | 24 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ ((cls‘(topGen‘ran (,)))‘ℚ) =
ℝ) |
26 | 9 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ ∧ 𝑎 ∈ (topGen‘ran (,)))
∧ 𝑥 ∈ 𝑎) → (topGen‘ran (,))
∈ Top) |
27 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ ∧ 𝑎 ∈ (topGen‘ran (,)))
∧ 𝑥 ∈ 𝑎) → 𝑎 ∈ (topGen‘ran
(,))) |
28 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ ∧ 𝑎 ∈ (topGen‘ran (,)))
∧ 𝑥 ∈ 𝑎) → 𝑥 ∈ 𝑎) |
29 | | opnneip 22016 |
. . . . . . . . . . . . . . . 16
⊢
(((topGen‘ran (,)) ∈ Top ∧ 𝑎 ∈ (topGen‘ran (,)) ∧ 𝑥 ∈ 𝑎) → 𝑎 ∈ ((nei‘(topGen‘ran
(,)))‘{𝑥})) |
30 | 26, 27, 28, 29 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ ∧ 𝑎 ∈ (topGen‘ran (,)))
∧ 𝑥 ∈ 𝑎) → 𝑎 ∈ ((nei‘(topGen‘ran
(,)))‘{𝑥})) |
31 | | fvex 6730 |
. . . . . . . . . . . . . . . 16
⊢
((nei‘(topGen‘ran (,)))‘{𝑥}) ∈ V |
32 | | qex 12557 |
. . . . . . . . . . . . . . . 16
⊢ ℚ
∈ V |
33 | | elrestr 16933 |
. . . . . . . . . . . . . . . 16
⊢
((((nei‘(topGen‘ran (,)))‘{𝑥}) ∈ V ∧ ℚ ∈ V ∧
𝑎 ∈
((nei‘(topGen‘ran (,)))‘{𝑥})) → (𝑎 ∩ ℚ) ∈
(((nei‘(topGen‘ran (,)))‘{𝑥}) ↾t
ℚ)) |
34 | 31, 32, 33 | mp3an12 1453 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈
((nei‘(topGen‘ran (,)))‘{𝑥}) → (𝑎 ∩ ℚ) ∈
(((nei‘(topGen‘ran (,)))‘{𝑥}) ↾t
ℚ)) |
35 | 30, 34 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ ∧ 𝑎 ∈ (topGen‘ran (,)))
∧ 𝑥 ∈ 𝑎) → (𝑎 ∩ ℚ) ∈
(((nei‘(topGen‘ran (,)))‘{𝑥}) ↾t
ℚ)) |
36 | | inss2 4144 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∩ ℚ) ⊆
ℚ |
37 | | resiima 5944 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∩ ℚ) ⊆ ℚ
→ (( I ↾ ℚ) “ (𝑎 ∩ ℚ)) = (𝑎 ∩ ℚ)) |
38 | 36, 37 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (( I
↾ ℚ) “ (𝑎
∩ ℚ)) = (𝑎 ∩
ℚ) |
39 | | inss1 4143 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∩ ℚ) ⊆ 𝑎 |
40 | 38, 39 | eqsstri 3935 |
. . . . . . . . . . . . . . 15
⊢ (( I
↾ ℚ) “ (𝑎
∩ ℚ)) ⊆ 𝑎 |
41 | 40 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ ∧ 𝑎 ∈ (topGen‘ran (,)))
∧ 𝑥 ∈ 𝑎) → (( I ↾ ℚ)
“ (𝑎 ∩ ℚ))
⊆ 𝑎) |
42 | | imaeq2 5925 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑎 ∩ ℚ) → (( I ↾ ℚ)
“ 𝑏) = (( I ↾
ℚ) “ (𝑎 ∩
ℚ))) |
43 | 42 | sseq1d 3932 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑎 ∩ ℚ) → ((( I ↾ ℚ)
“ 𝑏) ⊆ 𝑎 ↔ (( I ↾ ℚ)
“ (𝑎 ∩ ℚ))
⊆ 𝑎)) |
44 | 43 | rspcev 3537 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∩ ℚ) ∈
(((nei‘(topGen‘ran (,)))‘{𝑥}) ↾t ℚ) ∧ (( I
↾ ℚ) “ (𝑎
∩ ℚ)) ⊆ 𝑎)
→ ∃𝑏 ∈
(((nei‘(topGen‘ran (,)))‘{𝑥}) ↾t ℚ)(( I ↾
ℚ) “ 𝑏) ⊆
𝑎) |
45 | 35, 41, 44 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ ∧ 𝑎 ∈ (topGen‘ran (,)))
∧ 𝑥 ∈ 𝑎) → ∃𝑏 ∈
(((nei‘(topGen‘ran (,)))‘{𝑥}) ↾t ℚ)(( I ↾
ℚ) “ 𝑏) ⊆
𝑎) |
46 | 45 | ex 416 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 𝑎 ∈ (topGen‘ran (,)))
→ (𝑥 ∈ 𝑎 → ∃𝑏 ∈
(((nei‘(topGen‘ran (,)))‘{𝑥}) ↾t ℚ)(( I ↾
ℚ) “ 𝑏) ⊆
𝑎)) |
47 | 46 | ralrimiva 3105 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ →
∀𝑎 ∈
(topGen‘ran (,))(𝑥
∈ 𝑎 →
∃𝑏 ∈
(((nei‘(topGen‘ran (,)))‘{𝑥}) ↾t ℚ)(( I ↾
ℚ) “ 𝑏) ⊆
𝑎)) |
48 | 47 | ancli 552 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ → (𝑥 ∈ ℝ ∧
∀𝑎 ∈
(topGen‘ran (,))(𝑥
∈ 𝑎 →
∃𝑏 ∈
(((nei‘(topGen‘ran (,)))‘{𝑥}) ↾t ℚ)(( I ↾
ℚ) “ 𝑏) ⊆
𝑎))) |
49 | 24 | eleq2i 2829 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈
((cls‘(topGen‘ran (,)))‘ℚ) ↔ 𝑥 ∈ ℝ) |
50 | 49 | biimpri 231 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
((cls‘(topGen‘ran (,)))‘ℚ)) |
51 | | trnei 22789 |
. . . . . . . . . . . . 13
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ℚ
⊆ ℝ ∧ 𝑥
∈ ℝ) → (𝑥
∈ ((cls‘(topGen‘ran (,)))‘ℚ) ↔
(((nei‘(topGen‘ran (,)))‘{𝑥}) ↾t ℚ) ∈
(Fil‘ℚ))) |
52 | 11, 19, 51 | mp3an12 1453 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → (𝑥 ∈
((cls‘(topGen‘ran (,)))‘ℚ) ↔
(((nei‘(topGen‘ran (,)))‘{𝑥}) ↾t ℚ) ∈
(Fil‘ℚ))) |
53 | 50, 52 | mpbid 235 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ →
(((nei‘(topGen‘ran (,)))‘{𝑥}) ↾t ℚ) ∈
(Fil‘ℚ)) |
54 | | isflf 22890 |
. . . . . . . . . . . 12
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧
(((nei‘(topGen‘ran (,)))‘{𝑥}) ↾t ℚ) ∈
(Fil‘ℚ) ∧ ( I ↾ ℚ):ℚ⟶ℝ) →
(𝑥 ∈
(((topGen‘ran (,)) fLimf (((nei‘(topGen‘ran
(,)))‘{𝑥})
↾t ℚ))‘( I ↾ ℚ)) ↔ (𝑥 ∈ ℝ ∧
∀𝑎 ∈
(topGen‘ran (,))(𝑥
∈ 𝑎 →
∃𝑏 ∈
(((nei‘(topGen‘ran (,)))‘{𝑥}) ↾t ℚ)(( I ↾
ℚ) “ 𝑏) ⊆
𝑎)))) |
55 | 11, 21, 54 | mp3an13 1454 |
. . . . . . . . . . 11
⊢
((((nei‘(topGen‘ran (,)))‘{𝑥}) ↾t ℚ) ∈
(Fil‘ℚ) → (𝑥 ∈ (((topGen‘ran (,)) fLimf
(((nei‘(topGen‘ran (,)))‘{𝑥}) ↾t ℚ))‘( I
↾ ℚ)) ↔ (𝑥
∈ ℝ ∧ ∀𝑎 ∈ (topGen‘ran (,))(𝑥 ∈ 𝑎 → ∃𝑏 ∈ (((nei‘(topGen‘ran
(,)))‘{𝑥})
↾t ℚ)(( I ↾ ℚ) “ 𝑏) ⊆ 𝑎)))) |
56 | 53, 55 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ → (𝑥 ∈ (((topGen‘ran (,))
fLimf (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾t ℚ))‘( I
↾ ℚ)) ↔ (𝑥
∈ ℝ ∧ ∀𝑎 ∈ (topGen‘ran (,))(𝑥 ∈ 𝑎 → ∃𝑏 ∈ (((nei‘(topGen‘ran
(,)))‘{𝑥})
↾t ℚ)(( I ↾ ℚ) “ 𝑏) ⊆ 𝑎)))) |
57 | 48, 56 | mpbird 260 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → 𝑥 ∈ (((topGen‘ran (,))
fLimf (((nei‘(topGen‘ran (,)))‘{𝑥}) ↾t ℚ))‘( I
↾ ℚ))) |
58 | 57 | ne0d 4250 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ →
(((topGen‘ran (,)) fLimf (((nei‘(topGen‘ran
(,)))‘{𝑥})
↾t ℚ))‘( I ↾ ℚ)) ≠
∅) |
59 | 58 | adantl 485 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ) → (((topGen‘ran (,)) fLimf
(((nei‘(topGen‘ran (,)))‘{𝑥}) ↾t ℚ))‘( I
↾ ℚ)) ≠ ∅) |
60 | | recusp 24279 |
. . . . . . . . . 10
⊢
ℝfld ∈ CUnifSp |
61 | | cuspusp 23197 |
. . . . . . . . . 10
⊢
(ℝfld ∈ CUnifSp → ℝfld
∈ UnifSp) |
62 | 60, 61 | ax-mp 5 |
. . . . . . . . 9
⊢
ℝfld ∈ UnifSp |
63 | 6 | uspreg 23171 |
. . . . . . . . 9
⊢
((ℝfld ∈ UnifSp ∧ (topGen‘ran (,))
∈ Haus) → (topGen‘ran (,)) ∈ Reg) |
64 | 62, 2, 63 | mp2an 692 |
. . . . . . . 8
⊢
(topGen‘ran (,)) ∈ Reg |
65 | 64 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ (topGen‘ran (,)) ∈ Reg) |
66 | | resabs1 5881 |
. . . . . . . . . 10
⊢ (ℚ
⊆ ℝ → (( I ↾ ℝ) ↾ ℚ) = ( I ↾
ℚ)) |
67 | 19, 66 | ax-mp 5 |
. . . . . . . . 9
⊢ (( I
↾ ℝ) ↾ ℚ) = ( I ↾ ℚ) |
68 | 1 | cnrest 22182 |
. . . . . . . . . 10
⊢ ((( I
↾ ℝ) ∈ ((topGen‘ran (,)) Cn (topGen‘ran (,)))
∧ ℚ ⊆ ℝ) → (( I ↾ ℝ) ↾ ℚ)
∈ (((topGen‘ran (,)) ↾t ℚ) Cn
(topGen‘ran (,)))) |
69 | 13, 19, 68 | mp2an 692 |
. . . . . . . . 9
⊢ (( I
↾ ℝ) ↾ ℚ) ∈ (((topGen‘ran (,))
↾t ℚ) Cn (topGen‘ran (,))) |
70 | 67, 69 | eqeltrri 2835 |
. . . . . . . 8
⊢ ( I
↾ ℚ) ∈ (((topGen‘ran (,)) ↾t ℚ)
Cn (topGen‘ran (,))) |
71 | 70 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ ( I ↾ ℚ) ∈ (((topGen‘ran (,)) ↾t
ℚ) Cn (topGen‘ran (,)))) |
72 | 1, 1, 15, 3, 22, 23, 25, 59, 65, 71 | cnextfres1 22965 |
. . . . . 6
⊢ (⊤
→ ((((topGen‘ran (,))CnExt(topGen‘ran (,)))‘( I ↾
ℚ)) ↾ ℚ) = ( I ↾ ℚ)) |
73 | 72 | mptru 1550 |
. . . . 5
⊢
((((topGen‘ran (,))CnExt(topGen‘ran (,)))‘( I ↾
ℚ)) ↾ ℚ) = ( I ↾ ℚ) |
74 | | recms 24277 |
. . . . . . . . 9
⊢
ℝfld ∈ CMetSp |
75 | 74 | elexi 3427 |
. . . . . . . 8
⊢
ℝfld ∈ V |
76 | 5, 6 | rrhval 31658 |
. . . . . . . 8
⊢
(ℝfld ∈ V →
(ℝHom‘ℝfld) = (((topGen‘ran
(,))CnExt(topGen‘ran
(,)))‘(ℚHom‘ℝfld))) |
77 | 75, 76 | ax-mp 5 |
. . . . . . 7
⊢
(ℝHom‘ℝfld) = (((topGen‘ran
(,))CnExt(topGen‘ran
(,)))‘(ℚHom‘ℝfld)) |
78 | | qqhre 31682 |
. . . . . . . 8
⊢
(ℚHom‘ℝfld) = ( I ↾
ℚ) |
79 | 78 | fveq2i 6720 |
. . . . . . 7
⊢
(((topGen‘ran (,))CnExt(topGen‘ran
(,)))‘(ℚHom‘ℝfld)) = (((topGen‘ran
(,))CnExt(topGen‘ran (,)))‘( I ↾ ℚ)) |
80 | 77, 79 | eqtri 2765 |
. . . . . 6
⊢
(ℝHom‘ℝfld) = (((topGen‘ran
(,))CnExt(topGen‘ran (,)))‘( I ↾ ℚ)) |
81 | 80 | reseq1i 5847 |
. . . . 5
⊢
((ℝHom‘ℝfld) ↾ ℚ) =
((((topGen‘ran (,))CnExt(topGen‘ran (,)))‘( I ↾
ℚ)) ↾ ℚ) |
82 | 73, 81, 67 | 3eqtr4i 2775 |
. . . 4
⊢
((ℝHom‘ℝfld) ↾ ℚ) = (( I
↾ ℝ) ↾ ℚ) |
83 | 82 | a1i 11 |
. . 3
⊢ (⊤
→ ((ℝHom‘ℝfld) ↾ ℚ) = (( I
↾ ℝ) ↾ ℚ)) |
84 | 1, 3, 8, 14, 83, 23, 25 | hauseqcn 31562 |
. 2
⊢ (⊤
→ (ℝHom‘ℝfld) = ( I ↾
ℝ)) |
85 | 84 | mptru 1550 |
1
⊢
(ℝHom‘ℝfld) = ( I ↾
ℝ) |