Theorem heiborlem6 38137

Description: Lemma for heibor 38142. 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 12444	. . . 4 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
2		heibor.6	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))
3		cmetmet 25253	. . . . . . . 8 ⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
4	2, 3	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
5		metxmet 24299	. . . . . . 7 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
6	4, 5	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
7	6	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐷 ∈ (∞Met‘𝑋))
8		heibor.7	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))
9		inss1 4177	. . . . . . . . 9 ⊢ (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋
10		fss 6684	. . . . . . . . 9 ⊢ ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋) → 𝐹:ℕ0⟶𝒫 𝑋)
11	8, 9, 10	sylancl 587	. . . . . . . 8 ⊢ (𝜑 → 𝐹:ℕ0⟶𝒫 𝑋)
12		peano2nn0 12477	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
13		ffvelcdm 7033	. . . . . . . 8 ⊢ ((𝐹:ℕ0⟶𝒫 𝑋 ∧ (𝑘 + 1) ∈ ℕ0) → (𝐹‘(𝑘 + 1)) ∈ 𝒫 𝑋)
14	11, 12, 13	syl2an 597	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘(𝑘 + 1)) ∈ 𝒫 𝑋)
15	14	elpwid 4550	. . . . . 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 38135	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ ℕ0) → (𝑆‘(𝑘 + 1))𝐺(𝑘 + 1))
25	12, 24	sylan2 594	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1))𝐺(𝑘 + 1))
26		fvex 6853	. . . . . . . . 9 ⊢ (𝑆‘(𝑘 + 1)) ∈ V
27		ovex 7400	. . . . . . . . 9 ⊢ (𝑘 + 1) ∈ V
28	16, 17, 18, 26, 27	heiborlem2 38133	. . . . . . . 8 ⊢ ((𝑆‘(𝑘 + 1))𝐺(𝑘 + 1) ↔ ((𝑘 + 1) ∈ ℕ0 ∧ (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)) ∧ ((𝑆‘(𝑘 + 1))𝐵(𝑘 + 1)) ∈ 𝐾))
29	28	simp2bi 1147	. . . . . . 7 ⊢ ((𝑆‘(𝑘 + 1))𝐺(𝑘 + 1) → (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)))
30	25, 29	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)))
31	15, 30	sseldd 3922	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) ∈ 𝑋)
32	11	ffvelcdmda 7036	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) ∈ 𝒫 𝑋)
33	32	elpwid 4550	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) ⊆ 𝑋)
34	16, 17, 18, 19, 2, 8, 20, 21, 22, 23	heiborlem4 38135	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘𝑘)𝐺𝑘)
35		fvex 6853	. . . . . . . . 9 ⊢ (𝑆‘𝑘) ∈ V
36		vex 3433	. . . . . . . . 9 ⊢ 𝑘 ∈ V
37	16, 17, 18, 35, 36	heiborlem2 38133	. . . . . . . 8 ⊢ ((𝑆‘𝑘)𝐺𝑘 ↔ (𝑘 ∈ ℕ0 ∧ (𝑆‘𝑘) ∈ (𝐹‘𝑘) ∧ ((𝑆‘𝑘)𝐵𝑘) ∈ 𝐾))
38	37	simp2bi 1147	. . . . . . 7 ⊢ ((𝑆‘𝑘)𝐺𝑘 → (𝑆‘𝑘) ∈ (𝐹‘𝑘))
39	34, 38	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘𝑘) ∈ (𝐹‘𝑘))
40	33, 39	sseldd 3922	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘𝑘) ∈ 𝑋)
41		3re 12261	. . . . . 6 ⊢ 3 ∈ ℝ
42		2nn 12254	. . . . . . . . 9 ⊢ 2 ∈ ℕ
43		nnexpcl 14036	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ (𝑘 + 1) ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℕ)
44	42, 12, 43	sylancr 588	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) ∈ ℕ)
45	44	nnrpd 12984	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) ∈ ℝ+)
46	45	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℝ+)
47		rerpdivcl 12974	. . . . . 6 ⊢ ((3 ∈ ℝ ∧ (2↑(𝑘 + 1)) ∈ ℝ+) → (3 / (2↑(𝑘 + 1))) ∈ ℝ)
48	41, 46, 47	sylancr 588	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (3 / (2↑(𝑘 + 1))) ∈ ℝ)
49		nnexpcl 14036	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
50	42, 49	mpan 691	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → (2↑𝑘) ∈ ℕ)
51	50	nnrpd 12984	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 → (2↑𝑘) ∈ ℝ+)
52	51	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℝ+)
53		rerpdivcl 12974	. . . . . 6 ⊢ ((3 ∈ ℝ ∧ (2↑𝑘) ∈ ℝ+) → (3 / (2↑𝑘)) ∈ ℝ)
54	41, 52, 53	sylancr 588	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (3 / (2↑𝑘)) ∈ ℝ)
55		oveq1 7374	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝑆‘𝑘) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑚))))
56		oveq2 7375	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑘 → (2↑𝑚) = (2↑𝑘))
57	56	oveq2d 7383	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑘 → (1 / (2↑𝑚)) = (1 / (2↑𝑘)))
58	57	oveq2d 7383	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑘 → ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑚))) = ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
59		ovex 7400	. . . . . . . . . . . 12 ⊢ ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∈ V
60	55, 58, 19, 59	ovmpo 7527	. . . . . . . . . . 11 ⊢ (((𝑆‘𝑘) ∈ 𝑋 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐵𝑘) = ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
61	40, 60	sylancom 589	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐵𝑘) = ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
62		df-br 5086	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆‘𝑘)𝐺𝑘 ↔ ⟨(𝑆‘𝑘), 𝑘⟩ ∈ 𝐺)
63		fveq2 6840	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (𝑇‘𝑥) = (𝑇‘⟨(𝑆‘𝑘), 𝑘⟩))
64		df-ov 7370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆‘𝑘)𝑇𝑘) = (𝑇‘⟨(𝑆‘𝑘), 𝑘⟩)
65	63, 64	eqtr4di 2789	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (𝑇‘𝑥) = ((𝑆‘𝑘)𝑇𝑘))
66	35, 36	op2ndd 7953	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (2nd ‘𝑥) = 𝑘)
67	66	oveq1d 7382	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → ((2nd ‘𝑥) + 1) = (𝑘 + 1))
68	65, 67	breq12d 5098	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ↔ ((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1)))
69		fveq2 6840	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (𝐵‘𝑥) = (𝐵‘⟨(𝑆‘𝑘), 𝑘⟩))
70		df-ov 7370	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆‘𝑘)𝐵𝑘) = (𝐵‘⟨(𝑆‘𝑘), 𝑘⟩)
71	69, 70	eqtr4di 2789	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (𝐵‘𝑥) = ((𝑆‘𝑘)𝐵𝑘))
72	65, 67	oveq12d 7385	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1)) = (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1)))
73	71, 72	ineq12d 4161	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) = (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))))
74	73	eleq1d 2821	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 ↔ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾))
75	68, 74	anbi12d 633	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) ↔ (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
76	75	rspccv 3561	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) → (⟨(𝑆‘𝑘), 𝑘⟩ ∈ 𝐺 → (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
77	21, 76	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (⟨(𝑆‘𝑘), 𝑘⟩ ∈ 𝐺 → (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
78	62, 77	biimtrid 242	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑆‘𝑘)𝐺𝑘 → (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
79	78	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐺𝑘 → (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
80	34, 79	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾))
81	80	simpld 494	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1))
82		ovex 7400	. . . . . . . . . . . . . . 15 ⊢ ((𝑆‘𝑘)𝑇𝑘) ∈ V
83	16, 17, 18, 82, 27	heiborlem2 38133	. . . . . . . . . . . . . 14 ⊢ (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ↔ ((𝑘 + 1) ∈ ℕ0 ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)) ∧ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1)) ∈ 𝐾))
84	83	simp2bi 1147	. . . . . . . . . . . . 13 ⊢ (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) → ((𝑆‘𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)))
85	81, 84	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)))
86	15, 85	sseldd 3922	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋)
87	12	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℕ0)
88		oveq1 7374	. . . . . . . . . . . 12 ⊢ (𝑧 = ((𝑆‘𝑘)𝑇𝑘) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑𝑚))))
89		oveq2 7375	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑘 + 1) → (2↑𝑚) = (2↑(𝑘 + 1)))
90	89	oveq2d 7383	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑘 + 1) → (1 / (2↑𝑚)) = (1 / (2↑(𝑘 + 1))))
91	90	oveq2d 7383	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑘 + 1) → (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑𝑚))) = (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
92		ovex 7400	. . . . . . . . . . . 12 ⊢ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))) ∈ V
93	88, 91, 19, 92	ovmpo 7527	. . . . . . . . . . 11 ⊢ ((((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋 ∧ (𝑘 + 1) ∈ ℕ0) → (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1)) = (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
94	86, 87, 93	syl2anc 585	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1)) = (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
95	61, 94	ineq12d 4161	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) = (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))))
96	80	simprd 495	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)
97		0elpw 5297	. . . . . . . . . . . . 13 ⊢ ∅ ∈ 𝒫 𝑈
98		0fi 8989	. . . . . . . . . . . . 13 ⊢ ∅ ∈ Fin
99		elin 3905	. . . . . . . . . . . . 13 ⊢ (∅ ∈ (𝒫 𝑈 ∩ Fin) ↔ (∅ ∈ 𝒫 𝑈 ∧ ∅ ∈ Fin))
100	97, 98, 99	mpbir2an 712	. . . . . . . . . . . 12 ⊢ ∅ ∈ (𝒫 𝑈 ∩ Fin)
101		0ss 4340	. . . . . . . . . . . 12 ⊢ ∅ ⊆ ∪ ∅
102		unieq 4861	. . . . . . . . . . . . . 14 ⊢ (𝑣 = ∅ → ∪ 𝑣 = ∪ ∅)
103	102	sseq2d 3954	. . . . . . . . . . . . 13 ⊢ (𝑣 = ∅ → (∅ ⊆ ∪ 𝑣 ↔ ∅ ⊆ ∪ ∅))
104	103	rspcev 3564	. . . . . . . . . . . 12 ⊢ ((∅ ∈ (𝒫 𝑈 ∩ Fin) ∧ ∅ ⊆ ∪ ∅) → ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣)
105	100, 101, 104	mp2an 693	. . . . . . . . . . 11 ⊢ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣
106		0ex 5242	. . . . . . . . . . . . 13 ⊢ ∅ ∈ V
107		sseq1 3947	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = ∅ → (𝑢 ⊆ ∪ 𝑣 ↔ ∅ ⊆ ∪ 𝑣))
108	107	rexbidv 3161	. . . . . . . . . . . . . 14 ⊢ (𝑢 = ∅ → (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣 ↔ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣))
109	108	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑢 = ∅ → (¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣))
110	106, 109, 17	elab2 3625	. . . . . . . . . . . 12 ⊢ (∅ ∈ 𝐾 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣)
111	110	con2bii 357	. . . . . . . . . . 11 ⊢ (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣 ↔ ¬ ∅ ∈ 𝐾)
112	105, 111	mpbi 230	. . . . . . . . . 10 ⊢ ¬ ∅ ∈ 𝐾
113		nelne2 3030	. . . . . . . . . 10 ⊢ (((((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾 ∧ ¬ ∅ ∈ 𝐾) → (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ≠ ∅)
114	96, 112, 113	sylancl 587	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ≠ ∅)
115	95, 114	eqnetrrd 3000	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) ≠ ∅)
116	51	rpreccld 12996	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 → (1 / (2↑𝑘)) ∈ ℝ+)
117	116	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ+)
118	117	rpred 12986	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ)
119	45	rpreccld 12996	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 → (1 / (2↑(𝑘 + 1))) ∈ ℝ+)
120	119	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ+)
121	120	rpred 12986	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ)
122		rexadd 13184	. . . . . . . . . . . 12 ⊢ (((1 / (2↑𝑘)) ∈ ℝ ∧ (1 / (2↑(𝑘 + 1))) ∈ ℝ) → ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
123	118, 121, 122	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
124	123	breq1d 5095	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ↔ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘))))
125	117	rpxrd 12987	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ*)
126	120	rpxrd 12987	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ*)
127		bldisj 24363	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆‘𝑘) ∈ 𝑋 ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋) ∧ ((1 / (2↑𝑘)) ∈ ℝ* ∧ (1 / (2↑(𝑘 + 1))) ∈ ℝ* ∧ ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)))) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅)
128	127	3exp2 1356	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆‘𝑘) ∈ 𝑋 ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋) → ((1 / (2↑𝑘)) ∈ ℝ* → ((1 / (2↑(𝑘 + 1))) ∈ ℝ* → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))))
129	128	imp32 418	. . . . . . . . . . 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 1381	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))
131	124, 130	sylbird 260	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))
132	131	necon3ad 2945	. . . . . . . 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 13001	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ∈ ℝ+)
135	134	rpred 12986	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ∈ ℝ)
136	4	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐷 ∈ (Met‘𝑋))
137		metcl 24297	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝑆‘𝑘) ∈ 𝑋 ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋) → ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ∈ ℝ)
138	136, 40, 86, 137	syl3anc 1374	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ∈ ℝ)
139	135, 138	letrid 11298	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ∨ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ≤ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1))))))
140	139	ord 865	. . . . . . 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 13978	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ≥‘0) → (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1)) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
143		nn0uz 12826	. . . . . . . . . . . 12 ⊢ ℕ0 = (ℤ≥‘0)
144	142, 143	eleq2s 2854	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1)) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
145	23	fveq1i 6841	. . . . . . . . . . 11 ⊢ (𝑆‘(𝑘 + 1)) = (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1))
146	23	fveq1i 6841	. . . . . . . . . . . 12 ⊢ (𝑆‘𝑘) = (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)
147	146	oveq1i 7377	. . . . . . . . . . 11 ⊢ ((𝑆‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)))
148	144, 145, 147	3eqtr4g 2796	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → (𝑆‘(𝑘 + 1)) = ((𝑆‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
149		eqid 2736	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))) = (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))
150		eqeq1 2740	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑘 + 1) → (𝑚 = 0 ↔ (𝑘 + 1) = 0))
151		oveq1 7374	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑘 + 1) → (𝑚 − 1) = ((𝑘 + 1) − 1))
152	150, 151	ifbieq2d 4493	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑘 + 1) → if(𝑚 = 0, 𝐶, (𝑚 − 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)))
153		nn0p1nn 12476	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ)
154		nnne0 12211	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 + 1) ∈ ℕ → (𝑘 + 1) ≠ 0)
155	154	neneqd 2937	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 + 1) ∈ ℕ → ¬ (𝑘 + 1) = 0)
156	153, 155	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ0 → ¬ (𝑘 + 1) = 0)
157	156	iffalsed 4477	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 → if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)) = ((𝑘 + 1) − 1))
158		ovex 7400	. . . . . . . . . . . . . 14 ⊢ ((𝑘 + 1) − 1) ∈ V
159	157, 158	eqeltrdi 2844	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ0 → if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)) ∈ V)
160	149, 152, 12, 159	fvmptd3 6971	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)))
161		nn0cn 12447	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ)
162		ax-1cn 11096	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
163		pncan 11399	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
164	161, 162, 163	sylancl 587	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 → ((𝑘 + 1) − 1) = 𝑘)
165	160, 157, 164	3eqtrd 2775	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = 𝑘)
166	165	oveq2d 7383	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → ((𝑆‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))) = ((𝑆‘𝑘)𝑇𝑘))
167	148, 166	eqtrd 2771	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 → (𝑆‘(𝑘 + 1)) = ((𝑆‘𝑘)𝑇𝑘))
168	167	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) = ((𝑆‘𝑘)𝑇𝑘))
169	168	oveq1d 7382	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆‘𝑘)) = (((𝑆‘𝑘)𝑇𝑘)𝐷(𝑆‘𝑘)))
170		metsym 24315	. . . . . . . 8 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋 ∧ (𝑆‘𝑘) ∈ 𝑋) → (((𝑆‘𝑘)𝑇𝑘)𝐷(𝑆‘𝑘)) = ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)))
171	136, 86, 40, 170	syl3anc 1374	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝑇𝑘)𝐷(𝑆‘𝑘)) = ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)))
172	169, 171	eqtrd 2771	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆‘𝑘)) = ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)))
173		3cn 12262	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℂ
174	173	2timesi 12314	. . . . . . . . . . . 12 ⊢ (2 · 3) = (3 + 3)
175	174	oveq1i 7377	. . . . . . . . . . 11 ⊢ ((2 · 3) − 3) = ((3 + 3) − 3)
176	173, 173	pncan3oi 11409	. . . . . . . . . . 11 ⊢ ((3 + 3) − 3) = 3
177		df-3 12245	. . . . . . . . . . 11 ⊢ 3 = (2 + 1)
178	175, 176, 177	3eqtri 2763	. . . . . . . . . 10 ⊢ ((2 · 3) − 3) = (2 + 1)
179	178	oveq1i 7377	. . . . . . . . 9 ⊢ (((2 · 3) − 3) / (2↑(𝑘 + 1))) = ((2 + 1) / (2↑(𝑘 + 1)))
180		rpcn 12953	. . . . . . . . . . 11 ⊢ ((2↑(𝑘 + 1)) ∈ ℝ+ → (2↑(𝑘 + 1)) ∈ ℂ)
181		rpne0 12959	. . . . . . . . . . 11 ⊢ ((2↑(𝑘 + 1)) ∈ ℝ+ → (2↑(𝑘 + 1)) ≠ 0)
182		2cn 12256	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℂ
183	182, 173	mulcli 11152	. . . . . . . . . . . 12 ⊢ (2 · 3) ∈ ℂ
184		divsubdir 11848	. . . . . . . . . . . 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 1454	. . . . . . . . . . 11 ⊢ (((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0) → (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
186	180, 181, 185	syl2anc 585	. . . . . . . . . 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 11834	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 1 ∈ ℂ ∧ ((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0)) → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
189	182, 162, 188	mp3an12 1454	. . . . . . . . . . 11 ⊢ (((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0) → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
190	180, 181, 189	syl2anc 585	. . . . . . . . . 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 2795	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
193		rpcn 12953	. . . . . . . . . . . 12 ⊢ ((2↑𝑘) ∈ ℝ+ → (2↑𝑘) ∈ ℂ)
194		rpne0 12959	. . . . . . . . . . . 12 ⊢ ((2↑𝑘) ∈ ℝ+ → (2↑𝑘) ≠ 0)
195		2cnne0 12386	. . . . . . . . . . . . 13 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
196		divcan5 11857	. . . . . . . . . . . . 13 ⊢ ((3 ∈ ℂ ∧ ((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
197	173, 195, 196	mp3an13 1455	. . . . . . . . . . . 12 ⊢ (((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
198	193, 194, 197	syl2anc 585	. . . . . . . . . . 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 11124	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ (2↑𝑘) ∈ ℂ) → (2 · (2↑𝑘)) = ((2↑𝑘) · 2))
202	182, 200, 201	sylancr 588	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 → (2 · (2↑𝑘)) = ((2↑𝑘) · 2))
203		expp1 14030	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (2↑(𝑘 + 1)) = ((2↑𝑘) · 2))
204	182, 203	mpan 691	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) = ((2↑𝑘) · 2))
205	202, 204	eqtr4d 2774	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → (2 · (2↑𝑘)) = (2↑(𝑘 + 1)))
206	205	oveq2d 7383	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → ((2 · 3) / (2 · (2↑𝑘))) = ((2 · 3) / (2↑(𝑘 + 1))))
207	199, 206	eqtr3d 2773	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 → (3 / (2↑𝑘)) = ((2 · 3) / (2↑(𝑘 + 1))))
208	207	oveq1d 7382	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
209		divcan5 11857	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℂ ∧ ((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
210	162, 195, 209	mp3an13 1455	. . . . . . . . . . . 12 ⊢ (((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
211	193, 194, 210	syl2anc 585	. . . . . . . . . . 11 ⊢ ((2↑𝑘) ∈ ℝ+ → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
212	51, 211	syl 17	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
213		2t1e2 12339	. . . . . . . . . . . 12 ⊢ (2 · 1) = 2
214	213	a1i 11	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → (2 · 1) = 2)
215	214, 205	oveq12d 7385	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → ((2 · 1) / (2 · (2↑𝑘))) = (2 / (2↑(𝑘 + 1))))
216	212, 215	eqtr3d 2773	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 → (1 / (2↑𝑘)) = (2 / (2↑(𝑘 + 1))))
217	216	oveq1d 7382	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
218	192, 208, 217	3eqtr4d 2781	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
219	218	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
220	141, 172, 219	3brtr4d 5117	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆‘𝑘)) ≤ ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))))
221		blss2 24369	. . . . 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 1388	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) ⊆ ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
223	1, 222	sylan2 594	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) ⊆ ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
224		peano2nn 12186	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
225		fveq2 6840	. . . . . . . . 9 ⊢ (𝑛 = (𝑘 + 1) → (𝑆‘𝑛) = (𝑆‘(𝑘 + 1)))
226		oveq2 7375	. . . . . . . . . 10 ⊢ (𝑛 = (𝑘 + 1) → (2↑𝑛) = (2↑(𝑘 + 1)))
227	226	oveq2d 7383	. . . . . . . . 9 ⊢ (𝑛 = (𝑘 + 1) → (3 / (2↑𝑛)) = (3 / (2↑(𝑘 + 1))))
228	225, 227	opeq12d 4824	. . . . . . . 8 ⊢ (𝑛 = (𝑘 + 1) → ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩ = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
229		heibor.12	. . . . . . . 8 ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩)
230		opex 5416	. . . . . . . 8 ⊢ ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩ ∈ V
231	228, 229, 230	fvmpt 6947	. . . . . . 7 ⊢ ((𝑘 + 1) ∈ ℕ → (𝑀‘(𝑘 + 1)) = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
232	224, 231	syl 17	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (𝑀‘(𝑘 + 1)) = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
233	232	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑀‘(𝑘 + 1)) = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
234	233	fveq2d 6844	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) = ((ball‘𝐷)‘⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩))
235		df-ov 7370	. . . 4 ⊢ ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) = ((ball‘𝐷)‘⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
236	234, 235	eqtr4di 2789	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) = ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))))
237		fveq2 6840	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (𝑆‘𝑛) = (𝑆‘𝑘))
238		oveq2 7375	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (2↑𝑛) = (2↑𝑘))
239	238	oveq2d 7383	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (3 / (2↑𝑛)) = (3 / (2↑𝑘)))
240	237, 239	opeq12d 4824	. . . . . . 7 ⊢ (𝑛 = 𝑘 → ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩ = ⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩)
241		opex 5416	. . . . . . 7 ⊢ ⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩ ∈ V
242	240, 229, 241	fvmpt 6947	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (𝑀‘𝑘) = ⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩)
243	242	fveq2d 6844	. . . . 5 ⊢ (𝑘 ∈ ℕ → ((ball‘𝐷)‘(𝑀‘𝑘)) = ((ball‘𝐷)‘⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩))
244		df-ov 7370	. . . . 5 ⊢ ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))) = ((ball‘𝐷)‘⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩)
245	243, 244	eqtr4di 2789	. . . 4 ⊢ (𝑘 ∈ ℕ → ((ball‘𝐷)‘(𝑀‘𝑘)) = ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
246	245	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘𝑘)) = ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
247	223, 236, 246	3sstr4d 3977	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀‘𝑘)))
248	247	ralrimiva 3129	1 ⊢ (𝜑 → ∀𝑘 ∈ ℕ ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀‘𝑘)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  {cab 2714   ≠ wne 2932  ∀wral 3051  ∃wrex 3061  Vcvv 3429   ∩ cin 3888   ⊆ wss 3889  ∅c0 4273  ifcif 4466  𝒫 cpw 4541  ⟨cop 4573  ∪ cuni 4850  ∪ ciun 4933   class class class wbr 5085  {copab 5147   ↦ cmpt 5166  ⟶wf 6494  ‘cfv 6498  (class class class)co 7367   ∈ cmpo 7369  2^nd c2nd 7941  Fincfn 8893  ℂcc 11036  ℝcr 11037  0cc0 11038  1c1 11039   + caddc 11041   · cmul 11043  ℝ^*cxr 11178   ≤ cle 11180   − cmin 11377   / cdiv 11807  ℕcn 12174  2c2 12236  3c3 12237  ℕ₀cn0 12437  ℤ_≥cuz 12788  ℝ⁺crp 12942   +_𝑒 cxad 13061  seqcseq 13963  ↑cexp 14023  ∞Metcxmet 21337  Metcmet 21338  ballcbl 21339  MetOpencmopn 21342  CMetccmet 25221

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-1st 7942  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-er 8643  df-map 8775  df-en 8894  df-dom 8895  df-sdom 8896  df-fin 8897  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-div 11808  df-nn 12175  df-2 12244  df-3 12245  df-n0 12438  df-z 12525  df-uz 12789  df-rp 12943  df-xneg 13063  df-xadd 13064  df-xmul 13065  df-seq 13964  df-exp 14024  df-psmet 21344  df-xmet 21345  df-met 21346  df-bl 21347  df-cmet 25224

This theorem is referenced by:  heiborlem8  38139  heiborlem9  38140