Theorem ubthlem1 30842

Description: Lemma for ubth 30845. 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 25252, 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 4454	. . . . . . . . 9 ⊢ (𝑇 = ∅ → ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘)
2	1	ralrimivw 3128	. . . . . . . 8 ⊢ (𝑇 = ∅ → ∀𝑧 ∈ 𝑋 ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘)
3		rabid2 3428	. . . . . . . 8 ⊢ (𝑋 = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ ∀𝑧 ∈ 𝑋 ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘)
4	2, 3	sylibr 234	. . . . . . 7 ⊢ (𝑇 = ∅ → 𝑋 = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})
5	4	eqcomd 2737	. . . . . 6 ⊢ (𝑇 = ∅ → {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} = 𝑋)
6	5	eleq1d 2816	. . . . 5 ⊢ (𝑇 = ∅ → ({𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽) ↔ 𝑋 ∈ (Clsd‘𝐽)))
7		iinrab 5012	. . . . . . 7 ⊢ (𝑇 ≠ ∅ → ∩ 𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})
8	7	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑇 ≠ ∅) → ∩ 𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})
9		id 22	. . . . . . 7 ⊢ (𝑇 ≠ ∅ → 𝑇 ≠ ∅)
10		ubthlem.7	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑇 ⊆ (𝑈 BLnOp 𝑊))
11	10	sselda 3929	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ (𝑈 BLnOp 𝑊))
12		ubthlem.3	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐷 = (IndMet‘𝑈)
13		eqid 2731	. . . . . . . . . . . . . . . . . . . 20 ⊢ (IndMet‘𝑊) = (IndMet‘𝑊)
14		ubthlem.4	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐽 = (MetOpen‘𝐷)
15		eqid 2731	. . . . . . . . . . . . . . . . . . . 20 ⊢ (MetOpen‘(IndMet‘𝑊)) = (MetOpen‘(IndMet‘𝑊))
16		eqid 2731	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑈 BLnOp 𝑊) = (𝑈 BLnOp 𝑊)
17		ubthlem.5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑈 ∈ CBan
18		bnnv 30838	. . . . . . . . . . . . . . . . . . . . 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 30780	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ (𝑈 BLnOp 𝑊) → 𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))))
22		ubth.1	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑋 = (BaseSet‘𝑈)
23	22, 12	cbncms 30837	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑈 ∈ CBan → 𝐷 ∈ (CMet‘𝑋))
24	17, 23	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐷 ∈ (CMet‘𝑋)
25		cmetmet 25208	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
26		metxmet 24244	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
27	24, 25, 26	mp2b 10	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐷 ∈ (∞Met‘𝑋)
28	14	mopntopon 24349	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋))
29	27, 28	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐽 ∈ (TopOn‘𝑋)
30		eqid 2731	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (BaseSet‘𝑊) = (BaseSet‘𝑊)
31	30, 13	imsxmet 30664	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑊 ∈ NrmCVec → (IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊)))
32	20, 31	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊))
33	15	mopntopon 24349	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊)) → (MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊)))
34	32, 33	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊))
35		iscncl 23179	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊))) → (𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))) ↔ (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽))))
36	29, 34, 35	mp2an 692	. . . . . . . . . . . . . . . . . . 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 715	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → 𝑡:𝑋⟶(BaseSet‘𝑊))
41	40	ffvelcdmda 7012	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑡‘𝑥) ∈ (BaseSet‘𝑊))
42	41	biantrurd 532	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑁‘(𝑡‘𝑥)) ≤ 𝑘 ↔ ((𝑡‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)))
43		fveq2 6817	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑡‘𝑥) → (𝑁‘𝑦) = (𝑁‘(𝑡‘𝑥)))
44	43	breq1d 5096	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑡‘𝑥) → ((𝑁‘𝑦) ≤ 𝑘 ↔ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
45	44	elrab 3642	. . . . . . . . . . . . 13 ⊢ ((𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} ↔ ((𝑡‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
46	42, 45	bitr4di 289	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑁‘(𝑡‘𝑥)) ≤ 𝑘 ↔ (𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}))
47	46	pm5.32da 579	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → ((𝑥 ∈ 𝑋 ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘) ↔ (𝑥 ∈ 𝑋 ∧ (𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘})))
48		2fveq3 6822	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑥 → (𝑁‘(𝑡‘𝑧)) = (𝑁‘(𝑡‘𝑥)))
49	48	breq1d 5096	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑥 → ((𝑁‘(𝑡‘𝑧)) ≤ 𝑘 ↔ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
50	49	elrab 3642	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ (𝑥 ∈ 𝑋 ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
51	50	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ (𝑥 ∈ 𝑋 ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)))
52		ffn 6646	. . . . . . . . . . . 12 ⊢ (𝑡:𝑋⟶(BaseSet‘𝑊) → 𝑡 Fn 𝑋)
53		elpreima 6986	. . . . . . . . . . . 12 ⊢ (𝑡 Fn 𝑋 → (𝑥 ∈ (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}) ↔ (𝑥 ∈ 𝑋 ∧ (𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘})))
54	40, 52, 53	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → (𝑥 ∈ (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}) ↔ (𝑥 ∈ 𝑋 ∧ (𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘})))
55	47, 51, 54	3bitr4d 311	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ 𝑥 ∈ (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘})))
56	55	eqrdv 2729	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} = (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}))
57		imaeq2 6000	. . . . . . . . . . 11 ⊢ (𝑥 = {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} → (◡𝑡 “ 𝑥) = (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}))
58	57	eleq1d 2816	. . . . . . . . . 10 ⊢ (𝑥 = {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} → ((◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽) ↔ (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}) ∈ (Clsd‘𝐽)))
59	38	simprd 495	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽))
60	59	adantlr 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽))
61		nnre 12127	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
62	61	ad2antlr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → 𝑘 ∈ ℝ)
63	62	rexrd 11157	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → 𝑘 ∈ ℝ*)
64		eqid 2731	. . . . . . . . . . . . . 14 ⊢ (0vec‘𝑊) = (0vec‘𝑊)
65	30, 64	nvzcl 30606	. . . . . . . . . . . . 13 ⊢ (𝑊 ∈ NrmCVec → (0vec‘𝑊) ∈ (BaseSet‘𝑊))
66	20, 65	ax-mp 5	. . . . . . . . . . . 12 ⊢ (0vec‘𝑊) ∈ (BaseSet‘𝑊)
67		ubth.2	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑁 = (normCV‘𝑊)
68	30, 64, 67, 13	nvnd 30660	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ NrmCVec ∧ 𝑦 ∈ (BaseSet‘𝑊)) → (𝑁‘𝑦) = (𝑦(IndMet‘𝑊)(0vec‘𝑊)))
69	20, 68	mpan 690	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (BaseSet‘𝑊) → (𝑁‘𝑦) = (𝑦(IndMet‘𝑊)(0vec‘𝑊)))
70		xmetsym 24257	. . . . . . . . . . . . . . . . 17 ⊢ (((IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊)) ∧ (0vec‘𝑊) ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊)) → ((0vec‘𝑊)(IndMet‘𝑊)𝑦) = (𝑦(IndMet‘𝑊)(0vec‘𝑊)))
71	32, 66, 70	mp3an12 1453	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (BaseSet‘𝑊) → ((0vec‘𝑊)(IndMet‘𝑊)𝑦) = (𝑦(IndMet‘𝑊)(0vec‘𝑊)))
72	69, 71	eqtr4d 2769	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (BaseSet‘𝑊) → (𝑁‘𝑦) = ((0vec‘𝑊)(IndMet‘𝑊)𝑦))
73	72	breq1d 5096	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (BaseSet‘𝑊) → ((𝑁‘𝑦) ≤ 𝑘 ↔ ((0vec‘𝑊)(IndMet‘𝑊)𝑦) ≤ 𝑘))
74	73	rabbiia 3399	. . . . . . . . . . . . 13 ⊢ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} = {𝑦 ∈ (BaseSet‘𝑊) ∣ ((0vec‘𝑊)(IndMet‘𝑊)𝑦) ≤ 𝑘}
75	15, 74	blcld 24415	. . . . . . . . . . . 12 ⊢ (((IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊)) ∧ (0vec‘𝑊) ∈ (BaseSet‘𝑊) ∧ 𝑘 ∈ ℝ*) → {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊))))
76	32, 66, 75	mp3an12 1453	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℝ* → {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊))))
77	63, 76	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊))))
78	58, 60, 77	rspcdva 3573	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}) ∈ (Clsd‘𝐽))
79	56, 78	eqeltrd 2831	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
80	79	ralrimiva 3124	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∀𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
81		iincld 22949	. . . . . . 7 ⊢ ((𝑇 ≠ ∅ ∧ ∀𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽)) → ∩ 𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
82	9, 80, 81	syl2anr 597	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑇 ≠ ∅) → ∩ 𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
83	8, 82	eqeltrrd 2832	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑇 ≠ ∅) → {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
84	14	mopntop 24350	. . . . . . . 8 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
85	27, 84	ax-mp 5	. . . . . . 7 ⊢ 𝐽 ∈ Top
86	29	toponunii 22826	. . . . . . . 8 ⊢ 𝑋 = ∪ 𝐽
87	86	topcld 22945	. . . . . . 7 ⊢ (𝐽 ∈ Top → 𝑋 ∈ (Clsd‘𝐽))
88	85, 87	ax-mp 5	. . . . . 6 ⊢ 𝑋 ∈ (Clsd‘𝐽)
89	88	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑋 ∈ (Clsd‘𝐽))
90	6, 83, 89	pm2.61ne 3013	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
91		ubthlem.9	. . . 4 ⊢ 𝐴 = (𝑘 ∈ ℕ ↦ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})
92	90, 91	fmptd 7042	. . 3 ⊢ (𝜑 → 𝐴:ℕ⟶(Clsd‘𝐽))
93	92	frnd 6654	. . . . . 6 ⊢ (𝜑 → ran 𝐴 ⊆ (Clsd‘𝐽))
94	86	cldss2 22940	. . . . . 6 ⊢ (Clsd‘𝐽) ⊆ 𝒫 𝑋
95	93, 94	sstrdi 3942	. . . . 5 ⊢ (𝜑 → ran 𝐴 ⊆ 𝒫 𝑋)
96		sspwuni 5043	. . . . 5 ⊢ (ran 𝐴 ⊆ 𝒫 𝑋 ↔ ∪ ran 𝐴 ⊆ 𝑋)
97	95, 96	sylib 218	. . . 4 ⊢ (𝜑 → ∪ ran 𝐴 ⊆ 𝑋)
98		ubthlem.8	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐)
99		arch 12373	. . . . . . . . . 10 ⊢ (𝑐 ∈ ℝ → ∃𝑘 ∈ ℕ 𝑐 < 𝑘)
100	99	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) → ∃𝑘 ∈ ℕ 𝑐 < 𝑘)
101		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) → 𝑐 ∈ ℝ)
102		ltle 11196	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝑐 < 𝑘 → 𝑐 ≤ 𝑘))
103	101, 61, 102	syl2an 596	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (𝑐 < 𝑘 → 𝑐 ≤ 𝑘))
104	103	impr 454	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) → 𝑐 ≤ 𝑘)
105	104	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → 𝑐 ≤ 𝑘)
106	39	ffvelcdmda 7012	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑡‘𝑥) ∈ (BaseSet‘𝑊))
107	106	an32s 652	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑡 ∈ 𝑇) → (𝑡‘𝑥) ∈ (BaseSet‘𝑊))
108	30, 67	nvcl 30633	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ NrmCVec ∧ (𝑡‘𝑥) ∈ (BaseSet‘𝑊)) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ)
109	20, 107, 108	sylancr 587	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑡 ∈ 𝑇) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ)
110	109	adantlr 715	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑡 ∈ 𝑇) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ)
111	110	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ)
112		simpllr 775	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → 𝑐 ∈ ℝ)
113		simplrl 776	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → 𝑘 ∈ ℕ)
114	113, 61	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → 𝑘 ∈ ℝ)
115		letr 11202	. . . . . . . . . . . . . . 15 ⊢ (((𝑁‘(𝑡‘𝑥)) ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (((𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ∧ 𝑐 ≤ 𝑘) → (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
116	111, 112, 114, 115	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → (((𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ∧ 𝑐 ≤ 𝑘) → (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
117	105, 116	mpan2d 694	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → ((𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
118	117	ralimdva 3144	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
119	118	expr 456	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (𝑐 < 𝑘 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)))
120	22	fvexi 6831	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑋 ∈ V
121	120	rabex 5272	. . . . . . . . . . . . . . . . 17 ⊢ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ V
122	91	fvmpt2 6935	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ V) → (𝐴‘𝑘) = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})
123	121, 122	mpan2 691	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → (𝐴‘𝑘) = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})
124	123	eleq2d 2817	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ → (𝑥 ∈ (𝐴‘𝑘) ↔ 𝑥 ∈ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘}))
125	49	ralbidv 3155	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑥 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘 ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
126	125	elrab 3642	. . . . . . . . . . . . . . 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 6647	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 Fn ℕ)
133	132	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 Fn ℕ)
134		fnfvelrn 7008	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝐴‘𝑘) ∈ ran 𝐴)
135		elssuni 4884	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴‘𝑘) ∈ ran 𝐴 → (𝐴‘𝑘) ⊆ ∪ ran 𝐴)
136	134, 135	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝐴‘𝑘) ⊆ ∪ ran 𝐴)
137	136	sseld 3928	. . . . . . . . . . . . . 14 ⊢ ((𝐴 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ (𝐴‘𝑘) → 𝑥 ∈ ∪ ran 𝐴))
138	133, 137	sylan 580	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ (𝐴‘𝑘) → 𝑥 ∈ ∪ ran 𝐴))
139	131, 138	sylbird 260	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ ℕ) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘 → 𝑥 ∈ ∪ ran 𝐴))
140	139	adantlr 715	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘 → 𝑥 ∈ ∪ ran 𝐴))
141	119, 140	syl6d 75	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (𝑐 < 𝑘 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → 𝑥 ∈ ∪ ran 𝐴)))
142	141	rexlimdva 3133	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) → (∃𝑘 ∈ ℕ 𝑐 < 𝑘 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → 𝑥 ∈ ∪ ran 𝐴)))
143	100, 142	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → 𝑥 ∈ ∪ ran 𝐴))
144	143	rexlimdva 3133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → 𝑥 ∈ ∪ ran 𝐴))
145	144	ralimdva 3144	. . . . . 6 ⊢ (𝜑 → (∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → ∀𝑥 ∈ 𝑋 𝑥 ∈ ∪ ran 𝐴))
146	98, 145	mpd 15	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 𝑥 ∈ ∪ ran 𝐴)
147		dfss3 3918	. . . . 5 ⊢ (𝑋 ⊆ ∪ ran 𝐴 ↔ ∀𝑥 ∈ 𝑋 𝑥 ∈ ∪ ran 𝐴)
148	146, 147	sylibr 234	. . . 4 ⊢ (𝜑 → 𝑋 ⊆ ∪ ran 𝐴)
149	97, 148	eqssd 3947	. . 3 ⊢ (𝜑 → ∪ ran 𝐴 = 𝑋)
150		eqid 2731	. . . . . 6 ⊢ (0vec‘𝑈) = (0vec‘𝑈)
151	22, 150	nvzcl 30606	. . . . 5 ⊢ (𝑈 ∈ NrmCVec → (0vec‘𝑈) ∈ 𝑋)
152		ne0i 4286	. . . . 5 ⊢ ((0vec‘𝑈) ∈ 𝑋 → 𝑋 ≠ ∅)
153	19, 151, 152	mp2b 10	. . . 4 ⊢ 𝑋 ≠ ∅
154	14	bcth2 25252	. . . 4 ⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑋 ≠ ∅) ∧ (𝐴:ℕ⟶(Clsd‘𝐽) ∧ ∪ ran 𝐴 = 𝑋)) → ∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅)
155	24, 153, 154	mpanl12 702	. . 3 ⊢ ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ ∪ ran 𝐴 = 𝑋) → ∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅)
156	92, 149, 155	syl2anc 584	. 2 ⊢ (𝜑 → ∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅)
157		ffvelcdm 7009	. . . . . . . . . . 11 ⊢ ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ (Clsd‘𝐽))
158	94, 157	sselid 3927	. . . . . . . . . 10 ⊢ ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ 𝒫 𝑋)
159	158	elpwid 4554	. . . . . . . . 9 ⊢ ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ⊆ 𝑋)
160	92, 159	sylan 580	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ⊆ 𝑋)
161	86	ntrss3 22970	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ (𝐴‘𝑛) ⊆ 𝑋) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ 𝑋)
162	85, 160, 161	sylancr 587	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ 𝑋)
163	162	sseld 3928	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛)) → 𝑦 ∈ 𝑋))
164	86	ntropn 22959	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ (𝐴‘𝑛) ⊆ 𝑋) → ((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽)
165	85, 160, 164	sylancr 587	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽)
166	14	mopni2 24403	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽 ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → ∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)))
167	27, 166	mp3an1 1450	. . . . . . . . 9 ⊢ ((((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽 ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → ∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)))
168	165, 167	sylan 580	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → ∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)))
169		elssuni 4884	. . . . . . . . . . . 12 ⊢ (((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽 → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ ∪ 𝐽)
170	169, 86	sseqtrrdi 3971	. . . . . . . . . . 11 ⊢ (((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽 → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ 𝑋)
171	165, 170	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ 𝑋)
172	171	sselda 3929	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → 𝑦 ∈ 𝑋)
173	86	ntrss2 22967	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ (𝐴‘𝑛) ⊆ 𝑋) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ (𝐴‘𝑛))
174	85, 160, 173	sylancr 587	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ (𝐴‘𝑛))
175		sstr2 3936	. . . . . . . . . . . . 13 ⊢ ((𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → (((int‘𝐽)‘(𝐴‘𝑛)) ⊆ (𝐴‘𝑛) → (𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛)))
176	174, 175	syl5com 31	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → (𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛)))
177	176	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → ((𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → (𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛)))
178		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋)
179	178, 27	jctil 519	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) → (𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋))
180		rphalfcl 12914	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ+ → (𝑥 / 2) ∈ ℝ+)
181	180	rpxrd 12930	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ+ → (𝑥 / 2) ∈ ℝ*)
182		rpxr 12895	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ*)
183		rphalflt 12916	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ+ → (𝑥 / 2) < 𝑥)
184	181, 182, 183	3jca 1128	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ+ → ((𝑥 / 2) ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ (𝑥 / 2) < 𝑥))
185		eqid 2731	. . . . . . . . . . . . . 14 ⊢ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} = {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)}
186	14, 185	blsscls2 24414	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ ((𝑥 / 2) ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ (𝑥 / 2) < 𝑥)) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝑦(ball‘𝐷)𝑥))
187	179, 184, 186	syl2an 596	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝑦(ball‘𝐷)𝑥))
188		sstr2 3936	. . . . . . . . . . . 12 ⊢ ({𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝑦(ball‘𝐷)𝑥) → ((𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛)))
189	187, 188	syl 17	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → ((𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛)))
190	180	adantl 481	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈ ℝ+)
191		breq2 5090	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = (𝑥 / 2) → ((𝑦𝐷𝑧) ≤ 𝑟 ↔ (𝑦𝐷𝑧) ≤ (𝑥 / 2)))
192	191	rabbidv 3402	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = (𝑥 / 2) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} = {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)})
193	192	sseq1d 3961	. . . . . . . . . . . . . 14 ⊢ (𝑟 = (𝑥 / 2) → ({𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛) ↔ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛)))
194	193	rspcev 3572	. . . . . . . . . . . . 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 3133	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) → (∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
199	172, 198	syldan 591	. . . . . . . 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 1918	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∃𝑦 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛)) → ∃𝑦(𝑦 ∈ 𝑋 ∧ ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))))
204		n0 4298	. . . 4 ⊢ (((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛)))
205		df-rex 3057	. . . 4 ⊢ (∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛) ↔ ∃𝑦(𝑦 ∈ 𝑋 ∧ ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
206	203, 204, 205	3imtr4g 296	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅ → ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
207	206	reximdva 3145	. 2 ⊢ (𝜑 → (∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅ → ∃𝑛 ∈ ℕ ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
208	156, 207	mpd 15	1 ⊢ (𝜑 → ∃𝑛 ∈ ℕ ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541  ∃wex 1780   ∈ wcel 2111   ≠ wne 2928  ∀wral 3047  ∃wrex 3056  {crab 3395  Vcvv 3436   ⊆ wss 3897  ∅c0 4278  𝒫 cpw 4545  ∪ cuni 4854  ∩ ciin 4937   class class class wbr 5086   ↦ cmpt 5167  ^◡ccnv 5610  ran crn 5612   “ cima 5614   Fn wfn 6471  ⟶wf 6472  ‘cfv 6476  (class class class)co 7341  ℝcr 11000  ℝ^*cxr 11140   < clt 11141   ≤ cle 11142   / cdiv 11769  ℕcn 12120  2c2 12175  ℝ⁺crp 12885  ∞Metcxmet 21271  Metcmet 21272  ballcbl 21273  MetOpencmopn 21276  Topctop 22803  TopOnctopon 22820  Clsdccld 22926  intcnt 22927   Cn ccn 23134  CMetccmet 25176  NrmCVeccnv 30556  BaseSetcba 30558  0_veccn0v 30560  norm_CVcnmcv 30562  IndMetcims 30563   BLnOp cblo 30714  CBanccbn 30834

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5212  ax-sep 5229  ax-nul 5239  ax-pow 5298  ax-pr 5365  ax-un 7663  ax-inf2 9526  ax-dc 10332  ax-cnex 11057  ax-resscn 11058  ax-1cn 11059  ax-icn 11060  ax-addcl 11061  ax-addrcl 11062  ax-mulcl 11063  ax-mulrcl 11064  ax-mulcom 11065  ax-addass 11066  ax-mulass 11067  ax-distr 11068  ax-i2m1 11069  ax-1ne0 11070  ax-1rid 11071  ax-rnegex 11072  ax-rrecex 11073  ax-cnre 11074  ax-pre-lttri 11075  ax-pre-lttrn 11076  ax-pre-ltadd 11077  ax-pre-mulgt0 11078  ax-pre-sup 11079  ax-addf 11080  ax-mulf 11081

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-int 4893  df-iun 4938  df-iin 4939  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5506  df-eprel 5511  df-po 5519  df-so 5520  df-fr 5564  df-we 5566  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-pred 6243  df-ord 6304  df-on 6305  df-lim 6306  df-suc 6307  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-riota 7298  df-ov 7344  df-oprab 7345  df-mpo 7346  df-om 7792  df-1st 7916  df-2nd 7917  df-frecs 8206  df-wrecs 8237  df-recs 8286  df-rdg 8324  df-1o 8380  df-er 8617  df-map 8747  df-pm 8748  df-en 8865  df-dom 8866  df-sdom 8867  df-sup 9321  df-inf 9322  df-pnf 11143  df-mnf 11144  df-xr 11145  df-ltxr 11146  df-le 11147  df-sub 11341  df-neg 11342  df-div 11770  df-nn 12121  df-2 12183  df-3 12184  df-n0 12377  df-z 12464  df-uz 12728  df-q 12842  df-rp 12886  df-xneg 13006  df-xadd 13007  df-xmul 13008  df-ico 13246  df-seq 13904  df-exp 13964  df-cj 15001  df-re 15002  df-im 15003  df-sqrt 15137  df-abs 15138  df-rest 17321  df-topgen 17342  df-psmet 21278  df-xmet 21279  df-met 21280  df-bl 21281  df-mopn 21282  df-fbas 21283  df-fg 21284  df-top 22804  df-topon 22821  df-bases 22856  df-cld 22929  df-ntr 22930  df-cls 22931  df-nei 23008  df-cn 23137  df-cnp 23138  df-lm 23139  df-fil 23756  df-fm 23848  df-flim 23849  df-flf 23850  df-cfil 25177  df-cau 25178  df-cmet 25179  df-grpo 30465  df-gid 30466  df-ginv 30467  df-gdiv 30468  df-ablo 30517  df-vc 30531  df-nv 30564  df-va 30567  df-ba 30568  df-sm 30569  df-0v 30570  df-vs 30571  df-nmcv 30572  df-ims 30573  df-lno 30716  df-nmoo 30717  df-blo 30718  df-0o 30719  df-cbn 30835

This theorem is referenced by:  ubthlem3  30844