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) Revise df-cnfld . (Revised by Thierry Arnoux, 9-Nov-2026) (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 unifndx 
 |-  ( UnifSet ` ndx ) = ; 1 3
55 1nn0 
 |-  1 e. NN0
56 3nn0 
 |-  3 e. NN0
57 55 56 deccl 
 |-  ; 1 3 e. NN0
58 57 nn0rei 
 |-  ; 1 3 e. RR
59 54 58 eqeltri 
 |-  ( UnifSet ` ndx ) e. RR
60 2nn0 
 |-  2 e. NN0
61 3lt10 
 |-  3 < ; 1 0
62 1lt2 
 |-  1 < 2
63 55 60 56 55 61 62 decltc 
 |-  ; 1 3 < ; 2 1
64 eufndx 
 |-  ( EuclF ` ndx ) = ; 2 1
65 63 64 breqtrri 
 |-  ; 1 3 < ( EuclF ` ndx )
66 54 65 eqbrtri 
 |-  ( UnifSet ` ndx ) < ( EuclF ` ndx )
67 59 66 ltneii 
 |-  ( UnifSet ` ndx ) =/= ( EuclF ` ndx )
68 fvex 
 |-  ( UnifSet ` ndx ) e. _V
69 fvex 
 |-  ( EuclF ` ndx ) e. _V
70 fvex 
 |-  ( metUnif ` ( abs o. - ) ) e. _V
71 68 69 70 46 funpr 
 |-  ( ( UnifSet ` ndx ) =/= ( EuclF ` ndx ) -> Fun { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } )
72 67 71 ax-mp 
 |-  Fun { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. , <. ( EuclF ` ndx ) , abs >. }
73 53 72 pm3.2i 
 |-  ( Fun { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } /\ Fun { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } )
74 41 43 51 dmtpop 
 |-  dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } = { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) }
75 70 46 dmprop 
 |-  dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } = { ( UnifSet ` ndx ) , ( EuclF ` ndx ) }
76 74 75 ineq12i 
 |-  ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) = ( { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } i^i { ( UnifSet ` ndx ) , ( EuclF ` ndx ) } )
77 slotsdifunifndx 
 |-  ( ( ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) /\ ( *r ` ndx ) =/= ( UnifSet ` ndx ) ) /\ ( ( le ` ndx ) =/= ( UnifSet ` ndx ) /\ ( dist ` ndx ) =/= ( UnifSet ` ndx ) ) )
78 unifndxntsetndx 
 |-  ( UnifSet ` ndx ) =/= ( TopSet ` ndx )
79 78 necomi 
 |-  ( TopSet ` ndx ) =/= ( UnifSet ` ndx )
80 79 a1i 
 |-  ( ( ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) /\ ( *r ` ndx ) =/= ( UnifSet ` ndx ) ) -> ( TopSet ` ndx ) =/= ( UnifSet ` ndx ) )
81 80 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 ) ) ) )
82 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 ) ) ) )
83 81 82 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 ) ) )
84 77 83 ax-mp 
 |-  ( ( TopSet ` ndx ) =/= ( UnifSet ` ndx ) /\ ( le ` ndx ) =/= ( UnifSet ` ndx ) /\ ( dist ` ndx ) =/= ( UnifSet ` ndx ) )
85 tsetndx 
 |-  ( TopSet ` ndx ) = 9
86 9nn0 
 |-  9 e. NN0
87 85 86 eqeltri 
 |-  ( TopSet ` ndx ) e. NN0
88 87 nn0rei 
 |-  ( TopSet ` ndx ) e. RR
89 2nn 
 |-  2 e. NN
90 9lt10 
 |-  9 < ; 1 0
91 89 55 86 90 declti 
 |-  9 < ; 2 1
92 91 64 breqtrri 
 |-  9 < ( EuclF ` ndx )
93 85 92 eqbrtri 
 |-  ( TopSet ` ndx ) < ( EuclF ` ndx )
94 88 93 ltneii 
 |-  ( TopSet ` ndx ) =/= ( EuclF ` ndx )
95 plendx 
 |-  ( le ` ndx ) = ; 1 0
96 10nn0 
 |-  ; 1 0 e. NN0
97 95 96 eqeltri 
 |-  ( le ` ndx ) e. NN0
98 97 nn0rei 
 |-  ( le ` ndx ) e. RR
99 0nn0 
 |-  0 e. NN0
100 10pos 
 |-  0 < ; 1 0
101 55 60 99 55 100 62 decltc 
 |-  ; 1 0 < ; 2 1
102 101 64 breqtrri 
 |-  ; 1 0 < ( EuclF ` ndx )
103 95 102 eqbrtri 
 |-  ( le ` ndx ) < ( EuclF ` ndx )
104 98 103 ltneii 
 |-  ( le ` ndx ) =/= ( EuclF ` ndx )
105 dsndx 
 |-  ( dist ` ndx ) = ; 1 2
106 55 60 deccl 
 |-  ; 1 2 e. NN0
107 106 nn0rei 
 |-  ; 1 2 e. RR
108 105 107 eqeltri 
 |-  ( dist ` ndx ) e. RR
109 2lt10 
 |-  2 < ; 1 0
110 55 60 60 55 109 62 decltc 
 |-  ; 1 2 < ; 2 1
111 110 64 breqtrri 
 |-  ; 1 2 < ( EuclF ` ndx )
112 105 111 eqbrtri 
 |-  ( dist ` ndx ) < ( EuclF ` ndx )
113 108 112 ltneii 
 |-  ( dist ` ndx ) =/= ( EuclF ` ndx )
114 94 104 113 3pm3.2i 
 |-  ( ( TopSet ` ndx ) =/= ( EuclF ` ndx ) /\ ( le ` ndx ) =/= ( EuclF ` ndx ) /\ ( dist ` ndx ) =/= ( EuclF ` ndx ) )
115 disjtppr 
 |-  ( ( ( ( TopSet ` ndx ) =/= ( UnifSet ` ndx ) /\ ( le ` ndx ) =/= ( UnifSet ` ndx ) /\ ( dist ` ndx ) =/= ( UnifSet ` ndx ) ) /\ ( ( TopSet ` ndx ) =/= ( EuclF ` ndx ) /\ ( le ` ndx ) =/= ( EuclF ` ndx ) /\ ( dist ` ndx ) =/= ( EuclF ` ndx ) ) ) -> ( { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } i^i { ( UnifSet ` ndx ) , ( EuclF ` ndx ) } ) = (/) )
116 84 114 115 mp2an 
 |-  ( { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } i^i { ( UnifSet ` ndx ) , ( EuclF ` ndx ) } ) = (/)
117 76 116 eqtri 
 |-  ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) = (/)
118 funun 
 |-  ( ( ( Fun { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } /\ Fun { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) /\ ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) = (/) ) -> Fun ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) )
119 73 117 118 mp2an 
 |-  Fun ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } )
120 31 119 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) )
121 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 ) , * >. } )
122 dmun 
 |-  dom ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) = ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } )
123 121 122 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) ) = ( ( 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) )
124 18 74 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 ) } )
125 tsetndxnbasendx 
 |-  ( TopSet ` ndx ) =/= ( Base ` ndx )
126 125 necomi 
 |-  ( Base ` ndx ) =/= ( TopSet ` ndx )
127 tsetndxnplusgndx 
 |-  ( TopSet ` ndx ) =/= ( +g ` ndx )
128 127 necomi 
 |-  ( +g ` ndx ) =/= ( TopSet ` ndx )
129 tsetndxnmulrndx 
 |-  ( TopSet ` ndx ) =/= ( .r ` ndx )
130 129 necomi 
 |-  ( .r ` ndx ) =/= ( TopSet ` ndx )
131 126 128 130 3pm3.2i 
 |-  ( ( Base ` ndx ) =/= ( TopSet ` ndx ) /\ ( +g ` ndx ) =/= ( TopSet ` ndx ) /\ ( .r ` ndx ) =/= ( TopSet ` ndx ) )
132 plendxnbasendx 
 |-  ( le ` ndx ) =/= ( Base ` ndx )
133 132 necomi 
 |-  ( Base ` ndx ) =/= ( le ` ndx )
134 plendxnplusgndx 
 |-  ( le ` ndx ) =/= ( +g ` ndx )
135 134 necomi 
 |-  ( +g ` ndx ) =/= ( le ` ndx )
136 plendxnmulrndx 
 |-  ( le ` ndx ) =/= ( .r ` ndx )
137 136 necomi 
 |-  ( .r ` ndx ) =/= ( le ` ndx )
138 133 135 137 3pm3.2i 
 |-  ( ( Base ` ndx ) =/= ( le ` ndx ) /\ ( +g ` ndx ) =/= ( le ` ndx ) /\ ( .r ` ndx ) =/= ( le ` ndx ) )
139 dsndxnbasendx 
 |-  ( dist ` ndx ) =/= ( Base ` ndx )
140 139 necomi 
 |-  ( Base ` ndx ) =/= ( dist ` ndx )
141 dsndxnplusgndx 
 |-  ( dist ` ndx ) =/= ( +g ` ndx )
142 141 necomi 
 |-  ( +g ` ndx ) =/= ( dist ` ndx )
143 dsndxnmulrndx 
 |-  ( dist ` ndx ) =/= ( .r ` ndx )
144 143 necomi 
 |-  ( .r ` ndx ) =/= ( dist ` ndx )
145 140 142 144 3pm3.2i 
 |-  ( ( Base ` ndx ) =/= ( dist ` ndx ) /\ ( +g ` ndx ) =/= ( dist ` ndx ) /\ ( .r ` ndx ) =/= ( dist ` ndx ) )
146 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 ) } ) = (/) )
147 131 138 145 146 mp3an 
 |-  ( { ( Base ` ndx ) , ( +g ` ndx ) , ( .r ` ndx ) } i^i { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } ) = (/)
148 124 147 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. - ) >. } ) = (/)
149 18 75 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) = ( { ( Base ` ndx ) , ( +g ` ndx ) , ( .r ` ndx ) } i^i { ( UnifSet ` ndx ) , ( EuclF ` ndx ) } )
150 unifndxnbasendx 
 |-  ( UnifSet ` ndx ) =/= ( Base ` ndx )
151 150 necomi 
 |-  ( Base ` ndx ) =/= ( UnifSet ` ndx )
152 151 a1i 
 |-  ( ( ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) /\ ( *r ` ndx ) =/= ( UnifSet ` ndx ) ) -> ( Base ` ndx ) =/= ( UnifSet ` ndx ) )
153 3simpa 
 |-  ( ( ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) /\ ( *r ` ndx ) =/= ( UnifSet ` ndx ) ) -> ( ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) ) )
154 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 ) ) ) )
155 152 153 154 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 ) ) )
156 155 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 ) ) )
157 77 156 ax-mp 
 |-  ( ( Base ` ndx ) =/= ( UnifSet ` ndx ) /\ ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) )
158 basendx 
 |-  ( Base ` ndx ) = 1
159 158 55 eqeltri 
 |-  ( Base ` ndx ) e. NN0
160 159 nn0rei 
 |-  ( Base ` ndx ) e. RR
161 1lt10 
 |-  1 < ; 1 0
162 89 55 55 161 declti 
 |-  1 < ; 2 1
163 162 64 breqtrri 
 |-  1 < ( EuclF ` ndx )
164 158 163 eqbrtri 
 |-  ( Base ` ndx ) < ( EuclF ` ndx )
165 160 164 ltneii 
 |-  ( Base ` ndx ) =/= ( EuclF ` ndx )
166 plusgndx 
 |-  ( +g ` ndx ) = 2
167 166 60 eqeltri 
 |-  ( +g ` ndx ) e. NN0
168 167 nn0rei 
 |-  ( +g ` ndx ) e. RR
169 89 55 60 109 declti 
 |-  2 < ; 2 1
170 169 64 breqtrri 
 |-  2 < ( EuclF ` ndx )
171 166 170 eqbrtri 
 |-  ( +g ` ndx ) < ( EuclF ` ndx )
172 168 171 ltneii 
 |-  ( +g ` ndx ) =/= ( EuclF ` ndx )
173 mulrndx 
 |-  ( .r ` ndx ) = 3
174 173 56 eqeltri 
 |-  ( .r ` ndx ) e. NN0
175 174 nn0rei 
 |-  ( .r ` ndx ) e. RR
176 89 55 56 61 declti 
 |-  3 < ; 2 1
177 176 64 breqtrri 
 |-  3 < ( EuclF ` ndx )
178 173 177 eqbrtri 
 |-  ( .r ` ndx ) < ( EuclF ` ndx )
179 175 178 ltneii 
 |-  ( .r ` ndx ) =/= ( EuclF ` ndx )
180 165 172 179 3pm3.2i 
 |-  ( ( Base ` ndx ) =/= ( EuclF ` ndx ) /\ ( +g ` ndx ) =/= ( EuclF ` ndx ) /\ ( .r ` ndx ) =/= ( EuclF ` ndx ) )
181 disjtppr 
 |-  ( ( ( ( Base ` ndx ) =/= ( UnifSet ` ndx ) /\ ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) ) /\ ( ( Base ` ndx ) =/= ( EuclF ` ndx ) /\ ( +g ` ndx ) =/= ( EuclF ` ndx ) /\ ( .r ` ndx ) =/= ( EuclF ` ndx ) ) ) -> ( { ( Base ` ndx ) , ( +g ` ndx ) , ( .r ` ndx ) } i^i { ( UnifSet ` ndx ) , ( EuclF ` ndx ) } ) = (/) )
182 157 180 181 mp2an 
 |-  ( { ( Base ` ndx ) , ( +g ` ndx ) , ( .r ` ndx ) } i^i { ( UnifSet ` ndx ) , ( EuclF ` ndx ) } ) = (/)
183 149 182 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) = (/)
184 148 183 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) = (/) )
185 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) = (/) ) <-> ( 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) ) = (/) )
186 184 185 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) ) = (/)
187 19 74 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 ) } )
188 tsetndxnstarvndx 
 |-  ( TopSet ` ndx ) =/= ( *r ` ndx )
189 necom 
 |-  ( ( *r ` ndx ) =/= ( le ` ndx ) <-> ( le ` ndx ) =/= ( *r ` ndx ) )
190 189 birani 
 |-  ( ( ( *r ` ndx ) =/= ( le ` ndx ) /\ ( TopSet ` ndx ) =/= ( le ` ndx ) ) -> ( le ` ndx ) =/= ( *r ` ndx ) )
191 32 190 ax-mp 
 |-  ( le ` ndx ) =/= ( *r ` ndx )
192 necom 
 |-  ( ( *r ` ndx ) =/= ( dist ` ndx ) <-> ( dist ` ndx ) =/= ( *r ` ndx ) )
193 192 birani 
 |-  ( ( ( *r ` ndx ) =/= ( dist ` ndx ) /\ ( le ` ndx ) =/= ( dist ` ndx ) ) -> ( dist ` ndx ) =/= ( *r ` ndx ) )
194 36 193 ax-mp 
 |-  ( dist ` ndx ) =/= ( *r ` ndx )
195 disjtpsn 
 |-  ( ( ( TopSet ` ndx ) =/= ( *r ` ndx ) /\ ( le ` ndx ) =/= ( *r ` ndx ) /\ ( dist ` ndx ) =/= ( *r ` ndx ) ) -> ( { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } i^i { ( *r ` ndx ) } ) = (/) )
196 188 191 194 195 mp3an 
 |-  ( { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } i^i { ( *r ` ndx ) } ) = (/)
197 196 ineqcomi 
 |-  ( { ( *r ` ndx ) } i^i { ( TopSet ` ndx ) , ( le ` ndx ) , ( dist ` ndx ) } ) = (/)
198 187 197 eqtri 
 |-  ( dom { <. ( *r ` ndx ) , * >. } i^i dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } ) = (/)
199 19 75 ineq12i 
 |-  ( dom { <. ( *r ` ndx ) , * >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) = ( { ( *r ` ndx ) } i^i { ( UnifSet ` ndx ) , ( EuclF ` ndx ) } )
200 incom 
 |-  ( { ( *r ` ndx ) } i^i { ( UnifSet ` ndx ) , ( EuclF ` ndx ) } ) = ( { ( UnifSet ` ndx ) , ( EuclF ` ndx ) } i^i { ( *r ` ndx ) } )
201 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 ) )
202 77 201 ax-mp 
 |-  ( *r ` ndx ) =/= ( UnifSet ` ndx )
203 202 necomi 
 |-  ( UnifSet ` ndx ) =/= ( *r ` ndx )
204 starvndx 
 |-  ( *r ` ndx ) = 4
205 4nn0 
 |-  4 e. NN0
206 204 205 eqeltri 
 |-  ( *r ` ndx ) e. NN0
207 206 nn0rei 
 |-  ( *r ` ndx ) e. RR
208 4lt10 
 |-  4 < ; 1 0
209 89 55 205 208 declti 
 |-  4 < ; 2 1
210 209 64 breqtrri 
 |-  4 < ( EuclF ` ndx )
211 204 210 eqbrtri 
 |-  ( *r ` ndx ) < ( EuclF ` ndx )
212 207 211 gtneii 
 |-  ( EuclF ` ndx ) =/= ( *r ` ndx )
213 disjprsn 
 |-  ( ( ( UnifSet ` ndx ) =/= ( *r ` ndx ) /\ ( EuclF ` ndx ) =/= ( *r ` ndx ) ) -> ( { ( UnifSet ` ndx ) , ( EuclF ` ndx ) } i^i { ( *r ` ndx ) } ) = (/) )
214 203 212 213 mp2an 
 |-  ( { ( UnifSet ` ndx ) , ( EuclF ` ndx ) } i^i { ( *r ` ndx ) } ) = (/)
215 200 214 eqtri 
 |-  ( { ( *r ` ndx ) } i^i { ( UnifSet ` ndx ) , ( EuclF ` ndx ) } ) = (/)
216 199 215 eqtri 
 |-  ( dom { <. ( *r ` ndx ) , * >. } i^i dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) = (/)
217 198 216 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) = (/) )
218 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) = (/) ) <-> ( dom { <. ( *r ` ndx ) , * >. } i^i ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) ) = (/) )
219 217 218 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) ) = (/)
220 186 219 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) ) = (/) /\ ( dom { <. ( *r ` ndx ) , * >. } i^i ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) ) = (/) )
221 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) ) = (/) /\ ( dom { <. ( *r ` ndx ) , * >. } i^i ( dom { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. dom { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) ) = (/) ) <-> ( ( 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) ) = (/) )
222 220 221 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) ) = (/)
223 123 222 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) ) = (/)
224 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) ) /\ ( 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) ) = (/) ) -> 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) ) )
225 120 223 224 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) )
226 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) )
227 226 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) ) )
228 225 227 mpbir 
 |-  Fun CCfld