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 birani 
 |-  ( ( ( *r ` ndx ) =/= ( le ` ndx ) /\ ( TopSet ` ndx ) =/= ( le ` ndx ) ) -> ( le ` ndx ) =/= ( *r ` ndx ) )
122 32 121 ax-mp 
 |-  ( le ` ndx ) =/= ( *r ` ndx )
123 necom 
 |-  ( ( *r ` ndx ) =/= ( dist ` ndx ) <-> ( dist ` ndx ) =/= ( *r ` ndx ) )
124 123 birani 
 |-  ( ( ( *r ` ndx ) =/= ( dist ` ndx ) /\ ( le ` ndx ) =/= ( dist ` ndx ) ) -> ( dist ` ndx ) =/= ( *r ` ndx ) )
125 36 124 ax-mp 
 |-  ( dist ` ndx ) =/= ( *r ` ndx )
126 disjtpsn 
 |-  ( ( ( TopSet ` ndx ) =/= ( *r ` ndx ) /\ ( le ` ndx ) =/= ( *r ` ndx ) /\ ( dist ` ndx ) =/= ( *r ` ndx ) ) -> ( { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } i^i { ( *r ` ndx ) } ) = (/) )
127 119 122 125 126 mp3an 
 |-  ( { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } i^i { ( *r ` ndx ) } ) = (/)
128 127 ineqcomi 
 |-  ( { ( *r ` ndx ) } i^i { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } ) = (/)
129 118 128 eqtri 
 |-  ( dom { <. ( *r ` ndx ) , * >. } i^i dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } ) = (/)
130 19 59 ineq12i 
 |-  ( dom { <. ( *r ` ndx ) , * >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) = ( { ( *r ` ndx ) } i^i { ( UnifSet ` ndx ) } )
131 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 ) )
132 61 131 ax-mp 
 |-  ( *r ` ndx ) =/= ( UnifSet ` ndx )
133 disjsn2 
 |-  ( ( *r ` ndx ) =/= ( UnifSet ` ndx ) -> ( { ( *r ` ndx ) } i^i { ( UnifSet ` ndx ) } ) = (/) )
134 132 133 ax-mp 
 |-  ( { ( *r ` ndx ) } i^i { ( UnifSet ` ndx ) } ) = (/)
135 130 134 eqtri 
 |-  ( dom { <. ( *r ` ndx ) , * >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) = (/)
136 129 135 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. - ) ) >. } ) = (/) )
137 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. - ) ) >. } ) ) = (/) )
138 136 137 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. - ) ) >. } ) ) = (/)
139 117 138 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. - ) ) >. } ) ) = (/) )
140 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. - ) ) >. } ) ) = (/) )
141 139 140 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. - ) ) >. } ) ) = (/)
142 77 141 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. - ) ) >. } ) ) = (/)
143 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. - ) ) >. } ) ) )
144 74 142 143 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. - ) ) >. } ) )
145 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. - ) ) >. } ) )
146 145 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. - ) ) >. } ) ) )
147 144 146 mpbir 
 |-  Fun CCfld