Metamath Proof Explorer

Theorem cnfldfunOLD

Description: Obsolete proof of cnfldfun as of 10-Nov-2024. The field of complex numbers is a function. (Contributed by AV, 14-Nov-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cnfldfunOLD Fun ℂfld

Proof

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 basendx ⊢ ( Base ‘ ndx ) = 1
22 1re ⊢ 1 ∈ ℝ
23 1lt4 ⊢ 1 < 4
24 22 23 ltneii ⊢ 1 ≠ 4
25 starvndx ⊢ ( *𝑟 ‘ ndx ) = 4
26 24 25 neeqtrri ⊢ 1 ≠ ( *𝑟 ‘ ndx )
27 21 26 eqnetri ⊢ ( Base ‘ ndx ) ≠ ( *𝑟 ‘ ndx )
28 plusgndx ⊢ ( +g ‘ ndx ) = 2
29 2re ⊢ 2 ∈ ℝ
30 2lt4 ⊢ 2 < 4
31 29 30 ltneii ⊢ 2 ≠ 4
32 31 25 neeqtrri ⊢ 2 ≠ ( *𝑟 ‘ ndx )
33 28 32 eqnetri ⊢ ( +g ‘ ndx ) ≠ ( *𝑟 ‘ ndx )
34 mulrndx ⊢ ( .r ‘ ndx ) = 3
35 3re ⊢ 3 ∈ ℝ
36 3lt4 ⊢ 3 < 4
37 35 36 ltneii ⊢ 3 ≠ 4
38 37 25 neeqtrri ⊢ 3 ≠ ( *𝑟 ‘ ndx )
39 34 38 eqnetri ⊢ ( .r ‘ ndx ) ≠ ( *𝑟 ‘ ndx )
40 disjtpsn ⊢ ( ( ( Base ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ∧ ( +g ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ) → ( { ( Base ‘ ndx ) , ( +g ‘ ndx ) , ( .r ‘ ndx ) } ∩ { ( *𝑟 ‘ ndx ) } ) = ∅ )
41 27 33 39 40 mp3an ⊢ ( { ( Base ‘ ndx ) , ( +g ‘ ndx ) , ( .r ‘ ndx ) } ∩ { ( *𝑟 ‘ ndx ) } ) = ∅
42 20 41 eqtri ⊢ ( dom { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∩ dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) = ∅
43 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 ) , ∗ ⟩ } ) )
44 17 42 43 mp2an ⊢ Fun ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } )
45 tsetndx ⊢ ( TopSet ‘ ndx ) = 9
46 9re ⊢ 9 ∈ ℝ
47 9lt10 ⊢ 9 < 1 0
48 46 47 ltneii ⊢ 9 ≠ 1 0
49 plendx ⊢ ( le ‘ ndx ) = 1 0
50 48 49 neeqtrri ⊢ 9 ≠ ( le ‘ ndx )
51 45 50 eqnetri ⊢ ( TopSet ‘ ndx ) ≠ ( le ‘ ndx )
52 1nn ⊢ 1 ∈ ℕ
53 2nn0 ⊢ 2 ∈ ℕ0
54 9nn0 ⊢ 9 ∈ ℕ0
55 46 leidi ⊢ 9 ≤ 9
56 52 53 54 55 decltdi ⊢ 9 < 1 2
57 46 56 ltneii ⊢ 9 ≠ 1 2
58 dsndx ⊢ ( dist ‘ ndx ) = 1 2
59 57 58 neeqtrri ⊢ 9 ≠ ( dist ‘ ndx )
60 45 59 eqnetri ⊢ ( TopSet ‘ ndx ) ≠ ( dist ‘ ndx )
61 10re ⊢ 1 0 ∈ ℝ
62 1nn0 ⊢ 1 ∈ ℕ0
63 0nn0 ⊢ 0 ∈ ℕ0
64 2nn ⊢ 2 ∈ ℕ
65 2pos ⊢ 0 < 2
66 62 63 64 65 declt ⊢ 1 0 < 1 2
67 61 66 ltneii ⊢ 1 0 ≠ 1 2
68 67 58 neeqtrri ⊢ 1 0 ≠ ( dist ‘ ndx )
69 49 68 eqnetri ⊢ ( le ‘ ndx ) ≠ ( dist ‘ ndx )
70 fvex ⊢ ( TopSet ‘ ndx ) ∈ V
71 fvex ⊢ ( le ‘ ndx ) ∈ V
72 fvex ⊢ ( dist ‘ ndx ) ∈ V
73 fvex ⊢ ( MetOpen ‘ ( abs ∘ − ) ) ∈ V
74 letsr ⊢ ≤ ∈ TosetRel
75 74 elexi ⊢ ≤ ∈ V
76 absf ⊢ abs : ℂ ⟶ ℝ
77 fex ⊢ ( ( abs : ℂ ⟶ ℝ ∧ ℂ ∈ V ) → abs ∈ V )
78 76 7 77 mp2an ⊢ abs ∈ V
79 subf ⊢ − : ( ℂ × ℂ ) ⟶ ℂ
80 7 7 xpex ⊢ ( ℂ × ℂ ) ∈ V
81 fex ⊢ ( ( − : ( ℂ × ℂ ) ⟶ ℂ ∧ ( ℂ × ℂ ) ∈ V ) → − ∈ V )
82 79 80 81 mp2an ⊢ − ∈ V
83 78 82 coex ⊢ ( abs ∘ − ) ∈ V
84 70 71 72 73 75 83 funtp ⊢ ( ( ( TopSet ‘ ndx ) ≠ ( le ‘ ndx ) ∧ ( TopSet ‘ ndx ) ≠ ( dist ‘ ndx ) ∧ ( le ‘ ndx ) ≠ ( dist ‘ ndx ) ) → Fun { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } )
85 51 60 69 84 mp3an ⊢ Fun { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ }
86 fvex ⊢ ( UnifSet ‘ ndx ) ∈ V
87 fvex ⊢ ( metUnif ‘ ( abs ∘ − ) ) ∈ V
88 86 87 funsn ⊢ Fun { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ }
89 85 88 pm3.2i ⊢ ( Fun { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∧ Fun { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } )
90 73 75 83 dmtpop ⊢ dom { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } = { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) }
91 87 dmsnop ⊢ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } = { ( UnifSet ‘ ndx ) }
92 90 91 ineq12i ⊢ ( dom { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∩ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) = ( { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) } ∩ { ( UnifSet ‘ ndx ) } )
93 3nn0 ⊢ 3 ∈ ℕ0
94 52 93 54 55 decltdi ⊢ 9 < 1 3
95 46 94 ltneii ⊢ 9 ≠ 1 3
96 unifndx ⊢ ( UnifSet ‘ ndx ) = 1 3
97 95 96 neeqtrri ⊢ 9 ≠ ( UnifSet ‘ ndx )
98 45 97 eqnetri ⊢ ( TopSet ‘ ndx ) ≠ ( UnifSet ‘ ndx )
99 3nn ⊢ 3 ∈ ℕ
100 3pos ⊢ 0 < 3
101 62 63 99 100 declt ⊢ 1 0 < 1 3
102 61 101 ltneii ⊢ 1 0 ≠ 1 3
103 102 96 neeqtrri ⊢ 1 0 ≠ ( UnifSet ‘ ndx )
104 49 103 eqnetri ⊢ ( le ‘ ndx ) ≠ ( UnifSet ‘ ndx )
105 62 53 deccl ⊢ 1 2 ∈ ℕ0
106 105 nn0rei ⊢ 1 2 ∈ ℝ
107 2lt3 ⊢ 2 < 3
108 62 53 99 107 declt ⊢ 1 2 < 1 3
109 106 108 ltneii ⊢ 1 2 ≠ 1 3
110 109 96 neeqtrri ⊢ 1 2 ≠ ( UnifSet ‘ ndx )
111 58 110 eqnetri ⊢ ( dist ‘ ndx ) ≠ ( UnifSet ‘ ndx )
112 disjtpsn ⊢ ( ( ( TopSet ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( le ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( dist ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ) → ( { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) } ∩ { ( UnifSet ‘ ndx ) } ) = ∅ )
113 98 104 111 112 mp3an ⊢ ( { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) } ∩ { ( UnifSet ‘ ndx ) } ) = ∅
114 92 113 eqtri ⊢ ( dom { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∩ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) = ∅
115 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 ∘ − ) ) ⟩ } ) )
116 89 114 115 mp2an ⊢ Fun ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } )
117 44 116 pm3.2i ⊢ ( Fun ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∧ Fun ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) )
118 dmun ⊢ dom ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) = ( dom { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } )
119 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 ∘ − ) ) ⟩ } )
120 118 119 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 ∘ − ) ) ⟩ } ) )
121 18 90 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 ) } )
122 1lt9 ⊢ 1 < 9
123 22 122 ltneii ⊢ 1 ≠ 9
124 123 45 neeqtrri ⊢ 1 ≠ ( TopSet ‘ ndx )
125 21 124 eqnetri ⊢ ( Base ‘ ndx ) ≠ ( TopSet ‘ ndx )
126 2lt9 ⊢ 2 < 9
127 29 126 ltneii ⊢ 2 ≠ 9
128 127 45 neeqtrri ⊢ 2 ≠ ( TopSet ‘ ndx )
129 28 128 eqnetri ⊢ ( +g ‘ ndx ) ≠ ( TopSet ‘ ndx )
130 3lt9 ⊢ 3 < 9
131 35 130 ltneii ⊢ 3 ≠ 9
132 131 45 neeqtrri ⊢ 3 ≠ ( TopSet ‘ ndx )
133 34 132 eqnetri ⊢ ( .r ‘ ndx ) ≠ ( TopSet ‘ ndx )
134 125 129 133 3pm3.2i ⊢ ( ( Base ‘ ndx ) ≠ ( TopSet ‘ ndx ) ∧ ( +g ‘ ndx ) ≠ ( TopSet ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( TopSet ‘ ndx ) )
135 1lt10 ⊢ 1 < 1 0
136 22 135 ltneii ⊢ 1 ≠ 1 0
137 136 49 neeqtrri ⊢ 1 ≠ ( le ‘ ndx )
138 21 137 eqnetri ⊢ ( Base ‘ ndx ) ≠ ( le ‘ ndx )
139 2lt10 ⊢ 2 < 1 0
140 29 139 ltneii ⊢ 2 ≠ 1 0
141 140 49 neeqtrri ⊢ 2 ≠ ( le ‘ ndx )
142 28 141 eqnetri ⊢ ( +g ‘ ndx ) ≠ ( le ‘ ndx )
143 3lt10 ⊢ 3 < 1 0
144 35 143 ltneii ⊢ 3 ≠ 1 0
145 144 49 neeqtrri ⊢ 3 ≠ ( le ‘ ndx )
146 34 145 eqnetri ⊢ ( .r ‘ ndx ) ≠ ( le ‘ ndx )
147 138 142 146 3pm3.2i ⊢ ( ( Base ‘ ndx ) ≠ ( le ‘ ndx ) ∧ ( +g ‘ ndx ) ≠ ( le ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( le ‘ ndx ) )
148 22 46 122 ltleii ⊢ 1 ≤ 9
149 52 53 62 148 decltdi ⊢ 1 < 1 2
150 22 149 ltneii ⊢ 1 ≠ 1 2
151 150 58 neeqtrri ⊢ 1 ≠ ( dist ‘ ndx )
152 21 151 eqnetri ⊢ ( Base ‘ ndx ) ≠ ( dist ‘ ndx )
153 29 46 126 ltleii ⊢ 2 ≤ 9
154 52 53 53 153 decltdi ⊢ 2 < 1 2
155 29 154 ltneii ⊢ 2 ≠ 1 2
156 155 58 neeqtrri ⊢ 2 ≠ ( dist ‘ ndx )
157 28 156 eqnetri ⊢ ( +g ‘ ndx ) ≠ ( dist ‘ ndx )
158 35 46 130 ltleii ⊢ 3 ≤ 9
159 52 53 93 158 decltdi ⊢ 3 < 1 2
160 35 159 ltneii ⊢ 3 ≠ 1 2
161 160 58 neeqtrri ⊢ 3 ≠ ( dist ‘ ndx )
162 34 161 eqnetri ⊢ ( .r ‘ ndx ) ≠ ( dist ‘ ndx )
163 152 157 162 3pm3.2i ⊢ ( ( Base ‘ ndx ) ≠ ( dist ‘ ndx ) ∧ ( +g ‘ ndx ) ≠ ( dist ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( dist ‘ ndx ) )
164 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 ) } ) = ∅ )
165 134 147 163 164 mp3an ⊢ ( { ( Base ‘ ndx ) , ( +g ‘ ndx ) , ( .r ‘ ndx ) } ∩ { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) } ) = ∅
166 121 165 eqtri ⊢ ( dom { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∩ dom { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ) = ∅
167 18 91 ineq12i ⊢ ( dom { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∩ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) = ( { ( Base ‘ ndx ) , ( +g ‘ ndx ) , ( .r ‘ ndx ) } ∩ { ( UnifSet ‘ ndx ) } )
168 52 93 62 148 decltdi ⊢ 1 < 1 3
169 22 168 ltneii ⊢ 1 ≠ 1 3
170 169 96 neeqtrri ⊢ 1 ≠ ( UnifSet ‘ ndx )
171 21 170 eqnetri ⊢ ( Base ‘ ndx ) ≠ ( UnifSet ‘ ndx )
172 52 93 53 153 decltdi ⊢ 2 < 1 3
173 29 172 ltneii ⊢ 2 ≠ 1 3
174 173 96 neeqtrri ⊢ 2 ≠ ( UnifSet ‘ ndx )
175 28 174 eqnetri ⊢ ( +g ‘ ndx ) ≠ ( UnifSet ‘ ndx )
176 52 93 93 158 decltdi ⊢ 3 < 1 3
177 35 176 ltneii ⊢ 3 ≠ 1 3
178 177 96 neeqtrri ⊢ 3 ≠ ( UnifSet ‘ ndx )
179 34 178 eqnetri ⊢ ( .r ‘ ndx ) ≠ ( UnifSet ‘ ndx )
180 disjtpsn ⊢ ( ( ( Base ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( +g ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ) → ( { ( Base ‘ ndx ) , ( +g ‘ ndx ) , ( .r ‘ ndx ) } ∩ { ( UnifSet ‘ ndx ) } ) = ∅ )
181 171 175 179 180 mp3an ⊢ ( { ( Base ‘ ndx ) , ( +g ‘ ndx ) , ( .r ‘ ndx ) } ∩ { ( UnifSet ‘ ndx ) } ) = ∅
182 167 181 eqtri ⊢ ( dom { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∩ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) = ∅
183 166 182 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 ∘ − ) ) ⟩ } ) = ∅ )
184 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 ∘ − ) ) ⟩ } ) ) = ∅ )
185 183 184 mpbi ⊢ ( dom { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∩ ( dom { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) = ∅
186 19 90 ineq12i ⊢ ( dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ∩ dom { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ) = ( { ( *𝑟 ‘ ndx ) } ∩ { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) } )
187 incom ⊢ ( { ( *𝑟 ‘ ndx ) } ∩ { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) } ) = ( { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) } ∩ { ( *𝑟 ‘ ndx ) } )
188 4re ⊢ 4 ∈ ℝ
189 4lt9 ⊢ 4 < 9
190 188 189 gtneii ⊢ 9 ≠ 4
191 190 25 neeqtrri ⊢ 9 ≠ ( *𝑟 ‘ ndx )
192 45 191 eqnetri ⊢ ( TopSet ‘ ndx ) ≠ ( *𝑟 ‘ ndx )
193 4lt10 ⊢ 4 < 1 0
194 188 193 gtneii ⊢ 1 0 ≠ 4
195 194 25 neeqtrri ⊢ 1 0 ≠ ( *𝑟 ‘ ndx )
196 49 195 eqnetri ⊢ ( le ‘ ndx ) ≠ ( *𝑟 ‘ ndx )
197 4nn0 ⊢ 4 ∈ ℕ0
198 188 46 189 ltleii ⊢ 4 ≤ 9
199 52 53 197 198 decltdi ⊢ 4 < 1 2
200 188 199 gtneii ⊢ 1 2 ≠ 4
201 200 25 neeqtrri ⊢ 1 2 ≠ ( *𝑟 ‘ ndx )
202 58 201 eqnetri ⊢ ( dist ‘ ndx ) ≠ ( *𝑟 ‘ ndx )
203 disjtpsn ⊢ ( ( ( TopSet ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ∧ ( le ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ∧ ( dist ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ) → ( { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) } ∩ { ( *𝑟 ‘ ndx ) } ) = ∅ )
204 192 196 202 203 mp3an ⊢ ( { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) } ∩ { ( *𝑟 ‘ ndx ) } ) = ∅
205 187 204 eqtri ⊢ ( { ( *𝑟 ‘ ndx ) } ∩ { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) } ) = ∅
206 186 205 eqtri ⊢ ( dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ∩ dom { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ) = ∅
207 19 91 ineq12i ⊢ ( dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ∩ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) = ( { ( *𝑟 ‘ ndx ) } ∩ { ( UnifSet ‘ ndx ) } )
208 52 93 197 198 decltdi ⊢ 4 < 1 3
209 188 208 ltneii ⊢ 4 ≠ 1 3
210 209 96 neeqtrri ⊢ 4 ≠ ( UnifSet ‘ ndx )
211 25 210 eqnetri ⊢ ( *𝑟 ‘ ndx ) ≠ ( UnifSet ‘ ndx )
212 disjsn2 ⊢ ( ( *𝑟 ‘ ndx ) ≠ ( UnifSet ‘ ndx ) → ( { ( *𝑟 ‘ ndx ) } ∩ { ( UnifSet ‘ ndx ) } ) = ∅ )
213 211 212 ax-mp ⊢ ( { ( *𝑟 ‘ ndx ) } ∩ { ( UnifSet ‘ ndx ) } ) = ∅
214 207 213 eqtri ⊢ ( dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ∩ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) = ∅
215 206 214 pm3.2i ⊢ ( ( dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ∩ dom { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ) = ∅ ∧ ( dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ∩ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) = ∅ )
216 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 ∘ − ) ) ⟩ } ) ) = ∅ )
217 215 216 mpbi ⊢ ( dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ∩ ( dom { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) = ∅
218 185 217 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 ∘ − ) ) ⟩ } ) ) = ∅ )
219 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 ∘ − ) ) ⟩ } ) ) = ∅ )
220 218 219 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 ∘ − ) ) ⟩ } ) ) = ∅
221 120 220 eqtri ⊢ ( dom ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∩ dom ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) = ∅
222 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 ∘ − ) ) ⟩ } ) ) )
223 117 221 222 mp2an ⊢ Fun ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) )
224 df-cnfld ⊢ ℂfld = ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) )
225 224 funeqi ⊢ ( Fun ℂfld ↔ Fun ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) )
226 223 225 mpbir ⊢ Fun ℂfld