| Step |
Hyp |
Ref |
Expression |
| 1 |
|
basendxnplusgndx |
⊢ ( Base ‘ ndx ) ≠ ( +g ‘ ndx ) |
| 2 |
|
basendxnmulrndx |
⊢ ( Base ‘ ndx ) ≠ ( .r ‘ ndx ) |
| 3 |
|
plusgndxnmulrndx |
⊢ ( +g ‘ ndx ) ≠ ( .r ‘ ndx ) |
| 4 |
|
fvex |
⊢ ( Base ‘ ndx ) ∈ V |
| 5 |
|
fvex |
⊢ ( +g ‘ ndx ) ∈ V |
| 6 |
|
fvex |
⊢ ( .r ‘ ndx ) ∈ V |
| 7 |
|
cnex |
⊢ ℂ ∈ V |
| 8 |
|
addex |
⊢ + ∈ V |
| 9 |
|
mulex |
⊢ · ∈ V |
| 10 |
4 5 6 7 8 9
|
funtp |
⊢ ( ( ( 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 |
⊢ Fun { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } |
| 12 |
|
fvex |
⊢ ( *𝑟 ‘ ndx ) ∈ V |
| 13 |
|
cjf |
⊢ ∗ : ℂ ⟶ ℂ |
| 14 |
|
fex |
⊢ ( ( ∗ : ℂ ⟶ ℂ ∧ ℂ ∈ V ) → ∗ ∈ V ) |
| 15 |
13 7 14
|
mp2an |
⊢ ∗ ∈ V |
| 16 |
12 15
|
funsn |
⊢ Fun { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } |
| 17 |
11 16
|
pm3.2i |
⊢ ( Fun { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∧ Fun { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) |
| 18 |
7 8 9
|
dmtpop |
⊢ dom { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } = { ( Base ‘ ndx ) , ( +g ‘ ndx ) , ( .r ‘ ndx ) } |
| 19 |
15
|
dmsnop |
⊢ dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } = { ( *𝑟 ‘ ndx ) } |
| 20 |
18 19
|
ineq12i |
⊢ ( dom { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∩ dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) = ( { ( Base ‘ ndx ) , ( +g ‘ ndx ) , ( .r ‘ ndx ) } ∩ { ( *𝑟 ‘ ndx ) } ) |
| 21 |
|
starvndxnbasendx |
⊢ ( *𝑟 ‘ ndx ) ≠ ( Base ‘ ndx ) |
| 22 |
21
|
necomi |
⊢ ( Base ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) |
| 23 |
|
starvndxnplusgndx |
⊢ ( *𝑟 ‘ ndx ) ≠ ( +g ‘ ndx ) |
| 24 |
23
|
necomi |
⊢ ( +g ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) |
| 25 |
|
starvndxnmulrndx |
⊢ ( *𝑟 ‘ ndx ) ≠ ( .r ‘ ndx ) |
| 26 |
25
|
necomi |
⊢ ( .r ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) |
| 27 |
|
disjtpsn |
⊢ ( ( ( Base ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ∧ ( +g ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ) → ( { ( Base ‘ ndx ) , ( +g ‘ ndx ) , ( .r ‘ ndx ) } ∩ { ( *𝑟 ‘ ndx ) } ) = ∅ ) |
| 28 |
22 24 26 27
|
mp3an |
⊢ ( { ( Base ‘ ndx ) , ( +g ‘ ndx ) , ( .r ‘ ndx ) } ∩ { ( *𝑟 ‘ ndx ) } ) = ∅ |
| 29 |
20 28
|
eqtri |
⊢ ( dom { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∩ dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) = ∅ |
| 30 |
|
funun |
⊢ ( ( ( 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 |
⊢ Fun ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) |
| 32 |
|
slotsdifplendx |
⊢ ( ( *𝑟 ‘ ndx ) ≠ ( le ‘ ndx ) ∧ ( TopSet ‘ ndx ) ≠ ( le ‘ ndx ) ) |
| 33 |
32
|
simpri |
⊢ ( TopSet ‘ ndx ) ≠ ( le ‘ ndx ) |
| 34 |
|
dsndxntsetndx |
⊢ ( dist ‘ ndx ) ≠ ( TopSet ‘ ndx ) |
| 35 |
34
|
necomi |
⊢ ( TopSet ‘ ndx ) ≠ ( dist ‘ ndx ) |
| 36 |
|
slotsdifdsndx |
⊢ ( ( *𝑟 ‘ ndx ) ≠ ( dist ‘ ndx ) ∧ ( le ‘ ndx ) ≠ ( dist ‘ ndx ) ) |
| 37 |
36
|
simpri |
⊢ ( le ‘ ndx ) ≠ ( dist ‘ ndx ) |
| 38 |
|
fvex |
⊢ ( TopSet ‘ ndx ) ∈ V |
| 39 |
|
fvex |
⊢ ( le ‘ ndx ) ∈ V |
| 40 |
|
fvex |
⊢ ( dist ‘ ndx ) ∈ V |
| 41 |
|
fvex |
⊢ ( MetOpen ‘ ( abs ∘ − ) ) ∈ V |
| 42 |
|
letsr |
⊢ ≤ ∈ TosetRel |
| 43 |
42
|
elexi |
⊢ ≤ ∈ V |
| 44 |
|
absf |
⊢ abs : ℂ ⟶ ℝ |
| 45 |
|
fex |
⊢ ( ( abs : ℂ ⟶ ℝ ∧ ℂ ∈ V ) → abs ∈ V ) |
| 46 |
44 7 45
|
mp2an |
⊢ abs ∈ V |
| 47 |
|
subf |
⊢ − : ( ℂ × ℂ ) ⟶ ℂ |
| 48 |
7 7
|
xpex |
⊢ ( ℂ × ℂ ) ∈ V |
| 49 |
|
fex |
⊢ ( ( − : ( ℂ × ℂ ) ⟶ ℂ ∧ ( ℂ × ℂ ) ∈ V ) → − ∈ V ) |
| 50 |
47 48 49
|
mp2an |
⊢ − ∈ V |
| 51 |
46 50
|
coex |
⊢ ( abs ∘ − ) ∈ V |
| 52 |
38 39 40 41 43 51
|
funtp |
⊢ ( ( ( 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 |
⊢ Fun { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } |
| 54 |
|
fvex |
⊢ ( UnifSet ‘ ndx ) ∈ V |
| 55 |
|
fvex |
⊢ ( metUnif ‘ ( abs ∘ − ) ) ∈ V |
| 56 |
54 55
|
funsn |
⊢ Fun { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } |
| 57 |
53 56
|
pm3.2i |
⊢ ( Fun { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∧ Fun { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) |
| 58 |
41 43 51
|
dmtpop |
⊢ dom { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } = { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) } |
| 59 |
55
|
dmsnop |
⊢ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } = { ( UnifSet ‘ ndx ) } |
| 60 |
58 59
|
ineq12i |
⊢ ( 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 |
⊢ ( ( ( +g ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( *𝑟 ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ) ∧ ( ( le ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( dist ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ) ) |
| 62 |
|
unifndxntsetndx |
⊢ ( UnifSet ‘ ndx ) ≠ ( TopSet ‘ ndx ) |
| 63 |
62
|
necomi |
⊢ ( TopSet ‘ ndx ) ≠ ( UnifSet ‘ ndx ) |
| 64 |
63
|
a1i |
⊢ ( ( ( +g ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( *𝑟 ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ) → ( TopSet ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ) |
| 65 |
64
|
anim1i |
⊢ ( ( ( ( +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 |
⊢ ( ( ( 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 |
⊢ ( ( ( ( +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 |
⊢ ( ( TopSet ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( le ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( dist ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ) |
| 69 |
|
disjtpsn |
⊢ ( ( ( 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 |
⊢ ( { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) } ∩ { ( UnifSet ‘ ndx ) } ) = ∅ |
| 71 |
60 70
|
eqtri |
⊢ ( dom { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∩ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) = ∅ |
| 72 |
|
funun |
⊢ ( ( ( 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 |
⊢ Fun ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) |
| 74 |
31 73
|
pm3.2i |
⊢ ( Fun ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∧ Fun ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) |
| 75 |
|
dmun |
⊢ dom ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) = ( dom { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) |
| 76 |
|
dmun |
⊢ 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 |
⊢ ( 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 |
⊢ ( 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 |
⊢ ( TopSet ‘ ndx ) ≠ ( Base ‘ ndx ) |
| 80 |
79
|
necomi |
⊢ ( Base ‘ ndx ) ≠ ( TopSet ‘ ndx ) |
| 81 |
|
tsetndxnplusgndx |
⊢ ( TopSet ‘ ndx ) ≠ ( +g ‘ ndx ) |
| 82 |
81
|
necomi |
⊢ ( +g ‘ ndx ) ≠ ( TopSet ‘ ndx ) |
| 83 |
|
tsetndxnmulrndx |
⊢ ( TopSet ‘ ndx ) ≠ ( .r ‘ ndx ) |
| 84 |
83
|
necomi |
⊢ ( .r ‘ ndx ) ≠ ( TopSet ‘ ndx ) |
| 85 |
80 82 84
|
3pm3.2i |
⊢ ( ( Base ‘ ndx ) ≠ ( TopSet ‘ ndx ) ∧ ( +g ‘ ndx ) ≠ ( TopSet ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( TopSet ‘ ndx ) ) |
| 86 |
|
plendxnbasendx |
⊢ ( le ‘ ndx ) ≠ ( Base ‘ ndx ) |
| 87 |
86
|
necomi |
⊢ ( Base ‘ ndx ) ≠ ( le ‘ ndx ) |
| 88 |
|
plendxnplusgndx |
⊢ ( le ‘ ndx ) ≠ ( +g ‘ ndx ) |
| 89 |
88
|
necomi |
⊢ ( +g ‘ ndx ) ≠ ( le ‘ ndx ) |
| 90 |
|
plendxnmulrndx |
⊢ ( le ‘ ndx ) ≠ ( .r ‘ ndx ) |
| 91 |
90
|
necomi |
⊢ ( .r ‘ ndx ) ≠ ( le ‘ ndx ) |
| 92 |
87 89 91
|
3pm3.2i |
⊢ ( ( Base ‘ ndx ) ≠ ( le ‘ ndx ) ∧ ( +g ‘ ndx ) ≠ ( le ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( le ‘ ndx ) ) |
| 93 |
|
dsndxnbasendx |
⊢ ( dist ‘ ndx ) ≠ ( Base ‘ ndx ) |
| 94 |
93
|
necomi |
⊢ ( Base ‘ ndx ) ≠ ( dist ‘ ndx ) |
| 95 |
|
dsndxnplusgndx |
⊢ ( dist ‘ ndx ) ≠ ( +g ‘ ndx ) |
| 96 |
95
|
necomi |
⊢ ( +g ‘ ndx ) ≠ ( dist ‘ ndx ) |
| 97 |
|
dsndxnmulrndx |
⊢ ( dist ‘ ndx ) ≠ ( .r ‘ ndx ) |
| 98 |
97
|
necomi |
⊢ ( .r ‘ ndx ) ≠ ( dist ‘ ndx ) |
| 99 |
94 96 98
|
3pm3.2i |
⊢ ( ( Base ‘ ndx ) ≠ ( dist ‘ ndx ) ∧ ( +g ‘ ndx ) ≠ ( dist ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( dist ‘ ndx ) ) |
| 100 |
|
disjtp2 |
⊢ ( ( ( ( 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 |
⊢ ( { ( Base ‘ ndx ) , ( +g ‘ ndx ) , ( .r ‘ ndx ) } ∩ { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) } ) = ∅ |
| 102 |
78 101
|
eqtri |
⊢ ( dom { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∩ dom { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ) = ∅ |
| 103 |
18 59
|
ineq12i |
⊢ ( dom { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∩ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) = ( { ( Base ‘ ndx ) , ( +g ‘ ndx ) , ( .r ‘ ndx ) } ∩ { ( UnifSet ‘ ndx ) } ) |
| 104 |
|
unifndxnbasendx |
⊢ ( UnifSet ‘ ndx ) ≠ ( Base ‘ ndx ) |
| 105 |
104
|
necomi |
⊢ ( Base ‘ ndx ) ≠ ( UnifSet ‘ ndx ) |
| 106 |
105
|
a1i |
⊢ ( ( ( +g ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( *𝑟 ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ) → ( Base ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ) |
| 107 |
|
3simpa |
⊢ ( ( ( +g ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( *𝑟 ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ) → ( ( +g ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ) ) |
| 108 |
|
3anass |
⊢ ( ( ( 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 |
⊢ ( ( ( +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 |
⊢ ( ( ( ( +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 |
⊢ ( ( Base ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( +g ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ) |
| 112 |
|
disjtpsn |
⊢ ( ( ( 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 |
⊢ ( { ( Base ‘ ndx ) , ( +g ‘ ndx ) , ( .r ‘ ndx ) } ∩ { ( UnifSet ‘ ndx ) } ) = ∅ |
| 114 |
103 113
|
eqtri |
⊢ ( dom { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∩ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) = ∅ |
| 115 |
102 114
|
pm3.2i |
⊢ ( ( 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 |
⊢ ( ( ( 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 |
⊢ ( 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 |
⊢ ( dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ∩ dom { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ) = ( { ( *𝑟 ‘ ndx ) } ∩ { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) } ) |
| 119 |
|
tsetndxnstarvndx |
⊢ ( TopSet ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) |
| 120 |
|
necom |
⊢ ( ( *𝑟 ‘ ndx ) ≠ ( le ‘ ndx ) ↔ ( le ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ) |
| 121 |
120
|
biimpi |
⊢ ( ( *𝑟 ‘ ndx ) ≠ ( le ‘ ndx ) → ( le ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ) |
| 122 |
121
|
adantr |
⊢ ( ( ( *𝑟 ‘ ndx ) ≠ ( le ‘ ndx ) ∧ ( TopSet ‘ ndx ) ≠ ( le ‘ ndx ) ) → ( le ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ) |
| 123 |
32 122
|
ax-mp |
⊢ ( le ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) |
| 124 |
|
necom |
⊢ ( ( *𝑟 ‘ ndx ) ≠ ( dist ‘ ndx ) ↔ ( dist ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ) |
| 125 |
124
|
biimpi |
⊢ ( ( *𝑟 ‘ ndx ) ≠ ( dist ‘ ndx ) → ( dist ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ) |
| 126 |
125
|
adantr |
⊢ ( ( ( *𝑟 ‘ ndx ) ≠ ( dist ‘ ndx ) ∧ ( le ‘ ndx ) ≠ ( dist ‘ ndx ) ) → ( dist ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ) |
| 127 |
36 126
|
ax-mp |
⊢ ( dist ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) |
| 128 |
|
disjtpsn |
⊢ ( ( ( TopSet ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ∧ ( le ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ∧ ( dist ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ) → ( { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) } ∩ { ( *𝑟 ‘ ndx ) } ) = ∅ ) |
| 129 |
119 123 127 128
|
mp3an |
⊢ ( { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) } ∩ { ( *𝑟 ‘ ndx ) } ) = ∅ |
| 130 |
129
|
ineqcomi |
⊢ ( { ( *𝑟 ‘ ndx ) } ∩ { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) } ) = ∅ |
| 131 |
118 130
|
eqtri |
⊢ ( dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ∩ dom { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ) = ∅ |
| 132 |
19 59
|
ineq12i |
⊢ ( dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ∩ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) = ( { ( *𝑟 ‘ ndx ) } ∩ { ( UnifSet ‘ ndx ) } ) |
| 133 |
|
simpl3 |
⊢ ( ( ( ( +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 |
⊢ ( *𝑟 ‘ ndx ) ≠ ( UnifSet ‘ ndx ) |
| 135 |
|
disjsn2 |
⊢ ( ( *𝑟 ‘ ndx ) ≠ ( UnifSet ‘ ndx ) → ( { ( *𝑟 ‘ ndx ) } ∩ { ( UnifSet ‘ ndx ) } ) = ∅ ) |
| 136 |
134 135
|
ax-mp |
⊢ ( { ( *𝑟 ‘ ndx ) } ∩ { ( UnifSet ‘ ndx ) } ) = ∅ |
| 137 |
132 136
|
eqtri |
⊢ ( dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ∩ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) = ∅ |
| 138 |
131 137
|
pm3.2i |
⊢ ( ( dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ∩ dom { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ) = ∅ ∧ ( dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ∩ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) = ∅ ) |
| 139 |
|
undisj2 |
⊢ ( ( ( 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 |
⊢ ( dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ∩ ( dom { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) = ∅ |
| 141 |
117 140
|
pm3.2i |
⊢ ( ( 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 |
⊢ ( ( ( 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 |
⊢ ( ( 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 |
⊢ ( dom ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∩ dom ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) = ∅ |
| 145 |
|
funun |
⊢ ( ( ( 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 |
⊢ Fun ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) |
| 147 |
|
df-cnfld |
⊢ ℂfld = ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) |
| 148 |
147
|
funeqi |
⊢ ( 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 |
⊢ Fun ℂfld |