Step | Hyp | Ref
| Expression |
1 | | df-cnfld 14056 |
. 2
⊢
ℂfld = (({〈(Base‘ndx), ℂ〉,
〈(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))〉} ∪
{〈(*𝑟‘ndx), ∗〉}) ∪
({〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ {〈(UnifSet‘ndx), (metUnif‘(abs ∘ −
))〉})) |
2 | | eqid 2193 |
. . . . 5
⊢
({〈(Base‘ndx), ℂ〉,
〈(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))〉} ∪
{〈(*𝑟‘ndx), ∗〉}) =
({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx),
(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))〉} ∪
{〈(*𝑟‘ndx), ∗〉}) |
3 | | cnex 7998 |
. . . . . 6
⊢ ℂ
∈ V |
4 | 3 | a1i 9 |
. . . . 5
⊢ (⊤
→ ℂ ∈ V) |
5 | 3, 3 | mpoex 6269 |
. . . . . 6
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦)) ∈ V |
6 | 5 | a1i 9 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈ ℂ,
𝑦 ∈ ℂ ↦
(𝑥 + 𝑦)) ∈ V) |
7 | 3, 3 | mpoex 6269 |
. . . . . 6
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ∈ V |
8 | 7 | a1i 9 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈ ℂ,
𝑦 ∈ ℂ ↦
(𝑥 · 𝑦)) ∈ V) |
9 | | cjf 10994 |
. . . . . . 7
⊢
∗:ℂ⟶ℂ |
10 | | fex 5788 |
. . . . . . 7
⊢
((∗:ℂ⟶ℂ ∧ ℂ ∈ V) →
∗ ∈ V) |
11 | 9, 3, 10 | mp2an 426 |
. . . . . 6
⊢ ∗
∈ V |
12 | 11 | a1i 9 |
. . . . 5
⊢ (⊤
→ ∗ ∈ V) |
13 | 2, 4, 6, 8, 12 | srngstrd 12766 |
. . . 4
⊢ (⊤
→ ({〈(Base‘ndx), ℂ〉,
〈(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))〉} ∪
{〈(*𝑟‘ndx), ∗〉}) Struct 〈1,
4〉) |
14 | 13 | mptru 1373 |
. . 3
⊢
({〈(Base‘ndx), ℂ〉,
〈(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))〉} ∪
{〈(*𝑟‘ndx), ∗〉}) Struct 〈1,
4〉 |
15 | | cntopex 14053 |
. . . . 5
⊢
(MetOpen‘(abs ∘ − )) ∈ V |
16 | | xrex 9925 |
. . . . . . 7
⊢
ℝ* ∈ V |
17 | 16, 16 | xpex 4775 |
. . . . . 6
⊢
(ℝ* × ℝ*) ∈
V |
18 | | lerelxr 8084 |
. . . . . 6
⊢ ≤
⊆ (ℝ* × ℝ*) |
19 | 17, 18 | ssexi 4168 |
. . . . 5
⊢ ≤
∈ V |
20 | | cndsex 14052 |
. . . . 5
⊢ (abs
∘ − ) ∈ V |
21 | | 9nn 9153 |
. . . . . 6
⊢ 9 ∈
ℕ |
22 | | tsetndx 12806 |
. . . . . 6
⊢
(TopSet‘ndx) = 9 |
23 | | 9lt10 9581 |
. . . . . 6
⊢ 9 <
;10 |
24 | | 10nn 9466 |
. . . . . 6
⊢ ;10 ∈ ℕ |
25 | | plendx 12820 |
. . . . . 6
⊢
(le‘ndx) = ;10 |
26 | | 1nn0 9259 |
. . . . . . 7
⊢ 1 ∈
ℕ0 |
27 | | 0nn0 9258 |
. . . . . . 7
⊢ 0 ∈
ℕ0 |
28 | | 2nn 9146 |
. . . . . . 7
⊢ 2 ∈
ℕ |
29 | | 2pos 9075 |
. . . . . . 7
⊢ 0 <
2 |
30 | 26, 27, 28, 29 | declt 9478 |
. . . . . 6
⊢ ;10 < ;12 |
31 | 26, 28 | decnncl 9470 |
. . . . . 6
⊢ ;12 ∈ ℕ |
32 | | dsndx 12831 |
. . . . . 6
⊢
(dist‘ndx) = ;12 |
33 | 21, 22, 23, 24, 25, 30, 31, 32 | strle3g 12729 |
. . . . 5
⊢
(((MetOpen‘(abs ∘ − )) ∈ V ∧ ≤ ∈ V
∧ (abs ∘ − ) ∈ V) → {〈(TopSet‘ndx),
(MetOpen‘(abs ∘ − ))〉, 〈(le‘ndx), ≤
〉, 〈(dist‘ndx), (abs ∘ − )〉} Struct 〈9,
;12〉) |
34 | 15, 19, 20, 33 | mp3an 1348 |
. . . 4
⊢
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} Struct 〈9, ;12〉 |
35 | | metuex 14054 |
. . . . 5
⊢ ((abs
∘ − ) ∈ V → (metUnif‘(abs ∘ − )) ∈
V) |
36 | | 3nn 9147 |
. . . . . . 7
⊢ 3 ∈
ℕ |
37 | 26, 36 | decnncl 9470 |
. . . . . 6
⊢ ;13 ∈ ℕ |
38 | | unifndx 12842 |
. . . . . 6
⊢
(UnifSet‘ndx) = ;13 |
39 | 37, 38 | strle1g 12727 |
. . . . 5
⊢
((metUnif‘(abs ∘ − )) ∈ V →
{〈(UnifSet‘ndx), (metUnif‘(abs ∘ − ))〉}
Struct 〈;13, ;13〉) |
40 | 20, 35, 39 | mp2b 8 |
. . . 4
⊢
{〈(UnifSet‘ndx), (metUnif‘(abs ∘ −
))〉} Struct 〈;13, ;13〉 |
41 | | 2nn0 9260 |
. . . . 5
⊢ 2 ∈
ℕ0 |
42 | | 2lt3 9155 |
. . . . 5
⊢ 2 <
3 |
43 | 26, 41, 36, 42 | declt 9478 |
. . . 4
⊢ ;12 < ;13 |
44 | 34, 40, 43 | strleun 12725 |
. . 3
⊢
({〈(TopSet‘ndx), (MetOpen‘(abs ∘ −
))〉, 〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs
∘ − )〉} ∪ {〈(UnifSet‘ndx), (metUnif‘(abs
∘ − ))〉}) Struct 〈9, ;13〉 |
45 | | 4lt9 9186 |
. . 3
⊢ 4 <
9 |
46 | 14, 44, 45 | strleun 12725 |
. 2
⊢
(({〈(Base‘ndx), ℂ〉,
〈(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))〉} ∪
{〈(*𝑟‘ndx), ∗〉}) ∪
({〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ {〈(UnifSet‘ndx), (metUnif‘(abs ∘ −
))〉})) Struct 〈1, ;13〉 |
47 | 1, 46 | eqbrtri 4051 |
1
⊢
ℂfld Struct 〈1, ;13〉 |