ubthlem1

Description: Lemma for ubth . The function A exhibits a countable collection of sets that are closed, being the inverse image under t of the closed ball of radius k , and by assumption they cover X . Thus, by the Baire Category theorem bcth2 , for some n the set An has an interior, meaning that there is a closed ball { z e. X | ( y D z ) <_ r } in the set. (Contributed by Mario Carneiro, 11-Jan-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ubth.1	$⊢ X = BaseSet (U)$
	ubth.2	$⊢ N = {norm}_{CV} (W)$
	ubthlem.3	$⊢ D = IndMet (U)$
	ubthlem.4	$⊢ J = MetOpen (D)$
	ubthlem.5	$⊢ U \in CBan$
	ubthlem.6	$⊢ W \in NrmCVec$
	ubthlem.7	$⊢ φ \to T \subseteq U BLnOp W$
	ubthlem.8	$⊢ φ \to \forall x \in X \exists c \in ℝ \forall t \in T N (t (x)) \leq c$
	ubthlem.9	$⊢ A = (k \in ℕ ⟼ \{z \in X \| \forall t \in T N (t (z)) \leq k\})$
Assertion	ubthlem1	$⊢ φ \to \exists n \in ℕ \exists y \in X \exists r \in ℝ^{+} \{z \in X \| y D z \leq r\} \subseteq A (n)$

Proof

Step	Hyp	Ref	Expression
1		ubth.1	$⊢ X = BaseSet (U)$
2		ubth.2	$⊢ N = {norm}_{CV} (W)$
3		ubthlem.3	$⊢ D = IndMet (U)$
4		ubthlem.4	$⊢ J = MetOpen (D)$
5		ubthlem.5	$⊢ U \in CBan$
6		ubthlem.6	$⊢ W \in NrmCVec$
7		ubthlem.7	$⊢ φ \to T \subseteq U BLnOp W$
8		ubthlem.8	$⊢ φ \to \forall x \in X \exists c \in ℝ \forall t \in T N (t (x)) \leq c$
9		ubthlem.9	$⊢ A = (k \in ℕ ⟼ \{z \in X \| \forall t \in T N (t (z)) \leq k\})$
10		rzal	$⊢ T = \emptyset \to \forall t \in T N (t (z)) \leq k$
11	10	ralrimivw	$⊢ T = \emptyset \to \forall z \in X \forall t \in T N (t (z)) \leq k$
12		rabid2	$⊢ X = \{z \in X \| \forall t \in T N (t (z)) \leq k\} \leftrightarrow \forall z \in X \forall t \in T N (t (z)) \leq k$
13	11 12	sylibr	$⊢ T = \emptyset \to X = \{z \in X \| \forall t \in T N (t (z)) \leq k\}$
14	13	eqcomd	$⊢ T = \emptyset \to \{z \in X \| \forall t \in T N (t (z)) \leq k\} = X$
15	14	eleq1d	$⊢ T = \emptyset \to (\{z \in X \| \forall t \in T N (t (z)) \leq k\} \in Clsd (J) \leftrightarrow X \in Clsd (J))$
16		iinrab	$⊢ T \neq \emptyset \to ⋂_{t \in T} \{z \in X \| N (t (z)) \leq k\} = \{z \in X \| \forall t \in T N (t (z)) \leq k\}$
17	16	adantl	$⊢ ((φ \land k \in ℕ) \land T \neq \emptyset) \to ⋂_{t \in T} \{z \in X \| N (t (z)) \leq k\} = \{z \in X \| \forall t \in T N (t (z)) \leq k\}$
18		id	$⊢ T \neq \emptyset \to T \neq \emptyset$
19	7	sselda	$⊢ (φ \land t \in T) \to t \in (U BLnOp W)$
20		eqid	$⊢ IndMet (W) = IndMet (W)$
21		eqid	$⊢ MetOpen (IndMet (W)) = MetOpen (IndMet (W))$
22		eqid	$⊢ U BLnOp W = U BLnOp W$
23		bnnv	$⊢ U \in CBan \to U \in NrmCVec$
24	5 23	ax-mp	$⊢ U \in NrmCVec$
25	3 20 4 21 22 24 6	blocn2	$⊢ t \in (U BLnOp W) \to t \in (J Cn MetOpen (IndMet (W)))$
26	1 3	cbncms	$⊢ U \in CBan \to D \in CMet (X)$
27	5 26	ax-mp	$⊢ D \in CMet (X)$
28		cmetmet	$⊢ D \in CMet (X) \to D \in Met (X)$
29		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
30	27 28 29	mp2b	$⊢ D \in ∞Met (X)$
31	4	mopntopon	$⊢ D \in ∞Met (X) \to J \in TopOn (X)$
32	30 31	ax-mp	$⊢ J \in TopOn (X)$
33		eqid	$⊢ BaseSet (W) = BaseSet (W)$
34	33 20	imsxmet	$⊢ W \in NrmCVec \to IndMet (W) \in ∞Met (BaseSet (W))$
35	6 34	ax-mp	$⊢ IndMet (W) \in ∞Met (BaseSet (W))$
36	21	mopntopon	$⊢ IndMet (W) \in ∞Met (BaseSet (W)) \to MetOpen (IndMet (W)) \in TopOn (BaseSet (W))$
37	35 36	ax-mp	$⊢ MetOpen (IndMet (W)) \in TopOn (BaseSet (W))$
38		iscncl	$⊢ (J \in TopOn (X) \land MetOpen (IndMet (W)) \in TopOn (BaseSet (W))) \to (t \in (J Cn MetOpen (IndMet (W))) \leftrightarrow (t : X ⟶ BaseSet (W) \land \forall x \in Clsd (MetOpen (IndMet (W))) t^{-1} [x] \in Clsd (J)))$
39	32 37 38	mp2an	$⊢ t \in (J Cn MetOpen (IndMet (W))) \leftrightarrow (t : X ⟶ BaseSet (W) \land \forall x \in Clsd (MetOpen (IndMet (W))) t^{-1} [x] \in Clsd (J))$
40	25 39	sylib	$⊢ t \in (U BLnOp W) \to (t : X ⟶ BaseSet (W) \land \forall x \in Clsd (MetOpen (IndMet (W))) t^{-1} [x] \in Clsd (J))$
41	19 40	syl	$⊢ (φ \land t \in T) \to (t : X ⟶ BaseSet (W) \land \forall x \in Clsd (MetOpen (IndMet (W))) t^{-1} [x] \in Clsd (J))$
42	41	simpld	$⊢ (φ \land t \in T) \to t : X ⟶ BaseSet (W)$
43	42	adantlr	$⊢ ((φ \land k \in ℕ) \land t \in T) \to t : X ⟶ BaseSet (W)$
44	43	ffvelrnda	$⊢ (((φ \land k \in ℕ) \land t \in T) \land x \in X) \to t (x) \in BaseSet (W)$
45	44	biantrurd	$⊢ (((φ \land k \in ℕ) \land t \in T) \land x \in X) \to (N (t (x)) \leq k \leftrightarrow (t (x) \in BaseSet (W) \land N (t (x)) \leq k))$
46		fveq2	$⊢ y = t (x) \to N (y) = N (t (x))$
47	46	breq1d	$⊢ y = t (x) \to (N (y) \leq k \leftrightarrow N (t (x)) \leq k)$
48	47	elrab	$⊢ t (x) \in \{y \in BaseSet (W) \| N (y) \leq k\} \leftrightarrow (t (x) \in BaseSet (W) \land N (t (x)) \leq k)$
49	45 48	bitr4di	$⊢ (((φ \land k \in ℕ) \land t \in T) \land x \in X) \to (N (t (x)) \leq k \leftrightarrow t (x) \in \{y \in BaseSet (W) \| N (y) \leq k\})$
50	49	pm5.32da	$⊢ ((φ \land k \in ℕ) \land t \in T) \to ((x \in X \land N (t (x)) \leq k) \leftrightarrow (x \in X \land t (x) \in \{y \in BaseSet (W) \| N (y) \leq k\}))$
51		2fveq3	$⊢ z = x \to N (t (z)) = N (t (x))$
52	51	breq1d	$⊢ z = x \to (N (t (z)) \leq k \leftrightarrow N (t (x)) \leq k)$
53	52	elrab	$⊢ x \in \{z \in X \| N (t (z)) \leq k\} \leftrightarrow (x \in X \land N (t (x)) \leq k)$
54	53	a1i	$⊢ ((φ \land k \in ℕ) \land t \in T) \to (x \in \{z \in X \| N (t (z)) \leq k\} \leftrightarrow (x \in X \land N (t (x)) \leq k))$
55		ffn	$⊢ t : X ⟶ BaseSet (W) \to t Fn X$
56		elpreima	$⊢ t Fn X \to (x \in t^{-1} [\{y \in BaseSet (W) \| N (y) \leq k\}] \leftrightarrow (x \in X \land t (x) \in \{y \in BaseSet (W) \| N (y) \leq k\}))$
57	43 55 56	3syl	$⊢ ((φ \land k \in ℕ) \land t \in T) \to (x \in t^{-1} [\{y \in BaseSet (W) \| N (y) \leq k\}] \leftrightarrow (x \in X \land t (x) \in \{y \in BaseSet (W) \| N (y) \leq k\}))$
58	50 54 57	3bitr4d	$⊢ ((φ \land k \in ℕ) \land t \in T) \to (x \in \{z \in X \| N (t (z)) \leq k\} \leftrightarrow x \in t^{-1} [\{y \in BaseSet (W) \| N (y) \leq k\}])$
59	58	eqrdv	$⊢ ((φ \land k \in ℕ) \land t \in T) \to \{z \in X \| N (t (z)) \leq k\} = t^{-1} [\{y \in BaseSet (W) \| N (y) \leq k\}]$
60		imaeq2	$⊢ x = \{y \in BaseSet (W) \| N (y) \leq k\} \to t^{-1} [x] = t^{-1} [\{y \in BaseSet (W) \| N (y) \leq k\}]$
61	60	eleq1d	$⊢ x = \{y \in BaseSet (W) \| N (y) \leq k\} \to (t^{-1} [x] \in Clsd (J) \leftrightarrow t^{-1} [\{y \in BaseSet (W) \| N (y) \leq k\}] \in Clsd (J))$
62	41	simprd	$⊢ (φ \land t \in T) \to \forall x \in Clsd (MetOpen (IndMet (W))) t^{-1} [x] \in Clsd (J)$
63	62	adantlr	$⊢ ((φ \land k \in ℕ) \land t \in T) \to \forall x \in Clsd (MetOpen (IndMet (W))) t^{-1} [x] \in Clsd (J)$
64		nnre	$⊢ k \in ℕ \to k \in ℝ$
65	64	ad2antlr	$⊢ ((φ \land k \in ℕ) \land t \in T) \to k \in ℝ$
66	65	rexrd	$⊢ ((φ \land k \in ℕ) \land t \in T) \to k \in ℝ^{*}$
67		eqid	$⊢ 0_{vec} (W) = 0_{vec} (W)$
68	33 67	nvzcl	$⊢ W \in NrmCVec \to 0_{vec} (W) \in BaseSet (W)$
69	6 68	ax-mp	$⊢ 0_{vec} (W) \in BaseSet (W)$
70	33 67 2 20	nvnd	$⊢ (W \in NrmCVec \land y \in BaseSet (W)) \to N (y) = y IndMet (W) 0_{vec} (W)$
71	6 70	mpan	$⊢ y \in BaseSet (W) \to N (y) = y IndMet (W) 0_{vec} (W)$
72		xmetsym	$⊢ (IndMet (W) \in ∞Met (BaseSet (W)) \land 0_{vec} (W) \in BaseSet (W) \land y \in BaseSet (W)) \to 0_{vec} (W) IndMet (W) y = y IndMet (W) 0_{vec} (W)$
73	35 69 72	mp3an12	$⊢ y \in BaseSet (W) \to 0_{vec} (W) IndMet (W) y = y IndMet (W) 0_{vec} (W)$
74	71 73	eqtr4d	$⊢ y \in BaseSet (W) \to N (y) = 0_{vec} (W) IndMet (W) y$
75	74	breq1d	$⊢ y \in BaseSet (W) \to (N (y) \leq k \leftrightarrow 0_{vec} (W) IndMet (W) y \leq k)$
76	75	rabbiia	$⊢ \{y \in BaseSet (W) \| N (y) \leq k\} = \{y \in BaseSet (W) \| 0_{vec} (W) IndMet (W) y \leq k\}$
77	21 76	blcld	$⊢ (IndMet (W) \in ∞Met (BaseSet (W)) \land 0_{vec} (W) \in BaseSet (W) \land k \in ℝ^{*}) \to \{y \in BaseSet (W) \| N (y) \leq k\} \in Clsd (MetOpen (IndMet (W)))$
78	35 69 77	mp3an12	$⊢ k \in ℝ^{*} \to \{y \in BaseSet (W) \| N (y) \leq k\} \in Clsd (MetOpen (IndMet (W)))$
79	66 78	syl	$⊢ ((φ \land k \in ℕ) \land t \in T) \to \{y \in BaseSet (W) \| N (y) \leq k\} \in Clsd (MetOpen (IndMet (W)))$
80	61 63 79	rspcdva	$⊢ ((φ \land k \in ℕ) \land t \in T) \to t^{-1} [\{y \in BaseSet (W) \| N (y) \leq k\}] \in Clsd (J)$
81	59 80	eqeltrd	$⊢ ((φ \land k \in ℕ) \land t \in T) \to \{z \in X \| N (t (z)) \leq k\} \in Clsd (J)$
82	81	ralrimiva	$⊢ (φ \land k \in ℕ) \to \forall t \in T \{z \in X \| N (t (z)) \leq k\} \in Clsd (J)$
83		iincld	$⊢ (T \neq \emptyset \land \forall t \in T \{z \in X \| N (t (z)) \leq k\} \in Clsd (J)) \to ⋂_{t \in T} \{z \in X \| N (t (z)) \leq k\} \in Clsd (J)$
84	18 82 83	syl2anr	$⊢ ((φ \land k \in ℕ) \land T \neq \emptyset) \to ⋂_{t \in T} \{z \in X \| N (t (z)) \leq k\} \in Clsd (J)$
85	17 84	eqeltrrd	$⊢ ((φ \land k \in ℕ) \land T \neq \emptyset) \to \{z \in X \| \forall t \in T N (t (z)) \leq k\} \in Clsd (J)$
86	4	mopntop	$⊢ D \in ∞Met (X) \to J \in Top$
87	30 86	ax-mp	$⊢ J \in Top$
88	32	toponunii	$⊢ X = ⋃ J$
89	88	topcld	$⊢ J \in Top \to X \in Clsd (J)$
90	87 89	ax-mp	$⊢ X \in Clsd (J)$
91	90	a1i	$⊢ (φ \land k \in ℕ) \to X \in Clsd (J)$
92	15 85 91	pm2.61ne	$⊢ (φ \land k \in ℕ) \to \{z \in X \| \forall t \in T N (t (z)) \leq k\} \in Clsd (J)$
93	92 9	fmptd	$⊢ φ \to A : ℕ ⟶ Clsd (J)$
94	93	frnd	$⊢ φ \to ran A \subseteq Clsd (J)$
95	88	cldss2	$⊢ Clsd (J) \subseteq 𝒫 X$
96	94 95	sstrdi	$⊢ φ \to ran A \subseteq 𝒫 X$
97		sspwuni	$⊢ ran A \subseteq 𝒫 X \leftrightarrow ⋃ ran A \subseteq X$
98	96 97	sylib	$⊢ φ \to ⋃ ran A \subseteq X$
99		arch	$⊢ c \in ℝ \to \exists k \in ℕ c < k$
100	99	adantl	$⊢ ((φ \land x \in X) \land c \in ℝ) \to \exists k \in ℕ c < k$
101		simpr	$⊢ ((φ \land x \in X) \land c \in ℝ) \to c \in ℝ$
102		ltle	$⊢ (c \in ℝ \land k \in ℝ) \to (c < k \to c \leq k)$
103	101 64 102	syl2an	$⊢ (((φ \land x \in X) \land c \in ℝ) \land k \in ℕ) \to (c < k \to c \leq k)$
104	103	impr	$⊢ (((φ \land x \in X) \land c \in ℝ) \land (k \in ℕ \land c < k)) \to c \leq k$
105	104	adantr	$⊢ ((((φ \land x \in X) \land c \in ℝ) \land (k \in ℕ \land c < k)) \land t \in T) \to c \leq k$
106	42	ffvelrnda	$⊢ ((φ \land t \in T) \land x \in X) \to t (x) \in BaseSet (W)$
107	106	an32s	$⊢ ((φ \land x \in X) \land t \in T) \to t (x) \in BaseSet (W)$
108	33 2	nvcl	$⊢ (W \in NrmCVec \land t (x) \in BaseSet (W)) \to N (t (x)) \in ℝ$
109	6 107 108	sylancr	$⊢ ((φ \land x \in X) \land t \in T) \to N (t (x)) \in ℝ$
110	109	adantlr	$⊢ (((φ \land x \in X) \land c \in ℝ) \land t \in T) \to N (t (x)) \in ℝ$
111	110	adantlr	$⊢ ((((φ \land x \in X) \land c \in ℝ) \land (k \in ℕ \land c < k)) \land t \in T) \to N (t (x)) \in ℝ$
112		simpllr	$⊢ ((((φ \land x \in X) \land c \in ℝ) \land (k \in ℕ \land c < k)) \land t \in T) \to c \in ℝ$
113		simplrl	$⊢ ((((φ \land x \in X) \land c \in ℝ) \land (k \in ℕ \land c < k)) \land t \in T) \to k \in ℕ$
114	113 64	syl	$⊢ ((((φ \land x \in X) \land c \in ℝ) \land (k \in ℕ \land c < k)) \land t \in T) \to k \in ℝ$
115		letr	$⊢ (N (t (x)) \in ℝ \land c \in ℝ \land k \in ℝ) \to ((N (t (x)) \leq c \land c \leq k) \to N (t (x)) \leq k)$
116	111 112 114 115	syl3anc	$⊢ ((((φ \land x \in X) \land c \in ℝ) \land (k \in ℕ \land c < k)) \land t \in T) \to ((N (t (x)) \leq c \land c \leq k) \to N (t (x)) \leq k)$
117	105 116	mpan2d	$⊢ ((((φ \land x \in X) \land c \in ℝ) \land (k \in ℕ \land c < k)) \land t \in T) \to (N (t (x)) \leq c \to N (t (x)) \leq k)$
118	117	ralimdva	$⊢ (((φ \land x \in X) \land c \in ℝ) \land (k \in ℕ \land c < k)) \to (\forall t \in T N (t (x)) \leq c \to \forall t \in T N (t (x)) \leq k)$
119	118	expr	$⊢ (((φ \land x \in X) \land c \in ℝ) \land k \in ℕ) \to (c < k \to (\forall t \in T N (t (x)) \leq c \to \forall t \in T N (t (x)) \leq k))$
120	1	fvexi	$⊢ X \in V$
121	120	rabex	$⊢ \{z \in X \| \forall t \in T N (t (z)) \leq k\} \in V$
122	9	fvmpt2	$⊢ (k \in ℕ \land \{z \in X \| \forall t \in T N (t (z)) \leq k\} \in V) \to A (k) = \{z \in X \| \forall t \in T N (t (z)) \leq k\}$
123	121 122	mpan2	$⊢ k \in ℕ \to A (k) = \{z \in X \| \forall t \in T N (t (z)) \leq k\}$
124	123	eleq2d	$⊢ k \in ℕ \to (x \in A (k) \leftrightarrow x \in \{z \in X \| \forall t \in T N (t (z)) \leq k\})$
125	52	ralbidv	$⊢ z = x \to (\forall t \in T N (t (z)) \leq k \leftrightarrow \forall t \in T N (t (x)) \leq k)$
126	125	elrab	$⊢ x \in \{z \in X \| \forall t \in T N (t (z)) \leq k\} \leftrightarrow (x \in X \land \forall t \in T N (t (x)) \leq k)$
127	124 126	bitrdi	$⊢ k \in ℕ \to (x \in A (k) \leftrightarrow (x \in X \land \forall t \in T N (t (x)) \leq k))$
128		simpr	$⊢ (φ \land x \in X) \to x \in X$
129	128	biantrurd	$⊢ (φ \land x \in X) \to (\forall t \in T N (t (x)) \leq k \leftrightarrow (x \in X \land \forall t \in T N (t (x)) \leq k))$
130	129	bicomd	$⊢ (φ \land x \in X) \to ((x \in X \land \forall t \in T N (t (x)) \leq k) \leftrightarrow \forall t \in T N (t (x)) \leq k)$
131	127 130	sylan9bbr	$⊢ ((φ \land x \in X) \land k \in ℕ) \to (x \in A (k) \leftrightarrow \forall t \in T N (t (x)) \leq k)$
132	93	ffnd	$⊢ φ \to A Fn ℕ$
133	132	adantr	$⊢ (φ \land x \in X) \to A Fn ℕ$
134		fnfvelrn	$⊢ (A Fn ℕ \land k \in ℕ) \to A (k) \in ran A$
135		elssuni	$⊢ A (k) \in ran A \to A (k) \subseteq ⋃ ran A$
136	134 135	syl	$⊢ (A Fn ℕ \land k \in ℕ) \to A (k) \subseteq ⋃ ran A$
137	136	sseld	$⊢ (A Fn ℕ \land k \in ℕ) \to (x \in A (k) \to x \in ⋃ ran A)$
138	133 137	sylan	$⊢ ((φ \land x \in X) \land k \in ℕ) \to (x \in A (k) \to x \in ⋃ ran A)$
139	131 138	sylbird	$⊢ ((φ \land x \in X) \land k \in ℕ) \to (\forall t \in T N (t (x)) \leq k \to x \in ⋃ ran A)$
140	139	adantlr	$⊢ (((φ \land x \in X) \land c \in ℝ) \land k \in ℕ) \to (\forall t \in T N (t (x)) \leq k \to x \in ⋃ ran A)$
141	119 140	syl6d	$⊢ (((φ \land x \in X) \land c \in ℝ) \land k \in ℕ) \to (c < k \to (\forall t \in T N (t (x)) \leq c \to x \in ⋃ ran A))$
142	141	rexlimdva	$⊢ ((φ \land x \in X) \land c \in ℝ) \to (\exists k \in ℕ c < k \to (\forall t \in T N (t (x)) \leq c \to x \in ⋃ ran A))$
143	100 142	mpd	$⊢ ((φ \land x \in X) \land c \in ℝ) \to (\forall t \in T N (t (x)) \leq c \to x \in ⋃ ran A)$
144	143	rexlimdva	$⊢ (φ \land x \in X) \to (\exists c \in ℝ \forall t \in T N (t (x)) \leq c \to x \in ⋃ ran A)$
145	144	ralimdva	$⊢ φ \to (\forall x \in X \exists c \in ℝ \forall t \in T N (t (x)) \leq c \to \forall x \in X x \in ⋃ ran A)$
146	8 145	mpd	$⊢ φ \to \forall x \in X x \in ⋃ ran A$
147		dfss3	$⊢ X \subseteq ⋃ ran A \leftrightarrow \forall x \in X x \in ⋃ ran A$
148	146 147	sylibr	$⊢ φ \to X \subseteq ⋃ ran A$
149	98 148	eqssd	$⊢ φ \to ⋃ ran A = X$
150		eqid	$⊢ 0_{vec} (U) = 0_{vec} (U)$
151	1 150	nvzcl	$⊢ U \in NrmCVec \to 0_{vec} (U) \in X$
152		ne0i	$⊢ 0_{vec} (U) \in X \to X \neq \emptyset$
153	24 151 152	mp2b	$⊢ X \neq \emptyset$
154	4	bcth2	$⊢ ((D \in CMet (X) \land X \neq \emptyset) \land (A : ℕ ⟶ Clsd (J) \land ⋃ ran A = X)) \to \exists n \in ℕ int (J) (A (n)) \neq \emptyset$
155	27 153 154	mpanl12	$⊢ (A : ℕ ⟶ Clsd (J) \land ⋃ ran A = X) \to \exists n \in ℕ int (J) (A (n)) \neq \emptyset$
156	93 149 155	syl2anc	$⊢ φ \to \exists n \in ℕ int (J) (A (n)) \neq \emptyset$
157		ffvelrn	$⊢ (A : ℕ ⟶ Clsd (J) \land n \in ℕ) \to A (n) \in Clsd (J)$
158	95 157	sseldi	$⊢ (A : ℕ ⟶ Clsd (J) \land n \in ℕ) \to A (n) \in 𝒫 X$
159	158	elpwid	$⊢ (A : ℕ ⟶ Clsd (J) \land n \in ℕ) \to A (n) \subseteq X$
160	93 159	sylan	$⊢ (φ \land n \in ℕ) \to A (n) \subseteq X$
161	88	ntrss3	$⊢ (J \in Top \land A (n) \subseteq X) \to int (J) (A (n)) \subseteq X$
162	87 160 161	sylancr	$⊢ (φ \land n \in ℕ) \to int (J) (A (n)) \subseteq X$
163	162	sseld	$⊢ (φ \land n \in ℕ) \to (y \in int (J) (A (n)) \to y \in X)$
164	88	ntropn	$⊢ (J \in Top \land A (n) \subseteq X) \to int (J) (A (n)) \in J$
165	87 160 164	sylancr	$⊢ (φ \land n \in ℕ) \to int (J) (A (n)) \in J$
166	4	mopni2	$⊢ (D \in ∞Met (X) \land int (J) (A (n)) \in J \land y \in int (J) (A (n))) \to \exists x \in ℝ^{+} y ball (D) x \subseteq int (J) (A (n))$
167	30 166	mp3an1	$⊢ (int (J) (A (n)) \in J \land y \in int (J) (A (n))) \to \exists x \in ℝ^{+} y ball (D) x \subseteq int (J) (A (n))$
168	165 167	sylan	$⊢ ((φ \land n \in ℕ) \land y \in int (J) (A (n))) \to \exists x \in ℝ^{+} y ball (D) x \subseteq int (J) (A (n))$
169		elssuni	$⊢ int (J) (A (n)) \in J \to int (J) (A (n)) \subseteq ⋃ J$
170	169 88	sseqtrrdi	$⊢ int (J) (A (n)) \in J \to int (J) (A (n)) \subseteq X$
171	165 170	syl	$⊢ (φ \land n \in ℕ) \to int (J) (A (n)) \subseteq X$
172	171	sselda	$⊢ ((φ \land n \in ℕ) \land y \in int (J) (A (n))) \to y \in X$
173	88	ntrss2	$⊢ (J \in Top \land A (n) \subseteq X) \to int (J) (A (n)) \subseteq A (n)$
174	87 160 173	sylancr	$⊢ (φ \land n \in ℕ) \to int (J) (A (n)) \subseteq A (n)$
175		sstr2	$⊢ y ball (D) x \subseteq int (J) (A (n)) \to (int (J) (A (n)) \subseteq A (n) \to y ball (D) x \subseteq A (n))$
176	174 175	syl5com	$⊢ (φ \land n \in ℕ) \to (y ball (D) x \subseteq int (J) (A (n)) \to y ball (D) x \subseteq A (n))$
177	176	ad2antrr	$⊢ (((φ \land n \in ℕ) \land y \in X) \land x \in ℝ^{+}) \to (y ball (D) x \subseteq int (J) (A (n)) \to y ball (D) x \subseteq A (n))$
178		simpr	$⊢ ((φ \land n \in ℕ) \land y \in X) \to y \in X$
179	178 30	jctil	$⊢ ((φ \land n \in ℕ) \land y \in X) \to (D \in ∞Met (X) \land y \in X)$
180		rphalfcl	$⊢ x \in ℝ^{+} \to \frac{x}{2} \in ℝ^{+}$
181	180	rpxrd	$⊢ x \in ℝ^{+} \to \frac{x}{2} \in ℝ^{*}$
182		rpxr	$⊢ x \in ℝ^{+} \to x \in ℝ^{*}$
183		rphalflt	$⊢ x \in ℝ^{+} \to \frac{x}{2} < x$
184	181 182 183	3jca	$⊢ x \in ℝ^{+} \to (\frac{x}{2} \in ℝ^{} \land x \in ℝ^{} \land \frac{x}{2} < x)$
185		eqid	$⊢ \{z \in X \| y D z \leq \frac{x}{2}\} = \{z \in X \| y D z \leq \frac{x}{2}\}$
186	4 185	blsscls2	$⊢ ((D \in ∞Met (X) \land y \in X) \land (\frac{x}{2} \in ℝ^{} \land x \in ℝ^{} \land \frac{x}{2} < x)) \to \{z \in X \| y D z \leq \frac{x}{2}\} \subseteq y ball (D) x$
187	179 184 186	syl2an	$⊢ (((φ \land n \in ℕ) \land y \in X) \land x \in ℝ^{+}) \to \{z \in X \| y D z \leq \frac{x}{2}\} \subseteq y ball (D) x$
188		sstr2	$⊢ \{z \in X \| y D z \leq \frac{x}{2}\} \subseteq y ball (D) x \to (y ball (D) x \subseteq A (n) \to \{z \in X \| y D z \leq \frac{x}{2}\} \subseteq A (n))$
189	187 188	syl	$⊢ (((φ \land n \in ℕ) \land y \in X) \land x \in ℝ^{+}) \to (y ball (D) x \subseteq A (n) \to \{z \in X \| y D z \leq \frac{x}{2}\} \subseteq A (n))$
190	180	adantl	$⊢ (((φ \land n \in ℕ) \land y \in X) \land x \in ℝ^{+}) \to \frac{x}{2} \in ℝ^{+}$
191		breq2	$⊢ r = \frac{x}{2} \to (y D z \leq r \leftrightarrow y D z \leq \frac{x}{2})$
192	191	rabbidv	$⊢ r = \frac{x}{2} \to \{z \in X \| y D z \leq r\} = \{z \in X \| y D z \leq \frac{x}{2}\}$
193	192	sseq1d	$⊢ r = \frac{x}{2} \to (\{z \in X \| y D z \leq r\} \subseteq A (n) \leftrightarrow \{z \in X \| y D z \leq \frac{x}{2}\} \subseteq A (n))$
194	193	rspcev	$⊢ (\frac{x}{2} \in ℝ^{+} \land \{z \in X \| y D z \leq \frac{x}{2}\} \subseteq A (n)) \to \exists r \in ℝ^{+} \{z \in X \| y D z \leq r\} \subseteq A (n)$
195	194	ex	$⊢ \frac{x}{2} \in ℝ^{+} \to (\{z \in X \| y D z \leq \frac{x}{2}\} \subseteq A (n) \to \exists r \in ℝ^{+} \{z \in X \| y D z \leq r\} \subseteq A (n))$
196	190 195	syl	$⊢ (((φ \land n \in ℕ) \land y \in X) \land x \in ℝ^{+}) \to (\{z \in X \| y D z \leq \frac{x}{2}\} \subseteq A (n) \to \exists r \in ℝ^{+} \{z \in X \| y D z \leq r\} \subseteq A (n))$
197	177 189 196	3syld	$⊢ (((φ \land n \in ℕ) \land y \in X) \land x \in ℝ^{+}) \to (y ball (D) x \subseteq int (J) (A (n)) \to \exists r \in ℝ^{+} \{z \in X \| y D z \leq r\} \subseteq A (n))$
198	197	rexlimdva	$⊢ ((φ \land n \in ℕ) \land y \in X) \to (\exists x \in ℝ^{+} y ball (D) x \subseteq int (J) (A (n)) \to \exists r \in ℝ^{+} \{z \in X \| y D z \leq r\} \subseteq A (n))$
199	172 198	syldan	$⊢ ((φ \land n \in ℕ) \land y \in int (J) (A (n))) \to (\exists x \in ℝ^{+} y ball (D) x \subseteq int (J) (A (n)) \to \exists r \in ℝ^{+} \{z \in X \| y D z \leq r\} \subseteq A (n))$
200	168 199	mpd	$⊢ ((φ \land n \in ℕ) \land y \in int (J) (A (n))) \to \exists r \in ℝ^{+} \{z \in X \| y D z \leq r\} \subseteq A (n)$
201	200	ex	$⊢ (φ \land n \in ℕ) \to (y \in int (J) (A (n)) \to \exists r \in ℝ^{+} \{z \in X \| y D z \leq r\} \subseteq A (n))$
202	163 201	jcad	$⊢ (φ \land n \in ℕ) \to (y \in int (J) (A (n)) \to (y \in X \land \exists r \in ℝ^{+} \{z \in X \| y D z \leq r\} \subseteq A (n)))$
203	202	eximdv	$⊢ (φ \land n \in ℕ) \to (\exists y y \in int (J) (A (n)) \to \exists y (y \in X \land \exists r \in ℝ^{+} \{z \in X \| y D z \leq r\} \subseteq A (n)))$
204		n0	$⊢ int (J) (A (n)) \neq \emptyset \leftrightarrow \exists y y \in int (J) (A (n))$
205		df-rex	$⊢ \exists y \in X \exists r \in ℝ^{+} \{z \in X \| y D z \leq r\} \subseteq A (n) \leftrightarrow \exists y (y \in X \land \exists r \in ℝ^{+} \{z \in X \| y D z \leq r\} \subseteq A (n))$
206	203 204 205	3imtr4g	$⊢ (φ \land n \in ℕ) \to (int (J) (A (n)) \neq \emptyset \to \exists y \in X \exists r \in ℝ^{+} \{z \in X \| y D z \leq r\} \subseteq A (n))$
207	206	reximdva	$⊢ φ \to (\exists n \in ℕ int (J) (A (n)) \neq \emptyset \to \exists n \in ℕ \exists y \in X \exists r \in ℝ^{+} \{z \in X \| y D z \leq r\} \subseteq A (n))$
208	156 207	mpd	$⊢ φ \to \exists n \in ℕ \exists y \in X \exists r \in ℝ^{+} \{z \in X \| y D z \leq r\} \subseteq A (n)$

Metamath Proof Explorer

Theorem ubthlem1

Proof