| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | basendxnplusgndx 17328 | . . . . . . 7
⊢
(Base‘ndx) ≠ (+g‘ndx) | 
| 2 |  | basendxnmulrndx 17340 | . . . . . . 7
⊢
(Base‘ndx) ≠ (.r‘ndx) | 
| 3 |  | plusgndxnmulrndx 17342 | . . . . . . 7
⊢
(+g‘ndx) ≠
(.r‘ndx) | 
| 4 |  | fvex 6918 | . . . . . . . 8
⊢
(Base‘ndx) ∈ V | 
| 5 |  | fvex 6918 | . . . . . . . 8
⊢
(+g‘ndx) ∈ V | 
| 6 |  | fvex 6918 | . . . . . . . 8
⊢
(.r‘ndx) ∈ V | 
| 7 |  | cnex 11237 | . . . . . . . 8
⊢ ℂ
∈ V | 
| 8 |  | mpoaddex 13031 | . . . . . . . 8
⊢ (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣)) ∈ V | 
| 9 |  | mpomulex 13033 | . . . . . . . 8
⊢ (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ V | 
| 10 | 4, 5, 6, 7, 8, 9 | funtp 6622 | . . . . . . 7
⊢
(((Base‘ndx) ≠ (+g‘ndx) ∧ (Base‘ndx)
≠ (.r‘ndx) ∧ (+g‘ndx) ≠
(.r‘ndx)) → Fun {〈(Base‘ndx), ℂ〉,
〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉}) | 
| 11 | 1, 2, 3, 10 | mp3an 1462 | . . . . . 6
⊢ Fun
{〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} | 
| 12 |  | fvex 6918 | . . . . . . 7
⊢
(*𝑟‘ndx) ∈ V | 
| 13 |  | cjf 15144 | . . . . . . . 8
⊢
∗:ℂ⟶ℂ | 
| 14 |  | fex 7247 | . . . . . . . 8
⊢
((∗:ℂ⟶ℂ ∧ ℂ ∈ V) →
∗ ∈ V) | 
| 15 | 13, 7, 14 | mp2an 692 | . . . . . . 7
⊢ ∗
∈ V | 
| 16 | 12, 15 | funsn 6618 | . . . . . 6
⊢ Fun
{〈(*𝑟‘ndx), ∗〉} | 
| 17 | 11, 16 | pm3.2i 470 | . . . . 5
⊢ (Fun
{〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∧ Fun
{〈(*𝑟‘ndx), ∗〉}) | 
| 18 | 7, 8, 9 | dmtpop 6237 | . . . . . . 7
⊢ dom
{〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} = {(Base‘ndx),
(+g‘ndx), (.r‘ndx)} | 
| 19 | 15 | dmsnop 6235 | . . . . . . 7
⊢ dom
{〈(*𝑟‘ndx), ∗〉} =
{(*𝑟‘ndx)} | 
| 20 | 18, 19 | ineq12i 4217 | . . . . . 6
⊢ (dom
{〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∩ dom
{〈(*𝑟‘ndx), ∗〉}) =
({(Base‘ndx), (+g‘ndx), (.r‘ndx)} ∩
{(*𝑟‘ndx)}) | 
| 21 |  | starvndxnbasendx 17349 | . . . . . . . 8
⊢
(*𝑟‘ndx) ≠ (Base‘ndx) | 
| 22 | 21 | necomi 2994 | . . . . . . 7
⊢
(Base‘ndx) ≠ (*𝑟‘ndx) | 
| 23 |  | starvndxnplusgndx 17350 | . . . . . . . 8
⊢
(*𝑟‘ndx) ≠
(+g‘ndx) | 
| 24 | 23 | necomi 2994 | . . . . . . 7
⊢
(+g‘ndx) ≠
(*𝑟‘ndx) | 
| 25 |  | starvndxnmulrndx 17351 | . . . . . . . 8
⊢
(*𝑟‘ndx) ≠
(.r‘ndx) | 
| 26 | 25 | necomi 2994 | . . . . . . 7
⊢
(.r‘ndx) ≠
(*𝑟‘ndx) | 
| 27 |  | disjtpsn 4714 | . . . . . . 7
⊢
(((Base‘ndx) ≠ (*𝑟‘ndx) ∧
(+g‘ndx) ≠ (*𝑟‘ndx) ∧
(.r‘ndx) ≠ (*𝑟‘ndx)) →
({(Base‘ndx), (+g‘ndx), (.r‘ndx)} ∩
{(*𝑟‘ndx)}) = ∅) | 
| 28 | 22, 24, 26, 27 | mp3an 1462 | . . . . . 6
⊢
({(Base‘ndx), (+g‘ndx),
(.r‘ndx)} ∩ {(*𝑟‘ndx)}) =
∅ | 
| 29 | 20, 28 | eqtri 2764 | . . . . 5
⊢ (dom
{〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∩ dom
{〈(*𝑟‘ndx), ∗〉}) =
∅ | 
| 30 |  | funun 6611 | . . . . 5
⊢ (((Fun
{〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∧ Fun
{〈(*𝑟‘ndx), ∗〉}) ∧ (dom
{〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∩ dom
{〈(*𝑟‘ndx), ∗〉}) = ∅) →
Fun ({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∪
{〈(*𝑟‘ndx), ∗〉})) | 
| 31 | 17, 29, 30 | mp2an 692 | . . . 4
⊢ Fun
({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∪
{〈(*𝑟‘ndx), ∗〉}) | 
| 32 |  | slotsdifplendx 17420 | . . . . . . . 8
⊢
((*𝑟‘ndx) ≠ (le‘ndx) ∧
(TopSet‘ndx) ≠ (le‘ndx)) | 
| 33 | 32 | simpri 485 | . . . . . . 7
⊢
(TopSet‘ndx) ≠ (le‘ndx) | 
| 34 |  | dsndxntsetndx 17438 | . . . . . . . 8
⊢
(dist‘ndx) ≠ (TopSet‘ndx) | 
| 35 | 34 | necomi 2994 | . . . . . . 7
⊢
(TopSet‘ndx) ≠ (dist‘ndx) | 
| 36 |  | slotsdifdsndx 17439 | . . . . . . . 8
⊢
((*𝑟‘ndx) ≠ (dist‘ndx) ∧
(le‘ndx) ≠ (dist‘ndx)) | 
| 37 | 36 | simpri 485 | . . . . . . 7
⊢
(le‘ndx) ≠ (dist‘ndx) | 
| 38 |  | fvex 6918 | . . . . . . . 8
⊢
(TopSet‘ndx) ∈ V | 
| 39 |  | fvex 6918 | . . . . . . . 8
⊢
(le‘ndx) ∈ V | 
| 40 |  | fvex 6918 | . . . . . . . 8
⊢
(dist‘ndx) ∈ V | 
| 41 |  | fvex 6918 | . . . . . . . 8
⊢
(MetOpen‘(abs ∘ − )) ∈ V | 
| 42 |  | letsr 18639 | . . . . . . . . 9
⊢  ≤
∈ TosetRel | 
| 43 | 42 | elexi 3502 | . . . . . . . 8
⊢  ≤
∈ V | 
| 44 |  | absf 15377 | . . . . . . . . . 10
⊢
abs:ℂ⟶ℝ | 
| 45 |  | fex 7247 | . . . . . . . . . 10
⊢
((abs:ℂ⟶ℝ ∧ ℂ ∈ V) → abs ∈
V) | 
| 46 | 44, 7, 45 | mp2an 692 | . . . . . . . . 9
⊢ abs
∈ V | 
| 47 |  | subf 11511 | . . . . . . . . . 10
⊢  −
:(ℂ × ℂ)⟶ℂ | 
| 48 | 7, 7 | xpex 7774 | . . . . . . . . . 10
⊢ (ℂ
× ℂ) ∈ V | 
| 49 |  | fex 7247 | . . . . . . . . . 10
⊢ ((
− :(ℂ × ℂ)⟶ℂ ∧ (ℂ ×
ℂ) ∈ V) → − ∈ V) | 
| 50 | 47, 48, 49 | mp2an 692 | . . . . . . . . 9
⊢  −
∈ V | 
| 51 | 46, 50 | coex 7953 | . . . . . . . 8
⊢ (abs
∘ − ) ∈ V | 
| 52 | 38, 39, 40, 41, 43, 51 | funtp 6622 | . . . . . . 7
⊢
(((TopSet‘ndx) ≠ (le‘ndx) ∧ (TopSet‘ndx) ≠
(dist‘ndx) ∧ (le‘ndx) ≠ (dist‘ndx)) → Fun
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉}) | 
| 53 | 33, 35, 37, 52 | mp3an 1462 | . . . . . 6
⊢ Fun
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} | 
| 54 |  | fvex 6918 | . . . . . . 7
⊢
(UnifSet‘ndx) ∈ V | 
| 55 |  | fvex 6918 | . . . . . . 7
⊢
(metUnif‘(abs ∘ − )) ∈ V | 
| 56 | 54, 55 | funsn 6618 | . . . . . 6
⊢ Fun
{〈(UnifSet‘ndx), (metUnif‘(abs ∘ −
))〉} | 
| 57 | 53, 56 | pm3.2i 470 | . . . . 5
⊢ (Fun
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∧ Fun {〈(UnifSet‘ndx), (metUnif‘(abs ∘
− ))〉}) | 
| 58 | 41, 43, 51 | dmtpop 6237 | . . . . . . 7
⊢ dom
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} = {(TopSet‘ndx), (le‘ndx),
(dist‘ndx)} | 
| 59 | 55 | dmsnop 6235 | . . . . . . 7
⊢ dom
{〈(UnifSet‘ndx), (metUnif‘(abs ∘ − ))〉} =
{(UnifSet‘ndx)} | 
| 60 | 58, 59 | ineq12i 4217 | . . . . . 6
⊢ (dom
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∩ dom {〈(UnifSet‘ndx), (metUnif‘(abs ∘
− ))〉}) = ({(TopSet‘ndx), (le‘ndx), (dist‘ndx)}
∩ {(UnifSet‘ndx)}) | 
| 61 |  | slotsdifunifndx 17446 | . . . . . . . 8
⊢
(((+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx) ∧
(*𝑟‘ndx) ≠ (UnifSet‘ndx)) ∧
((le‘ndx) ≠ (UnifSet‘ndx) ∧ (dist‘ndx) ≠
(UnifSet‘ndx))) | 
| 62 |  | unifndxntsetndx 17445 | . . . . . . . . . . . 12
⊢
(UnifSet‘ndx) ≠ (TopSet‘ndx) | 
| 63 | 62 | necomi 2994 | . . . . . . . . . . 11
⊢
(TopSet‘ndx) ≠ (UnifSet‘ndx) | 
| 64 | 63 | a1i 11 | . . . . . . . . . 10
⊢
(((+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx) ∧
(*𝑟‘ndx) ≠ (UnifSet‘ndx)) →
(TopSet‘ndx) ≠ (UnifSet‘ndx)) | 
| 65 | 64 | anim1i 615 | . . . . . . . . 9
⊢
((((+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx) ∧
(*𝑟‘ndx) ≠ (UnifSet‘ndx)) ∧
((le‘ndx) ≠ (UnifSet‘ndx) ∧ (dist‘ndx) ≠
(UnifSet‘ndx))) → ((TopSet‘ndx) ≠ (UnifSet‘ndx) ∧
((le‘ndx) ≠ (UnifSet‘ndx) ∧ (dist‘ndx) ≠
(UnifSet‘ndx)))) | 
| 66 |  | 3anass 1094 | . . . . . . . . 9
⊢
(((TopSet‘ndx) ≠ (UnifSet‘ndx) ∧ (le‘ndx) ≠
(UnifSet‘ndx) ∧ (dist‘ndx) ≠ (UnifSet‘ndx)) ↔
((TopSet‘ndx) ≠ (UnifSet‘ndx) ∧ ((le‘ndx) ≠
(UnifSet‘ndx) ∧ (dist‘ndx) ≠
(UnifSet‘ndx)))) | 
| 67 | 65, 66 | sylibr 234 | . . . . . . . 8
⊢
((((+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx) ∧
(*𝑟‘ndx) ≠ (UnifSet‘ndx)) ∧
((le‘ndx) ≠ (UnifSet‘ndx) ∧ (dist‘ndx) ≠
(UnifSet‘ndx))) → ((TopSet‘ndx) ≠ (UnifSet‘ndx) ∧
(le‘ndx) ≠ (UnifSet‘ndx) ∧ (dist‘ndx) ≠
(UnifSet‘ndx))) | 
| 68 | 61, 67 | ax-mp 5 | . . . . . . 7
⊢
((TopSet‘ndx) ≠ (UnifSet‘ndx) ∧ (le‘ndx) ≠
(UnifSet‘ndx) ∧ (dist‘ndx) ≠
(UnifSet‘ndx)) | 
| 69 |  | disjtpsn 4714 | . . . . . . 7
⊢
(((TopSet‘ndx) ≠ (UnifSet‘ndx) ∧ (le‘ndx) ≠
(UnifSet‘ndx) ∧ (dist‘ndx) ≠ (UnifSet‘ndx)) →
({(TopSet‘ndx), (le‘ndx), (dist‘ndx)} ∩
{(UnifSet‘ndx)}) = ∅) | 
| 70 | 68, 69 | ax-mp 5 | . . . . . 6
⊢
({(TopSet‘ndx), (le‘ndx), (dist‘ndx)} ∩
{(UnifSet‘ndx)}) = ∅ | 
| 71 | 60, 70 | eqtri 2764 | . . . . 5
⊢ (dom
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∩ dom {〈(UnifSet‘ndx), (metUnif‘(abs ∘
− ))〉}) = ∅ | 
| 72 |  | funun 6611 | . . . . 5
⊢ (((Fun
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∧ Fun {〈(UnifSet‘ndx), (metUnif‘(abs ∘
− ))〉}) ∧ (dom {〈(TopSet‘ndx), (MetOpen‘(abs
∘ − ))〉, 〈(le‘ndx), ≤ 〉,
〈(dist‘ndx), (abs ∘ − )〉} ∩ dom
{〈(UnifSet‘ndx), (metUnif‘(abs ∘ − ))〉}) =
∅) → Fun ({〈(TopSet‘ndx), (MetOpen‘(abs ∘
− ))〉, 〈(le‘ndx), ≤ 〉, 〈(dist‘ndx),
(abs ∘ − )〉} ∪ {〈(UnifSet‘ndx),
(metUnif‘(abs ∘ − ))〉})) | 
| 73 | 57, 71, 72 | mp2an 692 | . . . 4
⊢ Fun
({〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ {〈(UnifSet‘ndx), (metUnif‘(abs ∘ −
))〉}) | 
| 74 | 31, 73 | pm3.2i 470 | . . 3
⊢ (Fun
({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∪
{〈(*𝑟‘ndx), ∗〉}) ∧ Fun
({〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ {〈(UnifSet‘ndx), (metUnif‘(abs ∘ −
))〉})) | 
| 75 |  | dmun 5920 | . . . . 5
⊢ dom
({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∪
{〈(*𝑟‘ndx), ∗〉}) = (dom
{〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∪ dom
{〈(*𝑟‘ndx), ∗〉}) | 
| 76 |  | dmun 5920 | . . . . 5
⊢ dom
({〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ {〈(UnifSet‘ndx), (metUnif‘(abs ∘ −
))〉}) = (dom {〈(TopSet‘ndx), (MetOpen‘(abs ∘
− ))〉, 〈(le‘ndx), ≤ 〉, 〈(dist‘ndx),
(abs ∘ − )〉} ∪ dom {〈(UnifSet‘ndx),
(metUnif‘(abs ∘ − ))〉}) | 
| 77 | 75, 76 | ineq12i 4217 | . . . 4
⊢ (dom
({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∪
{〈(*𝑟‘ndx), ∗〉}) ∩ dom
({〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ {〈(UnifSet‘ndx), (metUnif‘(abs ∘ −
))〉})) = ((dom {〈(Base‘ndx), ℂ〉,
〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∪ dom
{〈(*𝑟‘ndx), ∗〉}) ∩ (dom
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ dom {〈(UnifSet‘ndx), (metUnif‘(abs ∘
− ))〉})) | 
| 78 | 18, 58 | ineq12i 4217 | . . . . . . . . 9
⊢ (dom
{〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∩ dom
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉}) = ({(Base‘ndx), (+g‘ndx),
(.r‘ndx)} ∩ {(TopSet‘ndx), (le‘ndx),
(dist‘ndx)}) | 
| 79 |  | tsetndxnbasendx 17401 | . . . . . . . . . . . 12
⊢
(TopSet‘ndx) ≠ (Base‘ndx) | 
| 80 | 79 | necomi 2994 | . . . . . . . . . . 11
⊢
(Base‘ndx) ≠ (TopSet‘ndx) | 
| 81 |  | tsetndxnplusgndx 17402 | . . . . . . . . . . . 12
⊢
(TopSet‘ndx) ≠ (+g‘ndx) | 
| 82 | 81 | necomi 2994 | . . . . . . . . . . 11
⊢
(+g‘ndx) ≠ (TopSet‘ndx) | 
| 83 |  | tsetndxnmulrndx 17403 | . . . . . . . . . . . 12
⊢
(TopSet‘ndx) ≠ (.r‘ndx) | 
| 84 | 83 | necomi 2994 | . . . . . . . . . . 11
⊢
(.r‘ndx) ≠ (TopSet‘ndx) | 
| 85 | 80, 82, 84 | 3pm3.2i 1339 | . . . . . . . . . 10
⊢
((Base‘ndx) ≠ (TopSet‘ndx) ∧
(+g‘ndx) ≠ (TopSet‘ndx) ∧
(.r‘ndx) ≠ (TopSet‘ndx)) | 
| 86 |  | plendxnbasendx 17415 | . . . . . . . . . . . 12
⊢
(le‘ndx) ≠ (Base‘ndx) | 
| 87 | 86 | necomi 2994 | . . . . . . . . . . 11
⊢
(Base‘ndx) ≠ (le‘ndx) | 
| 88 |  | plendxnplusgndx 17416 | . . . . . . . . . . . 12
⊢
(le‘ndx) ≠ (+g‘ndx) | 
| 89 | 88 | necomi 2994 | . . . . . . . . . . 11
⊢
(+g‘ndx) ≠ (le‘ndx) | 
| 90 |  | plendxnmulrndx 17417 | . . . . . . . . . . . 12
⊢
(le‘ndx) ≠ (.r‘ndx) | 
| 91 | 90 | necomi 2994 | . . . . . . . . . . 11
⊢
(.r‘ndx) ≠ (le‘ndx) | 
| 92 | 87, 89, 91 | 3pm3.2i 1339 | . . . . . . . . . 10
⊢
((Base‘ndx) ≠ (le‘ndx) ∧ (+g‘ndx)
≠ (le‘ndx) ∧ (.r‘ndx) ≠
(le‘ndx)) | 
| 93 |  | dsndxnbasendx 17434 | . . . . . . . . . . . 12
⊢
(dist‘ndx) ≠ (Base‘ndx) | 
| 94 | 93 | necomi 2994 | . . . . . . . . . . 11
⊢
(Base‘ndx) ≠ (dist‘ndx) | 
| 95 |  | dsndxnplusgndx 17435 | . . . . . . . . . . . 12
⊢
(dist‘ndx) ≠ (+g‘ndx) | 
| 96 | 95 | necomi 2994 | . . . . . . . . . . 11
⊢
(+g‘ndx) ≠ (dist‘ndx) | 
| 97 |  | dsndxnmulrndx 17436 | . . . . . . . . . . . 12
⊢
(dist‘ndx) ≠ (.r‘ndx) | 
| 98 | 97 | necomi 2994 | . . . . . . . . . . 11
⊢
(.r‘ndx) ≠ (dist‘ndx) | 
| 99 | 94, 96, 98 | 3pm3.2i 1339 | . . . . . . . . . 10
⊢
((Base‘ndx) ≠ (dist‘ndx) ∧ (+g‘ndx)
≠ (dist‘ndx) ∧ (.r‘ndx) ≠
(dist‘ndx)) | 
| 100 |  | disjtp2 4715 | . . . . . . . . . 10
⊢
((((Base‘ndx) ≠ (TopSet‘ndx) ∧
(+g‘ndx) ≠ (TopSet‘ndx) ∧
(.r‘ndx) ≠ (TopSet‘ndx)) ∧ ((Base‘ndx) ≠
(le‘ndx) ∧ (+g‘ndx) ≠ (le‘ndx) ∧
(.r‘ndx) ≠ (le‘ndx)) ∧ ((Base‘ndx) ≠
(dist‘ndx) ∧ (+g‘ndx) ≠ (dist‘ndx) ∧
(.r‘ndx) ≠ (dist‘ndx))) → ({(Base‘ndx),
(+g‘ndx), (.r‘ndx)} ∩
{(TopSet‘ndx), (le‘ndx), (dist‘ndx)}) =
∅) | 
| 101 | 85, 92, 99, 100 | mp3an 1462 | . . . . . . . . 9
⊢
({(Base‘ndx), (+g‘ndx),
(.r‘ndx)} ∩ {(TopSet‘ndx), (le‘ndx),
(dist‘ndx)}) = ∅ | 
| 102 | 78, 101 | eqtri 2764 | . . . . . . . 8
⊢ (dom
{〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∩ dom
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉}) = ∅ | 
| 103 | 18, 59 | ineq12i 4217 | . . . . . . . . 9
⊢ (dom
{〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∩ dom
{〈(UnifSet‘ndx), (metUnif‘(abs ∘ − ))〉}) =
({(Base‘ndx), (+g‘ndx), (.r‘ndx)} ∩
{(UnifSet‘ndx)}) | 
| 104 |  | unifndxnbasendx 17444 | . . . . . . . . . . . . . . 15
⊢
(UnifSet‘ndx) ≠ (Base‘ndx) | 
| 105 | 104 | necomi 2994 | . . . . . . . . . . . . . 14
⊢
(Base‘ndx) ≠ (UnifSet‘ndx) | 
| 106 | 105 | a1i 11 | . . . . . . . . . . . . 13
⊢
(((+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx) ∧
(*𝑟‘ndx) ≠ (UnifSet‘ndx)) →
(Base‘ndx) ≠ (UnifSet‘ndx)) | 
| 107 |  | 3simpa 1148 | . . . . . . . . . . . . 13
⊢
(((+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx) ∧
(*𝑟‘ndx) ≠ (UnifSet‘ndx)) →
((+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx))) | 
| 108 |  | 3anass 1094 | . . . . . . . . . . . . 13
⊢
(((Base‘ndx) ≠ (UnifSet‘ndx) ∧
(+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx)) ↔ ((Base‘ndx)
≠ (UnifSet‘ndx) ∧ ((+g‘ndx) ≠
(UnifSet‘ndx) ∧ (.r‘ndx) ≠
(UnifSet‘ndx)))) | 
| 109 | 106, 107,
108 | sylanbrc 583 | . . . . . . . . . . . 12
⊢
(((+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx) ∧
(*𝑟‘ndx) ≠ (UnifSet‘ndx)) →
((Base‘ndx) ≠ (UnifSet‘ndx) ∧ (+g‘ndx) ≠
(UnifSet‘ndx) ∧ (.r‘ndx) ≠
(UnifSet‘ndx))) | 
| 110 | 109 | adantr 480 | . . . . . . . . . . 11
⊢
((((+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx) ∧
(*𝑟‘ndx) ≠ (UnifSet‘ndx)) ∧
((le‘ndx) ≠ (UnifSet‘ndx) ∧ (dist‘ndx) ≠
(UnifSet‘ndx))) → ((Base‘ndx) ≠ (UnifSet‘ndx) ∧
(+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx))) | 
| 111 | 61, 110 | ax-mp 5 | . . . . . . . . . 10
⊢
((Base‘ndx) ≠ (UnifSet‘ndx) ∧
(+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx)) | 
| 112 |  | disjtpsn 4714 | . . . . . . . . . 10
⊢
(((Base‘ndx) ≠ (UnifSet‘ndx) ∧
(+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx)) → ({(Base‘ndx),
(+g‘ndx), (.r‘ndx)} ∩
{(UnifSet‘ndx)}) = ∅) | 
| 113 | 111, 112 | ax-mp 5 | . . . . . . . . 9
⊢
({(Base‘ndx), (+g‘ndx),
(.r‘ndx)} ∩ {(UnifSet‘ndx)}) =
∅ | 
| 114 | 103, 113 | eqtri 2764 | . . . . . . . 8
⊢ (dom
{〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∩ dom
{〈(UnifSet‘ndx), (metUnif‘(abs ∘ − ))〉}) =
∅ | 
| 115 | 102, 114 | pm3.2i 470 | . . . . . . 7
⊢ ((dom
{〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∩ dom
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉}) = ∅ ∧ (dom {〈(Base‘ndx), ℂ〉,
〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∩ dom
{〈(UnifSet‘ndx), (metUnif‘(abs ∘ − ))〉}) =
∅) | 
| 116 |  | undisj2 4462 | . . . . . . 7
⊢ (((dom
{〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∩ dom
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉}) = ∅ ∧ (dom {〈(Base‘ndx), ℂ〉,
〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∩ dom
{〈(UnifSet‘ndx), (metUnif‘(abs ∘ − ))〉}) =
∅) ↔ (dom {〈(Base‘ndx), ℂ〉,
〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∩ (dom
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ dom {〈(UnifSet‘ndx), (metUnif‘(abs ∘
− ))〉})) = ∅) | 
| 117 | 115, 116 | mpbi 230 | . . . . . 6
⊢ (dom
{〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∩ (dom
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ dom {〈(UnifSet‘ndx), (metUnif‘(abs ∘
− ))〉})) = ∅ | 
| 118 | 19, 58 | ineq12i 4217 | . . . . . . . . 9
⊢ (dom
{〈(*𝑟‘ndx), ∗〉} ∩ dom
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉}) = ({(*𝑟‘ndx)} ∩ {(TopSet‘ndx),
(le‘ndx), (dist‘ndx)}) | 
| 119 |  | tsetndxnstarvndx 17404 | . . . . . . . . . . 11
⊢
(TopSet‘ndx) ≠
(*𝑟‘ndx) | 
| 120 |  | necom 2993 | . . . . . . . . . . . . . 14
⊢
((*𝑟‘ndx) ≠ (le‘ndx) ↔
(le‘ndx) ≠ (*𝑟‘ndx)) | 
| 121 | 120 | biimpi 216 | . . . . . . . . . . . . 13
⊢
((*𝑟‘ndx) ≠ (le‘ndx) →
(le‘ndx) ≠ (*𝑟‘ndx)) | 
| 122 | 121 | adantr 480 | . . . . . . . . . . . 12
⊢
(((*𝑟‘ndx) ≠ (le‘ndx) ∧
(TopSet‘ndx) ≠ (le‘ndx)) → (le‘ndx) ≠
(*𝑟‘ndx)) | 
| 123 | 32, 122 | ax-mp 5 | . . . . . . . . . . 11
⊢
(le‘ndx) ≠ (*𝑟‘ndx) | 
| 124 |  | necom 2993 | . . . . . . . . . . . . . 14
⊢
((*𝑟‘ndx) ≠ (dist‘ndx) ↔
(dist‘ndx) ≠ (*𝑟‘ndx)) | 
| 125 | 124 | biimpi 216 | . . . . . . . . . . . . 13
⊢
((*𝑟‘ndx) ≠ (dist‘ndx) →
(dist‘ndx) ≠ (*𝑟‘ndx)) | 
| 126 | 125 | adantr 480 | . . . . . . . . . . . 12
⊢
(((*𝑟‘ndx) ≠ (dist‘ndx) ∧
(le‘ndx) ≠ (dist‘ndx)) → (dist‘ndx) ≠
(*𝑟‘ndx)) | 
| 127 | 36, 126 | ax-mp 5 | . . . . . . . . . . 11
⊢
(dist‘ndx) ≠ (*𝑟‘ndx) | 
| 128 |  | disjtpsn 4714 | . . . . . . . . . . 11
⊢
(((TopSet‘ndx) ≠ (*𝑟‘ndx) ∧
(le‘ndx) ≠ (*𝑟‘ndx) ∧ (dist‘ndx)
≠ (*𝑟‘ndx)) → ({(TopSet‘ndx),
(le‘ndx), (dist‘ndx)} ∩ {(*𝑟‘ndx)}) =
∅) | 
| 129 | 119, 123,
127, 128 | mp3an 1462 | . . . . . . . . . 10
⊢
({(TopSet‘ndx), (le‘ndx), (dist‘ndx)} ∩
{(*𝑟‘ndx)}) = ∅ | 
| 130 | 129 | ineqcomi 4210 | . . . . . . . . 9
⊢
({(*𝑟‘ndx)} ∩ {(TopSet‘ndx),
(le‘ndx), (dist‘ndx)}) = ∅ | 
| 131 | 118, 130 | eqtri 2764 | . . . . . . . 8
⊢ (dom
{〈(*𝑟‘ndx), ∗〉} ∩ dom
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉}) = ∅ | 
| 132 | 19, 59 | ineq12i 4217 | . . . . . . . . 9
⊢ (dom
{〈(*𝑟‘ndx), ∗〉} ∩ dom
{〈(UnifSet‘ndx), (metUnif‘(abs ∘ − ))〉}) =
({(*𝑟‘ndx)} ∩
{(UnifSet‘ndx)}) | 
| 133 |  | simpl3 1193 | . . . . . . . . . . 11
⊢
((((+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx) ∧
(*𝑟‘ndx) ≠ (UnifSet‘ndx)) ∧
((le‘ndx) ≠ (UnifSet‘ndx) ∧ (dist‘ndx) ≠
(UnifSet‘ndx))) → (*𝑟‘ndx) ≠
(UnifSet‘ndx)) | 
| 134 | 61, 133 | ax-mp 5 | . . . . . . . . . 10
⊢
(*𝑟‘ndx) ≠
(UnifSet‘ndx) | 
| 135 |  | disjsn2 4711 | . . . . . . . . . 10
⊢
((*𝑟‘ndx) ≠ (UnifSet‘ndx) →
({(*𝑟‘ndx)} ∩ {(UnifSet‘ndx)}) =
∅) | 
| 136 | 134, 135 | ax-mp 5 | . . . . . . . . 9
⊢
({(*𝑟‘ndx)} ∩ {(UnifSet‘ndx)}) =
∅ | 
| 137 | 132, 136 | eqtri 2764 | . . . . . . . 8
⊢ (dom
{〈(*𝑟‘ndx), ∗〉} ∩ dom
{〈(UnifSet‘ndx), (metUnif‘(abs ∘ − ))〉}) =
∅ | 
| 138 | 131, 137 | pm3.2i 470 | . . . . . . 7
⊢ ((dom
{〈(*𝑟‘ndx), ∗〉} ∩ dom
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉}) = ∅ ∧ (dom {〈(*𝑟‘ndx),
∗〉} ∩ dom {〈(UnifSet‘ndx), (metUnif‘(abs
∘ − ))〉}) = ∅) | 
| 139 |  | undisj2 4462 | . . . . . . 7
⊢ (((dom
{〈(*𝑟‘ndx), ∗〉} ∩ dom
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉}) = ∅ ∧ (dom {〈(*𝑟‘ndx),
∗〉} ∩ dom {〈(UnifSet‘ndx), (metUnif‘(abs
∘ − ))〉}) = ∅) ↔ (dom
{〈(*𝑟‘ndx), ∗〉} ∩ (dom
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ dom {〈(UnifSet‘ndx), (metUnif‘(abs ∘
− ))〉})) = ∅) | 
| 140 | 138, 139 | mpbi 230 | . . . . . 6
⊢ (dom
{〈(*𝑟‘ndx), ∗〉} ∩ (dom
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ dom {〈(UnifSet‘ndx), (metUnif‘(abs ∘
− ))〉})) = ∅ | 
| 141 | 117, 140 | pm3.2i 470 | . . . . 5
⊢ ((dom
{〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∩ (dom
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ dom {〈(UnifSet‘ndx), (metUnif‘(abs ∘
− ))〉})) = ∅ ∧ (dom
{〈(*𝑟‘ndx), ∗〉} ∩ (dom
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ dom {〈(UnifSet‘ndx), (metUnif‘(abs ∘
− ))〉})) = ∅) | 
| 142 |  | undisj1 4461 | . . . . 5
⊢ (((dom
{〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∩ (dom
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ dom {〈(UnifSet‘ndx), (metUnif‘(abs ∘
− ))〉})) = ∅ ∧ (dom
{〈(*𝑟‘ndx), ∗〉} ∩ (dom
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ dom {〈(UnifSet‘ndx), (metUnif‘(abs ∘
− ))〉})) = ∅) ↔ ((dom {〈(Base‘ndx),
ℂ〉, 〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∪ dom
{〈(*𝑟‘ndx), ∗〉}) ∩ (dom
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ dom {〈(UnifSet‘ndx), (metUnif‘(abs ∘
− ))〉})) = ∅) | 
| 143 | 141, 142 | mpbi 230 | . . . 4
⊢ ((dom
{〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∪ dom
{〈(*𝑟‘ndx), ∗〉}) ∩ (dom
{〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ dom {〈(UnifSet‘ndx), (metUnif‘(abs ∘
− ))〉})) = ∅ | 
| 144 | 77, 143 | eqtri 2764 | . . 3
⊢ (dom
({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∪
{〈(*𝑟‘ndx), ∗〉}) ∩ dom
({〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ {〈(UnifSet‘ndx), (metUnif‘(abs ∘ −
))〉})) = ∅ | 
| 145 |  | funun 6611 | . . 3
⊢ (((Fun
({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∪
{〈(*𝑟‘ndx), ∗〉}) ∧ Fun
({〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ {〈(UnifSet‘ndx), (metUnif‘(abs ∘ −
))〉})) ∧ (dom ({〈(Base‘ndx), ℂ〉,
〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∪
{〈(*𝑟‘ndx), ∗〉}) ∩ dom
({〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ {〈(UnifSet‘ndx), (metUnif‘(abs ∘ −
))〉})) = ∅) → Fun (({〈(Base‘ndx), ℂ〉,
〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∪
{〈(*𝑟‘ndx), ∗〉}) ∪
({〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ {〈(UnifSet‘ndx), (metUnif‘(abs ∘ −
))〉}))) | 
| 146 | 74, 144, 145 | mp2an 692 | . 2
⊢ Fun
(({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∪
{〈(*𝑟‘ndx), ∗〉}) ∪
({〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ {〈(UnifSet‘ndx), (metUnif‘(abs ∘ −
))〉})) | 
| 147 |  | df-cnfld 21366 | . . 3
⊢
ℂfld = (({〈(Base‘ndx), ℂ〉,
〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∪
{〈(*𝑟‘ndx), ∗〉}) ∪
({〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ {〈(UnifSet‘ndx), (metUnif‘(abs ∘ −
))〉})) | 
| 148 | 147 | funeqi 6586 | . 2
⊢ (Fun
ℂfld ↔ Fun (({〈(Base‘ndx), ℂ〉,
〈(+g‘ndx), (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 + 𝑣))〉, 〈(.r‘ndx),
(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))〉} ∪
{〈(*𝑟‘ndx), ∗〉}) ∪
({〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉,
〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ −
)〉} ∪ {〈(UnifSet‘ndx), (metUnif‘(abs ∘ −
))〉}))) | 
| 149 | 146, 148 | mpbir 231 | 1
⊢ Fun
ℂfld |