Theorem metnrmlem2

Description: Lemma for metnrm . (Contributed by Mario Carneiro, 14-Jan-2014) (Revised by Mario Carneiro, 5-Sep-2015)

	Ref	Expression
Hypotheses	metdscn.f	$$⊢F=\left(x\in X⟼inf\left(\mathrm{ran}\left(y\in S⟼xDy\right),{ℝ}^{*},<\right)\right)$$
	metdscn.j	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
	metnrmlem.1	$$⊢\phi \to D\in \mathrm{\infty Met}\left(X\right)$$
	metnrmlem.2	$$⊢\phi \to S\in \mathrm{Clsd}\left(J\right)$$
	metnrmlem.3	$$⊢\phi \to T\in \mathrm{Clsd}\left(J\right)$$
	metnrmlem.4	$$⊢\phi \to S\cap T=\varnothing$$
	metnrmlem.u	$$⊢U=\bigcup _{t\in T}\left(t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\right)$$
Assertion	metnrmlem2	$$⊢\phi \to \left(U\in J\wedge T\subseteq U\right)$$

Proof

Step	Hyp	Ref	Expression
1		metdscn.f	$$⊢F=\left(x\in X⟼inf\left(\mathrm{ran}\left(y\in S⟼xDy\right),{ℝ}^{*},<\right)\right)$$
2		metdscn.j	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
3		metnrmlem.1	$$⊢\phi \to D\in \mathrm{\infty Met}\left(X\right)$$
4		metnrmlem.2	$$⊢\phi \to S\in \mathrm{Clsd}\left(J\right)$$
5		metnrmlem.3	$$⊢\phi \to T\in \mathrm{Clsd}\left(J\right)$$
6		metnrmlem.4	$$⊢\phi \to S\cap T=\varnothing$$
7		metnrmlem.u	$$⊢U=\bigcup _{t\in T}\left(t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\right)$$
8	2	mopntop	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to J\in \mathrm{Top}$$
9	3 8	syl	$$⊢\phi \to J\in \mathrm{Top}$$
10	3	adantr	$$⊢\left(\phi \wedge t\in T\right)\to D\in \mathrm{\infty Met}\left(X\right)$$
11		eqid	$$⊢\bigcup J=\bigcup J$$
12	11	cldss	$$⊢T\in \mathrm{Clsd}\left(J\right)\to T\subseteq \bigcup J$$
13	5 12	syl	$$⊢\phi \to T\subseteq \bigcup J$$
14	2	mopnuni	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to X=\bigcup J$$
15	3 14	syl	$$⊢\phi \to X=\bigcup J$$
16	13 15	sseqtrrd	$$⊢\phi \to T\subseteq X$$
17	16	sselda	$$⊢\left(\phi \wedge t\in T\right)\to t\in X$$
18	1 2 3 4 5 6	metnrmlem1a	$$⊢\left(\phi \wedge t\in T\right)\to \left(0<F\left(t\right)\wedge if\left(1\le F\left(t\right),1,F\left(t\right)\right)\in {ℝ}^{+}\right)$$
19	18	simprd	$$⊢\left(\phi \wedge t\in T\right)\to if\left(1\le F\left(t\right),1,F\left(t\right)\right)\in {ℝ}^{+}$$
20	19	rphalfcld	$$⊢\left(\phi \wedge t\in T\right)\to \frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\in {ℝ}^{+}$$
21	20	rpxrd	$$⊢\left(\phi \wedge t\in T\right)\to \frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\in {ℝ}^{*}$$
22	2	blopn	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge t\in X\wedge \frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\in {ℝ}^{*}\right)\to t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\in J$$
23	10 17 21 22	syl3anc	$$⊢\left(\phi \wedge t\in T\right)\to t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\in J$$
24	23	ralrimiva	$$⊢\phi \to \forall t\in Tt\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\in J$$
25		iunopn	$$⊢\left(J\in \mathrm{Top}\wedge \forall t\in Tt\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\in J\right)\to \bigcup _{t\in T}\left(t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\right)\in J$$
26	9 24 25	syl2anc	$$⊢\phi \to \bigcup _{t\in T}\left(t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\right)\in J$$
27	7 26	eqeltrid	$$⊢\phi \to U\in J$$
28		blcntr	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge t\in X\wedge \frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\in {ℝ}^{+}\right)\to t\in \left(t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\right)$$
29	10 17 20 28	syl3anc	$$⊢\left(\phi \wedge t\in T\right)\to t\in \left(t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\right)$$
30	29	snssd	$$⊢\left(\phi \wedge t\in T\right)\to \left\{t\right\}\subseteq t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)$$
31	30	ralrimiva	$$⊢\phi \to \forall t\in T\left\{t\right\}\subseteq t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)$$
32		ss2iun	$$⊢\forall t\in T\left\{t\right\}\subseteq t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\to \bigcup _{t\in T}\left\{t\right\}\subseteq \bigcup _{t\in T}\left(t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\right)$$
33	31 32	syl	$$⊢\phi \to \bigcup _{t\in T}\left\{t\right\}\subseteq \bigcup _{t\in T}\left(t\mathrm{ball}\left(D\right)\left(\frac{if\left(1\le F\left(t\right),1,F\left(t\right)\right)}{2}\right)\right)$$
34		iunid	$$⊢\bigcup _{t\in T}\left\{t\right\}=T$$
35	34	eqcomi	$$⊢T=\bigcup _{t\in T}\left\{t\right\}$$
36	33 35 7	3sstr4g	$$⊢\phi \to T\subseteq U$$
37	27 36	jca	$$⊢\phi \to \left(U\in J\wedge T\subseteq U\right)$$