Theorem ubthlem1 30957

Description: Lemma for ubth 30960. The function 𝐴 exhibits a countable collection of sets that are closed, being the inverse image under 𝑡 of the closed ball of radius 𝑘, and by assumption they cover 𝑋. Thus, by the Baire Category theorem bcth2 25298, for some 𝑛 the set 𝐴‘𝑛 has an interior, meaning that there is a closed ball {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} in the set. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.)

Hypotheses

Ref	Expression
ubth.1	⊢ 𝑋 = (BaseSet‘𝑈)
ubth.2	⊢ 𝑁 = (normCV‘𝑊)
ubthlem.3	⊢ 𝐷 = (IndMet‘𝑈)
ubthlem.4	⊢ 𝐽 = (MetOpen‘𝐷)
ubthlem.5	⊢ 𝑈 ∈ CBan
ubthlem.6	⊢ 𝑊 ∈ NrmCVec
ubthlem.7	⊢ (𝜑 → 𝑇 ⊆ (𝑈 BLnOp 𝑊))
ubthlem.8	⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐)
ubthlem.9	⊢ 𝐴 = (𝑘 ∈ ℕ ↦ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})

Assertion

Ref	Expression
ubthlem1	⊢ (𝜑 → ∃𝑛 ∈ ℕ ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))

Distinct variable groups:   𝑘,𝑐,𝑛,𝑟,𝑥,𝑦,𝑧,𝐴   𝑡,𝑐,𝐷,𝑘,𝑛,𝑟,𝑥,𝑧   𝑘,𝐽,𝑛   𝑦,𝑡,𝐽,𝑥   𝑁,𝑐,𝑘,𝑛,𝑟,𝑡,𝑥,𝑦,𝑧   𝜑,𝑐,𝑘,𝑛,𝑟,𝑡,𝑥,𝑦   𝑇,𝑐,𝑘,𝑛,𝑟,𝑡,𝑥,𝑦,𝑧   𝑈,𝑐,𝑛,𝑟,𝑡,𝑥,𝑦,𝑧   𝑊,𝑐,𝑛,𝑟,𝑡,𝑥,𝑦   𝑋,𝑐,𝑘,𝑛,𝑟,𝑡,𝑥,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑧)   𝐴(𝑡)   𝐷(𝑦)   𝑈(𝑘)   𝐽(𝑧,𝑟,𝑐)   𝑊(𝑧,𝑘)

Proof of Theorem ubthlem1

Step	Hyp	Ref	Expression
1		rzal 4449	. . . . . . . . 9 ⊢ (𝑇 = ∅ → ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘)
2	1	ralrimivw 3134	. . . . . . . 8 ⊢ (𝑇 = ∅ → ∀𝑧 ∈ 𝑋 ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘)
3		rabid2 3434	. . . . . . . 8 ⊢ (𝑋 = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ ∀𝑧 ∈ 𝑋 ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘)
4	2, 3	sylibr 234	. . . . . . 7 ⊢ (𝑇 = ∅ → 𝑋 = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})
5	4	eqcomd 2743	. . . . . 6 ⊢ (𝑇 = ∅ → {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} = 𝑋)
6	5	eleq1d 2822	. . . . 5 ⊢ (𝑇 = ∅ → ({𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽) ↔ 𝑋 ∈ (Clsd‘𝐽)))
7		iinrab 5026	. . . . . . 7 ⊢ (𝑇 ≠ ∅ → ∩ 𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})
8	7	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑇 ≠ ∅) → ∩ 𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})
9		id 22	. . . . . . 7 ⊢ (𝑇 ≠ ∅ → 𝑇 ≠ ∅)
10		ubthlem.7	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑇 ⊆ (𝑈 BLnOp 𝑊))
11	10	sselda 3935	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ (𝑈 BLnOp 𝑊))
12		ubthlem.3	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐷 = (IndMet‘𝑈)
13		eqid 2737	. . . . . . . . . . . . . . . . . . . 20 ⊢ (IndMet‘𝑊) = (IndMet‘𝑊)
14		ubthlem.4	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐽 = (MetOpen‘𝐷)
15		eqid 2737	. . . . . . . . . . . . . . . . . . . 20 ⊢ (MetOpen‘(IndMet‘𝑊)) = (MetOpen‘(IndMet‘𝑊))
16		eqid 2737	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑈 BLnOp 𝑊) = (𝑈 BLnOp 𝑊)
17		ubthlem.5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑈 ∈ CBan
18		bnnv 30953	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑈 ∈ CBan → 𝑈 ∈ NrmCVec)
19	17, 18	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑈 ∈ NrmCVec
20		ubthlem.6	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑊 ∈ NrmCVec
21	12, 13, 14, 15, 16, 19, 20	blocn2 30895	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ (𝑈 BLnOp 𝑊) → 𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))))
22		ubth.1	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑋 = (BaseSet‘𝑈)
23	22, 12	cbncms 30952	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑈 ∈ CBan → 𝐷 ∈ (CMet‘𝑋))
24	17, 23	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐷 ∈ (CMet‘𝑋)
25		cmetmet 25254	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
26		metxmet 24290	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
27	24, 25, 26	mp2b 10	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐷 ∈ (∞Met‘𝑋)
28	14	mopntopon 24395	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋))
29	27, 28	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐽 ∈ (TopOn‘𝑋)
30		eqid 2737	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (BaseSet‘𝑊) = (BaseSet‘𝑊)
31	30, 13	imsxmet 30779	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑊 ∈ NrmCVec → (IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊)))
32	20, 31	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊))
33	15	mopntopon 24395	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊)) → (MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊)))
34	32, 33	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊))
35		iscncl 23225	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊))) → (𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))) ↔ (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽))))
36	29, 34, 35	mp2an 693	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))) ↔ (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽)))
37	21, 36	sylib 218	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (𝑈 BLnOp 𝑊) → (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽)))
38	11, 37	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽)))
39	38	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡:𝑋⟶(BaseSet‘𝑊))
40	39	adantlr 716	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → 𝑡:𝑋⟶(BaseSet‘𝑊))
41	40	ffvelcdmda 7038	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑡‘𝑥) ∈ (BaseSet‘𝑊))
42	41	biantrurd 532	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑁‘(𝑡‘𝑥)) ≤ 𝑘 ↔ ((𝑡‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)))
43		fveq2 6842	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑡‘𝑥) → (𝑁‘𝑦) = (𝑁‘(𝑡‘𝑥)))
44	43	breq1d 5110	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑡‘𝑥) → ((𝑁‘𝑦) ≤ 𝑘 ↔ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
45	44	elrab 3648	. . . . . . . . . . . . 13 ⊢ ((𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} ↔ ((𝑡‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
46	42, 45	bitr4di 289	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑁‘(𝑡‘𝑥)) ≤ 𝑘 ↔ (𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}))
47	46	pm5.32da 579	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → ((𝑥 ∈ 𝑋 ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘) ↔ (𝑥 ∈ 𝑋 ∧ (𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘})))
48		2fveq3 6847	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑥 → (𝑁‘(𝑡‘𝑧)) = (𝑁‘(𝑡‘𝑥)))
49	48	breq1d 5110	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑥 → ((𝑁‘(𝑡‘𝑧)) ≤ 𝑘 ↔ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
50	49	elrab 3648	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ (𝑥 ∈ 𝑋 ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
51	50	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ (𝑥 ∈ 𝑋 ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)))
52		ffn 6670	. . . . . . . . . . . 12 ⊢ (𝑡:𝑋⟶(BaseSet‘𝑊) → 𝑡 Fn 𝑋)
53		elpreima 7012	. . . . . . . . . . . 12 ⊢ (𝑡 Fn 𝑋 → (𝑥 ∈ (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}) ↔ (𝑥 ∈ 𝑋 ∧ (𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘})))
54	40, 52, 53	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → (𝑥 ∈ (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}) ↔ (𝑥 ∈ 𝑋 ∧ (𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘})))
55	47, 51, 54	3bitr4d 311	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ 𝑥 ∈ (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘})))
56	55	eqrdv 2735	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} = (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}))
57		imaeq2 6023	. . . . . . . . . . 11 ⊢ (𝑥 = {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} → (◡𝑡 “ 𝑥) = (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}))
58	57	eleq1d 2822	. . . . . . . . . 10 ⊢ (𝑥 = {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} → ((◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽) ↔ (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}) ∈ (Clsd‘𝐽)))
59	38	simprd 495	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽))
60	59	adantlr 716	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽))
61		nnre 12164	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
62	61	ad2antlr 728	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → 𝑘 ∈ ℝ)
63	62	rexrd 11194	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → 𝑘 ∈ ℝ*)
64		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (0vec‘𝑊) = (0vec‘𝑊)
65	30, 64	nvzcl 30721	. . . . . . . . . . . . 13 ⊢ (𝑊 ∈ NrmCVec → (0vec‘𝑊) ∈ (BaseSet‘𝑊))
66	20, 65	ax-mp 5	. . . . . . . . . . . 12 ⊢ (0vec‘𝑊) ∈ (BaseSet‘𝑊)
67		ubth.2	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑁 = (normCV‘𝑊)
68	30, 64, 67, 13	nvnd 30775	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ NrmCVec ∧ 𝑦 ∈ (BaseSet‘𝑊)) → (𝑁‘𝑦) = (𝑦(IndMet‘𝑊)(0vec‘𝑊)))
69	20, 68	mpan 691	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (BaseSet‘𝑊) → (𝑁‘𝑦) = (𝑦(IndMet‘𝑊)(0vec‘𝑊)))
70		xmetsym 24303	. . . . . . . . . . . . . . . . 17 ⊢ (((IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊)) ∧ (0vec‘𝑊) ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊)) → ((0vec‘𝑊)(IndMet‘𝑊)𝑦) = (𝑦(IndMet‘𝑊)(0vec‘𝑊)))
71	32, 66, 70	mp3an12 1454	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (BaseSet‘𝑊) → ((0vec‘𝑊)(IndMet‘𝑊)𝑦) = (𝑦(IndMet‘𝑊)(0vec‘𝑊)))
72	69, 71	eqtr4d 2775	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (BaseSet‘𝑊) → (𝑁‘𝑦) = ((0vec‘𝑊)(IndMet‘𝑊)𝑦))
73	72	breq1d 5110	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (BaseSet‘𝑊) → ((𝑁‘𝑦) ≤ 𝑘 ↔ ((0vec‘𝑊)(IndMet‘𝑊)𝑦) ≤ 𝑘))
74	73	rabbiia 3405	. . . . . . . . . . . . 13 ⊢ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} = {𝑦 ∈ (BaseSet‘𝑊) ∣ ((0vec‘𝑊)(IndMet‘𝑊)𝑦) ≤ 𝑘}
75	15, 74	blcld 24461	. . . . . . . . . . . 12 ⊢ (((IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊)) ∧ (0vec‘𝑊) ∈ (BaseSet‘𝑊) ∧ 𝑘 ∈ ℝ*) → {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊))))
76	32, 66, 75	mp3an12 1454	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℝ* → {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊))))
77	63, 76	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊))))
78	58, 60, 77	rspcdva 3579	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}) ∈ (Clsd‘𝐽))
79	56, 78	eqeltrd 2837	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
80	79	ralrimiva 3130	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∀𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
81		iincld 22995	. . . . . . 7 ⊢ ((𝑇 ≠ ∅ ∧ ∀𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽)) → ∩ 𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
82	9, 80, 81	syl2anr 598	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑇 ≠ ∅) → ∩ 𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
83	8, 82	eqeltrrd 2838	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑇 ≠ ∅) → {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
84	14	mopntop 24396	. . . . . . . 8 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
85	27, 84	ax-mp 5	. . . . . . 7 ⊢ 𝐽 ∈ Top
86	29	toponunii 22872	. . . . . . . 8 ⊢ 𝑋 = ∪ 𝐽
87	86	topcld 22991	. . . . . . 7 ⊢ (𝐽 ∈ Top → 𝑋 ∈ (Clsd‘𝐽))
88	85, 87	ax-mp 5	. . . . . 6 ⊢ 𝑋 ∈ (Clsd‘𝐽)
89	88	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑋 ∈ (Clsd‘𝐽))
90	6, 83, 89	pm2.61ne 3018	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
91		ubthlem.9	. . . 4 ⊢ 𝐴 = (𝑘 ∈ ℕ ↦ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})
92	90, 91	fmptd 7068	. . 3 ⊢ (𝜑 → 𝐴:ℕ⟶(Clsd‘𝐽))
93	92	frnd 6678	. . . . . 6 ⊢ (𝜑 → ran 𝐴 ⊆ (Clsd‘𝐽))
94	86	cldss2 22986	. . . . . 6 ⊢ (Clsd‘𝐽) ⊆ 𝒫 𝑋
95	93, 94	sstrdi 3948	. . . . 5 ⊢ (𝜑 → ran 𝐴 ⊆ 𝒫 𝑋)
96		sspwuni 5057	. . . . 5 ⊢ (ran 𝐴 ⊆ 𝒫 𝑋 ↔ ∪ ran 𝐴 ⊆ 𝑋)
97	95, 96	sylib 218	. . . 4 ⊢ (𝜑 → ∪ ran 𝐴 ⊆ 𝑋)
98		ubthlem.8	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐)
99		arch 12410	. . . . . . . . . 10 ⊢ (𝑐 ∈ ℝ → ∃𝑘 ∈ ℕ 𝑐 < 𝑘)
100	99	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) → ∃𝑘 ∈ ℕ 𝑐 < 𝑘)
101		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) → 𝑐 ∈ ℝ)
102		ltle 11233	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝑐 < 𝑘 → 𝑐 ≤ 𝑘))
103	101, 61, 102	syl2an 597	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (𝑐 < 𝑘 → 𝑐 ≤ 𝑘))
104	103	impr 454	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) → 𝑐 ≤ 𝑘)
105	104	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → 𝑐 ≤ 𝑘)
106	39	ffvelcdmda 7038	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑡‘𝑥) ∈ (BaseSet‘𝑊))
107	106	an32s 653	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑡 ∈ 𝑇) → (𝑡‘𝑥) ∈ (BaseSet‘𝑊))
108	30, 67	nvcl 30748	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ NrmCVec ∧ (𝑡‘𝑥) ∈ (BaseSet‘𝑊)) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ)
109	20, 107, 108	sylancr 588	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑡 ∈ 𝑇) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ)
110	109	adantlr 716	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑡 ∈ 𝑇) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ)
111	110	adantlr 716	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ)
112		simpllr 776	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → 𝑐 ∈ ℝ)
113		simplrl 777	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → 𝑘 ∈ ℕ)
114	113, 61	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → 𝑘 ∈ ℝ)
115		letr 11239	. . . . . . . . . . . . . . 15 ⊢ (((𝑁‘(𝑡‘𝑥)) ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (((𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ∧ 𝑐 ≤ 𝑘) → (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
116	111, 112, 114, 115	syl3anc 1374	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → (((𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ∧ 𝑐 ≤ 𝑘) → (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
117	105, 116	mpan2d 695	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → ((𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
118	117	ralimdva 3150	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
119	118	expr 456	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (𝑐 < 𝑘 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)))
120	22	fvexi 6856	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑋 ∈ V
121	120	rabex 5286	. . . . . . . . . . . . . . . . 17 ⊢ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ V
122	91	fvmpt2 6961	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ V) → (𝐴‘𝑘) = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})
123	121, 122	mpan2 692	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → (𝐴‘𝑘) = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})
124	123	eleq2d 2823	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ → (𝑥 ∈ (𝐴‘𝑘) ↔ 𝑥 ∈ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘}))
125	49	ralbidv 3161	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑥 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘 ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
126	125	elrab 3648	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
127	124, 126	bitrdi 287	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → (𝑥 ∈ (𝐴‘𝑘) ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)))
128		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋)
129	128	biantrurd 532	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘 ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)))
130	129	bicomd 223	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘) ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
131	127, 130	sylan9bbr 510	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ (𝐴‘𝑘) ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
132	92	ffnd 6671	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 Fn ℕ)
133	132	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 Fn ℕ)
134		fnfvelrn 7034	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝐴‘𝑘) ∈ ran 𝐴)
135		elssuni 4896	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴‘𝑘) ∈ ran 𝐴 → (𝐴‘𝑘) ⊆ ∪ ran 𝐴)
136	134, 135	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝐴‘𝑘) ⊆ ∪ ran 𝐴)
137	136	sseld 3934	. . . . . . . . . . . . . 14 ⊢ ((𝐴 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ (𝐴‘𝑘) → 𝑥 ∈ ∪ ran 𝐴))
138	133, 137	sylan 581	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ (𝐴‘𝑘) → 𝑥 ∈ ∪ ran 𝐴))
139	131, 138	sylbird 260	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ ℕ) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘 → 𝑥 ∈ ∪ ran 𝐴))
140	139	adantlr 716	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘 → 𝑥 ∈ ∪ ran 𝐴))
141	119, 140	syl6d 75	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (𝑐 < 𝑘 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → 𝑥 ∈ ∪ ran 𝐴)))
142	141	rexlimdva 3139	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) → (∃𝑘 ∈ ℕ 𝑐 < 𝑘 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → 𝑥 ∈ ∪ ran 𝐴)))
143	100, 142	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → 𝑥 ∈ ∪ ran 𝐴))
144	143	rexlimdva 3139	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → 𝑥 ∈ ∪ ran 𝐴))
145	144	ralimdva 3150	. . . . . 6 ⊢ (𝜑 → (∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → ∀𝑥 ∈ 𝑋 𝑥 ∈ ∪ ran 𝐴))
146	98, 145	mpd 15	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 𝑥 ∈ ∪ ran 𝐴)
147		dfss3 3924	. . . . 5 ⊢ (𝑋 ⊆ ∪ ran 𝐴 ↔ ∀𝑥 ∈ 𝑋 𝑥 ∈ ∪ ran 𝐴)
148	146, 147	sylibr 234	. . . 4 ⊢ (𝜑 → 𝑋 ⊆ ∪ ran 𝐴)
149	97, 148	eqssd 3953	. . 3 ⊢ (𝜑 → ∪ ran 𝐴 = 𝑋)
150		eqid 2737	. . . . . 6 ⊢ (0vec‘𝑈) = (0vec‘𝑈)
151	22, 150	nvzcl 30721	. . . . 5 ⊢ (𝑈 ∈ NrmCVec → (0vec‘𝑈) ∈ 𝑋)
152		ne0i 4295	. . . . 5 ⊢ ((0vec‘𝑈) ∈ 𝑋 → 𝑋 ≠ ∅)
153	19, 151, 152	mp2b 10	. . . 4 ⊢ 𝑋 ≠ ∅
154	14	bcth2 25298	. . . 4 ⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑋 ≠ ∅) ∧ (𝐴:ℕ⟶(Clsd‘𝐽) ∧ ∪ ran 𝐴 = 𝑋)) → ∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅)
155	24, 153, 154	mpanl12 703	. . 3 ⊢ ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ ∪ ran 𝐴 = 𝑋) → ∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅)
156	92, 149, 155	syl2anc 585	. 2 ⊢ (𝜑 → ∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅)
157		ffvelcdm 7035	. . . . . . . . . . 11 ⊢ ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ (Clsd‘𝐽))
158	94, 157	sselid 3933	. . . . . . . . . 10 ⊢ ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ 𝒫 𝑋)
159	158	elpwid 4565	. . . . . . . . 9 ⊢ ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ⊆ 𝑋)
160	92, 159	sylan 581	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ⊆ 𝑋)
161	86	ntrss3 23016	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ (𝐴‘𝑛) ⊆ 𝑋) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ 𝑋)
162	85, 160, 161	sylancr 588	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ 𝑋)
163	162	sseld 3934	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛)) → 𝑦 ∈ 𝑋))
164	86	ntropn 23005	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ (𝐴‘𝑛) ⊆ 𝑋) → ((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽)
165	85, 160, 164	sylancr 588	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽)
166	14	mopni2 24449	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽 ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → ∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)))
167	27, 166	mp3an1 1451	. . . . . . . . 9 ⊢ ((((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽 ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → ∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)))
168	165, 167	sylan 581	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → ∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)))
169		elssuni 4896	. . . . . . . . . . . 12 ⊢ (((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽 → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ ∪ 𝐽)
170	169, 86	sseqtrrdi 3977	. . . . . . . . . . 11 ⊢ (((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽 → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ 𝑋)
171	165, 170	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ 𝑋)
172	171	sselda 3935	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → 𝑦 ∈ 𝑋)
173	86	ntrss2 23013	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ (𝐴‘𝑛) ⊆ 𝑋) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ (𝐴‘𝑛))
174	85, 160, 173	sylancr 588	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ (𝐴‘𝑛))
175		sstr2 3942	. . . . . . . . . . . . 13 ⊢ ((𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → (((int‘𝐽)‘(𝐴‘𝑛)) ⊆ (𝐴‘𝑛) → (𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛)))
176	174, 175	syl5com 31	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → (𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛)))
177	176	ad2antrr 727	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → ((𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → (𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛)))
178		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋)
179	178, 27	jctil 519	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) → (𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋))
180		rphalfcl 12946	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ+ → (𝑥 / 2) ∈ ℝ+)
181	180	rpxrd 12962	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ+ → (𝑥 / 2) ∈ ℝ*)
182		rpxr 12927	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ*)
183		rphalflt 12948	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ+ → (𝑥 / 2) < 𝑥)
184	181, 182, 183	3jca 1129	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ+ → ((𝑥 / 2) ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ (𝑥 / 2) < 𝑥))
185		eqid 2737	. . . . . . . . . . . . . 14 ⊢ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} = {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)}
186	14, 185	blsscls2 24460	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ ((𝑥 / 2) ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ (𝑥 / 2) < 𝑥)) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝑦(ball‘𝐷)𝑥))
187	179, 184, 186	syl2an 597	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝑦(ball‘𝐷)𝑥))
188		sstr2 3942	. . . . . . . . . . . 12 ⊢ ({𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝑦(ball‘𝐷)𝑥) → ((𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛)))
189	187, 188	syl 17	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → ((𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛)))
190	180	adantl 481	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈ ℝ+)
191		breq2 5104	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = (𝑥 / 2) → ((𝑦𝐷𝑧) ≤ 𝑟 ↔ (𝑦𝐷𝑧) ≤ (𝑥 / 2)))
192	191	rabbidv 3408	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = (𝑥 / 2) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} = {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)})
193	192	sseq1d 3967	. . . . . . . . . . . . . 14 ⊢ (𝑟 = (𝑥 / 2) → ({𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛) ↔ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛)))
194	193	rspcev 3578	. . . . . . . . . . . . 13 ⊢ (((𝑥 / 2) ∈ ℝ+ ∧ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))
195	194	ex 412	. . . . . . . . . . . 12 ⊢ ((𝑥 / 2) ∈ ℝ+ → ({𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
196	190, 195	syl 17	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → ({𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
197	177, 189, 196	3syld 60	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → ((𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
198	197	rexlimdva 3139	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) → (∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
199	172, 198	syldan 592	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → (∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
200	168, 199	mpd 15	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))
201	200	ex 412	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
202	163, 201	jcad 512	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛)) → (𝑦 ∈ 𝑋 ∧ ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))))
203	202	eximdv 1919	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∃𝑦 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛)) → ∃𝑦(𝑦 ∈ 𝑋 ∧ ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))))
204		n0 4307	. . . 4 ⊢ (((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛)))
205		df-rex 3063	. . . 4 ⊢ (∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛) ↔ ∃𝑦(𝑦 ∈ 𝑋 ∧ ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
206	203, 204, 205	3imtr4g 296	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅ → ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
207	206	reximdva 3151	. 2 ⊢ (𝜑 → (∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅ → ∃𝑛 ∈ ℕ ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
208	156, 207	mpd 15	1 ⊢ (𝜑 → ∃𝑛 ∈ ℕ ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  ∃wrex 3062  {crab 3401  Vcvv 3442   ⊆ wss 3903  ∅c0 4287  𝒫 cpw 4556  ∪ cuni 4865  ∩ ciin 4949   class class class wbr 5100   ↦ cmpt 5181  ^◡ccnv 5631  ran crn 5633   “ cima 5635   Fn wfn 6495  ⟶wf 6496  ‘cfv 6500  (class class class)co 7368  ℝcr 11037  ℝ^*cxr 11177   < clt 11178   ≤ cle 11179   / cdiv 11806  ℕcn 12157  2c2 12212  ℝ⁺crp 12917  ∞Metcxmet 21306  Metcmet 21307  ballcbl 21308  MetOpencmopn 21311  Topctop 22849  TopOnctopon 22866  Clsdccld 22972  intcnt 22973   Cn ccn 23180  CMetccmet 25222  NrmCVeccnv 30671  BaseSetcba 30673  0_veccn0v 30675  norm_CVcnmcv 30677  IndMetcims 30678   BLnOp cblo 30829  CBanccbn 30949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-inf2 9562  ax-dc 10368  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-pre-sup 11116  ax-addf 11117  ax-mulf 11118

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-int 4905  df-iun 4950  df-iin 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-om 7819  df-1st 7943  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-1o 8407  df-er 8645  df-map 8777  df-pm 8778  df-en 8896  df-dom 8897  df-sdom 8898  df-sup 9357  df-inf 9358  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-div 11807  df-nn 12158  df-2 12220  df-3 12221  df-n0 12414  df-z 12501  df-uz 12764  df-q 12874  df-rp 12918  df-xneg 13038  df-xadd 13039  df-xmul 13040  df-ico 13279  df-seq 13937  df-exp 13997  df-cj 15034  df-re 15035  df-im 15036  df-sqrt 15170  df-abs 15171  df-rest 17354  df-topgen 17375  df-psmet 21313  df-xmet 21314  df-met 21315  df-bl 21316  df-mopn 21317  df-fbas 21318  df-fg 21319  df-top 22850  df-topon 22867  df-bases 22902  df-cld 22975  df-ntr 22976  df-cls 22977  df-nei 23054  df-cn 23183  df-cnp 23184  df-lm 23185  df-fil 23802  df-fm 23894  df-flim 23895  df-flf 23896  df-cfil 25223  df-cau 25224  df-cmet 25225  df-grpo 30580  df-gid 30581  df-ginv 30582  df-gdiv 30583  df-ablo 30632  df-vc 30646  df-nv 30679  df-va 30682  df-ba 30683  df-sm 30684  df-0v 30685  df-vs 30686  df-nmcv 30687  df-ims 30688  df-lno 30831  df-nmoo 30832  df-blo 30833  df-0o 30834  df-cbn 30950

This theorem is referenced by:  ubthlem3  30959