Theorem lmcau 23329

Description: Every convergent sequence in a metric space is a Cauchy sequence. Theorem 1.4-5 of [Kreyszig] p. 28. (Contributed by NM, 29-Jan-2008.) (Proof shortened by Mario Carneiro, 5-May-2014.)

Hypothesis

Ref	Expression
lmcau.1	⊢ 𝐽 = (MetOpen‘𝐷)

Assertion

Ref	Expression
lmcau	⊢ (𝐷 ∈ (∞Met‘𝑋) → dom (⇝𝑡‘𝐽) ⊆ (Cau‘𝐷))

Proof of Theorem lmcau

Dummy variables 𝑥 𝑦 𝑓 𝑗 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lmcau.1	. . . . 5 ⊢ 𝐽 = (MetOpen‘𝐷)
2	1	methaus 22544	. . . 4 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Haus)
3		lmfun 21405	. . . 4 ⊢ (𝐽 ∈ Haus → Fun (⇝𝑡‘𝐽))
4		funfvbrb 6475	. . . 4 ⊢ (Fun (⇝𝑡‘𝐽) → (𝑓 ∈ dom (⇝𝑡‘𝐽) ↔ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)))
5	2, 3, 4	3syl 18	. . 3 ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑓 ∈ dom (⇝𝑡‘𝐽) ↔ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)))
6		id 22	. . . . . . . 8 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
7	1, 6	lmmbr 23274	. . . . . . 7 ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓) ↔ (𝑓 ∈ (𝑋 ↑pm ℂ) ∧ ((⇝𝑡‘𝐽)‘𝑓) ∈ 𝑋 ∧ ∀𝑦 ∈ ℝ+ ∃𝑢 ∈ ran ℤ≥(𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)𝑦))))
8	7	biimpa 462	. . . . . 6 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) → (𝑓 ∈ (𝑋 ↑pm ℂ) ∧ ((⇝𝑡‘𝐽)‘𝑓) ∈ 𝑋 ∧ ∀𝑦 ∈ ℝ+ ∃𝑢 ∈ ran ℤ≥(𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)𝑦)))
9	8	simp1d 1136	. . . . 5 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) → 𝑓 ∈ (𝑋 ↑pm ℂ))
10		simprr 756	. . . . . . . 8 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))
11		simplll 758	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → 𝐷 ∈ (∞Met‘𝑋))
12	8	simp2d 1137	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) → ((⇝𝑡‘𝐽)‘𝑓) ∈ 𝑋)
13	12	ad2antrr 705	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → ((⇝𝑡‘𝐽)‘𝑓) ∈ 𝑋)
14		rpre 12041	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ)
15	14	ad2antlr 706	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → 𝑥 ∈ ℝ)
16		uzid 11907	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℤ → 𝑗 ∈ (ℤ≥‘𝑗))
17	16	ad2antrl 707	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → 𝑗 ∈ (ℤ≥‘𝑗))
18		fvres 6350	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (ℤ≥‘𝑗) → ((𝑓 ↾ (ℤ≥‘𝑗))‘𝑗) = (𝑓‘𝑗))
19	17, 18	syl 17	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → ((𝑓 ↾ (ℤ≥‘𝑗))‘𝑗) = (𝑓‘𝑗))
20	10, 17	ffvelrnd 6505	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → ((𝑓 ↾ (ℤ≥‘𝑗))‘𝑗) ∈ (((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))
21	19, 20	eqeltrrd 2851	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → (𝑓‘𝑗) ∈ (((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))
22		blhalf 22429	. . . . . . . . 9 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ ((⇝𝑡‘𝐽)‘𝑓) ∈ 𝑋) ∧ (𝑥 ∈ ℝ ∧ (𝑓‘𝑗) ∈ (((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → (((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)) ⊆ ((𝑓‘𝑗)(ball‘𝐷)𝑥))
23	11, 13, 15, 21, 22	syl22anc 1477	. . . . . . . 8 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → (((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)) ⊆ ((𝑓‘𝑗)(ball‘𝐷)𝑥))
24	10, 23	fssd 6198	. . . . . . 7 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℤ ∧ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))) → (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝐷)𝑥))
25		rphalfcl 12060	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ+ → (𝑥 / 2) ∈ ℝ+)
26	8	simp3d 1138	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) → ∀𝑦 ∈ ℝ+ ∃𝑢 ∈ ran ℤ≥(𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)𝑦))
27		oveq2 6803	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑥 / 2) → (((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)𝑦) = (((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))
28	27	feq3d 6171	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑥 / 2) → ((𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)𝑦) ↔ (𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2))))
29	28	rexbidv 3200	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑥 / 2) → (∃𝑢 ∈ ran ℤ≥(𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)𝑦) ↔ ∃𝑢 ∈ ran ℤ≥(𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2))))
30	29	rspcv 3456	. . . . . . . . . 10 ⊢ ((𝑥 / 2) ∈ ℝ+ → (∀𝑦 ∈ ℝ+ ∃𝑢 ∈ ran ℤ≥(𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)𝑦) → ∃𝑢 ∈ ran ℤ≥(𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2))))
31	25, 26, 30	syl2im 40	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ+ → ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) → ∃𝑢 ∈ ran ℤ≥(𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2))))
32	31	impcom 394	. . . . . . . 8 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) → ∃𝑢 ∈ ran ℤ≥(𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))
33		uzf 11895	. . . . . . . . 9 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
34		ffn 6184	. . . . . . . . 9 ⊢ (ℤ≥:ℤ⟶𝒫 ℤ → ℤ≥ Fn ℤ)
35		reseq2 5528	. . . . . . . . . . 11 ⊢ (𝑢 = (ℤ≥‘𝑗) → (𝑓 ↾ 𝑢) = (𝑓 ↾ (ℤ≥‘𝑗)))
36		id 22	. . . . . . . . . . 11 ⊢ (𝑢 = (ℤ≥‘𝑗) → 𝑢 = (ℤ≥‘𝑗))
37	35, 36	feq12d 6172	. . . . . . . . . 10 ⊢ (𝑢 = (ℤ≥‘𝑗) → ((𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)) ↔ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2))))
38	37	rexrn 6506	. . . . . . . . 9 ⊢ (ℤ≥ Fn ℤ → (∃𝑢 ∈ ran ℤ≥(𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)) ↔ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2))))
39	33, 34, 38	mp2b 10	. . . . . . . 8 ⊢ (∃𝑢 ∈ ran ℤ≥(𝑓 ↾ 𝑢):𝑢⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)) ↔ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))
40	32, 39	sylib 208	. . . . . . 7 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) → ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶(((⇝𝑡‘𝐽)‘𝑓)(ball‘𝐷)(𝑥 / 2)))
41	24, 40	reximddv 3166	. . . . . 6 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) ∧ 𝑥 ∈ ℝ+) → ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝐷)𝑥))
42	41	ralrimiva 3115	. . . . 5 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝐷)𝑥))
43		iscau 23292	. . . . . 6 ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑓 ∈ (Cau‘𝐷) ↔ (𝑓 ∈ (𝑋 ↑pm ℂ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝐷)𝑥))))
44	43	adantr 466	. . . . 5 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) → (𝑓 ∈ (Cau‘𝐷) ↔ (𝑓 ∈ (𝑋 ↑pm ℂ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝐷)𝑥))))
45	9, 42, 44	mpbir2and 692	. . . 4 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓)) → 𝑓 ∈ (Cau‘𝐷))
46	45	ex 397	. . 3 ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑓(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝑓) → 𝑓 ∈ (Cau‘𝐷)))
47	5, 46	sylbid 230	. 2 ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑓 ∈ dom (⇝𝑡‘𝐽) → 𝑓 ∈ (Cau‘𝐷)))
48	47	ssrdv 3758	1 ⊢ (𝐷 ∈ (∞Met‘𝑋) → dom (⇝𝑡‘𝐽) ⊆ (Cau‘𝐷))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   ∧ w3a 1071   = wceq 1631   ∈ wcel 2145  ∀wral 3061  ∃wrex 3062   ⊆ wss 3723  𝒫 cpw 4298   class class class wbr 4787  dom cdm 5250  ran crn 5251   ↾ cres 5252  Fun wfun 6024   Fn wfn 6025  ⟶wf 6026  ‘cfv 6030  (class class class)co 6795   ↑_pm cpm 8013  ℂcc 10139  ℝcr 10140   / cdiv 10889  2c2 11275  ℤcz 11583  ℤ_≥cuz 11892  ℝ⁺crp 12034  ∞Metcxmt 19945  ballcbl 19947  MetOpencmopn 19950  ⇝_𝑡clm 21250  Hauscha 21332  Caucca 23269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7099  ax-cnex 10197  ax-resscn 10198  ax-1cn 10199  ax-icn 10200  ax-addcl 10201  ax-addrcl 10202  ax-mulcl 10203  ax-mulrcl 10204  ax-mulcom 10205  ax-addass 10206  ax-mulass 10207  ax-distr 10208  ax-i2m1 10209  ax-1ne0 10210  ax-1rid 10211  ax-rnegex 10212  ax-rrecex 10213  ax-cnre 10214  ax-pre-lttri 10215  ax-pre-lttrn 10216  ax-pre-ltadd 10217  ax-pre-mulgt0 10218  ax-pre-sup 10219

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5822  df-ord 5868  df-on 5869  df-lim 5870  df-suc 5871  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-riota 6756  df-ov 6798  df-oprab 6799  df-mpt2 6800  df-om 7216  df-1st 7318  df-2nd 7319  df-wrecs 7562  df-recs 7624  df-rdg 7662  df-er 7899  df-map 8014  df-pm 8015  df-en 8113  df-dom 8114  df-sdom 8115  df-sup 8507  df-inf 8508  df-pnf 10281  df-mnf 10282  df-xr 10283  df-ltxr 10284  df-le 10285  df-sub 10473  df-neg 10474  df-div 10890  df-nn 11226  df-2 11284  df-n0 11499  df-z 11584  df-uz 11893  df-q 11996  df-rp 12035  df-xneg 12150  df-xadd 12151  df-xmul 12152  df-icc 12386  df-topgen 16311  df-psmet 19952  df-xmet 19953  df-met 19954  df-bl 19955  df-mopn 19956  df-top 20918  df-topon 20935  df-bases 20970  df-lm 21253  df-haus 21339  df-cau 23272

This theorem is referenced by:  hlimcaui  28432