Metamath Proof Explorer

Theorem cnfldfunALT

Description: Alternate proof of cnfldfun (much shorter proof, using cnfldstr and structn0fun : in addition, it must be shown that (/) e/ CCfld ). (Contributed by AV, 18-Nov-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cnfldfunALT Fun ℂfld

Proof

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 addex ⊢ + ∈ V
9 7 8 opnzi ⊢ ⟨ ( +g ‘ ndx ) , + ⟩ ≠ ∅
10 9 nesymi ⊢ ¬ ∅ = ⟨ ( +g ‘ ndx ) , + ⟩
11 fvex ⊢ ( .r ‘ ndx ) ∈ V
12 mulex ⊢ · ∈ 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 3ioran ⊢ ( ¬ ( ∅ = ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ ∨ ∅ = ⟨ ( le ‘ ndx ) , ≤ ⟩ ∨ ∅ = ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ ) ↔ ( ¬ ∅ = ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ ∧ ¬ ∅ = ⟨ ( le ‘ ndx ) , ≤ ⟩ ∧ ¬ ∅ = ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ ) )
50 32 37 48 49 mpbir3an ⊢ ¬ ( ∅ = ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ ∨ ∅ = ⟨ ( le ‘ ndx ) , ≤ ⟩ ∨ ∅ = ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ )
51 16 eltp ⊢ ( ∅ ∈ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ↔ ( ∅ = ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ ∨ ∅ = ⟨ ( le ‘ ndx ) , ≤ ⟩ ∨ ∅ = ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ ) )
52 50 51 mtbir ⊢ ¬ ∅ ∈ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ }
53 fvex ⊢ ( UnifSet ‘ ndx ) ∈ V
54 fvex ⊢ ( metUnif ‘ ( abs ∘ − ) ) ∈ V
55 53 54 opnzi ⊢ ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ ≠ ∅
56 55 necomi ⊢ ∅ ≠ ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩
57 nelsn ⊢ ( ∅ ≠ ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ → ¬ ∅ ∈ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } )
58 56 57 ax-mp ⊢ ¬ ∅ ∈ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ }
59 52 58 pm3.2i ⊢ ( ¬ ∅ ∈ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∧ ¬ ∅ ∈ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } )
60 28 59 pm3.2i ⊢ ( ( ¬ ∅ ∈ { ⟨ ( 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 ) , ∗ ⟩ } ) ∨ ( ∅ ∈ { ⟨ ( 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 ⊢ ( ¬ ( ∅ ∈ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∨ ∅ ∈ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ↔ ( ¬ ∅ ∈ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∧ ¬ ∅ ∈ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) )
63 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 ∘ − ) ) ⟩ } ) )
64 62 63 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 ∘ − ) ) ⟩ } ) ) )
65 61 64 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 ∘ − ) ) ⟩ } ) ) )
66 60 65 mpbir ⊢ ¬ ( ( ∅ ∈ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∨ ∅ ∈ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∨ ( ∅ ∈ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∨ ∅ ∈ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) )
67 df-cnfld ⊢ ℂfld = ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) )
68 67 eleq2i ⊢ ( ∅ ∈ ℂfld ↔ ∅ ∈ ( ( { ⟨ ( 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 ) , ∗ ⟩ } ) ∪ ( { ⟨ ( 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 ⊢ ( ∅ ∈ ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ↔ ( ∅ ∈ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∨ ∅ ∈ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) )
71 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 ∘ − ) ) ⟩ } ) )
72 70 71 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 ∘ − ) ) ⟩ } ) ) )
73 68 69 72 3bitri ⊢ ( ∅ ∈ ℂ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 ⊢ ¬ ∅ ∈ ℂfld
75 disjsn ⊢ ( ( ℂfld ∩ { ∅ } ) = ∅ ↔ ¬ ∅ ∈ ℂfld )
76 74 75 mpbir ⊢ ( ℂfld ∩ { ∅ } ) = ∅
77 disjdif2 ⊢ ( ( ℂfld ∩ { ∅ } ) = ∅ → ( ℂfld ∖ { ∅ } ) = ℂfld )
78 76 77 ax-mp ⊢ ( ℂfld ∖ { ∅ } ) = ℂfld
79 78 funeqi ⊢ ( Fun ( ℂfld ∖ { ∅ } ) ↔ Fun ℂfld )
80 2 79 sylib ⊢ ( ℂfld Struct ⟨ 1 , 1 3 ⟩ → Fun ℂfld )
81 1 80 ax-mp ⊢ Fun ℂfld