Theorem ubthlem1 31518

Description: Lemma for ubth 31521. 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 25695, 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 4453	. . . . . . . . 9 ⊢ (𝑇 = ∅ → ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘)
2	1	ralrimivw 3162	. . . . . . . 8 ⊢ (𝑇 = ∅ → ∀𝑧 ∈ 𝑋 ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘)
3		rabid2 3448	. . . . . . . 8 ⊢ (𝑋 = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ ∀𝑧 ∈ 𝑋 ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘)
4	2, 3	sylibr 237	. . . . . . 7 ⊢ (𝑇 = ∅ → 𝑋 = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})
5	4	eqcomd 2769	. . . . . 6 ⊢ (𝑇 = ∅ → {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} = 𝑋)
6	5	eleq1d 2849	. . . . 5 ⊢ (𝑇 = ∅ → ({𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽) ↔ 𝑋 ∈ (Clsd‘𝐽)))
7		iinrab 5030	. . . . . . 7 ⊢ (𝑇 ≠ ∅ → ∩ 𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})
8	7	adantl 487	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑇 ≠ ∅) → ∩ 𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})
9		id 23	. . . . . . 7 ⊢ (𝑇 ≠ ∅ → 𝑇 ≠ ∅)
10		ubthlem.7	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑇 ⊆ (𝑈 BLnOp 𝑊))
11	10	sselda 3913	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ (𝑈 BLnOp 𝑊))
12		ubthlem.3	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐷 = (IndMet‘𝑈)
13		eqid 2763	. . . . . . . . . . . . . . . . . . . 20 ⊢ (IndMet‘𝑊) = (IndMet‘𝑊)
14		ubthlem.4	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐽 = (MetOpen‘𝐷)
15		eqid 2763	. . . . . . . . . . . . . . . . . . . 20 ⊢ (MetOpen‘(IndMet‘𝑊)) = (MetOpen‘(IndMet‘𝑊))
16		eqid 2763	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑈 BLnOp 𝑊) = (𝑈 BLnOp 𝑊)
17		ubthlem.5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑈 ∈ CBan
18		bnnv 31514	. . . . . . . . . . . . . . . . . . . . 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 31456	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ (𝑈 BLnOp 𝑊) → 𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))))
22		ubth.1	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑋 = (BaseSet‘𝑈)
23	22, 12	cbncms 31513	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑈 ∈ CBan → 𝐷 ∈ (CMet‘𝑋))
24	17, 23	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐷 ∈ (CMet‘𝑋)
25		cmetmet 25651	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
26		metxmet 24697	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
27	24, 25, 26	mp2b 10	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐷 ∈ (∞Met‘𝑋)
28	14	mopntopon 24802	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋))
29	27, 28	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐽 ∈ (TopOn‘𝑋)
30		eqid 2763	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (BaseSet‘𝑊) = (BaseSet‘𝑊)
31	30, 13	imsxmet 31340	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑊 ∈ NrmCVec → (IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊)))
32	20, 31	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊))
33	15	mopntopon 24802	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊)) → (MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊)))
34	32, 33	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊))
35		iscncl 23631	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊))) → (𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))) ↔ (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽))))
36	29, 34, 35	mp2an 705	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))) ↔ (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽)))
37	21, 36	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (𝑈 BLnOp 𝑊) → (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽)))
38	11, 37	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽)))
39	38	simpld 500	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡:𝑋⟶(BaseSet‘𝑊))
40	39	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → 𝑡:𝑋⟶(BaseSet‘𝑊))
41	40	ffvelcdmda 7114	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑡‘𝑥) ∈ (BaseSet‘𝑊))
42	41	biantrurd 542	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑁‘(𝑡‘𝑥)) ≤ 𝑘 ↔ ((𝑡‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)))
43		fveq2 6914	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑡‘𝑥) → (𝑁‘𝑦) = (𝑁‘(𝑡‘𝑥)))
44	43	breq1d 5116	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑡‘𝑥) → ((𝑁‘𝑦) ≤ 𝑘 ↔ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
45	44	elrab 3648	. . . . . . . . . . . . 13 ⊢ ((𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} ↔ ((𝑡‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
46	42, 45	bitr4di 292	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑁‘(𝑡‘𝑥)) ≤ 𝑘 ↔ (𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}))
47	46	pm5.32da 590	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → ((𝑥 ∈ 𝑋 ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘) ↔ (𝑥 ∈ 𝑋 ∧ (𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘})))
48		2fveq3 6919	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑥 → (𝑁‘(𝑡‘𝑧)) = (𝑁‘(𝑡‘𝑥)))
49	48	breq1d 5116	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑥 → ((𝑁‘(𝑡‘𝑧)) ≤ 𝑘 ↔ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
50	49	elrab 3648	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ (𝑥 ∈ 𝑋 ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
51	50	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ (𝑥 ∈ 𝑋 ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)))
52		ffn 6737	. . . . . . . . . . . 12 ⊢ (𝑡:𝑋⟶(BaseSet‘𝑊) → 𝑡 Fn 𝑋)
53		elpreima 7086	. . . . . . . . . . . 12 ⊢ (𝑡 Fn 𝑋 → (𝑥 ∈ (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}) ↔ (𝑥 ∈ 𝑋 ∧ (𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘})))
54	40, 52, 53	3syl 19	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → (𝑥 ∈ (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}) ↔ (𝑥 ∈ 𝑋 ∧ (𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘})))
55	47, 51, 54	3bitr4d 314	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ 𝑥 ∈ (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘})))
56	55	eqrdv 2761	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} = (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}))
57		imaeq2 6064	. . . . . . . . . . 11 ⊢ (𝑥 = {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} → (◡𝑡 “ 𝑥) = (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}))
58	57	eleq1d 2849	. . . . . . . . . 10 ⊢ (𝑥 = {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} → ((◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽) ↔ (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}) ∈ (Clsd‘𝐽)))
59	38	simprd 501	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽))
60	59	adantlr 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽))
61		nnre 12380	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
62	61	ad2antlr 740	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → 𝑘 ∈ ℝ)
63	62	rexrd 11396	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → 𝑘 ∈ ℝ*)
64		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (0vec‘𝑊) = (0vec‘𝑊)
65	30, 64	nvzcl 31282	. . . . . . . . . . . . 13 ⊢ (𝑊 ∈ NrmCVec → (0vec‘𝑊) ∈ (BaseSet‘𝑊))
66	20, 65	ax-mp 5	. . . . . . . . . . . 12 ⊢ (0vec‘𝑊) ∈ (BaseSet‘𝑊)
67		ubth.2	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑁 = (normCV‘𝑊)
68	30, 64, 67, 13	nvnd 31336	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ NrmCVec ∧ 𝑦 ∈ (BaseSet‘𝑊)) → (𝑁‘𝑦) = (𝑦(IndMet‘𝑊)(0vec‘𝑊)))
69	20, 68	mpan 703	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (BaseSet‘𝑊) → (𝑁‘𝑦) = (𝑦(IndMet‘𝑊)(0vec‘𝑊)))
70		xmetsym 24710	. . . . . . . . . . . . . . . . 17 ⊢ (((IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊)) ∧ (0vec‘𝑊) ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊)) → ((0vec‘𝑊)(IndMet‘𝑊)𝑦) = (𝑦(IndMet‘𝑊)(0vec‘𝑊)))
71	32, 66, 70	mp3an12 1481	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (BaseSet‘𝑊) → ((0vec‘𝑊)(IndMet‘𝑊)𝑦) = (𝑦(IndMet‘𝑊)(0vec‘𝑊)))
72	69, 71	eqtr4d 2801	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (BaseSet‘𝑊) → (𝑁‘𝑦) = ((0vec‘𝑊)(IndMet‘𝑊)𝑦))
73	72	breq1d 5116	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (BaseSet‘𝑊) → ((𝑁‘𝑦) ≤ 𝑘 ↔ ((0vec‘𝑊)(IndMet‘𝑊)𝑦) ≤ 𝑘))
74	73	rabbiia 3420	. . . . . . . . . . . . 13 ⊢ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} = {𝑦 ∈ (BaseSet‘𝑊) ∣ ((0vec‘𝑊)(IndMet‘𝑊)𝑦) ≤ 𝑘}
75	15, 74	blcld 24868	. . . . . . . . . . . 12 ⊢ (((IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊)) ∧ (0vec‘𝑊) ∈ (BaseSet‘𝑊) ∧ 𝑘 ∈ ℝ*) → {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊))))
76	32, 66, 75	mp3an12 1481	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℝ* → {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊))))
77	63, 76	syl 18	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊))))
78	58, 60, 77	rspcdva 3581	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}) ∈ (Clsd‘𝐽))
79	56, 78	eqeltrd 2864	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
80	79	ralrimiva 3158	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∀𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
81		iincld 23401	. . . . . . 7 ⊢ ((𝑇 ≠ ∅ ∧ ∀𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽)) → ∩ 𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
82	9, 80, 81	syl2anr 609	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑇 ≠ ∅) → ∩ 𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
83	8, 82	eqeltrrd 2865	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑇 ≠ ∅) → {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
84	14	mopntop 24803	. . . . . . . 8 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
85	27, 84	ax-mp 5	. . . . . . 7 ⊢ 𝐽 ∈ Top
86	29	toponunii 23278	. . . . . . . 8 ⊢ 𝑋 = ∪ 𝐽
87	86	topcld 23397	. . . . . . 7 ⊢ (𝐽 ∈ Top → 𝑋 ∈ (Clsd‘𝐽))
88	85, 87	ax-mp 5	. . . . . 6 ⊢ 𝑋 ∈ (Clsd‘𝐽)
89	88	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑋 ∈ (Clsd‘𝐽))
90	6, 83, 89	pm2.61ne 3044	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
91		ubthlem.9	. . . 4 ⊢ 𝐴 = (𝑘 ∈ ℕ ↦ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})
92	90, 91	fmptd 7144	. . 3 ⊢ (𝜑 → 𝐴:ℕ⟶(Clsd‘𝐽))
93	92	frnd 6746	. . . . . 6 ⊢ (𝜑 → ran 𝐴 ⊆ (Clsd‘𝐽))
94	86	cldss2 23392	. . . . . 6 ⊢ (Clsd‘𝐽) ⊆ 𝒫 𝑋
95	93, 94	sstrdi 3925	. . . . 5 ⊢ (𝜑 → ran 𝐴 ⊆ 𝒫 𝑋)
96		sspwuni 5063	. . . . 5 ⊢ (ran 𝐴 ⊆ 𝒫 𝑋 ↔ ∪ ran 𝐴 ⊆ 𝑋)
97	95, 96	sylib 221	. . . 4 ⊢ (𝜑 → ∪ ran 𝐴 ⊆ 𝑋)
98		ubthlem.8	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐)
99		arch 12641	. . . . . . . . . 10 ⊢ (𝑐 ∈ ℝ → ∃𝑘 ∈ ℕ 𝑐 < 𝑘)
100	99	adantl 487	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) → ∃𝑘 ∈ ℕ 𝑐 < 𝑘)
101		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) → 𝑐 ∈ ℝ)
102		ltle 11435	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝑐 < 𝑘 → 𝑐 ≤ 𝑘))
103	101, 61, 102	syl2an 608	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (𝑐 < 𝑘 → 𝑐 ≤ 𝑘))
104	103	impr 460	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) → 𝑐 ≤ 𝑘)
105	104	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → 𝑐 ≤ 𝑘)
106	39	ffvelcdmda 7114	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑡‘𝑥) ∈ (BaseSet‘𝑊))
107	106	an32s 665	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑡 ∈ 𝑇) → (𝑡‘𝑥) ∈ (BaseSet‘𝑊))
108	30, 67	nvcl 31309	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ NrmCVec ∧ (𝑡‘𝑥) ∈ (BaseSet‘𝑊)) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ)
109	20, 107, 108	sylancr 599	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑡 ∈ 𝑇) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ)
110	109	adantlr 728	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑡 ∈ 𝑇) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ)
111	110	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ)
112		simpllr 788	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → 𝑐 ∈ ℝ)
113		simplrl 789	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → 𝑘 ∈ ℕ)
114	113, 61	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → 𝑘 ∈ ℝ)
115		letr 11441	. . . . . . . . . . . . . . 15 ⊢ (((𝑁‘(𝑡‘𝑥)) ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (((𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ∧ 𝑐 ≤ 𝑘) → (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
116	111, 112, 114, 115	syl3anc 1399	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → (((𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ∧ 𝑐 ≤ 𝑘) → (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
117	105, 116	mpan2d 707	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → ((𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
118	117	ralimdva 3178	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
119	118	expr 462	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (𝑐 < 𝑘 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)))
120	22	fvexi 6928	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑋 ∈ V
121	120	rabex 5305	. . . . . . . . . . . . . . . . 17 ⊢ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ V
122	91	fvmpt2 7034	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ V) → (𝐴‘𝑘) = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})
123	121, 122	mpan2 704	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → (𝐴‘𝑘) = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})
124	123	eleq2d 2850	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ → (𝑥 ∈ (𝐴‘𝑘) ↔ 𝑥 ∈ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘}))
125	49	ralbidv 3189	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑥 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘 ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
126	125	elrab 3648	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
127	124, 126	bitrdi 290	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → (𝑥 ∈ (𝐴‘𝑘) ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)))
128		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋)
129	128	biantrurd 542	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘 ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)))
130	129	bicomd 226	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘) ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
131	127, 130	sylan9bbr 520	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ (𝐴‘𝑘) ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
132	92	ffnd 6738	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 Fn ℕ)
133	132	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 Fn ℕ)
134		fnfvelrn 7110	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝐴‘𝑘) ∈ ran 𝐴)
135		elssuni 4902	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴‘𝑘) ∈ ran 𝐴 → (𝐴‘𝑘) ⊆ ∪ ran 𝐴)
136	134, 135	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝐴‘𝑘) ⊆ ∪ ran 𝐴)
137	136	sseld 3912	. . . . . . . . . . . . . 14 ⊢ ((𝐴 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ (𝐴‘𝑘) → 𝑥 ∈ ∪ ran 𝐴))
138	133, 137	sylan 592	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ (𝐴‘𝑘) → 𝑥 ∈ ∪ ran 𝐴))
139	131, 138	sylbird 263	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ ℕ) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘 → 𝑥 ∈ ∪ ran 𝐴))
140	139	adantlr 728	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘 → 𝑥 ∈ ∪ ran 𝐴))
141	119, 140	syl6d 76	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (𝑐 < 𝑘 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → 𝑥 ∈ ∪ ran 𝐴)))
142	141	rexlimdva 3167	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) → (∃𝑘 ∈ ℕ 𝑐 < 𝑘 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → 𝑥 ∈ ∪ ran 𝐴)))
143	100, 142	mpd 16	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → 𝑥 ∈ ∪ ran 𝐴))
144	143	rexlimdva 3167	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → 𝑥 ∈ ∪ ran 𝐴))
145	144	ralimdva 3178	. . . . . 6 ⊢ (𝜑 → (∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → ∀𝑥 ∈ 𝑋 𝑥 ∈ ∪ ran 𝐴))
146	98, 145	mpd 16	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 𝑥 ∈ ∪ ran 𝐴)
147		dfss3 3902	. . . . 5 ⊢ (𝑋 ⊆ ∪ ran 𝐴 ↔ ∀𝑥 ∈ 𝑋 𝑥 ∈ ∪ ran 𝐴)
148	146, 147	sylibr 237	. . . 4 ⊢ (𝜑 → 𝑋 ⊆ ∪ ran 𝐴)
149	97, 148	eqssd 3930	. . 3 ⊢ (𝜑 → ∪ ran 𝐴 = 𝑋)
150		eqid 2763	. . . . . 6 ⊢ (0vec‘𝑈) = (0vec‘𝑈)
151	22, 150	nvzcl 31282	. . . . 5 ⊢ (𝑈 ∈ NrmCVec → (0vec‘𝑈) ∈ 𝑋)
152		ne0i 4290	. . . . 5 ⊢ ((0vec‘𝑈) ∈ 𝑋 → 𝑋 ≠ ∅)
153	19, 151, 152	mp2b 10	. . . 4 ⊢ 𝑋 ≠ ∅
154	14	bcth2 25695	. . . 4 ⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑋 ≠ ∅) ∧ (𝐴:ℕ⟶(Clsd‘𝐽) ∧ ∪ ran 𝐴 = 𝑋)) → ∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅)
155	24, 153, 154	mpanl12 715	. . 3 ⊢ ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ ∪ ran 𝐴 = 𝑋) → ∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅)
156	92, 149, 155	syl2anc 596	. 2 ⊢ (𝜑 → ∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅)
157		ffvelcdm 7111	. . . . . . . . . . 11 ⊢ ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ (Clsd‘𝐽))
158	94, 157	sselid 3911	. . . . . . . . . 10 ⊢ ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ 𝒫 𝑋)
159	158	elpwid 4569	. . . . . . . . 9 ⊢ ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ⊆ 𝑋)
160	92, 159	sylan 592	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ⊆ 𝑋)
161	86	ntrss3 23422	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ (𝐴‘𝑛) ⊆ 𝑋) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ 𝑋)
162	85, 160, 161	sylancr 599	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ 𝑋)
163	162	sseld 3912	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛)) → 𝑦 ∈ 𝑋))
164	86	ntropn 23411	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ (𝐴‘𝑛) ⊆ 𝑋) → ((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽)
165	85, 160, 164	sylancr 599	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽)
166	14	mopni2 24856	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽 ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → ∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)))
167	27, 166	mp3an1 1478	. . . . . . . . 9 ⊢ ((((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽 ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → ∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)))
168	165, 167	sylan 592	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → ∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)))
169		elssuni 4902	. . . . . . . . . . . 12 ⊢ (((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽 → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ ∪ 𝐽)
170	169, 86	sseqtrrdi 3954	. . . . . . . . . . 11 ⊢ (((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽 → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ 𝑋)
171	165, 170	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ 𝑋)
172	171	sselda 3913	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → 𝑦 ∈ 𝑋)
173	86	ntrss2 23419	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ (𝐴‘𝑛) ⊆ 𝑋) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ (𝐴‘𝑛))
174	85, 160, 173	sylancr 599	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ (𝐴‘𝑛))
175		sstr2 3920	. . . . . . . . . . . . 13 ⊢ ((𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → (((int‘𝐽)‘(𝐴‘𝑛)) ⊆ (𝐴‘𝑛) → (𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛)))
176	174, 175	syl5com 32	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → (𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛)))
177	176	ad2antrr 739	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → ((𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → (𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛)))
178		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋)
179	178, 27	jctil 529	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) → (𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋))
180		rphalfcl 13187	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ+ → (𝑥 / 2) ∈ ℝ+)
181	180	rpxrd 13203	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ+ → (𝑥 / 2) ∈ ℝ*)
182		rpxr 13168	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ*)
183		rphalflt 13189	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ+ → (𝑥 / 2) < 𝑥)
184	181, 182, 183	3jca 1146	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ+ → ((𝑥 / 2) ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ (𝑥 / 2) < 𝑥))
185		eqid 2763	. . . . . . . . . . . . . 14 ⊢ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} = {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)}
186	14, 185	blsscls2 24867	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ ((𝑥 / 2) ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ (𝑥 / 2) < 𝑥)) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝑦(ball‘𝐷)𝑥))
187	179, 184, 186	syl2an 608	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝑦(ball‘𝐷)𝑥))
188		sstr2 3920	. . . . . . . . . . . 12 ⊢ ({𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝑦(ball‘𝐷)𝑥) → ((𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛)))
189	187, 188	syl 18	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → ((𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛)))
190	180	adantl 487	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈ ℝ+)
191		breq2 5110	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = (𝑥 / 2) → ((𝑦𝐷𝑧) ≤ 𝑟 ↔ (𝑦𝐷𝑧) ≤ (𝑥 / 2)))
192	191	rabbidv 3423	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = (𝑥 / 2) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} = {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)})
193	192	sseq1d 3944	. . . . . . . . . . . . . 14 ⊢ (𝑟 = (𝑥 / 2) → ({𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛) ↔ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛)))
194	193	rspcev 3580	. . . . . . . . . . . . 13 ⊢ (((𝑥 / 2) ∈ ℝ+ ∧ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))
195	194	ex 418	. . . . . . . . . . . 12 ⊢ ((𝑥 / 2) ∈ ℝ+ → ({𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
196	190, 195	syl 18	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → ({𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
197	177, 189, 196	3syld 61	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → ((𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
198	197	rexlimdva 3167	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) → (∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
199	172, 198	syldan 603	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → (∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
200	168, 199	mpd 16	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))
201	200	ex 418	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
202	163, 201	jcad 522	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛)) → (𝑦 ∈ 𝑋 ∧ ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))))
203	202	eximdv 1952	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∃𝑦 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛)) → ∃𝑦(𝑦 ∈ 𝑋 ∧ ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))))
204		n0 4303	. . . 4 ⊢ (((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛)))
205		df-rex 3091	. . . 4 ⊢ (∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛) ↔ ∃𝑦(𝑦 ∈ 𝑋 ∧ ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
206	203, 204, 205	3imtr4g 299	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅ → ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
207	206	reximdva 3179	. 2 ⊢ (𝜑 → (∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅ → ∃𝑛 ∈ ℕ ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
208	156, 207	mpd 16	1 ⊢ (𝜑 → ∃𝑛 ∈ ℕ ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080  ∃wrex 3090  {crab 3416  Vcvv 3454   ⊆ wss 3900  ∅c0 4281  𝒫 cpw 4560  ∪ cuni 4870  ∩ ciin 4955   class class class wbr 5106   ↦ cmpt 5190  ^◡ccnv 5655  ran crn 5657   “ cima 5659   Fn wfn 6559  ⟶wf 6560  ‘cfv 6564  (class class class)co 7449  ℝcr 11236  ℝ^*cxr 11379   < clt 11380   ≤ cle 11381   / cdiv 12011  ℕcn 12373  2c2 12435  ℝ⁺crp 13158  ∞Metcxmet 21705  Metcmet 21706  ballcbl 21707  MetOpencmopn 21710  Topctop 23255  TopOnctopon 23272  Clsdccld 23378  intcnt 23379   Cn ccn 23586  CMetccmet 25619  NrmCVeccnv 31232  BaseSetcba 31234  0_veccn0v 31236  norm_CVcnmcv 31238  IndMetcims 31239   BLnOp cblo 31390  CBanccbn 31510

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5236  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7781  ax-inf2 9677  ax-dc 10561  ax-cnex 11293  ax-resscn 11294  ax-1cn 11295  ax-icn 11296  ax-addcl 11297  ax-addrcl 11298  ax-mulcl 11299  ax-mulrcl 11300  ax-mulcom 11301  ax-addass 11302  ax-mulass 11303  ax-distr 11304  ax-i2m1 11305  ax-1ne0 11306  ax-1rid 11307  ax-rnegex 11308  ax-rrecex 11309  ax-cnre 11310  ax-pre-lttri 11311  ax-pre-lttrn 11312  ax-pre-ltadd 11313  ax-pre-mulgt0 11314  ax-pre-sup 11315  ax-addf 11316  ax-mulf 11317

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5107  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5551  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-we 5611  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-pred 6328  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6518  df-fun 6566  df-fn 6567  df-f 6568  df-f1 6569  df-fo 6570  df-f1o 6571  df-fv 6572  df-riota 7406  df-ov 7452  df-oprab 7453  df-mpo 7454  df-om 7910  df-1st 8033  df-2nd 8034  df-frecs 8335  df-wrecs 8366  df-recs 8415  df-rdg 8454  df-1o 8512  df-er 8753  df-map 8885  df-pm 8886  df-en 9010  df-dom 9011  df-sdom 9012  df-sup 9469  df-inf 9470  df-pnf 11382  df-mnf 11383  df-xr 11384  df-ltxr 11385  df-le 11386  df-sub 11580  df-neg 11581  df-div 12012  df-nn 12374  df-2 12443  df-3 12444  df-n0 12645  df-z 12732  df-uz 13004  df-q 13114  df-rp 13159  df-xneg 13279  df-xadd 13280  df-xmul 13281  df-ico 13520  df-seq 14183  df-exp 14243  df-cj 15307  df-re 15308  df-im 15309  df-sqrt 15443  df-abs 15444  df-rest 17634  df-topgen 17655  df-psmet 21712  df-xmet 21713  df-met 21714  df-bl 21715  df-mopn 21716  df-fbas 21717  df-fg 21718  df-top 23256  df-topon 23273  df-bases 23308  df-cld 23381  df-ntr 23382  df-cls 23383  df-nei 23460  df-cn 23589  df-cnp 23590  df-lm 23591  df-fil 24209  df-fm 24301  df-flim 24302  df-flf 24303  df-cfil 25620  df-cau 25621  df-cmet 25622  df-grpo 31141  df-gid 31142  df-ginv 31143  df-gdiv 31144  df-ablo 31193  df-vc 31207  df-nv 31240  df-va 31243  df-ba 31244  df-sm 31245  df-0v 31246  df-vs 31247  df-nmcv 31248  df-ims 31249  df-lno 31392  df-nmoo 31393  df-blo 31394  df-0o 31395  df-cbn 31511

This theorem is used by:  ubthlem3  31520