| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cnfldstr |
⊢ ℂfld Struct ⟨ 1 , ; 1 3 ⟩ |
| 2 |
|
structn0fun |
⊢ ( ℂfld Struct ⟨ 1 , ; 1 3 ⟩ → Fun ( ℂfld ∖ { ∅ } ) ) |
| 3 |
|
fvex |
⊢ ( Base ‘ ndx ) ∈ V |
| 4 |
|
cnex |
⊢ ℂ ∈ V |
| 5 |
3 4
|
opnzi |
⊢ ⟨ ( Base ‘ ndx ) , ℂ ⟩ ≠ ∅ |
| 6 |
5
|
nesymi |
⊢ ¬ ∅ = ⟨ ( Base ‘ ndx ) , ℂ ⟩ |
| 7 |
|
fvex |
⊢ ( +g ‘ ndx ) ∈ V |
| 8 |
|
mpoaddex |
⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ∈ V |
| 9 |
7 8
|
opnzi |
⊢ ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ ≠ ∅ |
| 10 |
9
|
nesymi |
⊢ ¬ ∅ = ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ |
| 11 |
|
fvex |
⊢ ( .r ‘ ndx ) ∈ V |
| 12 |
|
mpomulex |
⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ V |
| 13 |
11 12
|
opnzi |
⊢ ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ ≠ ∅ |
| 14 |
13
|
nesymi |
⊢ ¬ ∅ = ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ |
| 15 |
|
3ioran |
⊢ ( ¬ ( ∅ = ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∨ ∅ = ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ ∨ ∅ = ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ ) ↔ ( ¬ ∅ = ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∧ ¬ ∅ = ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ ∧ ¬ ∅ = ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ ) ) |
| 16 |
|
0ex |
⊢ ∅ ∈ V |
| 17 |
16
|
eltp |
⊢ ( ∅ ∈ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ↔ ( ∅ = ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∨ ∅ = ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ ∨ ∅ = ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ ) ) |
| 18 |
15 17
|
xchnxbir |
⊢ ( ¬ ∅ ∈ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ↔ ( ¬ ∅ = ⟨ ( Base ‘ ndx ) , ℂ ⟩ ∧ ¬ ∅ = ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ ∧ ¬ ∅ = ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ ) ) |
| 19 |
6 10 14 18
|
mpbir3an |
⊢ ¬ ∅ ∈ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } |
| 20 |
|
fvex |
⊢ ( *𝑟 ‘ ndx ) ∈ V |
| 21 |
|
cjf |
⊢ ∗ : ℂ ⟶ ℂ |
| 22 |
|
fex |
⊢ ( ( ∗ : ℂ ⟶ ℂ ∧ ℂ ∈ V ) → ∗ ∈ V ) |
| 23 |
21 4 22
|
mp2an |
⊢ ∗ ∈ V |
| 24 |
20 23
|
opnzi |
⊢ ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ ≠ ∅ |
| 25 |
24
|
necomi |
⊢ ∅ ≠ ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ |
| 26 |
|
nelsn |
⊢ ( ∅ ≠ ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ → ¬ ∅ ∈ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) |
| 27 |
25 26
|
ax-mp |
⊢ ¬ ∅ ∈ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } |
| 28 |
19 27
|
pm3.2i |
⊢ ( ¬ ∅ ∈ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∧ ¬ ∅ ∈ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) |
| 29 |
|
fvex |
⊢ ( TopSet ‘ ndx ) ∈ V |
| 30 |
|
fvex |
⊢ ( MetOpen ‘ ( abs ∘ − ) ) ∈ V |
| 31 |
29 30
|
opnzi |
⊢ ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ ≠ ∅ |
| 32 |
31
|
nesymi |
⊢ ¬ ∅ = ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ |
| 33 |
|
fvex |
⊢ ( le ‘ ndx ) ∈ V |
| 34 |
|
letsr |
⊢ ≤ ∈ TosetRel |
| 35 |
34
|
elexi |
⊢ ≤ ∈ V |
| 36 |
33 35
|
opnzi |
⊢ ⟨ ( le ‘ ndx ) , ≤ ⟩ ≠ ∅ |
| 37 |
36
|
nesymi |
⊢ ¬ ∅ = ⟨ ( le ‘ ndx ) , ≤ ⟩ |
| 38 |
|
fvex |
⊢ ( dist ‘ ndx ) ∈ V |
| 39 |
|
absf |
⊢ abs : ℂ ⟶ ℝ |
| 40 |
|
fex |
⊢ ( ( abs : ℂ ⟶ ℝ ∧ ℂ ∈ V ) → abs ∈ V ) |
| 41 |
39 4 40
|
mp2an |
⊢ abs ∈ V |
| 42 |
|
subf |
⊢ − : ( ℂ × ℂ ) ⟶ ℂ |
| 43 |
4 4
|
xpex |
⊢ ( ℂ × ℂ ) ∈ V |
| 44 |
|
fex |
⊢ ( ( − : ( ℂ × ℂ ) ⟶ ℂ ∧ ( ℂ × ℂ ) ∈ V ) → − ∈ V ) |
| 45 |
42 43 44
|
mp2an |
⊢ − ∈ V |
| 46 |
41 45
|
coex |
⊢ ( abs ∘ − ) ∈ V |
| 47 |
38 46
|
opnzi |
⊢ ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ ≠ ∅ |
| 48 |
47
|
nesymi |
⊢ ¬ ∅ = ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ |
| 49 |
32 37 48
|
3pm3.2ni |
⊢ ¬ ( ∅ = ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ ∨ ∅ = ⟨ ( le ‘ ndx ) , ≤ ⟩ ∨ ∅ = ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ ) |
| 50 |
16
|
eltp |
⊢ ( ∅ ∈ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ↔ ( ∅ = ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ ∨ ∅ = ⟨ ( le ‘ ndx ) , ≤ ⟩ ∨ ∅ = ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ ) ) |
| 51 |
49 50
|
mtbir |
⊢ ¬ ∅ ∈ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } |
| 52 |
|
fvex |
⊢ ( UnifSet ‘ ndx ) ∈ V |
| 53 |
|
fvex |
⊢ ( metUnif ‘ ( abs ∘ − ) ) ∈ V |
| 54 |
52 53
|
opnzi |
⊢ ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ ≠ ∅ |
| 55 |
54
|
necomi |
⊢ ∅ ≠ ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ |
| 56 |
|
nelsn |
⊢ ( ∅ ≠ ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ → ¬ ∅ ∈ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) |
| 57 |
55 56
|
ax-mp |
⊢ ¬ ∅ ∈ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } |
| 58 |
51 57
|
pm3.2i |
⊢ ( ¬ ∅ ∈ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∧ ¬ ∅ ∈ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) |
| 59 |
28 58
|
pm3.2i |
⊢ ( ( ¬ ∅ ∈ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∧ ¬ ∅ ∈ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∧ ( ¬ ∅ ∈ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∧ ¬ ∅ ∈ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) |
| 60 |
|
ioran |
⊢ ( ¬ ( ( ∅ ∈ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∨ ∅ ∈ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∨ ( ∅ ∈ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∨ ∅ ∈ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) ↔ ( ¬ ( ∅ ∈ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∨ ∅ ∈ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∧ ¬ ( ∅ ∈ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∨ ∅ ∈ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) ) |
| 61 |
|
ioran |
⊢ ( ¬ ( ∅ ∈ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∨ ∅ ∈ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ↔ ( ¬ ∅ ∈ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∧ ¬ ∅ ∈ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ) |
| 62 |
|
ioran |
⊢ ( ¬ ( ∅ ∈ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∨ ∅ ∈ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ↔ ( ¬ ∅ ∈ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∧ ¬ ∅ ∈ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) |
| 63 |
61 62
|
anbi12i |
⊢ ( ( ¬ ( ∅ ∈ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∨ ∅ ∈ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∧ ¬ ( ∅ ∈ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∨ ∅ ∈ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) ↔ ( ( ¬ ∅ ∈ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∧ ¬ ∅ ∈ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∧ ( ¬ ∅ ∈ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∧ ¬ ∅ ∈ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) ) |
| 64 |
60 63
|
bitri |
⊢ ( ¬ ( ( ∅ ∈ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∨ ∅ ∈ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∨ ( ∅ ∈ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∨ ∅ ∈ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) ↔ ( ( ¬ ∅ ∈ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∧ ¬ ∅ ∈ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∧ ( ¬ ∅ ∈ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∧ ¬ ∅ ∈ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) ) |
| 65 |
59 64
|
mpbir |
⊢ ¬ ( ( ∅ ∈ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∨ ∅ ∈ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∨ ( ∅ ∈ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∨ ∅ ∈ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) |
| 66 |
|
df-cnfld |
⊢ ℂfld = ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) |
| 67 |
66
|
eleq2i |
⊢ ( ∅ ∈ ℂfld ↔ ∅ ∈ ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) ) |
| 68 |
|
elun |
⊢ ( ∅ ∈ ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) ↔ ( ∅ ∈ ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∨ ∅ ∈ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) ) |
| 69 |
|
elun |
⊢ ( ∅ ∈ ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ↔ ( ∅ ∈ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∨ ∅ ∈ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ) |
| 70 |
|
elun |
⊢ ( ∅ ∈ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ↔ ( ∅ ∈ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∨ ∅ ∈ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) |
| 71 |
69 70
|
orbi12i |
⊢ ( ( ∅ ∈ ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∨ ∅ ∈ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) ↔ ( ( ∅ ∈ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∨ ∅ ∈ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∨ ( ∅ ∈ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∨ ∅ ∈ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) ) |
| 72 |
67 68 71
|
3bitri |
⊢ ( ∅ ∈ ℂfld ↔ ( ( ∅ ∈ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∨ ∅ ∈ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∨ ( ∅ ∈ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∨ ∅ ∈ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) ) |
| 73 |
65 72
|
mtbir |
⊢ ¬ ∅ ∈ ℂfld |
| 74 |
|
disjsn |
⊢ ( ( ℂfld ∩ { ∅ } ) = ∅ ↔ ¬ ∅ ∈ ℂfld ) |
| 75 |
73 74
|
mpbir |
⊢ ( ℂfld ∩ { ∅ } ) = ∅ |
| 76 |
|
disjdif2 |
⊢ ( ( ℂfld ∩ { ∅ } ) = ∅ → ( ℂfld ∖ { ∅ } ) = ℂfld ) |
| 77 |
75 76
|
ax-mp |
⊢ ( ℂfld ∖ { ∅ } ) = ℂfld |
| 78 |
77
|
funeqi |
⊢ ( Fun ( ℂfld ∖ { ∅ } ) ↔ Fun ℂfld ) |
| 79 |
2 78
|
sylib |
⊢ ( ℂfld Struct ⟨ 1 , ; 1 3 ⟩ → Fun ℂfld ) |
| 80 |
1 79
|
ax-mp |
⊢ Fun ℂfld |