Metamath Proof Explorer

Theorem ioorrnopnlem

Description: The a point in an indexed product of open intervals is contained in an open ball that is contained in the indexed product of open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses ioorrnopnlem.x 
|- ( ph -> X e. Fin )
ioorrnopnlem.n 
|- ( ph -> X =/= (/) )
ioorrnopnlem.a 
|- ( ph -> A : X --> RR )
ioorrnopnlem.b 
|- ( ph -> B : X --> RR )
ioorrnopnlem.f 
|- ( ph -> F e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) )
ioorrnopnlem.h 
|- H = ran ( i e. X |-> if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) )
ioorrnopnlem.e 
|- E = inf ( H , RR , < )
ioorrnopnlem.v 
|- V = ( F ( ball ` D ) E )
ioorrnopnlem.d 
|- D = ( f e. ( RR ^m X ) , g e. ( RR ^m X ) |-> ( sqrt ` sum_ k e. X ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) )
Assertion ioorrnopnlem 
|- ( ph -> E. v e. ( TopOpen ` ( RR^ ` X ) ) ( F e. v /\ v C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) )

Proof

Step Hyp Ref Expression
1 ioorrnopnlem.x 
 |-  ( ph -> X e. Fin )
2 ioorrnopnlem.n 
 |-  ( ph -> X =/= (/) )
3 ioorrnopnlem.a 
 |-  ( ph -> A : X --> RR )
4 ioorrnopnlem.b 
 |-  ( ph -> B : X --> RR )
5 ioorrnopnlem.f 
 |-  ( ph -> F e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) )
6 ioorrnopnlem.h 
 |-  H = ran ( i e. X |-> if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) )
7 ioorrnopnlem.e 
 |-  E = inf ( H , RR , < )
8 ioorrnopnlem.v 
 |-  V = ( F ( ball ` D ) E )
9 ioorrnopnlem.d 
 |-  D = ( f e. ( RR ^m X ) , g e. ( RR ^m X ) |-> ( sqrt ` sum_ k e. X ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) )
10 1 9 rrndsxmet 
 |-  ( ph -> D e. ( *Met ` ( RR ^m X ) ) )
11 nfv 
 |-  F/ i ph
12 reex 
 |-  RR e. _V
13 12 a1i 
 |-  ( ph -> RR e. _V )
14 ioossre 
 |-  ( ( A ` i ) (,) ( B ` i ) ) C_ RR
15 14 a1i 
 |-  ( ( ph /\ i e. X ) -> ( ( A ` i ) (,) ( B ` i ) ) C_ RR )
16 11 13 15 ixpssmapc 
 |-  ( ph -> X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) C_ ( RR ^m X ) )
17 16 5 sseldd 
 |-  ( ph -> F e. ( RR ^m X ) )
18 6 a1i 
 |-  ( ph -> H = ran ( i e. X |-> if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) ) )
19 4 ffvelrnda 
 |-  ( ( ph /\ i e. X ) -> ( B ` i ) e. RR )
20 5 adantr 
 |-  ( ( ph /\ i e. X ) -> F e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) )
21 simpr 
 |-  ( ( ph /\ i e. X ) -> i e. X )
22 fvixp2 
 |-  ( ( F e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) /\ i e. X ) -> ( F ` i ) e. ( ( A ` i ) (,) ( B ` i ) ) )
23 20 21 22 syl2anc 
 |-  ( ( ph /\ i e. X ) -> ( F ` i ) e. ( ( A ` i ) (,) ( B ` i ) ) )
24 14 23 sseldi 
 |-  ( ( ph /\ i e. X ) -> ( F ` i ) e. RR )
25 19 24 resubcld 
 |-  ( ( ph /\ i e. X ) -> ( ( B ` i ) - ( F ` i ) ) e. RR )
26 3 ffvelrnda 
 |-  ( ( ph /\ i e. X ) -> ( A ` i ) e. RR )
27 26 rexrd 
 |-  ( ( ph /\ i e. X ) -> ( A ` i ) e. RR* )
28 19 rexrd 
 |-  ( ( ph /\ i e. X ) -> ( B ` i ) e. RR* )
29 iooltub 
 |-  ( ( ( A ` i ) e. RR* /\ ( B ` i ) e. RR* /\ ( F ` i ) e. ( ( A ` i ) (,) ( B ` i ) ) ) -> ( F ` i ) < ( B ` i ) )
30 27 28 23 29 syl3anc 
 |-  ( ( ph /\ i e. X ) -> ( F ` i ) < ( B ` i ) )
31 24 19 posdifd 
 |-  ( ( ph /\ i e. X ) -> ( ( F ` i ) < ( B ` i ) <-> 0 < ( ( B ` i ) - ( F ` i ) ) ) )
32 30 31 mpbid 
 |-  ( ( ph /\ i e. X ) -> 0 < ( ( B ` i ) - ( F ` i ) ) )
33 25 32 elrpd 
 |-  ( ( ph /\ i e. X ) -> ( ( B ` i ) - ( F ` i ) ) e. RR+ )
34 24 26 resubcld 
 |-  ( ( ph /\ i e. X ) -> ( ( F ` i ) - ( A ` i ) ) e. RR )
35 ioogtlb 
 |-  ( ( ( A ` i ) e. RR* /\ ( B ` i ) e. RR* /\ ( F ` i ) e. ( ( A ` i ) (,) ( B ` i ) ) ) -> ( A ` i ) < ( F ` i ) )
36 27 28 23 35 syl3anc 
 |-  ( ( ph /\ i e. X ) -> ( A ` i ) < ( F ` i ) )
37 26 24 posdifd 
 |-  ( ( ph /\ i e. X ) -> ( ( A ` i ) < ( F ` i ) <-> 0 < ( ( F ` i ) - ( A ` i ) ) ) )
38 36 37 mpbid 
 |-  ( ( ph /\ i e. X ) -> 0 < ( ( F ` i ) - ( A ` i ) ) )
39 34 38 elrpd 
 |-  ( ( ph /\ i e. X ) -> ( ( F ` i ) - ( A ` i ) ) e. RR+ )
40 33 39 ifcld 
 |-  ( ( ph /\ i e. X ) -> if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) e. RR+ )
41 40 ralrimiva 
 |-  ( ph -> A. i e. X if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) e. RR+ )
42 eqid 
 |-  ( i e. X |-> if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) ) = ( i e. X |-> if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) )
43 42 rnmptss 
 |-  ( A. i e. X if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) e. RR+ -> ran ( i e. X |-> if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) ) C_ RR+ )
44 41 43 syl 
 |-  ( ph -> ran ( i e. X |-> if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) ) C_ RR+ )
45 18 44 eqsstrd 
 |-  ( ph -> H C_ RR+ )
46 ltso 
 |-  < Or RR
47 46 a1i 
 |-  ( ph -> < Or RR )
48 42 rnmptfi 
 |-  ( X e. Fin -> ran ( i e. X |-> if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) ) e. Fin )
49 1 48 syl 
 |-  ( ph -> ran ( i e. X |-> if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) ) e. Fin )
50 6 49 eqeltrid 
 |-  ( ph -> H e. Fin )
51 11 40 42 2 rnmptn0 
 |-  ( ph -> ran ( i e. X |-> if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) ) =/= (/) )
52 18 51 eqnetrd 
 |-  ( ph -> H =/= (/) )
53 rpssre 
 |-  RR+ C_ RR
54 53 a1i 
 |-  ( ph -> RR+ C_ RR )
55 45 54 sstrd 
 |-  ( ph -> H C_ RR )
56 fiinfcl 
 |-  ( ( < Or RR /\ ( H e. Fin /\ H =/= (/) /\ H C_ RR ) ) -> inf ( H , RR , < ) e. H )
57 47 50 52 55 56 syl13anc 
 |-  ( ph -> inf ( H , RR , < ) e. H )
58 45 57 sseldd 
 |-  ( ph -> inf ( H , RR , < ) e. RR+ )
59 7 58 eqeltrid 
 |-  ( ph -> E e. RR+ )
60 rpxr 
 |-  ( E e. RR+ -> E e. RR* )
61 59 60 syl 
 |-  ( ph -> E e. RR* )
62 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
63 62 blopn 
 |-  ( ( D e. ( *Met ` ( RR ^m X ) ) /\ F e. ( RR ^m X ) /\ E e. RR* ) -> ( F ( ball ` D ) E ) e. ( MetOpen ` D ) )
64 10 17 61 63 syl3anc 
 |-  ( ph -> ( F ( ball ` D ) E ) e. ( MetOpen ` D ) )
65 8 a1i 
 |-  ( ph -> V = ( F ( ball ` D ) E ) )
66 1 rrxtopnfi 
 |-  ( ph -> ( TopOpen ` ( RR^ ` X ) ) = ( MetOpen ` ( f e. ( RR ^m X ) , g e. ( RR ^m X ) |-> ( sqrt ` sum_ k e. X ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) ) )
67 9 eqcomi 
 |-  ( f e. ( RR ^m X ) , g e. ( RR ^m X ) |-> ( sqrt ` sum_ k e. X ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) = D
68 67 a1i 
 |-  ( ph -> ( f e. ( RR ^m X ) , g e. ( RR ^m X ) |-> ( sqrt ` sum_ k e. X ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) = D )
69 68 fveq2d 
 |-  ( ph -> ( MetOpen ` ( f e. ( RR ^m X ) , g e. ( RR ^m X ) |-> ( sqrt ` sum_ k e. X ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) ) = ( MetOpen ` D ) )
70 66 69 eqtrd 
 |-  ( ph -> ( TopOpen ` ( RR^ ` X ) ) = ( MetOpen ` D ) )
71 65 70 eleq12d 
 |-  ( ph -> ( V e. ( TopOpen ` ( RR^ ` X ) ) <-> ( F ( ball ` D ) E ) e. ( MetOpen ` D ) ) )
72 64 71 mpbird 
 |-  ( ph -> V e. ( TopOpen ` ( RR^ ` X ) ) )
73 xmetpsmet 
 |-  ( D e. ( *Met ` ( RR ^m X ) ) -> D e. ( PsMet ` ( RR ^m X ) ) )
74 10 73 syl 
 |-  ( ph -> D e. ( PsMet ` ( RR ^m X ) ) )
75 blcntrps 
 |-  ( ( D e. ( PsMet ` ( RR ^m X ) ) /\ F e. ( RR ^m X ) /\ E e. RR+ ) -> F e. ( F ( ball ` D ) E ) )
76 74 17 59 75 syl3anc 
 |-  ( ph -> F e. ( F ( ball ` D ) E ) )
77 65 eqcomd 
 |-  ( ph -> ( F ( ball ` D ) E ) = V )
78 76 77 eleqtrd 
 |-  ( ph -> F e. V )
79 nfv 
 |-  F/ g ph
80 elmapfn 
 |-  ( g e. ( RR ^m X ) -> g Fn X )
81 80 3ad2ant2 
 |-  ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) -> g Fn X )
82 27 3ad2antl1 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( A ` i ) e. RR* )
83 28 3ad2antl1 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( B ` i ) e. RR* )
84 simpl2 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> g e. ( RR ^m X ) )
85 simpr 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> i e. X )
86 elmapi 
 |-  ( g e. ( RR ^m X ) -> g : X --> RR )
87 86 adantr 
 |-  ( ( g e. ( RR ^m X ) /\ i e. X ) -> g : X --> RR )
88 simpr 
 |-  ( ( g e. ( RR ^m X ) /\ i e. X ) -> i e. X )
89 87 88 ffvelrnd 
 |-  ( ( g e. ( RR ^m X ) /\ i e. X ) -> ( g ` i ) e. RR )
90 84 85 89 syl2anc 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( g ` i ) e. RR )
91 26 3ad2antl1 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( A ` i ) e. RR )
92 53 59 sseldi 
 |-  ( ph -> E e. RR )
93 92 adantr 
 |-  ( ( ph /\ i e. X ) -> E e. RR )
94 24 93 resubcld 
 |-  ( ( ph /\ i e. X ) -> ( ( F ` i ) - E ) e. RR )
95 94 3ad2antl1 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( ( F ` i ) - E ) e. RR )
96 53 40 sseldi 
 |-  ( ( ph /\ i e. X ) -> if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) e. RR )
97 7 a1i 
 |-  ( ph -> E = inf ( H , RR , < ) )
98 infxrrefi 
 |-  ( ( H C_ RR /\ H e. Fin /\ H =/= (/) ) -> inf ( H , RR* , < ) = inf ( H , RR , < ) )
99 55 50 52 98 syl3anc 
 |-  ( ph -> inf ( H , RR* , < ) = inf ( H , RR , < ) )
100 99 eqcomd 
 |-  ( ph -> inf ( H , RR , < ) = inf ( H , RR* , < ) )
101 97 100 eqtrd 
 |-  ( ph -> E = inf ( H , RR* , < ) )
102 101 adantr 
 |-  ( ( ph /\ i e. X ) -> E = inf ( H , RR* , < ) )
103 ressxr 
 |-  RR C_ RR*
104 103 a1i 
 |-  ( ph -> RR C_ RR* )
105 55 104 sstrd 
 |-  ( ph -> H C_ RR* )
106 105 adantr 
 |-  ( ( ph /\ i e. X ) -> H C_ RR* )
107 40 elexd 
 |-  ( ( ph /\ i e. X ) -> if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) e. _V )
108 42 elrnmpt1 
 |-  ( ( i e. X /\ if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) e. _V ) -> if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) e. ran ( i e. X |-> if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) ) )
109 21 107 108 syl2anc 
 |-  ( ( ph /\ i e. X ) -> if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) e. ran ( i e. X |-> if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) ) )
110 109 6 eleqtrrdi 
 |-  ( ( ph /\ i e. X ) -> if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) e. H )
111 infxrlb 
 |-  ( ( H C_ RR* /\ if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) e. H ) -> inf ( H , RR* , < ) <_ if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) )
112 106 110 111 syl2anc 
 |-  ( ( ph /\ i e. X ) -> inf ( H , RR* , < ) <_ if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) )
113 102 112 eqbrtrd 
 |-  ( ( ph /\ i e. X ) -> E <_ if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) )
114 min2 
 |-  ( ( ( ( B ` i ) - ( F ` i ) ) e. RR /\ ( ( F ` i ) - ( A ` i ) ) e. RR ) -> if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) <_ ( ( F ` i ) - ( A ` i ) ) )
115 25 34 114 syl2anc 
 |-  ( ( ph /\ i e. X ) -> if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) <_ ( ( F ` i ) - ( A ` i ) ) )
116 93 96 34 113 115 letrd 
 |-  ( ( ph /\ i e. X ) -> E <_ ( ( F ` i ) - ( A ` i ) ) )
117 93 24 26 116 lesubd 
 |-  ( ( ph /\ i e. X ) -> ( A ` i ) <_ ( ( F ` i ) - E ) )
118 117 3ad2antl1 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( A ` i ) <_ ( ( F ` i ) - E ) )
119 24 adantlr 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> ( F ` i ) e. RR )
120 89 adantll 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> ( g ` i ) e. RR )
121 119 120 resubcld 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> ( ( F ` i ) - ( g ` i ) ) e. RR )
122 121 3adantl3 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( ( F ` i ) - ( g ` i ) ) e. RR )
123 1 9 rrndsmet 
 |-  ( ph -> D e. ( Met ` ( RR ^m X ) ) )
124 123 ad2antrr 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> D e. ( Met ` ( RR ^m X ) ) )
125 17 ad2antrr 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> F e. ( RR ^m X ) )
126 simplr 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> g e. ( RR ^m X ) )
127 metcl 
 |-  ( ( D e. ( Met ` ( RR ^m X ) ) /\ F e. ( RR ^m X ) /\ g e. ( RR ^m X ) ) -> ( F D g ) e. RR )
128 124 125 126 127 syl3anc 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> ( F D g ) e. RR )
129 128 3adantl3 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( F D g ) e. RR )
130 93 adantlr 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> E e. RR )
131 130 3adantl3 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> E e. RR )
132 121 recnd 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> ( ( F ` i ) - ( g ` i ) ) e. CC )
133 132 abscld 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> ( abs ` ( ( F ` i ) - ( g ` i ) ) ) e. RR )
134 121 leabsd 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> ( ( F ` i ) - ( g ` i ) ) <_ ( abs ` ( ( F ` i ) - ( g ` i ) ) ) )
135 1 ad2antrr 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> X e. Fin )
136 ixpf 
 |-  ( F e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) -> F : X --> U_ i e. X ( ( A ` i ) (,) ( B ` i ) ) )
137 5 136 syl 
 |-  ( ph -> F : X --> U_ i e. X ( ( A ` i ) (,) ( B ` i ) ) )
138 15 ralrimiva 
 |-  ( ph -> A. i e. X ( ( A ` i ) (,) ( B ` i ) ) C_ RR )
139 iunss 
 |-  ( U_ i e. X ( ( A ` i ) (,) ( B ` i ) ) C_ RR <-> A. i e. X ( ( A ` i ) (,) ( B ` i ) ) C_ RR )
140 138 139 sylibr 
 |-  ( ph -> U_ i e. X ( ( A ` i ) (,) ( B ` i ) ) C_ RR )
141 137 140 fssd 
 |-  ( ph -> F : X --> RR )
142 141 ad2antrr 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> F : X --> RR )
143 126 86 syl 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> g : X --> RR )
144 simpr 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> i e. X )
145 eqid 
 |-  ( dist ` ( RR^ ` X ) ) = ( dist ` ( RR^ ` X ) )
146 135 142 143 144 145 rrnprjdstle 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> ( abs ` ( ( F ` i ) - ( g ` i ) ) ) <_ ( F ( dist ` ( RR^ ` X ) ) g ) )
147 eqid 
 |-  ( RR^ ` X ) = ( RR^ ` X )
148 eqid 
 |-  ( RR ^m X ) = ( RR ^m X )
149 147 148 rrxdsfi 
 |-  ( X e. Fin -> ( dist ` ( RR^ ` X ) ) = ( f e. ( RR ^m X ) , g e. ( RR ^m X ) |-> ( sqrt ` sum_ k e. X ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) )
150 1 149 syl 
 |-  ( ph -> ( dist ` ( RR^ ` X ) ) = ( f e. ( RR ^m X ) , g e. ( RR ^m X ) |-> ( sqrt ` sum_ k e. X ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) )
151 150 68 eqtrd 
 |-  ( ph -> ( dist ` ( RR^ ` X ) ) = D )
152 151 oveqd 
 |-  ( ph -> ( F ( dist ` ( RR^ ` X ) ) g ) = ( F D g ) )
153 152 ad2antrr 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> ( F ( dist ` ( RR^ ` X ) ) g ) = ( F D g ) )
154 146 153 breqtrd 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> ( abs ` ( ( F ` i ) - ( g ` i ) ) ) <_ ( F D g ) )
155 121 133 128 134 154 letrd 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> ( ( F ` i ) - ( g ` i ) ) <_ ( F D g ) )
156 155 3adantl3 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( ( F ` i ) - ( g ` i ) ) <_ ( F D g ) )
157 simpl3 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( F D g ) < E )
158 122 129 131 156 157 lelttrd 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( ( F ` i ) - ( g ` i ) ) < E )
159 ltsub23 
 |-  ( ( ( F ` i ) e. RR /\ ( g ` i ) e. RR /\ E e. RR ) -> ( ( ( F ` i ) - ( g ` i ) ) < E <-> ( ( F ` i ) - E ) < ( g ` i ) ) )
160 119 120 130 159 syl3anc 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> ( ( ( F ` i ) - ( g ` i ) ) < E <-> ( ( F ` i ) - E ) < ( g ` i ) ) )
161 160 3adantl3 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( ( ( F ` i ) - ( g ` i ) ) < E <-> ( ( F ` i ) - E ) < ( g ` i ) ) )
162 158 161 mpbid 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( ( F ` i ) - E ) < ( g ` i ) )
163 91 95 90 118 162 lelttrd 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( A ` i ) < ( g ` i ) )
164 24 93 readdcld 
 |-  ( ( ph /\ i e. X ) -> ( ( F ` i ) + E ) e. RR )
165 164 3ad2antl1 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( ( F ` i ) + E ) e. RR )
166 19 3ad2antl1 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( B ` i ) e. RR )
167 120 119 resubcld 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> ( ( g ` i ) - ( F ` i ) ) e. RR )
168 167 3adantl3 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( ( g ` i ) - ( F ` i ) ) e. RR )
169 167 leabsd 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> ( ( g ` i ) - ( F ` i ) ) <_ ( abs ` ( ( g ` i ) - ( F ` i ) ) ) )
170 120 recnd 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> ( g ` i ) e. CC )
171 119 recnd 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> ( F ` i ) e. CC )
172 170 171 abssubd 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> ( abs ` ( ( g ` i ) - ( F ` i ) ) ) = ( abs ` ( ( F ` i ) - ( g ` i ) ) ) )
173 169 172 breqtrd 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> ( ( g ` i ) - ( F ` i ) ) <_ ( abs ` ( ( F ` i ) - ( g ` i ) ) ) )
174 167 133 128 173 154 letrd 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) ) /\ i e. X ) -> ( ( g ` i ) - ( F ` i ) ) <_ ( F D g ) )
175 174 3adantl3 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( ( g ` i ) - ( F ` i ) ) <_ ( F D g ) )
176 168 129 131 175 157 lelttrd 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( ( g ` i ) - ( F ` i ) ) < E )
177 119 3adantl3 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( F ` i ) e. RR )
178 90 177 131 ltsubadd2d 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( ( ( g ` i ) - ( F ` i ) ) < E <-> ( g ` i ) < ( ( F ` i ) + E ) ) )
179 176 178 mpbid 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( g ` i ) < ( ( F ` i ) + E ) )
180 min1 
 |-  ( ( ( ( B ` i ) - ( F ` i ) ) e. RR /\ ( ( F ` i ) - ( A ` i ) ) e. RR ) -> if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) <_ ( ( B ` i ) - ( F ` i ) ) )
181 25 34 180 syl2anc 
 |-  ( ( ph /\ i e. X ) -> if ( ( ( B ` i ) - ( F ` i ) ) <_ ( ( F ` i ) - ( A ` i ) ) , ( ( B ` i ) - ( F ` i ) ) , ( ( F ` i ) - ( A ` i ) ) ) <_ ( ( B ` i ) - ( F ` i ) ) )
182 93 96 25 113 181 letrd 
 |-  ( ( ph /\ i e. X ) -> E <_ ( ( B ` i ) - ( F ` i ) ) )
183 24 93 19 leaddsub2d 
 |-  ( ( ph /\ i e. X ) -> ( ( ( F ` i ) + E ) <_ ( B ` i ) <-> E <_ ( ( B ` i ) - ( F ` i ) ) ) )
184 182 183 mpbird 
 |-  ( ( ph /\ i e. X ) -> ( ( F ` i ) + E ) <_ ( B ` i ) )
185 184 3ad2antl1 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( ( F ` i ) + E ) <_ ( B ` i ) )
186 90 165 166 179 185 ltletrd 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( g ` i ) < ( B ` i ) )
187 82 83 90 163 186 eliood 
 |-  ( ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) /\ i e. X ) -> ( g ` i ) e. ( ( A ` i ) (,) ( B ` i ) ) )
188 187 ralrimiva 
 |-  ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) -> A. i e. X ( g ` i ) e. ( ( A ` i ) (,) ( B ` i ) ) )
189 81 188 jca 
 |-  ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) -> ( g Fn X /\ A. i e. X ( g ` i ) e. ( ( A ` i ) (,) ( B ` i ) ) ) )
190 vex 
 |-  g e. _V
191 190 elixp 
 |-  ( g e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) <-> ( g Fn X /\ A. i e. X ( g ` i ) e. ( ( A ` i ) (,) ( B ` i ) ) ) )
192 189 191 sylibr 
 |-  ( ( ph /\ g e. ( RR ^m X ) /\ ( F D g ) < E ) -> g e. X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) )
193 79 74 17 61 192 ballss3 
 |-  ( ph -> ( F ( ball ` D ) E ) C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) )
194 65 193 eqsstrd 
 |-  ( ph -> V C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) )
195 78 194 jca 
 |-  ( ph -> ( F e. V /\ V C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) )
196 eleq2 
 |-  ( v = V -> ( F e. v <-> F e. V ) )
197 sseq1 
 |-  ( v = V -> ( v C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) <-> V C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) )
198 196 197 anbi12d 
 |-  ( v = V -> ( ( F e. v /\ v C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) <-> ( F e. V /\ V C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) ) )
199 198 rspcev 
 |-  ( ( V e. ( TopOpen ` ( RR^ ` X ) ) /\ ( F e. V /\ V C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) ) -> E. v e. ( TopOpen ` ( RR^ ` X ) ) ( F e. v /\ v C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) )
200 72 195 199 syl2anc 
 |-  ( ph -> E. v e. ( TopOpen ` ( RR^ ` X ) ) ( F e. v /\ v C_ X_ i e. X ( ( A ` i ) (,) ( B ` i ) ) ) )