Step | Hyp | Ref
| Expression |
1 | | cnfldstr 20946 |
. 2
⊢
ℂfld Struct ⟨1, ;13⟩ |
2 | | structn0fun 17084 |
. . 3
⊢
(ℂfld Struct ⟨1, ;13⟩ → Fun (ℂfld ∖
{∅})) |
3 | | fvex 6905 |
. . . . . . . . . . . . 13
⊢
(Base‘ndx) ∈ V |
4 | | cnex 11191 |
. . . . . . . . . . . . 13
⊢ ℂ
∈ V |
5 | 3, 4 | opnzi 5475 |
. . . . . . . . . . . 12
⊢
⟨(Base‘ndx), ℂ⟩ ≠ ∅ |
6 | 5 | nesymi 2999 |
. . . . . . . . . . 11
⊢ ¬
∅ = ⟨(Base‘ndx), ℂ⟩ |
7 | | fvex 6905 |
. . . . . . . . . . . . 13
⊢
(+g‘ndx) ∈ V |
8 | | addex 12972 |
. . . . . . . . . . . . 13
⊢ + ∈
V |
9 | 7, 8 | opnzi 5475 |
. . . . . . . . . . . 12
⊢
⟨(+g‘ndx), + ⟩ ≠ ∅ |
10 | 9 | nesymi 2999 |
. . . . . . . . . . 11
⊢ ¬
∅ = ⟨(+g‘ndx), + ⟩ |
11 | | fvex 6905 |
. . . . . . . . . . . . 13
⊢
(.r‘ndx) ∈ V |
12 | | mulex 12973 |
. . . . . . . . . . . . 13
⊢ ·
∈ V |
13 | 11, 12 | opnzi 5475 |
. . . . . . . . . . . 12
⊢
⟨(.r‘ndx), · ⟩ ≠
∅ |
14 | 13 | nesymi 2999 |
. . . . . . . . . . 11
⊢ ¬
∅ = ⟨(.r‘ndx), · ⟩ |
15 | | 3ioran 1107 |
. . . . . . . . . . . 12
⊢ (¬
(∅ = ⟨(Base‘ndx), ℂ⟩ ∨ ∅ =
⟨(+g‘ndx), + ⟩ ∨ ∅ =
⟨(.r‘ndx), · ⟩) ↔ (¬ ∅ =
⟨(Base‘ndx), ℂ⟩ ∧ ¬ ∅ =
⟨(+g‘ndx), + ⟩ ∧ ¬ ∅ =
⟨(.r‘ndx), · ⟩)) |
16 | | 0ex 5308 |
. . . . . . . . . . . . 13
⊢ ∅
∈ V |
17 | 16 | eltp 4693 |
. . . . . . . . . . . 12
⊢ (∅
∈ {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx),
+ ⟩, ⟨(.r‘ndx), · ⟩} ↔ (∅ =
⟨(Base‘ndx), ℂ⟩ ∨ ∅ =
⟨(+g‘ndx), + ⟩ ∨ ∅ =
⟨(.r‘ndx), · ⟩)) |
18 | 15, 17 | xchnxbir 333 |
. . . . . . . . . . 11
⊢ (¬
∅ ∈ {⟨(Base‘ndx), ℂ⟩,
⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx),
· ⟩} ↔ (¬ ∅ = ⟨(Base‘ndx), ℂ⟩
∧ ¬ ∅ = ⟨(+g‘ndx), + ⟩ ∧ ¬
∅ = ⟨(.r‘ndx), · ⟩)) |
19 | 6, 10, 14, 18 | mpbir3an 1342 |
. . . . . . . . . 10
⊢ ¬
∅ ∈ {⟨(Base‘ndx), ℂ⟩,
⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx),
· ⟩} |
20 | | fvex 6905 |
. . . . . . . . . . . . 13
⊢
(*𝑟‘ndx) ∈ V |
21 | | cjf 15051 |
. . . . . . . . . . . . . 14
⊢
∗:ℂ⟶ℂ |
22 | | fex 7228 |
. . . . . . . . . . . . . 14
⊢
((∗:ℂ⟶ℂ ∧ ℂ ∈ V) →
∗ ∈ V) |
23 | 21, 4, 22 | mp2an 691 |
. . . . . . . . . . . . 13
⊢ ∗
∈ V |
24 | 20, 23 | opnzi 5475 |
. . . . . . . . . . . 12
⊢
⟨(*𝑟‘ndx), ∗⟩ ≠
∅ |
25 | 24 | necomi 2996 |
. . . . . . . . . . 11
⊢ ∅
≠ ⟨(*𝑟‘ndx), ∗⟩ |
26 | | nelsn 4669 |
. . . . . . . . . . 11
⊢ (∅
≠ ⟨(*𝑟‘ndx), ∗⟩ → ¬
∅ ∈ {⟨(*𝑟‘ndx),
∗⟩}) |
27 | 25, 26 | ax-mp 5 |
. . . . . . . . . 10
⊢ ¬
∅ ∈ {⟨(*𝑟‘ndx),
∗⟩} |
28 | 19, 27 | pm3.2i 472 |
. . . . . . . . 9
⊢ (¬
∅ ∈ {⟨(Base‘ndx), ℂ⟩,
⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx),
· ⟩} ∧ ¬ ∅ ∈
{⟨(*𝑟‘ndx), ∗⟩}) |
29 | | fvex 6905 |
. . . . . . . . . . . . . 14
⊢
(TopSet‘ndx) ∈ V |
30 | | fvex 6905 |
. . . . . . . . . . . . . 14
⊢
(MetOpen‘(abs ∘ − )) ∈ V |
31 | 29, 30 | opnzi 5475 |
. . . . . . . . . . . . 13
⊢
⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩
≠ ∅ |
32 | 31 | nesymi 2999 |
. . . . . . . . . . . 12
⊢ ¬
∅ = ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ −
))⟩ |
33 | | fvex 6905 |
. . . . . . . . . . . . . 14
⊢
(le‘ndx) ∈ V |
34 | | letsr 18546 |
. . . . . . . . . . . . . . 15
⊢ ≤
∈ TosetRel |
35 | 34 | elexi 3494 |
. . . . . . . . . . . . . 14
⊢ ≤
∈ V |
36 | 33, 35 | opnzi 5475 |
. . . . . . . . . . . . 13
⊢
⟨(le‘ndx), ≤ ⟩ ≠ ∅ |
37 | 36 | nesymi 2999 |
. . . . . . . . . . . 12
⊢ ¬
∅ = ⟨(le‘ndx), ≤ ⟩ |
38 | | fvex 6905 |
. . . . . . . . . . . . . 14
⊢
(dist‘ndx) ∈ V |
39 | | absf 15284 |
. . . . . . . . . . . . . . . 16
⊢
abs:ℂ⟶ℝ |
40 | | fex 7228 |
. . . . . . . . . . . . . . . 16
⊢
((abs:ℂ⟶ℝ ∧ ℂ ∈ V) → abs ∈
V) |
41 | 39, 4, 40 | mp2an 691 |
. . . . . . . . . . . . . . 15
⊢ abs
∈ V |
42 | | subf 11462 |
. . . . . . . . . . . . . . . 16
⊢ −
:(ℂ × ℂ)⟶ℂ |
43 | 4, 4 | xpex 7740 |
. . . . . . . . . . . . . . . 16
⊢ (ℂ
× ℂ) ∈ V |
44 | | fex 7228 |
. . . . . . . . . . . . . . . 16
⊢ ((
− :(ℂ × ℂ)⟶ℂ ∧ (ℂ ×
ℂ) ∈ V) → − ∈ V) |
45 | 42, 43, 44 | mp2an 691 |
. . . . . . . . . . . . . . 15
⊢ −
∈ V |
46 | 41, 45 | coex 7921 |
. . . . . . . . . . . . . 14
⊢ (abs
∘ − ) ∈ V |
47 | 38, 46 | opnzi 5475 |
. . . . . . . . . . . . 13
⊢
⟨(dist‘ndx), (abs ∘ − )⟩ ≠
∅ |
48 | 47 | nesymi 2999 |
. . . . . . . . . . . 12
⊢ ¬
∅ = ⟨(dist‘ndx), (abs ∘ − )⟩ |
49 | | 3ioran 1107 |
. . . . . . . . . . . 12
⊢ (¬
(∅ = ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ −
))⟩ ∨ ∅ = ⟨(le‘ndx), ≤ ⟩ ∨ ∅ =
⟨(dist‘ndx), (abs ∘ − )⟩) ↔ (¬ ∅ =
⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩ ∧
¬ ∅ = ⟨(le‘ndx), ≤ ⟩ ∧ ¬ ∅ =
⟨(dist‘ndx), (abs ∘ − )⟩)) |
50 | 32, 37, 48, 49 | mpbir3an 1342 |
. . . . . . . . . . 11
⊢ ¬
(∅ = ⟨(TopSet‘ndx), (MetOpen‘(abs ∘ −
))⟩ ∨ ∅ = ⟨(le‘ndx), ≤ ⟩ ∨ ∅ =
⟨(dist‘ndx), (abs ∘ − )⟩) |
51 | 16 | eltp 4693 |
. . . . . . . . . . 11
⊢ (∅
∈ {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ↔ (∅ = ⟨(TopSet‘ndx), (MetOpen‘(abs
∘ − ))⟩ ∨ ∅ = ⟨(le‘ndx), ≤ ⟩ ∨
∅ = ⟨(dist‘ndx), (abs ∘ −
)⟩)) |
52 | 50, 51 | mtbir 323 |
. . . . . . . . . 10
⊢ ¬
∅ ∈ {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ −
))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs
∘ − )⟩} |
53 | | fvex 6905 |
. . . . . . . . . . . . 13
⊢
(UnifSet‘ndx) ∈ V |
54 | | fvex 6905 |
. . . . . . . . . . . . 13
⊢
(metUnif‘(abs ∘ − )) ∈ V |
55 | 53, 54 | opnzi 5475 |
. . . . . . . . . . . 12
⊢
⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
≠ ∅ |
56 | 55 | necomi 2996 |
. . . . . . . . . . 11
⊢ ∅
≠ ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ −
))⟩ |
57 | | nelsn 4669 |
. . . . . . . . . . 11
⊢ (∅
≠ ⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩
→ ¬ ∅ ∈ {⟨(UnifSet‘ndx), (metUnif‘(abs
∘ − ))⟩}) |
58 | 56, 57 | ax-mp 5 |
. . . . . . . . . 10
⊢ ¬
∅ ∈ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ −
))⟩} |
59 | 52, 58 | pm3.2i 472 |
. . . . . . . . 9
⊢ (¬
∅ ∈ {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ −
))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs
∘ − )⟩} ∧ ¬ ∅ ∈ {⟨(UnifSet‘ndx),
(metUnif‘(abs ∘ − ))⟩}) |
60 | 28, 59 | pm3.2i 472 |
. . . . . . . 8
⊢ ((¬
∅ ∈ {⟨(Base‘ndx), ℂ⟩,
⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx),
· ⟩} ∧ ¬ ∅ ∈
{⟨(*𝑟‘ndx), ∗⟩}) ∧ (¬ ∅
∈ {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∧ ¬ ∅ ∈ {⟨(UnifSet‘ndx),
(metUnif‘(abs ∘ − ))⟩})) |
61 | | ioran 983 |
. . . . . . . . 9
⊢ (¬
((∅ ∈ {⟨(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
∘ − ))⟩}))) |
62 | | ioran 983 |
. . . . . . . . . 10
⊢ (¬
(∅ ∈ {⟨(Base‘ndx), ℂ⟩,
⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx),
· ⟩} ∨ ∅ ∈ {⟨(*𝑟‘ndx),
∗⟩}) ↔ (¬ ∅ ∈ {⟨(Base‘ndx),
ℂ⟩, ⟨(+g‘ndx), + ⟩,
⟨(.r‘ndx), · ⟩} ∧ ¬ ∅ ∈
{⟨(*𝑟‘ndx), ∗⟩})) |
63 | | ioran 983 |
. . . . . . . . . 10
⊢ (¬
(∅ ∈ {⟨(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 ∘ − ))⟩})) |
64 | 62, 63 | anbi12i 628 |
. . . . . . . . 9
⊢ ((¬
(∅ ∈ {⟨(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 | 61, 64 | bitri 275 |
. . . . . . . 8
⊢ (¬
((∅ ∈ {⟨(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 ∘ − ))⟩}))) |
66 | 60, 65 | mpbir 230 |
. . . . . . 7
⊢ ¬
((∅ ∈ {⟨(Base‘ndx), ℂ⟩,
⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx),
· ⟩} ∨ ∅ ∈ {⟨(*𝑟‘ndx),
∗⟩}) ∨ (∅ ∈ {⟨(TopSet‘ndx),
(MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤
⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∨ ∅
∈ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ −
))⟩})) |
67 | | df-cnfld 20945 |
. . . . . . . . 9
⊢
ℂfld = (({⟨(Base‘ndx), ℂ⟩,
⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx),
· ⟩} ∪ {⟨(*𝑟‘ndx),
∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘
− ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx),
(abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx),
(metUnif‘(abs ∘ − ))⟩})) |
68 | 67 | eleq2i 2826 |
. . . . . . . 8
⊢ (∅
∈ ℂfld ↔ ∅ ∈ (({⟨(Base‘ndx),
ℂ⟩, ⟨(+g‘ndx), + ⟩,
⟨(.r‘ndx), · ⟩} ∪
{⟨(*𝑟‘ndx), ∗⟩}) ∪
({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ −
))⟩}))) |
69 | | elun 4149 |
. . . . . . . 8
⊢ (∅
∈ (({⟨(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 ∘ −
))⟩}))) |
70 | | elun 4149 |
. . . . . . . . 9
⊢ (∅
∈ ({⟨(Base‘ndx), ℂ⟩,
⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx),
· ⟩} ∪ {⟨(*𝑟‘ndx),
∗⟩}) ↔ (∅ ∈ {⟨(Base‘ndx), ℂ⟩,
⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx),
· ⟩} ∨ ∅ ∈ {⟨(*𝑟‘ndx),
∗⟩})) |
71 | | elun 4149 |
. . . . . . . . 9
⊢ (∅
∈ ({⟨(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 ∘ −
))⟩})) |
72 | 70, 71 | orbi12i 914 |
. . . . . . . 8
⊢ ((∅
∈ ({⟨(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 ∘ −
))⟩}))) |
73 | 68, 69, 72 | 3bitri 297 |
. . . . . . 7
⊢ (∅
∈ ℂfld ↔ ((∅ ∈ {⟨(Base‘ndx),
ℂ⟩, ⟨(+g‘ndx), + ⟩,
⟨(.r‘ndx), · ⟩} ∨ ∅ ∈
{⟨(*𝑟‘ndx), ∗⟩}) ∨ (∅ ∈
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∨ ∅ ∈ {⟨(UnifSet‘ndx), (metUnif‘(abs
∘ − ))⟩}))) |
74 | 66, 73 | mtbir 323 |
. . . . . 6
⊢ ¬
∅ ∈ ℂfld |
75 | | disjsn 4716 |
. . . . . 6
⊢
((ℂfld ∩ {∅}) = ∅ ↔ ¬ ∅
∈ ℂfld) |
76 | 74, 75 | mpbir 230 |
. . . . 5
⊢
(ℂfld ∩ {∅}) = ∅ |
77 | | disjdif2 4480 |
. . . . 5
⊢
((ℂfld ∩ {∅}) = ∅ →
(ℂfld ∖ {∅}) =
ℂfld) |
78 | 76, 77 | ax-mp 5 |
. . . 4
⊢
(ℂfld ∖ {∅}) =
ℂfld |
79 | 78 | funeqi 6570 |
. . 3
⊢ (Fun
(ℂfld ∖ {∅}) ↔ Fun
ℂfld) |
80 | 2, 79 | sylib 217 |
. 2
⊢
(ℂfld Struct ⟨1, ;13⟩ → Fun
ℂfld) |
81 | 1, 80 | ax-mp 5 |
1
⊢ Fun
ℂfld |