Theorem heiborlem6 35974

Description: Lemma for heibor 35979. Since the sequence of balls connected by the function 𝑇 ensures that each ball nontrivially intersects with the next (since the empty set has a finite subcover, the intersection of any two successive balls in the sequence is nonempty), and each ball is half the size of the previous one, the distance between the centers is at most 3 / 2 times the size of the larger, and so if we expand each ball by a factor of 3 we get a nested sequence of balls. (Contributed by Jeff Madsen, 23-Jan-2014.)

Hypotheses

Ref	Expression
heibor.1	⊢ 𝐽 = (MetOpen‘𝐷)
heibor.3	⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}
heibor.4	⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}
heibor.5	⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))
heibor.6	⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))
heibor.7	⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))
heibor.8	⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛))
heibor.9	⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))
heibor.10	⊢ (𝜑 → 𝐶𝐺0)
heibor.11	⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))
heibor.12	⊢ 𝑀 = (𝑛 ∈ ℕ ↦ ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩)

Assertion

Ref	Expression
heiborlem6	⊢ (𝜑 → ∀𝑘 ∈ ℕ ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀‘𝑘)))

Distinct variable groups:   𝑥,𝑛,𝑦,𝑘,𝑢,𝐹   𝑘,𝐺,𝑥   𝜑,𝑘,𝑥   𝑘,𝑚,𝑣,𝑧,𝐷,𝑛,𝑢,𝑥,𝑦   𝑘,𝑀,𝑚,𝑢,𝑥,𝑦,𝑧   𝑇,𝑚,𝑛,𝑥,𝑦,𝑧   𝐵,𝑛,𝑢,𝑣,𝑦   𝑘,𝐽,𝑚,𝑛,𝑢,𝑣,𝑥,𝑦,𝑧   𝑈,𝑛,𝑢,𝑣,𝑥,𝑦,𝑧   𝑆,𝑘,𝑚,𝑛,𝑢,𝑣,𝑥,𝑦,𝑧   𝑘,𝑋,𝑚,𝑛,𝑢,𝑣,𝑥,𝑦,𝑧   𝐶,𝑚,𝑛,𝑢,𝑣,𝑦   𝑛,𝐾,𝑥,𝑦,𝑧   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑦,𝑧,𝑣,𝑢,𝑚,𝑛)   𝐵(𝑧,𝑘,𝑚)   𝐶(𝑥,𝑧,𝑘)   𝑇(𝑣,𝑢,𝑘)   𝑈(𝑘,𝑚)   𝐹(𝑧,𝑣,𝑚)   𝐺(𝑦,𝑧,𝑣,𝑢,𝑚,𝑛)   𝐾(𝑣,𝑢,𝑘,𝑚)   𝑀(𝑣,𝑛)

Proof of Theorem heiborlem6

Step	Hyp	Ref	Expression
1		nnnn0 12240	. . . 4 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
2		heibor.6	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))
3		cmetmet 24450	. . . . . . . 8 ⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
4	2, 3	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
5		metxmet 23487	. . . . . . 7 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
6	4, 5	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
7	6	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐷 ∈ (∞Met‘𝑋))
8		heibor.7	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))
9		inss1 4162	. . . . . . . . 9 ⊢ (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋
10		fss 6617	. . . . . . . . 9 ⊢ ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋) → 𝐹:ℕ0⟶𝒫 𝑋)
11	8, 9, 10	sylancl 586	. . . . . . . 8 ⊢ (𝜑 → 𝐹:ℕ0⟶𝒫 𝑋)
12		peano2nn0 12273	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
13		ffvelrn 6959	. . . . . . . 8 ⊢ ((𝐹:ℕ0⟶𝒫 𝑋 ∧ (𝑘 + 1) ∈ ℕ0) → (𝐹‘(𝑘 + 1)) ∈ 𝒫 𝑋)
14	11, 12, 13	syl2an 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘(𝑘 + 1)) ∈ 𝒫 𝑋)
15	14	elpwid 4544	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘(𝑘 + 1)) ⊆ 𝑋)
16		heibor.1	. . . . . . . . 9 ⊢ 𝐽 = (MetOpen‘𝐷)
17		heibor.3	. . . . . . . . 9 ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}
18		heibor.4	. . . . . . . . 9 ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}
19		heibor.5	. . . . . . . . 9 ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))
20		heibor.8	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛))
21		heibor.9	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))
22		heibor.10	. . . . . . . . 9 ⊢ (𝜑 → 𝐶𝐺0)
23		heibor.11	. . . . . . . . 9 ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))
24	16, 17, 18, 19, 2, 8, 20, 21, 22, 23	heiborlem4 35972	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ ℕ0) → (𝑆‘(𝑘 + 1))𝐺(𝑘 + 1))
25	12, 24	sylan2 593	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1))𝐺(𝑘 + 1))
26		fvex 6787	. . . . . . . . 9 ⊢ (𝑆‘(𝑘 + 1)) ∈ V
27		ovex 7308	. . . . . . . . 9 ⊢ (𝑘 + 1) ∈ V
28	16, 17, 18, 26, 27	heiborlem2 35970	. . . . . . . 8 ⊢ ((𝑆‘(𝑘 + 1))𝐺(𝑘 + 1) ↔ ((𝑘 + 1) ∈ ℕ0 ∧ (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)) ∧ ((𝑆‘(𝑘 + 1))𝐵(𝑘 + 1)) ∈ 𝐾))
29	28	simp2bi 1145	. . . . . . 7 ⊢ ((𝑆‘(𝑘 + 1))𝐺(𝑘 + 1) → (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)))
30	25, 29	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)))
31	15, 30	sseldd 3922	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) ∈ 𝑋)
32	11	ffvelrnda 6961	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) ∈ 𝒫 𝑋)
33	32	elpwid 4544	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) ⊆ 𝑋)
34	16, 17, 18, 19, 2, 8, 20, 21, 22, 23	heiborlem4 35972	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘𝑘)𝐺𝑘)
35		fvex 6787	. . . . . . . . 9 ⊢ (𝑆‘𝑘) ∈ V
36		vex 3436	. . . . . . . . 9 ⊢ 𝑘 ∈ V
37	16, 17, 18, 35, 36	heiborlem2 35970	. . . . . . . 8 ⊢ ((𝑆‘𝑘)𝐺𝑘 ↔ (𝑘 ∈ ℕ0 ∧ (𝑆‘𝑘) ∈ (𝐹‘𝑘) ∧ ((𝑆‘𝑘)𝐵𝑘) ∈ 𝐾))
38	37	simp2bi 1145	. . . . . . 7 ⊢ ((𝑆‘𝑘)𝐺𝑘 → (𝑆‘𝑘) ∈ (𝐹‘𝑘))
39	34, 38	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘𝑘) ∈ (𝐹‘𝑘))
40	33, 39	sseldd 3922	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘𝑘) ∈ 𝑋)
41		3re 12053	. . . . . 6 ⊢ 3 ∈ ℝ
42		2nn 12046	. . . . . . . . 9 ⊢ 2 ∈ ℕ
43		nnexpcl 13795	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ (𝑘 + 1) ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℕ)
44	42, 12, 43	sylancr 587	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) ∈ ℕ)
45	44	nnrpd 12770	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) ∈ ℝ+)
46	45	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℝ+)
47		rerpdivcl 12760	. . . . . 6 ⊢ ((3 ∈ ℝ ∧ (2↑(𝑘 + 1)) ∈ ℝ+) → (3 / (2↑(𝑘 + 1))) ∈ ℝ)
48	41, 46, 47	sylancr 587	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (3 / (2↑(𝑘 + 1))) ∈ ℝ)
49		nnexpcl 13795	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
50	42, 49	mpan 687	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → (2↑𝑘) ∈ ℕ)
51	50	nnrpd 12770	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 → (2↑𝑘) ∈ ℝ+)
52	51	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℝ+)
53		rerpdivcl 12760	. . . . . 6 ⊢ ((3 ∈ ℝ ∧ (2↑𝑘) ∈ ℝ+) → (3 / (2↑𝑘)) ∈ ℝ)
54	41, 52, 53	sylancr 587	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (3 / (2↑𝑘)) ∈ ℝ)
55		oveq1 7282	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝑆‘𝑘) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑚))))
56		oveq2 7283	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑘 → (2↑𝑚) = (2↑𝑘))
57	56	oveq2d 7291	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑘 → (1 / (2↑𝑚)) = (1 / (2↑𝑘)))
58	57	oveq2d 7291	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑘 → ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑚))) = ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
59		ovex 7308	. . . . . . . . . . . 12 ⊢ ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∈ V
60	55, 58, 19, 59	ovmpo 7433	. . . . . . . . . . 11 ⊢ (((𝑆‘𝑘) ∈ 𝑋 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐵𝑘) = ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
61	40, 60	sylancom 588	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐵𝑘) = ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
62		df-br 5075	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆‘𝑘)𝐺𝑘 ↔ ⟨(𝑆‘𝑘), 𝑘⟩ ∈ 𝐺)
63		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (𝑇‘𝑥) = (𝑇‘⟨(𝑆‘𝑘), 𝑘⟩))
64		df-ov 7278	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆‘𝑘)𝑇𝑘) = (𝑇‘⟨(𝑆‘𝑘), 𝑘⟩)
65	63, 64	eqtr4di 2796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (𝑇‘𝑥) = ((𝑆‘𝑘)𝑇𝑘))
66	35, 36	op2ndd 7842	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (2nd ‘𝑥) = 𝑘)
67	66	oveq1d 7290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → ((2nd ‘𝑥) + 1) = (𝑘 + 1))
68	65, 67	breq12d 5087	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ↔ ((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1)))
69		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (𝐵‘𝑥) = (𝐵‘⟨(𝑆‘𝑘), 𝑘⟩))
70		df-ov 7278	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆‘𝑘)𝐵𝑘) = (𝐵‘⟨(𝑆‘𝑘), 𝑘⟩)
71	69, 70	eqtr4di 2796	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (𝐵‘𝑥) = ((𝑆‘𝑘)𝐵𝑘))
72	65, 67	oveq12d 7293	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1)) = (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1)))
73	71, 72	ineq12d 4147	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) = (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))))
74	73	eleq1d 2823	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 ↔ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾))
75	68, 74	anbi12d 631	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) ↔ (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
76	75	rspccv 3558	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) → (⟨(𝑆‘𝑘), 𝑘⟩ ∈ 𝐺 → (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
77	21, 76	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (⟨(𝑆‘𝑘), 𝑘⟩ ∈ 𝐺 → (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
78	62, 77	syl5bi 241	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑆‘𝑘)𝐺𝑘 → (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
79	78	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐺𝑘 → (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
80	34, 79	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾))
81	80	simpld 495	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1))
82		ovex 7308	. . . . . . . . . . . . . . 15 ⊢ ((𝑆‘𝑘)𝑇𝑘) ∈ V
83	16, 17, 18, 82, 27	heiborlem2 35970	. . . . . . . . . . . . . 14 ⊢ (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ↔ ((𝑘 + 1) ∈ ℕ0 ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)) ∧ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1)) ∈ 𝐾))
84	83	simp2bi 1145	. . . . . . . . . . . . 13 ⊢ (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) → ((𝑆‘𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)))
85	81, 84	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)))
86	15, 85	sseldd 3922	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋)
87	12	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℕ0)
88		oveq1 7282	. . . . . . . . . . . 12 ⊢ (𝑧 = ((𝑆‘𝑘)𝑇𝑘) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑𝑚))))
89		oveq2 7283	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑘 + 1) → (2↑𝑚) = (2↑(𝑘 + 1)))
90	89	oveq2d 7291	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑘 + 1) → (1 / (2↑𝑚)) = (1 / (2↑(𝑘 + 1))))
91	90	oveq2d 7291	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑘 + 1) → (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑𝑚))) = (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
92		ovex 7308	. . . . . . . . . . . 12 ⊢ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))) ∈ V
93	88, 91, 19, 92	ovmpo 7433	. . . . . . . . . . 11 ⊢ ((((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋 ∧ (𝑘 + 1) ∈ ℕ0) → (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1)) = (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
94	86, 87, 93	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1)) = (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
95	61, 94	ineq12d 4147	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) = (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))))
96	80	simprd 496	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)
97		0elpw 5278	. . . . . . . . . . . . 13 ⊢ ∅ ∈ 𝒫 𝑈
98		0fin 8954	. . . . . . . . . . . . 13 ⊢ ∅ ∈ Fin
99		elin 3903	. . . . . . . . . . . . 13 ⊢ (∅ ∈ (𝒫 𝑈 ∩ Fin) ↔ (∅ ∈ 𝒫 𝑈 ∧ ∅ ∈ Fin))
100	97, 98, 99	mpbir2an 708	. . . . . . . . . . . 12 ⊢ ∅ ∈ (𝒫 𝑈 ∩ Fin)
101		0ss 4330	. . . . . . . . . . . 12 ⊢ ∅ ⊆ ∪ ∅
102		unieq 4850	. . . . . . . . . . . . . 14 ⊢ (𝑣 = ∅ → ∪ 𝑣 = ∪ ∅)
103	102	sseq2d 3953	. . . . . . . . . . . . 13 ⊢ (𝑣 = ∅ → (∅ ⊆ ∪ 𝑣 ↔ ∅ ⊆ ∪ ∅))
104	103	rspcev 3561	. . . . . . . . . . . 12 ⊢ ((∅ ∈ (𝒫 𝑈 ∩ Fin) ∧ ∅ ⊆ ∪ ∅) → ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣)
105	100, 101, 104	mp2an 689	. . . . . . . . . . 11 ⊢ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣
106		0ex 5231	. . . . . . . . . . . . 13 ⊢ ∅ ∈ V
107		sseq1 3946	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = ∅ → (𝑢 ⊆ ∪ 𝑣 ↔ ∅ ⊆ ∪ 𝑣))
108	107	rexbidv 3226	. . . . . . . . . . . . . 14 ⊢ (𝑢 = ∅ → (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣 ↔ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣))
109	108	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑢 = ∅ → (¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣))
110	106, 109, 17	elab2 3613	. . . . . . . . . . . 12 ⊢ (∅ ∈ 𝐾 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣)
111	110	con2bii 358	. . . . . . . . . . 11 ⊢ (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣 ↔ ¬ ∅ ∈ 𝐾)
112	105, 111	mpbi 229	. . . . . . . . . 10 ⊢ ¬ ∅ ∈ 𝐾
113		nelne2 3042	. . . . . . . . . 10 ⊢ (((((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾 ∧ ¬ ∅ ∈ 𝐾) → (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ≠ ∅)
114	96, 112, 113	sylancl 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ≠ ∅)
115	95, 114	eqnetrrd 3012	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) ≠ ∅)
116	51	rpreccld 12782	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 → (1 / (2↑𝑘)) ∈ ℝ+)
117	116	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ+)
118	117	rpred 12772	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ)
119	45	rpreccld 12782	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 → (1 / (2↑(𝑘 + 1))) ∈ ℝ+)
120	119	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ+)
121	120	rpred 12772	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ)
122		rexadd 12966	. . . . . . . . . . . 12 ⊢ (((1 / (2↑𝑘)) ∈ ℝ ∧ (1 / (2↑(𝑘 + 1))) ∈ ℝ) → ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
123	118, 121, 122	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
124	123	breq1d 5084	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ↔ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘))))
125	117	rpxrd 12773	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ*)
126	120	rpxrd 12773	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ*)
127		bldisj 23551	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆‘𝑘) ∈ 𝑋 ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋) ∧ ((1 / (2↑𝑘)) ∈ ℝ* ∧ (1 / (2↑(𝑘 + 1))) ∈ ℝ* ∧ ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)))) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅)
128	127	3exp2 1353	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆‘𝑘) ∈ 𝑋 ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋) → ((1 / (2↑𝑘)) ∈ ℝ* → ((1 / (2↑(𝑘 + 1))) ∈ ℝ* → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))))
129	128	imp32 419	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆‘𝑘) ∈ 𝑋 ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋) ∧ ((1 / (2↑𝑘)) ∈ ℝ* ∧ (1 / (2↑(𝑘 + 1))) ∈ ℝ*)) → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))
130	7, 40, 86, 125, 126, 129	syl32anc 1377	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))
131	124, 130	sylbird 259	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))
132	131	necon3ad 2956	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) ≠ ∅ → ¬ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘))))
133	115, 132	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ¬ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)))
134	117, 120	rpaddcld 12787	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ∈ ℝ+)
135	134	rpred 12772	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ∈ ℝ)
136	4	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐷 ∈ (Met‘𝑋))
137		metcl 23485	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝑆‘𝑘) ∈ 𝑋 ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋) → ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ∈ ℝ)
138	136, 40, 86, 137	syl3anc 1370	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ∈ ℝ)
139	135, 138	letrid 11127	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ∨ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ≤ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1))))))
140	139	ord 861	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (¬ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) → ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ≤ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1))))))
141	133, 140	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ≤ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
142		seqp1 13736	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ≥‘0) → (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1)) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
143		nn0uz 12620	. . . . . . . . . . . 12 ⊢ ℕ0 = (ℤ≥‘0)
144	142, 143	eleq2s 2857	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1)) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
145	23	fveq1i 6775	. . . . . . . . . . 11 ⊢ (𝑆‘(𝑘 + 1)) = (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1))
146	23	fveq1i 6775	. . . . . . . . . . . 12 ⊢ (𝑆‘𝑘) = (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)
147	146	oveq1i 7285	. . . . . . . . . . 11 ⊢ ((𝑆‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)))
148	144, 145, 147	3eqtr4g 2803	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → (𝑆‘(𝑘 + 1)) = ((𝑆‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
149		eqid 2738	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))) = (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))
150		eqeq1 2742	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑘 + 1) → (𝑚 = 0 ↔ (𝑘 + 1) = 0))
151		oveq1 7282	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑘 + 1) → (𝑚 − 1) = ((𝑘 + 1) − 1))
152	150, 151	ifbieq2d 4485	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑘 + 1) → if(𝑚 = 0, 𝐶, (𝑚 − 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)))
153		nn0p1nn 12272	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ)
154		nnne0 12007	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 + 1) ∈ ℕ → (𝑘 + 1) ≠ 0)
155	154	neneqd 2948	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 + 1) ∈ ℕ → ¬ (𝑘 + 1) = 0)
156	153, 155	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ0 → ¬ (𝑘 + 1) = 0)
157	156	iffalsed 4470	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 → if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)) = ((𝑘 + 1) − 1))
158		ovex 7308	. . . . . . . . . . . . . 14 ⊢ ((𝑘 + 1) − 1) ∈ V
159	157, 158	eqeltrdi 2847	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ0 → if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)) ∈ V)
160	149, 152, 12, 159	fvmptd3 6898	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)))
161		nn0cn 12243	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ)
162		ax-1cn 10929	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
163		pncan 11227	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
164	161, 162, 163	sylancl 586	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 → ((𝑘 + 1) − 1) = 𝑘)
165	160, 157, 164	3eqtrd 2782	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = 𝑘)
166	165	oveq2d 7291	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → ((𝑆‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))) = ((𝑆‘𝑘)𝑇𝑘))
167	148, 166	eqtrd 2778	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 → (𝑆‘(𝑘 + 1)) = ((𝑆‘𝑘)𝑇𝑘))
168	167	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) = ((𝑆‘𝑘)𝑇𝑘))
169	168	oveq1d 7290	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆‘𝑘)) = (((𝑆‘𝑘)𝑇𝑘)𝐷(𝑆‘𝑘)))
170		metsym 23503	. . . . . . . 8 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋 ∧ (𝑆‘𝑘) ∈ 𝑋) → (((𝑆‘𝑘)𝑇𝑘)𝐷(𝑆‘𝑘)) = ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)))
171	136, 86, 40, 170	syl3anc 1370	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝑇𝑘)𝐷(𝑆‘𝑘)) = ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)))
172	169, 171	eqtrd 2778	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆‘𝑘)) = ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)))
173		3cn 12054	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℂ
174	173	2timesi 12111	. . . . . . . . . . . 12 ⊢ (2 · 3) = (3 + 3)
175	174	oveq1i 7285	. . . . . . . . . . 11 ⊢ ((2 · 3) − 3) = ((3 + 3) − 3)
176	173, 173	pncan3oi 11237	. . . . . . . . . . 11 ⊢ ((3 + 3) − 3) = 3
177		df-3 12037	. . . . . . . . . . 11 ⊢ 3 = (2 + 1)
178	175, 176, 177	3eqtri 2770	. . . . . . . . . 10 ⊢ ((2 · 3) − 3) = (2 + 1)
179	178	oveq1i 7285	. . . . . . . . 9 ⊢ (((2 · 3) − 3) / (2↑(𝑘 + 1))) = ((2 + 1) / (2↑(𝑘 + 1)))
180		rpcn 12740	. . . . . . . . . . 11 ⊢ ((2↑(𝑘 + 1)) ∈ ℝ+ → (2↑(𝑘 + 1)) ∈ ℂ)
181		rpne0 12746	. . . . . . . . . . 11 ⊢ ((2↑(𝑘 + 1)) ∈ ℝ+ → (2↑(𝑘 + 1)) ≠ 0)
182		2cn 12048	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℂ
183	182, 173	mulcli 10982	. . . . . . . . . . . 12 ⊢ (2 · 3) ∈ ℂ
184		divsubdir 11669	. . . . . . . . . . . 12 ⊢ (((2 · 3) ∈ ℂ ∧ 3 ∈ ℂ ∧ ((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0)) → (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
185	183, 173, 184	mp3an12 1450	. . . . . . . . . . 11 ⊢ (((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0) → (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
186	180, 181, 185	syl2anc 584	. . . . . . . . . 10 ⊢ ((2↑(𝑘 + 1)) ∈ ℝ+ → (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
187	45, 186	syl 17	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 → (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
188		divdir 11658	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 1 ∈ ℂ ∧ ((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0)) → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
189	182, 162, 188	mp3an12 1450	. . . . . . . . . . 11 ⊢ (((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0) → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
190	180, 181, 189	syl2anc 584	. . . . . . . . . 10 ⊢ ((2↑(𝑘 + 1)) ∈ ℝ+ → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
191	45, 190	syl 17	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
192	179, 187, 191	3eqtr3a 2802	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
193		rpcn 12740	. . . . . . . . . . . 12 ⊢ ((2↑𝑘) ∈ ℝ+ → (2↑𝑘) ∈ ℂ)
194		rpne0 12746	. . . . . . . . . . . 12 ⊢ ((2↑𝑘) ∈ ℝ+ → (2↑𝑘) ≠ 0)
195		2cnne0 12183	. . . . . . . . . . . . 13 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
196		divcan5 11677	. . . . . . . . . . . . 13 ⊢ ((3 ∈ ℂ ∧ ((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
197	173, 195, 196	mp3an13 1451	. . . . . . . . . . . 12 ⊢ (((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
198	193, 194, 197	syl2anc 584	. . . . . . . . . . 11 ⊢ ((2↑𝑘) ∈ ℝ+ → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
199	51, 198	syl 17	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
200	51, 193	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ0 → (2↑𝑘) ∈ ℂ)
201		mulcom 10957	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ (2↑𝑘) ∈ ℂ) → (2 · (2↑𝑘)) = ((2↑𝑘) · 2))
202	182, 200, 201	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 → (2 · (2↑𝑘)) = ((2↑𝑘) · 2))
203		expp1 13789	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (2↑(𝑘 + 1)) = ((2↑𝑘) · 2))
204	182, 203	mpan 687	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) = ((2↑𝑘) · 2))
205	202, 204	eqtr4d 2781	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → (2 · (2↑𝑘)) = (2↑(𝑘 + 1)))
206	205	oveq2d 7291	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → ((2 · 3) / (2 · (2↑𝑘))) = ((2 · 3) / (2↑(𝑘 + 1))))
207	199, 206	eqtr3d 2780	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 → (3 / (2↑𝑘)) = ((2 · 3) / (2↑(𝑘 + 1))))
208	207	oveq1d 7290	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
209		divcan5 11677	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℂ ∧ ((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
210	162, 195, 209	mp3an13 1451	. . . . . . . . . . . 12 ⊢ (((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
211	193, 194, 210	syl2anc 584	. . . . . . . . . . 11 ⊢ ((2↑𝑘) ∈ ℝ+ → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
212	51, 211	syl 17	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
213		2t1e2 12136	. . . . . . . . . . . 12 ⊢ (2 · 1) = 2
214	213	a1i 11	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → (2 · 1) = 2)
215	214, 205	oveq12d 7293	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → ((2 · 1) / (2 · (2↑𝑘))) = (2 / (2↑(𝑘 + 1))))
216	212, 215	eqtr3d 2780	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 → (1 / (2↑𝑘)) = (2 / (2↑(𝑘 + 1))))
217	216	oveq1d 7290	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
218	192, 208, 217	3eqtr4d 2788	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
219	218	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
220	141, 172, 219	3brtr4d 5106	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆‘𝑘)) ≤ ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))))
221		blss2 23557	. . . . 5 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆‘(𝑘 + 1)) ∈ 𝑋 ∧ (𝑆‘𝑘) ∈ 𝑋) ∧ ((3 / (2↑(𝑘 + 1))) ∈ ℝ ∧ (3 / (2↑𝑘)) ∈ ℝ ∧ ((𝑆‘(𝑘 + 1))𝐷(𝑆‘𝑘)) ≤ ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))))) → ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) ⊆ ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
222	7, 31, 40, 48, 54, 220, 221	syl33anc 1384	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) ⊆ ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
223	1, 222	sylan2 593	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) ⊆ ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
224		peano2nn 11985	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
225		fveq2 6774	. . . . . . . . 9 ⊢ (𝑛 = (𝑘 + 1) → (𝑆‘𝑛) = (𝑆‘(𝑘 + 1)))
226		oveq2 7283	. . . . . . . . . 10 ⊢ (𝑛 = (𝑘 + 1) → (2↑𝑛) = (2↑(𝑘 + 1)))
227	226	oveq2d 7291	. . . . . . . . 9 ⊢ (𝑛 = (𝑘 + 1) → (3 / (2↑𝑛)) = (3 / (2↑(𝑘 + 1))))
228	225, 227	opeq12d 4812	. . . . . . . 8 ⊢ (𝑛 = (𝑘 + 1) → ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩ = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
229		heibor.12	. . . . . . . 8 ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩)
230		opex 5379	. . . . . . . 8 ⊢ ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩ ∈ V
231	228, 229, 230	fvmpt 6875	. . . . . . 7 ⊢ ((𝑘 + 1) ∈ ℕ → (𝑀‘(𝑘 + 1)) = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
232	224, 231	syl 17	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (𝑀‘(𝑘 + 1)) = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
233	232	adantl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑀‘(𝑘 + 1)) = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
234	233	fveq2d 6778	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) = ((ball‘𝐷)‘⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩))
235		df-ov 7278	. . . 4 ⊢ ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) = ((ball‘𝐷)‘⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
236	234, 235	eqtr4di 2796	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) = ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))))
237		fveq2 6774	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (𝑆‘𝑛) = (𝑆‘𝑘))
238		oveq2 7283	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (2↑𝑛) = (2↑𝑘))
239	238	oveq2d 7291	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (3 / (2↑𝑛)) = (3 / (2↑𝑘)))
240	237, 239	opeq12d 4812	. . . . . . 7 ⊢ (𝑛 = 𝑘 → ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩ = ⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩)
241		opex 5379	. . . . . . 7 ⊢ ⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩ ∈ V
242	240, 229, 241	fvmpt 6875	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (𝑀‘𝑘) = ⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩)
243	242	fveq2d 6778	. . . . 5 ⊢ (𝑘 ∈ ℕ → ((ball‘𝐷)‘(𝑀‘𝑘)) = ((ball‘𝐷)‘⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩))
244		df-ov 7278	. . . . 5 ⊢ ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))) = ((ball‘𝐷)‘⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩)
245	243, 244	eqtr4di 2796	. . . 4 ⊢ (𝑘 ∈ ℕ → ((ball‘𝐷)‘(𝑀‘𝑘)) = ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
246	245	adantl 482	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘𝑘)) = ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
247	223, 236, 246	3sstr4d 3968	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀‘𝑘)))
248	247	ralrimiva 3103	1 ⊢ (𝜑 → ∀𝑘 ∈ ℕ ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀‘𝑘)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106  {cab 2715   ≠ wne 2943  ∀wral 3064  ∃wrex 3065  Vcvv 3432   ∩ cin 3886   ⊆ wss 3887  ∅c0 4256  ifcif 4459  𝒫 cpw 4533  ⟨cop 4567  ∪ cuni 4839  ∪ ciun 4924   class class class wbr 5074  {copab 5136   ↦ cmpt 5157  ⟶wf 6429  ‘cfv 6433  (class class class)co 7275   ∈ cmpo 7277  2^nd c2nd 7830  Fincfn 8733  ℂcc 10869  ℝcr 10870  0cc0 10871  1c1 10872   + caddc 10874   · cmul 10876  ℝ^*cxr 11008   ≤ cle 11010   − cmin 11205   / cdiv 11632  ℕcn 11973  2c2 12028  3c3 12029  ℕ₀cn0 12233  ℤ_≥cuz 12582  ℝ⁺crp 12730   +_𝑒 cxad 12846  seqcseq 13721  ↑cexp 13782  ∞Metcxmet 20582  Metcmet 20583  ballcbl 20584  MetOpencmopn 20587  CMetccmet 24418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-1st 7831  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-er 8498  df-map 8617  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-2 12036  df-3 12037  df-n0 12234  df-z 12320  df-uz 12583  df-rp 12731  df-xneg 12848  df-xadd 12849  df-xmul 12850  df-seq 13722  df-exp 13783  df-psmet 20589  df-xmet 20590  df-met 20591  df-bl 20592  df-cmet 24421

This theorem is referenced by:  heiborlem8  35976  heiborlem9  35977