This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnfldfunALT

Description: The field of complex numbers is a function. Alternate proof of cnfldfun not requiring that the index set of the components is ordered, but using quadratically many inequalities for the indices. (Contributed by AV, 14-Nov-2021) (Proof shortened by AV, 11-Nov-2024) Revise df-cnfld . (Revised by GG, 31-Mar-2025) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cnfldfunALT 
|- 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 mpoaddex 
 |-  ( u e. CC , v e. CC |-> ( u + v ) ) e. _V
9 mpomulex 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) 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 ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } )
11 1 2 3 10 mp3an 
 |-  Fun { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. }
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 ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } /\ Fun { <. ( *r ` ndx ) , * >. } )
18 7 8 9 dmtpop 
 |-  dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } = { ( Base ` ndx ) , ( +g ` ndx ) , ( .r ` ndx ) }
19 15 dmsnop 
 |-  dom { <. ( *r ` ndx ) , * >. } = { ( *r ` ndx ) }
20 18 19 ineq12i 
 |-  ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } i^i dom { <. ( *r ` ndx ) , * >. } ) = ( { ( Base ` ndx ) , ( +g ` ndx ) , ( .r ` ndx ) } i^i { ( *r ` ndx ) } )
21 starvndxnbasendx 
 |-  ( *r ` ndx ) =/= ( Base ` ndx )
22 21 necomi 
 |-  ( Base ` ndx ) =/= ( *r ` ndx )
23 starvndxnplusgndx 
 |-  ( *r ` ndx ) =/= ( +g ` ndx )
24 23 necomi 
 |-  ( +g ` ndx ) =/= ( *r ` ndx )
25 starvndxnmulrndx 
 |-  ( *r ` ndx ) =/= ( .r ` ndx )
26 25 necomi 
 |-  ( .r ` ndx ) =/= ( *r ` ndx )
27 disjtpsn 
 |-  ( ( ( Base ` ndx ) =/= ( *r ` ndx ) /\ ( +g ` ndx ) =/= ( *r ` ndx ) /\ ( .r ` ndx ) =/= ( *r ` ndx ) ) -> ( { ( Base ` ndx ) , ( +g ` ndx ) , ( .r ` ndx ) } i^i { ( *r ` ndx ) } ) = (/) )
28 22 24 26 27 mp3an 
 |-  ( { ( Base ` ndx ) , ( +g ` ndx ) , ( .r ` ndx ) } i^i { ( *r ` ndx ) } ) = (/)
29 20 28 eqtri 
 |-  ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } i^i dom { <. ( *r ` ndx ) , * >. } ) = (/)
30 funun 
 |-  ( ( ( Fun { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } /\ Fun { <. ( *r ` ndx ) , * >. } ) /\ ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } i^i dom { <. ( *r ` ndx ) , * >. } ) = (/) ) -> Fun ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } u. { <. ( *r ` ndx ) , * >. } ) )
31 17 29 30 mp2an 
 |-  Fun ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } u. { <. ( *r ` ndx ) , * >. } )
32 slotsdifplendx 
 |-  ( ( *r ` ndx ) =/= ( le ` ndx ) /\ ( TopSet ` ndx ) =/= ( le ` ndx ) )
33 32 simpri 
 |-  ( TopSet ` ndx ) =/= ( le ` ndx )
34 dsndxntsetndx 
 |-  ( dist ` ndx ) =/= ( TopSet ` ndx )
35 34 necomi 
 |-  ( TopSet ` ndx ) =/= ( dist ` ndx )
36 slotsdifdsndx 
 |-  ( ( *r ` ndx ) =/= ( dist ` ndx ) /\ ( le ` ndx ) =/= ( dist ` ndx ) )
37 36 simpri 
 |-  ( le ` ndx ) =/= ( dist ` ndx )
38 fvex 
 |-  ( TopSet ` ndx ) e. _V
39 fvex 
 |-  ( le ` ndx ) e. _V
40 fvex 
 |-  ( dist ` ndx ) e. _V
41 fvex 
 |-  ( MetOpen ` ( abs o. - ) ) e. _V
42 letsr 
 |-  <_ e. TosetRel
43 42 elexi 
 |-  <_ e. _V
44 absf 
 |-  abs : CC --> RR
45 fex 
 |-  ( ( abs : CC --> RR /\ CC e. _V ) -> abs e. _V )
46 44 7 45 mp2an 
 |-  abs e. _V
47 subf 
 |-  - : ( CC X. CC ) --> CC
48 7 7 xpex 
 |-  ( CC X. CC ) e. _V
49 fex 
 |-  ( ( - : ( CC X. CC ) --> CC /\ ( CC X. CC ) e. _V ) -> - e. _V )
50 47 48 49 mp2an 
 |-  - e. _V
51 46 50 coex 
 |-  ( abs o. - ) e. _V
52 38 39 40 41 43 51 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. - ) >. } )
53 33 35 37 52 mp3an 
 |-  Fun { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. }
54 fvex 
 |-  ( UnifSet ` ndx ) e. _V
55 fvex 
 |-  ( metUnif ` ( abs o. - ) ) e. _V
56 54 55 funsn 
 |-  Fun { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. }
57 53 56 pm3.2i 
 |-  ( Fun { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } /\ Fun { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } )
58 41 43 51 dmtpop 
 |-  dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } = { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) }
59 55 dmsnop 
 |-  dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } = { ( UnifSet ` ndx ) }
60 58 59 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 ) } )
61 slotsdifunifndx 
 |-  ( ( ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) /\ ( *r ` ndx ) =/= ( UnifSet ` ndx ) ) /\ ( ( le ` ndx ) =/= ( UnifSet ` ndx ) /\ ( dist ` ndx ) =/= ( UnifSet ` ndx ) ) )
62 unifndxntsetndx 
 |-  ( UnifSet ` ndx ) =/= ( TopSet ` ndx )
63 62 necomi 
 |-  ( TopSet ` ndx ) =/= ( UnifSet ` ndx )
64 63 a1i 
 |-  ( ( ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) /\ ( *r ` ndx ) =/= ( UnifSet ` ndx ) ) -> ( TopSet ` ndx ) =/= ( UnifSet ` ndx ) )
65 64 anim1i 
 |-  ( ( ( ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) /\ ( *r ` ndx ) =/= ( UnifSet ` ndx ) ) /\ ( ( le ` ndx ) =/= ( UnifSet ` ndx ) /\ ( dist ` ndx ) =/= ( UnifSet ` ndx ) ) ) -> ( ( TopSet ` ndx ) =/= ( UnifSet ` ndx ) /\ ( ( le ` ndx ) =/= ( UnifSet ` ndx ) /\ ( dist ` ndx ) =/= ( UnifSet ` ndx ) ) ) )
66 3anass 
 |-  ( ( ( TopSet ` ndx ) =/= ( UnifSet ` ndx ) /\ ( le ` ndx ) =/= ( UnifSet ` ndx ) /\ ( dist ` ndx ) =/= ( UnifSet ` ndx ) ) <-> ( ( TopSet ` ndx ) =/= ( UnifSet ` ndx ) /\ ( ( le ` ndx ) =/= ( UnifSet ` ndx ) /\ ( dist ` ndx ) =/= ( UnifSet ` ndx ) ) ) )
67 65 66 sylibr 
 |-  ( ( ( ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) /\ ( *r ` ndx ) =/= ( UnifSet ` ndx ) ) /\ ( ( le ` ndx ) =/= ( UnifSet ` ndx ) /\ ( dist ` ndx ) =/= ( UnifSet ` ndx ) ) ) -> ( ( TopSet ` ndx ) =/= ( UnifSet ` ndx ) /\ ( le ` ndx ) =/= ( UnifSet ` ndx ) /\ ( dist ` ndx ) =/= ( UnifSet ` ndx ) ) )
68 61 67 ax-mp 
 |-  ( ( TopSet ` ndx ) =/= ( UnifSet ` ndx ) /\ ( le ` ndx ) =/= ( UnifSet ` ndx ) /\ ( dist ` ndx ) =/= ( UnifSet ` ndx ) )
69 disjtpsn 
 |-  ( ( ( TopSet ` ndx ) =/= ( UnifSet ` ndx ) /\ ( le ` ndx ) =/= ( UnifSet ` ndx ) /\ ( dist ` ndx ) =/= ( UnifSet ` ndx ) ) -> ( { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } i^i { ( UnifSet ` ndx ) } ) = (/) )
70 68 69 ax-mp 
 |-  ( { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } i^i { ( UnifSet ` ndx ) } ) = (/)
71 60 70 eqtri 
 |-  ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) = (/)
72 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. - ) ) >. } ) )
73 57 71 72 mp2an 
 |-  Fun ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } )
74 31 73 pm3.2i 
 |-  ( Fun ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } u. { <. ( *r ` ndx ) , * >. } ) /\ Fun ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )
75 dmun 
 |-  dom ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } u. { <. ( *r ` ndx ) , * >. } ) = ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } u. dom { <. ( *r ` ndx ) , * >. } )
76 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. - ) ) >. } )
77 75 76 ineq12i 
 |-  ( dom ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } 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 ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } 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. - ) ) >. } ) )
78 18 58 ineq12i 
 |-  ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } 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 ) } )
79 tsetndxnbasendx 
 |-  ( TopSet ` ndx ) =/= ( Base ` ndx )
80 79 necomi 
 |-  ( Base ` ndx ) =/= ( TopSet ` ndx )
81 tsetndxnplusgndx 
 |-  ( TopSet ` ndx ) =/= ( +g ` ndx )
82 81 necomi 
 |-  ( +g ` ndx ) =/= ( TopSet ` ndx )
83 tsetndxnmulrndx 
 |-  ( TopSet ` ndx ) =/= ( .r ` ndx )
84 83 necomi 
 |-  ( .r ` ndx ) =/= ( TopSet ` ndx )
85 80 82 84 3pm3.2i 
 |-  ( ( Base ` ndx ) =/= ( TopSet ` ndx ) /\ ( +g ` ndx ) =/= ( TopSet ` ndx ) /\ ( .r ` ndx ) =/= ( TopSet ` ndx ) )
86 plendxnbasendx 
 |-  ( le ` ndx ) =/= ( Base ` ndx )
87 86 necomi 
 |-  ( Base ` ndx ) =/= ( le ` ndx )
88 plendxnplusgndx 
 |-  ( le ` ndx ) =/= ( +g ` ndx )
89 88 necomi 
 |-  ( +g ` ndx ) =/= ( le ` ndx )
90 plendxnmulrndx 
 |-  ( le ` ndx ) =/= ( .r ` ndx )
91 90 necomi 
 |-  ( .r ` ndx ) =/= ( le ` ndx )
92 87 89 91 3pm3.2i 
 |-  ( ( Base ` ndx ) =/= ( le ` ndx ) /\ ( +g ` ndx ) =/= ( le ` ndx ) /\ ( .r ` ndx ) =/= ( le ` ndx ) )
93 dsndxnbasendx 
 |-  ( dist ` ndx ) =/= ( Base ` ndx )
94 93 necomi 
 |-  ( Base ` ndx ) =/= ( dist ` ndx )
95 dsndxnplusgndx 
 |-  ( dist ` ndx ) =/= ( +g ` ndx )
96 95 necomi 
 |-  ( +g ` ndx ) =/= ( dist ` ndx )
97 dsndxnmulrndx 
 |-  ( dist ` ndx ) =/= ( .r ` ndx )
98 97 necomi 
 |-  ( .r ` ndx ) =/= ( dist ` ndx )
99 94 96 98 3pm3.2i 
 |-  ( ( Base ` ndx ) =/= ( dist ` ndx ) /\ ( +g ` ndx ) =/= ( dist ` ndx ) /\ ( .r ` ndx ) =/= ( dist ` ndx ) )
100 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 ) } ) = (/) )
101 85 92 99 100 mp3an 
 |-  ( { ( Base ` ndx ) , ( +g ` ndx ) , ( .r ` ndx ) } i^i { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } ) = (/)
102 78 101 eqtri 
 |-  ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } i^i dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } ) = (/)
103 18 59 ineq12i 
 |-  ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) = ( { ( Base ` ndx ) , ( +g ` ndx ) , ( .r ` ndx ) } i^i { ( UnifSet ` ndx ) } )
104 unifndxnbasendx 
 |-  ( UnifSet ` ndx ) =/= ( Base ` ndx )
105 104 necomi 
 |-  ( Base ` ndx ) =/= ( UnifSet ` ndx )
106 105 a1i 
 |-  ( ( ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) /\ ( *r ` ndx ) =/= ( UnifSet ` ndx ) ) -> ( Base ` ndx ) =/= ( UnifSet ` ndx ) )
107 3simpa 
 |-  ( ( ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) /\ ( *r ` ndx ) =/= ( UnifSet ` ndx ) ) -> ( ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) ) )
108 3anass 
 |-  ( ( ( Base ` ndx ) =/= ( UnifSet ` ndx ) /\ ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) ) <-> ( ( Base ` ndx ) =/= ( UnifSet ` ndx ) /\ ( ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) ) ) )
109 106 107 108 sylanbrc 
 |-  ( ( ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) /\ ( *r ` ndx ) =/= ( UnifSet ` ndx ) ) -> ( ( Base ` ndx ) =/= ( UnifSet ` ndx ) /\ ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) ) )
110 109 adantr 
 |-  ( ( ( ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) /\ ( *r ` ndx ) =/= ( UnifSet ` ndx ) ) /\ ( ( le ` ndx ) =/= ( UnifSet ` ndx ) /\ ( dist ` ndx ) =/= ( UnifSet ` ndx ) ) ) -> ( ( Base ` ndx ) =/= ( UnifSet ` ndx ) /\ ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) ) )
111 61 110 ax-mp 
 |-  ( ( Base ` ndx ) =/= ( UnifSet ` ndx ) /\ ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) )
112 disjtpsn 
 |-  ( ( ( Base ` ndx ) =/= ( UnifSet ` ndx ) /\ ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) ) -> ( { ( Base ` ndx ) , ( +g ` ndx ) , ( .r ` ndx ) } i^i { ( UnifSet ` ndx ) } ) = (/) )
113 111 112 ax-mp 
 |-  ( { ( Base ` ndx ) , ( +g ` ndx ) , ( .r ` ndx ) } i^i { ( UnifSet ` ndx ) } ) = (/)
114 103 113 eqtri 
 |-  ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) = (/)
115 102 114 pm3.2i 
 |-  ( ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } i^i dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } ) = (/) /\ ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) = (/) )
116 undisj2 
 |-  ( ( ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } i^i dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } ) = (/) /\ ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) = (/) ) <-> ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } i^i ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) = (/) )
117 115 116 mpbi 
 |-  ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } i^i ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) = (/)
118 19 58 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 ) } )
119 tsetndxnstarvndx 
 |-  ( TopSet ` ndx ) =/= ( *r ` ndx )
120 necom 
 |-  ( ( *r ` ndx ) =/= ( le ` ndx ) <-> ( le ` ndx ) =/= ( *r ` ndx ) )
121 120 biimpi 
 |-  ( ( *r ` ndx ) =/= ( le ` ndx ) -> ( le ` ndx ) =/= ( *r ` ndx ) )
122 121 adantr 
 |-  ( ( ( *r ` ndx ) =/= ( le ` ndx ) /\ ( TopSet ` ndx ) =/= ( le ` ndx ) ) -> ( le ` ndx ) =/= ( *r ` ndx ) )
123 32 122 ax-mp 
 |-  ( le ` ndx ) =/= ( *r ` ndx )
124 necom 
 |-  ( ( *r ` ndx ) =/= ( dist ` ndx ) <-> ( dist ` ndx ) =/= ( *r ` ndx ) )
125 124 biimpi 
 |-  ( ( *r ` ndx ) =/= ( dist ` ndx ) -> ( dist ` ndx ) =/= ( *r ` ndx ) )
126 125 adantr 
 |-  ( ( ( *r ` ndx ) =/= ( dist ` ndx ) /\ ( le ` ndx ) =/= ( dist ` ndx ) ) -> ( dist ` ndx ) =/= ( *r ` ndx ) )
127 36 126 ax-mp 
 |-  ( dist ` ndx ) =/= ( *r ` ndx )
128 disjtpsn 
 |-  ( ( ( TopSet ` ndx ) =/= ( *r ` ndx ) /\ ( le ` ndx ) =/= ( *r ` ndx ) /\ ( dist ` ndx ) =/= ( *r ` ndx ) ) -> ( { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } i^i { ( *r ` ndx ) } ) = (/) )
129 119 123 127 128 mp3an 
 |-  ( { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } i^i { ( *r ` ndx ) } ) = (/)
130 129 ineqcomi 
 |-  ( { ( *r ` ndx ) } i^i { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } ) = (/)
131 118 130 eqtri 
 |-  ( dom { <. ( *r ` ndx ) , * >. } i^i dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } ) = (/)
132 19 59 ineq12i 
 |-  ( dom { <. ( *r ` ndx ) , * >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) = ( { ( *r ` ndx ) } i^i { ( UnifSet ` ndx ) } )
133 simpl3 
 |-  ( ( ( ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) /\ ( *r ` ndx ) =/= ( UnifSet ` ndx ) ) /\ ( ( le ` ndx ) =/= ( UnifSet ` ndx ) /\ ( dist ` ndx ) =/= ( UnifSet ` ndx ) ) ) -> ( *r ` ndx ) =/= ( UnifSet ` ndx ) )
134 61 133 ax-mp 
 |-  ( *r ` ndx ) =/= ( UnifSet ` ndx )
135 disjsn2 
 |-  ( ( *r ` ndx ) =/= ( UnifSet ` ndx ) -> ( { ( *r ` ndx ) } i^i { ( UnifSet ` ndx ) } ) = (/) )
136 134 135 ax-mp 
 |-  ( { ( *r ` ndx ) } i^i { ( UnifSet ` ndx ) } ) = (/)
137 132 136 eqtri 
 |-  ( dom { <. ( *r ` ndx ) , * >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) = (/)
138 131 137 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. - ) ) >. } ) = (/) )
139 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. - ) ) >. } ) ) = (/) )
140 138 139 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. - ) ) >. } ) ) = (/)
141 117 140 pm3.2i 
 |-  ( ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } 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. - ) ) >. } ) ) = (/) )
142 undisj1 
 |-  ( ( ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } 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 ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } 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. - ) ) >. } ) ) = (/) )
143 141 142 mpbi 
 |-  ( ( dom { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } 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. - ) ) >. } ) ) = (/)
144 77 143 eqtri 
 |-  ( dom ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } u. { <. ( *r ` ndx ) , * >. } ) i^i dom ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) = (/)
145 funun 
 |-  ( ( ( Fun ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } 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 ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } 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 ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) )
146 74 144 145 mp2an 
 |-  Fun ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )
147 df-cnfld 
 |-  CCfld = ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )
148 147 funeqi 
 |-  ( Fun CCfld <-> Fun ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) )
149 146 148 mpbir 
 |-  Fun CCfld