bcthlem2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > bcthlem2		Structured version Visualization version GIF version

Theorem bcthlem2 23122

Description: Lemma for bcth 23126. The balls in the sequence form an inclusion chain. (Contributed by Mario Carneiro, 7-Jan-2014.)

**Hypotheses**
Ref	Expression
bcth.2	⊢ 𝐽 = (MetOpen‘𝐷)
bcthlem.4	⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))
bcthlem.5	⊢ 𝐹 = (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ⁺) ↦ {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))})
bcthlem.6	⊢ (𝜑 → 𝑀:ℕ⟶(Clsd‘𝐽))
bcthlem.7	⊢ (𝜑 → 𝑅 ∈ ℝ⁺)
bcthlem.8	⊢ (𝜑 → 𝐶 ∈ 𝑋)
bcthlem.9	⊢ (𝜑 → 𝑔:ℕ⟶(𝑋 × ℝ⁺))
bcthlem.10	⊢ (𝜑 → (𝑔‘1) = ⟨𝐶, 𝑅⟩)
bcthlem.11	⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘)))

**Assertion**
Ref	Expression
bcthlem2	⊢ (𝜑 → ∀𝑛 ∈ ℕ ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝑔‘𝑛)))

Distinct variable groups: 𝑘,𝑛,𝑟,𝑥,𝑧 𝐶,𝑟,𝑥 𝑔,𝑘,𝑛,𝑟,𝑥,𝑧,𝐷 𝑔,𝐹,𝑘,𝑛,𝑟,𝑥,𝑧 𝑔,𝐽,𝑘,𝑛,𝑟,𝑥,𝑧 𝑔,𝑀,𝑘,𝑛,𝑟,𝑥,𝑧 𝜑,𝑘,𝑛,𝑟,𝑥,𝑧 𝑥,𝑅 𝑔,𝑋,𝑘,𝑛,𝑟,𝑥,𝑧 Allowed substitution hints: 𝜑(𝑔) 𝐶(𝑧,𝑔,𝑘,𝑛) 𝑅(𝑧,𝑔,𝑘,𝑛,𝑟)

**Proof of Theorem bcthlem2**
Step	Hyp	Ref	Expression
1		bcthlem.11	. . . . 5 ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘)))
2		oveq1 6657	. . . . . . . 8 ⊢ (𝑘 = 𝑛 → (𝑘 + 1) = (𝑛 + 1))
3	2	fveq2d 6195	. . . . . . 7 ⊢ (𝑘 = 𝑛 → (𝑔‘(𝑘 + 1)) = (𝑔‘(𝑛 + 1)))
4		id 22	. . . . . . . 8 ⊢ (𝑘 = 𝑛 → 𝑘 = 𝑛)
5		fveq2 6191	. . . . . . . 8 ⊢ (𝑘 = 𝑛 → (𝑔‘𝑘) = (𝑔‘𝑛))
6	4, 5	oveq12d 6668	. . . . . . 7 ⊢ (𝑘 = 𝑛 → (𝑘𝐹(𝑔‘𝑘)) = (𝑛𝐹(𝑔‘𝑛)))
7	3, 6	eleq12d 2695	. . . . . 6 ⊢ (𝑘 = 𝑛 → ((𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘)) ↔ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛))))
8	7	rspccva 3308	. . . . 5 ⊢ ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘)) ∧ 𝑛 ∈ ℕ) → (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))
9	1, 8	sylan 488	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)))
10		bcthlem.9	. . . . . 6 ⊢ (𝜑 → 𝑔:ℕ⟶(𝑋 × ℝ⁺))
11	10	ffvelrnda 6359	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑔‘𝑛) ∈ (𝑋 × ℝ⁺))
12		bcth.2	. . . . . . 7 ⊢ 𝐽 = (MetOpen‘𝐷)
13		bcthlem.4	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))
14		bcthlem.5	. . . . . . 7 ⊢ 𝐹 = (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ⁺) ↦ {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))})
15	12, 13, 14	bcthlem1 23121	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (𝑔‘𝑛) ∈ (𝑋 × ℝ⁺))) → ((𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)) ↔ ((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ⁺) ∧ (2^nd ‘(𝑔‘(𝑛 + 1))) < (1 / 𝑛) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔‘𝑛)) ∖ (𝑀‘𝑛)))))
16	15	expr 643	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑔‘𝑛) ∈ (𝑋 × ℝ⁺) → ((𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)) ↔ ((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ⁺) ∧ (2^nd ‘(𝑔‘(𝑛 + 1))) < (1 / 𝑛) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔‘𝑛)) ∖ (𝑀‘𝑛))))))
17	11, 16	mpd 15	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔‘𝑛)) ↔ ((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ⁺) ∧ (2^nd ‘(𝑔‘(𝑛 + 1))) < (1 / 𝑛) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔‘𝑛)) ∖ (𝑀‘𝑛)))))
18	9, 17	mpbid 222	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ⁺) ∧ (2^nd ‘(𝑔‘(𝑛 + 1))) < (1 / 𝑛) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔‘𝑛)) ∖ (𝑀‘𝑛))))
19		cmetmet 23084	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
20	13, 19	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
21		metxmet 22139	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
22	20, 21	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
23	12	mopntop 22245	. . . . . . . . . . 11 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
24	22, 23	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ Top)
25	24	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ⁺)) → 𝐽 ∈ Top)
26		xp1st 7198	. . . . . . . . . . . 12 ⊢ ((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ⁺) → (1^st ‘(𝑔‘(𝑛 + 1))) ∈ 𝑋)
27		xp2nd 7199	. . . . . . . . . . . . 13 ⊢ ((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ⁺) → (2^nd ‘(𝑔‘(𝑛 + 1))) ∈ ℝ⁺)
28	27	rpxrd 11873	. . . . . . . . . . . 12 ⊢ ((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ⁺) → (2^nd ‘(𝑔‘(𝑛 + 1))) ∈ ℝ^*)
29	26, 28	jca 554	. . . . . . . . . . 11 ⊢ ((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ⁺) → ((1^st ‘(𝑔‘(𝑛 + 1))) ∈ 𝑋 ∧ (2^nd ‘(𝑔‘(𝑛 + 1))) ∈ ℝ^*))
30		blssm 22223	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (1^st ‘(𝑔‘(𝑛 + 1))) ∈ 𝑋 ∧ (2^nd ‘(𝑔‘(𝑛 + 1))) ∈ ℝ^*) → ((1^st ‘(𝑔‘(𝑛 + 1)))(ball‘𝐷)(2^nd ‘(𝑔‘(𝑛 + 1)))) ⊆ 𝑋)
31	30	3expb 1266	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((1^st ‘(𝑔‘(𝑛 + 1))) ∈ 𝑋 ∧ (2^nd ‘(𝑔‘(𝑛 + 1))) ∈ ℝ^*)) → ((1^st ‘(𝑔‘(𝑛 + 1)))(ball‘𝐷)(2^nd ‘(𝑔‘(𝑛 + 1)))) ⊆ 𝑋)
32	22, 29, 31	syl2an 494	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ⁺)) → ((1^st ‘(𝑔‘(𝑛 + 1)))(ball‘𝐷)(2^nd ‘(𝑔‘(𝑛 + 1)))) ⊆ 𝑋)
33		1st2nd2 7205	. . . . . . . . . . . . 13 ⊢ ((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ⁺) → (𝑔‘(𝑛 + 1)) = ⟨(1^st ‘(𝑔‘(𝑛 + 1))), (2^nd ‘(𝑔‘(𝑛 + 1)))⟩)
34	33	fveq2d 6195	. . . . . . . . . . . 12 ⊢ ((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ⁺) → ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) = ((ball‘𝐷)‘⟨(1^st ‘(𝑔‘(𝑛 + 1))), (2^nd ‘(𝑔‘(𝑛 + 1)))⟩))
35		df-ov 6653	. . . . . . . . . . . 12 ⊢ ((1^st ‘(𝑔‘(𝑛 + 1)))(ball‘𝐷)(2^nd ‘(𝑔‘(𝑛 + 1)))) = ((ball‘𝐷)‘⟨(1^st ‘(𝑔‘(𝑛 + 1))), (2^nd ‘(𝑔‘(𝑛 + 1)))⟩)
36	34, 35	syl6reqr 2675	. . . . . . . . . . 11 ⊢ ((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ⁺) → ((1^st ‘(𝑔‘(𝑛 + 1)))(ball‘𝐷)(2^nd ‘(𝑔‘(𝑛 + 1)))) = ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))))
37	36	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ⁺)) → ((1^st ‘(𝑔‘(𝑛 + 1)))(ball‘𝐷)(2^nd ‘(𝑔‘(𝑛 + 1)))) = ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))))
38	12	mopnuni 22246	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽)
39	22, 38	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
40	39	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ⁺)) → 𝑋 = ∪ 𝐽)
41	32, 37, 40	3sstr3d 3647	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ⁺)) → ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ∪ 𝐽)
42		eqid 2622	. . . . . . . . . 10 ⊢ ∪ 𝐽 = ∪ 𝐽
43	42	sscls 20860	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ∪ 𝐽) → ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))))
44	25, 41, 43	syl2anc 693	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ⁺)) → ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))))
45		difss2 3739	. . . . . . . 8 ⊢ (((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔‘𝑛)) ∖ (𝑀‘𝑛)) → ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) ⊆ ((ball‘𝐷)‘(𝑔‘𝑛)))
46		sstr2 3610	. . . . . . . 8 ⊢ (((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) → (((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) ⊆ ((ball‘𝐷)‘(𝑔‘𝑛)) → ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝑔‘𝑛))))
47	44, 45, 46	syl2im 40	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ⁺)) → (((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔‘𝑛)) ∖ (𝑀‘𝑛)) → ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝑔‘𝑛))))
48	47	a1d 25	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ⁺)) → ((2^nd ‘(𝑔‘(𝑛 + 1))) < (1 / 𝑛) → (((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔‘𝑛)) ∖ (𝑀‘𝑛)) → ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝑔‘𝑛)))))
49	48	ex 450	. . . . 5 ⊢ (𝜑 → ((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ⁺) → ((2^nd ‘(𝑔‘(𝑛 + 1))) < (1 / 𝑛) → (((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔‘𝑛)) ∖ (𝑀‘𝑛)) → ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝑔‘𝑛))))))
50	49	3impd 1281	. . . 4 ⊢ (𝜑 → (((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ⁺) ∧ (2^nd ‘(𝑔‘(𝑛 + 1))) < (1 / 𝑛) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔‘𝑛)) ∖ (𝑀‘𝑛))) → ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝑔‘𝑛))))
51	50	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ⁺) ∧ (2^nd ‘(𝑔‘(𝑛 + 1))) < (1 / 𝑛) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔‘𝑛)) ∖ (𝑀‘𝑛))) → ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝑔‘𝑛))))
52	18, 51	mpd 15	. 2 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝑔‘𝑛)))
53	52	ralrimiva 2966	1 ⊢ (𝜑 → ∀𝑛 ∈ ℕ ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝑔‘𝑛)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ∀wral 2912 ∖ cdif 3571 ⊆ wss 3574 ⟨cop 4183 ∪ cuni 4436 class class class wbr 4653 {copab 4712 × cxp 5112 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 ↦ cmpt2 6652 1^st c1st 7166 2^nd c2nd 7167 1c1 9937 + caddc 9939 ℝ^*cxr 10073 < clt 10074 / cdiv 10684 ℕcn 11020 ℝ⁺crp 11832 ∞Metcxmt 19731 Metcme 19732 ballcbl 19733 MetOpencmopn 19736 Topctop 20698 Clsdccld 20820 clsccl 20822 CMetcms 23052

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-sup 8348 df-inf 8349 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-n0 11293 df-z 11378 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-topgen 16104 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-top 20699 df-topon 20716 df-bases 20750 df-cld 20823 df-cls 20825 df-cmet 23055

This theorem is referenced by: bcthlem3 23123 bcthlem4 23124

W3C validator