Theorem ubthlem1 30814

Description: Lemma for ubth 30817. 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 25228, 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 4460	. . . . . . . . 9 ⊢ (𝑇 = ∅ → ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘)
2	1	ralrimivw 3125	. . . . . . . 8 ⊢ (𝑇 = ∅ → ∀𝑧 ∈ 𝑋 ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘)
3		rabid2 3428	. . . . . . . 8 ⊢ (𝑋 = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ ∀𝑧 ∈ 𝑋 ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘)
4	2, 3	sylibr 234	. . . . . . 7 ⊢ (𝑇 = ∅ → 𝑋 = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})
5	4	eqcomd 2735	. . . . . 6 ⊢ (𝑇 = ∅ → {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} = 𝑋)
6	5	eleq1d 2813	. . . . 5 ⊢ (𝑇 = ∅ → ({𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽) ↔ 𝑋 ∈ (Clsd‘𝐽)))
7		iinrab 5018	. . . . . . 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 2729	. . . . . . . . . . . . . . . . . . . 20 ⊢ (IndMet‘𝑊) = (IndMet‘𝑊)
14		ubthlem.4	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐽 = (MetOpen‘𝐷)
15		eqid 2729	. . . . . . . . . . . . . . . . . . . 20 ⊢ (MetOpen‘(IndMet‘𝑊)) = (MetOpen‘(IndMet‘𝑊))
16		eqid 2729	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑈 BLnOp 𝑊) = (𝑈 BLnOp 𝑊)
17		ubthlem.5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑈 ∈ CBan
18		bnnv 30810	. . . . . . . . . . . . . . . . . . . . 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 30752	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ (𝑈 BLnOp 𝑊) → 𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))))
22		ubth.1	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑋 = (BaseSet‘𝑈)
23	22, 12	cbncms 30809	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑈 ∈ CBan → 𝐷 ∈ (CMet‘𝑋))
24	17, 23	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐷 ∈ (CMet‘𝑋)
25		cmetmet 25184	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
26		metxmet 24220	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
27	24, 25, 26	mp2b 10	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐷 ∈ (∞Met‘𝑋)
28	14	mopntopon 24325	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋))
29	27, 28	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐽 ∈ (TopOn‘𝑋)
30		eqid 2729	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (BaseSet‘𝑊) = (BaseSet‘𝑊)
31	30, 13	imsxmet 30636	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑊 ∈ NrmCVec → (IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊)))
32	20, 31	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊))
33	15	mopntopon 24325	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊)) → (MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊)))
34	32, 33	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊))
35		iscncl 23154	. . . . . . . . . . . . . . . . . . . 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 7018	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑡‘𝑥) ∈ (BaseSet‘𝑊))
42	41	biantrurd 532	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑁‘(𝑡‘𝑥)) ≤ 𝑘 ↔ ((𝑡‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)))
43		fveq2 6822	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑡‘𝑥) → (𝑁‘𝑦) = (𝑁‘(𝑡‘𝑥)))
44	43	breq1d 5102	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑡‘𝑥) → ((𝑁‘𝑦) ≤ 𝑘 ↔ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
45	44	elrab 3648	. . . . . . . . . . . . 13 ⊢ ((𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} ↔ ((𝑡‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
46	42, 45	bitr4di 289	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑁‘(𝑡‘𝑥)) ≤ 𝑘 ↔ (𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}))
47	46	pm5.32da 579	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → ((𝑥 ∈ 𝑋 ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘) ↔ (𝑥 ∈ 𝑋 ∧ (𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘})))
48		2fveq3 6827	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑥 → (𝑁‘(𝑡‘𝑧)) = (𝑁‘(𝑡‘𝑥)))
49	48	breq1d 5102	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑥 → ((𝑁‘(𝑡‘𝑧)) ≤ 𝑘 ↔ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
50	49	elrab 3648	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ (𝑥 ∈ 𝑋 ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
51	50	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ (𝑥 ∈ 𝑋 ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)))
52		ffn 6652	. . . . . . . . . . . 12 ⊢ (𝑡:𝑋⟶(BaseSet‘𝑊) → 𝑡 Fn 𝑋)
53		elpreima 6992	. . . . . . . . . . . 12 ⊢ (𝑡 Fn 𝑋 → (𝑥 ∈ (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}) ↔ (𝑥 ∈ 𝑋 ∧ (𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘})))
54	40, 52, 53	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → (𝑥 ∈ (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}) ↔ (𝑥 ∈ 𝑋 ∧ (𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘})))
55	47, 51, 54	3bitr4d 311	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ 𝑥 ∈ (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘})))
56	55	eqrdv 2727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} = (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}))
57		imaeq2 6007	. . . . . . . . . . 11 ⊢ (𝑥 = {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} → (◡𝑡 “ 𝑥) = (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}))
58	57	eleq1d 2813	. . . . . . . . . 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 12135	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
62	61	ad2antlr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → 𝑘 ∈ ℝ)
63	62	rexrd 11165	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → 𝑘 ∈ ℝ*)
64		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (0vec‘𝑊) = (0vec‘𝑊)
65	30, 64	nvzcl 30578	. . . . . . . . . . . . 13 ⊢ (𝑊 ∈ NrmCVec → (0vec‘𝑊) ∈ (BaseSet‘𝑊))
66	20, 65	ax-mp 5	. . . . . . . . . . . 12 ⊢ (0vec‘𝑊) ∈ (BaseSet‘𝑊)
67		ubth.2	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑁 = (normCV‘𝑊)
68	30, 64, 67, 13	nvnd 30632	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ NrmCVec ∧ 𝑦 ∈ (BaseSet‘𝑊)) → (𝑁‘𝑦) = (𝑦(IndMet‘𝑊)(0vec‘𝑊)))
69	20, 68	mpan 690	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (BaseSet‘𝑊) → (𝑁‘𝑦) = (𝑦(IndMet‘𝑊)(0vec‘𝑊)))
70		xmetsym 24233	. . . . . . . . . . . . . . . . 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 2767	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (BaseSet‘𝑊) → (𝑁‘𝑦) = ((0vec‘𝑊)(IndMet‘𝑊)𝑦))
73	72	breq1d 5102	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (BaseSet‘𝑊) → ((𝑁‘𝑦) ≤ 𝑘 ↔ ((0vec‘𝑊)(IndMet‘𝑊)𝑦) ≤ 𝑘))
74	73	rabbiia 3398	. . . . . . . . . . . . 13 ⊢ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} = {𝑦 ∈ (BaseSet‘𝑊) ∣ ((0vec‘𝑊)(IndMet‘𝑊)𝑦) ≤ 𝑘}
75	15, 74	blcld 24391	. . . . . . . . . . . 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 3578	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}) ∈ (Clsd‘𝐽))
79	56, 78	eqeltrd 2828	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
80	79	ralrimiva 3121	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∀𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
81		iincld 22924	. . . . . . 7 ⊢ ((𝑇 ≠ ∅ ∧ ∀𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽)) → ∩ 𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
82	9, 80, 81	syl2anr 597	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑇 ≠ ∅) → ∩ 𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
83	8, 82	eqeltrrd 2829	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑇 ≠ ∅) → {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
84	14	mopntop 24326	. . . . . . . 8 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
85	27, 84	ax-mp 5	. . . . . . 7 ⊢ 𝐽 ∈ Top
86	29	toponunii 22801	. . . . . . . 8 ⊢ 𝑋 = ∪ 𝐽
87	86	topcld 22920	. . . . . . 7 ⊢ (𝐽 ∈ Top → 𝑋 ∈ (Clsd‘𝐽))
88	85, 87	ax-mp 5	. . . . . 6 ⊢ 𝑋 ∈ (Clsd‘𝐽)
89	88	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑋 ∈ (Clsd‘𝐽))
90	6, 83, 89	pm2.61ne 3010	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
91		ubthlem.9	. . . 4 ⊢ 𝐴 = (𝑘 ∈ ℕ ↦ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})
92	90, 91	fmptd 7048	. . 3 ⊢ (𝜑 → 𝐴:ℕ⟶(Clsd‘𝐽))
93	92	frnd 6660	. . . . . 6 ⊢ (𝜑 → ran 𝐴 ⊆ (Clsd‘𝐽))
94	86	cldss2 22915	. . . . . 6 ⊢ (Clsd‘𝐽) ⊆ 𝒫 𝑋
95	93, 94	sstrdi 3948	. . . . 5 ⊢ (𝜑 → ran 𝐴 ⊆ 𝒫 𝑋)
96		sspwuni 5049	. . . . 5 ⊢ (ran 𝐴 ⊆ 𝒫 𝑋 ↔ ∪ ran 𝐴 ⊆ 𝑋)
97	95, 96	sylib 218	. . . 4 ⊢ (𝜑 → ∪ ran 𝐴 ⊆ 𝑋)
98		ubthlem.8	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐)
99		arch 12381	. . . . . . . . . 10 ⊢ (𝑐 ∈ ℝ → ∃𝑘 ∈ ℕ 𝑐 < 𝑘)
100	99	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) → ∃𝑘 ∈ ℕ 𝑐 < 𝑘)
101		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) → 𝑐 ∈ ℝ)
102		ltle 11204	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝑐 < 𝑘 → 𝑐 ≤ 𝑘))
103	101, 61, 102	syl2an 596	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (𝑐 < 𝑘 → 𝑐 ≤ 𝑘))
104	103	impr 454	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) → 𝑐 ≤ 𝑘)
105	104	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → 𝑐 ≤ 𝑘)
106	39	ffvelcdmda 7018	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑡‘𝑥) ∈ (BaseSet‘𝑊))
107	106	an32s 652	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑡 ∈ 𝑇) → (𝑡‘𝑥) ∈ (BaseSet‘𝑊))
108	30, 67	nvcl 30605	. . . . . . . . . . . . . . . . . 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 11210	. . . . . . . . . . . . . . 15 ⊢ (((𝑁‘(𝑡‘𝑥)) ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (((𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ∧ 𝑐 ≤ 𝑘) → (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
116	111, 112, 114, 115	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → (((𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ∧ 𝑐 ≤ 𝑘) → (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
117	105, 116	mpan2d 694	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → ((𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
118	117	ralimdva 3141	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))
119	118	expr 456	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (𝑐 < 𝑘 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)))
120	22	fvexi 6836	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑋 ∈ V
121	120	rabex 5278	. . . . . . . . . . . . . . . . 17 ⊢ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ V
122	91	fvmpt2 6941	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ V) → (𝐴‘𝑘) = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})
123	121, 122	mpan2 691	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → (𝐴‘𝑘) = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})
124	123	eleq2d 2814	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ → (𝑥 ∈ (𝐴‘𝑘) ↔ 𝑥 ∈ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘}))
125	49	ralbidv 3152	. . . . . . . . . . . . . . . 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 6653	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 Fn ℕ)
133	132	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 Fn ℕ)
134		fnfvelrn 7014	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝐴‘𝑘) ∈ ran 𝐴)
135		elssuni 4888	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴‘𝑘) ∈ ran 𝐴 → (𝐴‘𝑘) ⊆ ∪ ran 𝐴)
136	134, 135	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝐴‘𝑘) ⊆ ∪ ran 𝐴)
137	136	sseld 3934	. . . . . . . . . . . . . 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 3130	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) → (∃𝑘 ∈ ℕ 𝑐 < 𝑘 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → 𝑥 ∈ ∪ ran 𝐴)))
143	100, 142	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → 𝑥 ∈ ∪ ran 𝐴))
144	143	rexlimdva 3130	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → 𝑥 ∈ ∪ ran 𝐴))
145	144	ralimdva 3141	. . . . . 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 2729	. . . . . 6 ⊢ (0vec‘𝑈) = (0vec‘𝑈)
151	22, 150	nvzcl 30578	. . . . 5 ⊢ (𝑈 ∈ NrmCVec → (0vec‘𝑈) ∈ 𝑋)
152		ne0i 4292	. . . . 5 ⊢ ((0vec‘𝑈) ∈ 𝑋 → 𝑋 ≠ ∅)
153	19, 151, 152	mp2b 10	. . . 4 ⊢ 𝑋 ≠ ∅
154	14	bcth2 25228	. . . 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 7015	. . . . . . . . . . 11 ⊢ ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ (Clsd‘𝐽))
158	94, 157	sselid 3933	. . . . . . . . . 10 ⊢ ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ 𝒫 𝑋)
159	158	elpwid 4560	. . . . . . . . 9 ⊢ ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ⊆ 𝑋)
160	92, 159	sylan 580	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ⊆ 𝑋)
161	86	ntrss3 22945	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ (𝐴‘𝑛) ⊆ 𝑋) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ 𝑋)
162	85, 160, 161	sylancr 587	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ 𝑋)
163	162	sseld 3934	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛)) → 𝑦 ∈ 𝑋))
164	86	ntropn 22934	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ (𝐴‘𝑛) ⊆ 𝑋) → ((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽)
165	85, 160, 164	sylancr 587	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽)
166	14	mopni2 24379	. . . . . . . . . 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 4888	. . . . . . . . . . . 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 22942	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ (𝐴‘𝑛) ⊆ 𝑋) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ (𝐴‘𝑛))
174	85, 160, 173	sylancr 587	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ (𝐴‘𝑛))
175		sstr2 3942	. . . . . . . . . . . . 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 12922	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ+ → (𝑥 / 2) ∈ ℝ+)
181	180	rpxrd 12938	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ+ → (𝑥 / 2) ∈ ℝ*)
182		rpxr 12903	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ*)
183		rphalflt 12924	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ+ → (𝑥 / 2) < 𝑥)
184	181, 182, 183	3jca 1128	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ+ → ((𝑥 / 2) ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ (𝑥 / 2) < 𝑥))
185		eqid 2729	. . . . . . . . . . . . . 14 ⊢ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} = {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)}
186	14, 185	blsscls2 24390	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ ((𝑥 / 2) ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ (𝑥 / 2) < 𝑥)) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝑦(ball‘𝐷)𝑥))
187	179, 184, 186	syl2an 596	. . . . . . . . . . . 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 5096	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = (𝑥 / 2) → ((𝑦𝐷𝑧) ≤ 𝑟 ↔ (𝑦𝐷𝑧) ≤ (𝑥 / 2)))
192	191	rabbidv 3402	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = (𝑥 / 2) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} = {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)})
193	192	sseq1d 3967	. . . . . . . . . . . . . 14 ⊢ (𝑟 = (𝑥 / 2) → ({𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛) ↔ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛)))
194	193	rspcev 3577	. . . . . . . . . . . . 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 3130	. . . . . . . . 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 1917	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∃𝑦 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛)) → ∃𝑦(𝑦 ∈ 𝑋 ∧ ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))))
204		n0 4304	. . . 4 ⊢ (((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛)))
205		df-rex 3054	. . . 4 ⊢ (∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛) ↔ ∃𝑦(𝑦 ∈ 𝑋 ∧ ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
206	203, 204, 205	3imtr4g 296	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅ → ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
207	206	reximdva 3142	. 2 ⊢ (𝜑 → (∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅ → ∃𝑛 ∈ ℕ ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))
208	156, 207	mpd 15	1 ⊢ (𝜑 → ∃𝑛 ∈ ℕ ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  {crab 3394  Vcvv 3436   ⊆ wss 3903  ∅c0 4284  𝒫 cpw 4551  ∪ cuni 4858  ∩ ciin 4942   class class class wbr 5092   ↦ cmpt 5173  ^◡ccnv 5618  ran crn 5620   “ cima 5622   Fn wfn 6477  ⟶wf 6478  ‘cfv 6482  (class class class)co 7349  ℝcr 11008  ℝ^*cxr 11148   < clt 11149   ≤ cle 11150   / cdiv 11777  ℕcn 12128  2c2 12183  ℝ⁺crp 12893  ∞Metcxmet 21246  Metcmet 21247  ballcbl 21248  MetOpencmopn 21251  Topctop 22778  TopOnctopon 22795  Clsdccld 22901  intcnt 22902   Cn ccn 23109  CMetccmet 25152  NrmCVeccnv 30528  BaseSetcba 30530  0_veccn0v 30532  norm_CVcnmcv 30534  IndMetcims 30535   BLnOp cblo 30686  CBanccbn 30806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5218  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-inf2 9537  ax-dc 10340  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086  ax-pre-sup 11087  ax-addf 11088  ax-mulf 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-int 4897  df-iun 4943  df-iin 4944  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-1st 7924  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-1o 8388  df-er 8625  df-map 8755  df-pm 8756  df-en 8873  df-dom 8874  df-sdom 8875  df-sup 9332  df-inf 9333  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-div 11778  df-nn 12129  df-2 12191  df-3 12192  df-n0 12385  df-z 12472  df-uz 12736  df-q 12850  df-rp 12894  df-xneg 13014  df-xadd 13015  df-xmul 13016  df-ico 13254  df-seq 13909  df-exp 13969  df-cj 15006  df-re 15007  df-im 15008  df-sqrt 15142  df-abs 15143  df-rest 17326  df-topgen 17347  df-psmet 21253  df-xmet 21254  df-met 21255  df-bl 21256  df-mopn 21257  df-fbas 21258  df-fg 21259  df-top 22779  df-topon 22796  df-bases 22831  df-cld 22904  df-ntr 22905  df-cls 22906  df-nei 22983  df-cn 23112  df-cnp 23113  df-lm 23114  df-fil 23731  df-fm 23823  df-flim 23824  df-flf 23825  df-cfil 25153  df-cau 25154  df-cmet 25155  df-grpo 30437  df-gid 30438  df-ginv 30439  df-gdiv 30440  df-ablo 30489  df-vc 30503  df-nv 30536  df-va 30539  df-ba 30540  df-sm 30541  df-0v 30542  df-vs 30543  df-nmcv 30544  df-ims 30545  df-lno 30688  df-nmoo 30689  df-blo 30690  df-0o 30691  df-cbn 30807

This theorem is referenced by:  ubthlem3  30816