Metamath Proof Explorer

Theorem cnfldfun

Description: The field of complex numbers is a function. (Contributed by AV, 14-Nov-2021)

Ref Expression
Assertion cnfldfun 
|- Fun CCfld

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 ) e. _V
5 fvex 
 |-  ( +g ` ndx ) e. _V
6 fvex 
 |-  ( .r ` ndx ) e. _V
7 cnex 
 |-  CC e. _V
8 addex 
 |-  + e. _V
9 mulex 
 |-  x. e. _V
10 4 5 6 7 8 9 funtp 
 |-  ( ( ( Base ` ndx ) =/= ( +g ` ndx ) /\ ( Base ` ndx ) =/= ( .r ` ndx ) /\ ( +g ` ndx ) =/= ( .r ` ndx ) ) -> Fun { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } )
11 1 2 3 10 mp3an 
 |-  Fun { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. }
12 fvex 
 |-  ( *r ` ndx ) e. _V
13 cjf 
 |-  * : CC --> CC
14 fex 
 |-  ( ( * : CC --> CC /\ CC e. _V ) -> * e. _V )
15 13 7 14 mp2an 
 |-  * e. _V
16 12 15 funsn 
 |-  Fun { <. ( *r ` ndx ) , * >. }
17 11 16 pm3.2i 
 |-  ( Fun { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } /\ Fun { <. ( *r ` ndx ) , * >. } )
18 7 8 9 dmtpop 
 |-  dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } = { ( Base ` ndx ) , ( +g ` ndx ) , ( .r ` ndx ) }
19 15 dmsnop 
 |-  dom { <. ( *r ` ndx ) , * >. } = { ( *r ` ndx ) }
20 18 19 ineq12i 
 |-  ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } i^i dom { <. ( *r ` ndx ) , * >. } ) = ( { ( Base ` ndx ) , ( +g ` ndx ) , ( .r ` ndx ) } i^i { ( *r ` ndx ) } )
21 basendx 
 |-  ( Base ` ndx ) = 1
22 1re 
 |-  1 e. RR
23 1lt4 
 |-  1 < 4
24 22 23 ltneii 
 |-  1 =/= 4
25 starvndx 
 |-  ( *r ` ndx ) = 4
26 24 25 neeqtrri 
 |-  1 =/= ( *r ` ndx )
27 21 26 eqnetri 
 |-  ( Base ` ndx ) =/= ( *r ` ndx )
28 plusgndx 
 |-  ( +g ` ndx ) = 2
29 2re 
 |-  2 e. RR
30 2lt4 
 |-  2 < 4
31 29 30 ltneii 
 |-  2 =/= 4
32 31 25 neeqtrri 
 |-  2 =/= ( *r ` ndx )
33 28 32 eqnetri 
 |-  ( +g ` ndx ) =/= ( *r ` ndx )
34 mulrndx 
 |-  ( .r ` ndx ) = 3
35 3re 
 |-  3 e. RR
36 3lt4 
 |-  3 < 4
37 35 36 ltneii 
 |-  3 =/= 4
38 37 25 neeqtrri 
 |-  3 =/= ( *r ` ndx )
39 34 38 eqnetri 
 |-  ( .r ` ndx ) =/= ( *r ` ndx )
40 disjtpsn 
 |-  ( ( ( Base ` ndx ) =/= ( *r ` ndx ) /\ ( +g ` ndx ) =/= ( *r ` ndx ) /\ ( .r ` ndx ) =/= ( *r ` ndx ) ) -> ( { ( Base ` ndx ) , ( +g ` ndx ) , ( .r ` ndx ) } i^i { ( *r ` ndx ) } ) = (/) )
41 27 33 39 40 mp3an 
 |-  ( { ( Base ` ndx ) , ( +g ` ndx ) , ( .r ` ndx ) } i^i { ( *r ` ndx ) } ) = (/)
42 20 41 eqtri 
 |-  ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } i^i dom { <. ( *r ` ndx ) , * >. } ) = (/)
43 funun 
 |-  ( ( ( Fun { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } /\ Fun { <. ( *r ` ndx ) , * >. } ) /\ ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } i^i dom { <. ( *r ` ndx ) , * >. } ) = (/) ) -> Fun ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) )
44 17 42 43 mp2an 
 |-  Fun ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } )
45 tsetndx 
 |-  ( TopSet ` ndx ) = 9
46 9re 
 |-  9 e. RR
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 e. NN
53 2nn0 
 |-  2 e. NN0
54 9nn0 
 |-  9 e. NN0
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 e. RR
62 1nn0 
 |-  1 e. NN0
63 0nn0 
 |-  0 e. NN0
64 2nn 
 |-  2 e. NN
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 ) e. _V
71 fvex 
 |-  ( le ` ndx ) e. _V
72 fvex 
 |-  ( dist ` ndx ) e. _V
73 fvex 
 |-  ( MetOpen ` ( abs o. - ) ) e. _V
74 letsr 
 |-  <_ e. TosetRel
75 74 elexi 
 |-  <_ e. _V
76 absf 
 |-  abs : CC --> RR
77 fex 
 |-  ( ( abs : CC --> RR /\ CC e. _V ) -> abs e. _V )
78 76 7 77 mp2an 
 |-  abs e. _V
79 subf 
 |-  - : ( CC X. CC ) --> CC
80 7 7 xpex 
 |-  ( CC X. CC ) e. _V
81 fex 
 |-  ( ( - : ( CC X. CC ) --> CC /\ ( CC X. CC ) e. _V ) -> - e. _V )
82 79 80 81 mp2an 
 |-  - e. _V
83 78 82 coex 
 |-  ( abs o. - ) e. _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 o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } )
85 51 60 69 84 mp3an 
 |-  Fun { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. }
86 fvex 
 |-  ( UnifSet ` ndx ) e. _V
87 fvex 
 |-  ( metUnif ` ( abs o. - ) ) e. _V
88 86 87 funsn 
 |-  Fun { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. }
89 85 88 pm3.2i 
 |-  ( Fun { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } /\ Fun { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } )
90 73 75 83 dmtpop 
 |-  dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } = { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) }
91 87 dmsnop 
 |-  dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } = { ( UnifSet ` ndx ) }
92 90 91 ineq12i 
 |-  ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) = ( { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } i^i { ( UnifSet ` ndx ) } )
93 3nn0 
 |-  3 e. NN0
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 e. NN
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 e. NN0
106 105 nn0rei 
 |-  ; 1 2 e. RR
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 ) } i^i { ( UnifSet ` ndx ) } ) = (/) )
113 98 104 111 112 mp3an 
 |-  ( { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } i^i { ( UnifSet ` ndx ) } ) = (/)
114 92 113 eqtri 
 |-  ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) = (/)
115 funun 
 |-  ( ( ( Fun { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } /\ Fun { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) /\ ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) = (/) ) -> Fun ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )
116 89 114 115 mp2an 
 |-  Fun ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } )
117 44 116 pm3.2i 
 |-  ( Fun ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) /\ Fun ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )
118 dmun 
 |-  dom ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) = ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. dom { <. ( *r ` ndx ) , * >. } )
119 dmun 
 |-  dom ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) = ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } )
120 118 119 ineq12i 
 |-  ( dom ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) i^i dom ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) = ( ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. dom { <. ( *r ` ndx ) , * >. } ) i^i ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )
121 18 90 ineq12i 
 |-  ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } i^i dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } ) = ( { ( Base ` ndx ) , ( +g ` ndx ) , ( .r ` ndx ) } i^i { ( 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 ) } i^i { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } ) = (/) )
165 134 147 163 164 mp3an 
 |-  ( { ( Base ` ndx ) , ( +g ` ndx ) , ( .r ` ndx ) } i^i { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } ) = (/)
166 121 165 eqtri 
 |-  ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } i^i dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } ) = (/)
167 18 91 ineq12i 
 |-  ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) = ( { ( Base ` ndx ) , ( +g ` ndx ) , ( .r ` ndx ) } i^i { ( 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 ) } i^i { ( UnifSet ` ndx ) } ) = (/) )
181 171 175 179 180 mp3an 
 |-  ( { ( Base ` ndx ) , ( +g ` ndx ) , ( .r ` ndx ) } i^i { ( UnifSet ` ndx ) } ) = (/)
182 167 181 eqtri 
 |-  ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) = (/)
183 166 182 pm3.2i 
 |-  ( ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } i^i dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } ) = (/) /\ ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) = (/) )
184 undisj2 
 |-  ( ( ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } i^i dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } ) = (/) /\ ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) = (/) ) <-> ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } i^i ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) = (/) )
185 183 184 mpbi 
 |-  ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } i^i ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) = (/)
186 19 90 ineq12i 
 |-  ( dom { <. ( *r ` ndx ) , * >. } i^i dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } ) = ( { ( *r ` ndx ) } i^i { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } )
187 incom 
 |-  ( { ( *r ` ndx ) } i^i { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } ) = ( { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } i^i { ( *r ` ndx ) } )
188 4re 
 |-  4 e. RR
189 4lt9 
 |-  4 < 9
190 188 189 gtneii 
 |-  9 =/= 4
191 190 25 neeqtrri 
 |-  9 =/= ( *r ` ndx )
192 45 191 eqnetri 
 |-  ( TopSet ` ndx ) =/= ( *r ` ndx )
193 4lt10 
 |-  4 < ; 1 0
194 188 193 gtneii 
 |-  ; 1 0 =/= 4
195 194 25 neeqtrri 
 |-  ; 1 0 =/= ( *r ` ndx )
196 49 195 eqnetri 
 |-  ( le ` ndx ) =/= ( *r ` ndx )
197 4nn0 
 |-  4 e. NN0
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 =/= ( *r ` ndx )
202 58 201 eqnetri 
 |-  ( dist ` ndx ) =/= ( *r ` ndx )
203 disjtpsn 
 |-  ( ( ( TopSet ` ndx ) =/= ( *r ` ndx ) /\ ( le ` ndx ) =/= ( *r ` ndx ) /\ ( dist ` ndx ) =/= ( *r ` ndx ) ) -> ( { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } i^i { ( *r ` ndx ) } ) = (/) )
204 192 196 202 203 mp3an 
 |-  ( { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } i^i { ( *r ` ndx ) } ) = (/)
205 187 204 eqtri 
 |-  ( { ( *r ` ndx ) } i^i { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } ) = (/)
206 186 205 eqtri 
 |-  ( dom { <. ( *r ` ndx ) , * >. } i^i dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } ) = (/)
207 19 91 ineq12i 
 |-  ( dom { <. ( *r ` ndx ) , * >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) = ( { ( *r ` ndx ) } i^i { ( 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 
 |-  ( *r ` ndx ) =/= ( UnifSet ` ndx )
212 disjsn2 
 |-  ( ( *r ` ndx ) =/= ( UnifSet ` ndx ) -> ( { ( *r ` ndx ) } i^i { ( UnifSet ` ndx ) } ) = (/) )
213 211 212 ax-mp 
 |-  ( { ( *r ` ndx ) } i^i { ( UnifSet ` ndx ) } ) = (/)
214 207 213 eqtri 
 |-  ( dom { <. ( *r ` ndx ) , * >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) = (/)
215 206 214 pm3.2i 
 |-  ( ( dom { <. ( *r ` ndx ) , * >. } i^i dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } ) = (/) /\ ( dom { <. ( *r ` ndx ) , * >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) = (/) )
216 undisj2 
 |-  ( ( ( dom { <. ( *r ` ndx ) , * >. } i^i dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } ) = (/) /\ ( dom { <. ( *r ` ndx ) , * >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) = (/) ) <-> ( dom { <. ( *r ` ndx ) , * >. } i^i ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) = (/) )
217 215 216 mpbi 
 |-  ( dom { <. ( *r ` ndx ) , * >. } i^i ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) = (/)
218 185 217 pm3.2i 
 |-  ( ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } i^i ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) = (/) /\ ( dom { <. ( *r ` ndx ) , * >. } i^i ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) = (/) )
219 undisj1 
 |-  ( ( ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } i^i ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) = (/) /\ ( dom { <. ( *r ` ndx ) , * >. } i^i ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) = (/) ) <-> ( ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. dom { <. ( *r ` ndx ) , * >. } ) i^i ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) = (/) )
220 218 219 mpbi 
 |-  ( ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. dom { <. ( *r ` ndx ) , * >. } ) i^i ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) = (/)
221 120 220 eqtri 
 |-  ( dom ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) i^i dom ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) = (/)
222 funun 
 |-  ( ( ( Fun ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) /\ Fun ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) /\ ( dom ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) i^i dom ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) = (/) ) -> Fun ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) )
223 117 221 222 mp2an 
 |-  Fun ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )
224 df-cnfld 
 |-  CCfld = ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )
225 224 funeqi 
 |-  ( Fun CCfld <-> Fun ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) )
226 223 225 mpbir 
 |-  Fun CCfld