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	$⊢ φ \to X \in Fin$
	ioorrnopnlem.n	$⊢ φ \to X \neq \emptyset$
	ioorrnopnlem.a	$⊢ φ \to A : X ⟶ ℝ$
	ioorrnopnlem.b	$⊢ φ \to B : X ⟶ ℝ$
	ioorrnopnlem.f	$⊢ φ \to F \in \underset{i \in X}{⨉} (A (i), B (i))$
	ioorrnopnlem.h	$⊢ H = ran (i \in X ⟼ if (B (i) - F (i) \leq F (i) - A (i), B (i) - F (i), F (i) - A (i)))$
	ioorrnopnlem.e	$⊢ E = sup (H ℝ <)$
	ioorrnopnlem.v	$⊢ V = F ball (D) E$
	ioorrnopnlem.d	$⊢ D = (f \in (ℝ^{X}), g \in (ℝ^{X}) ⟼ \sqrt{\sum_{k \in X} {(f (k) - g (k))}^{2}})$
Assertion	ioorrnopnlem	$⊢ φ \to \exists v \in TopOpen (X) (F \in v \land v \subseteq \underset{i \in X}{⨉} (A (i), B (i)))$

Proof

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

Metamath Proof Explorer

Theorem ioorrnopnlem

Proof