Theorem heiborlem6 35901

Description: Lemma for heibor 35906. 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 12170	. . . 4 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
2		heibor.6	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))
3		cmetmet 24355	. . . . . . . 8 ⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
4	2, 3	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
5		metxmet 23395	. . . . . . 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 4159	. . . . . . . . 9 ⊢ (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋
10		fss 6601	. . . . . . . . 9 ⊢ ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋) → 𝐹:ℕ0⟶𝒫 𝑋)
11	8, 9, 10	sylancl 585	. . . . . . . 8 ⊢ (𝜑 → 𝐹:ℕ0⟶𝒫 𝑋)
12		peano2nn0 12203	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
13		ffvelrn 6941	. . . . . . . 8 ⊢ ((𝐹:ℕ0⟶𝒫 𝑋 ∧ (𝑘 + 1) ∈ ℕ0) → (𝐹‘(𝑘 + 1)) ∈ 𝒫 𝑋)
14	11, 12, 13	syl2an 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘(𝑘 + 1)) ∈ 𝒫 𝑋)
15	14	elpwid 4541	. . . . . 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 35899	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ ℕ0) → (𝑆‘(𝑘 + 1))𝐺(𝑘 + 1))
25	12, 24	sylan2 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1))𝐺(𝑘 + 1))
26		fvex 6769	. . . . . . . . 9 ⊢ (𝑆‘(𝑘 + 1)) ∈ V
27		ovex 7288	. . . . . . . . 9 ⊢ (𝑘 + 1) ∈ V
28	16, 17, 18, 26, 27	heiborlem2 35897	. . . . . . . 8 ⊢ ((𝑆‘(𝑘 + 1))𝐺(𝑘 + 1) ↔ ((𝑘 + 1) ∈ ℕ0 ∧ (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)) ∧ ((𝑆‘(𝑘 + 1))𝐵(𝑘 + 1)) ∈ 𝐾))
29	28	simp2bi 1144	. . . . . . 7 ⊢ ((𝑆‘(𝑘 + 1))𝐺(𝑘 + 1) → (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)))
30	25, 29	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)))
31	15, 30	sseldd 3918	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) ∈ 𝑋)
32	11	ffvelrnda 6943	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) ∈ 𝒫 𝑋)
33	32	elpwid 4541	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) ⊆ 𝑋)
34	16, 17, 18, 19, 2, 8, 20, 21, 22, 23	heiborlem4 35899	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘𝑘)𝐺𝑘)
35		fvex 6769	. . . . . . . . 9 ⊢ (𝑆‘𝑘) ∈ V
36		vex 3426	. . . . . . . . 9 ⊢ 𝑘 ∈ V
37	16, 17, 18, 35, 36	heiborlem2 35897	. . . . . . . 8 ⊢ ((𝑆‘𝑘)𝐺𝑘 ↔ (𝑘 ∈ ℕ0 ∧ (𝑆‘𝑘) ∈ (𝐹‘𝑘) ∧ ((𝑆‘𝑘)𝐵𝑘) ∈ 𝐾))
38	37	simp2bi 1144	. . . . . . 7 ⊢ ((𝑆‘𝑘)𝐺𝑘 → (𝑆‘𝑘) ∈ (𝐹‘𝑘))
39	34, 38	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘𝑘) ∈ (𝐹‘𝑘))
40	33, 39	sseldd 3918	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘𝑘) ∈ 𝑋)
41		3re 11983	. . . . . 6 ⊢ 3 ∈ ℝ
42		2nn 11976	. . . . . . . . 9 ⊢ 2 ∈ ℕ
43		nnexpcl 13723	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ (𝑘 + 1) ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℕ)
44	42, 12, 43	sylancr 586	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) ∈ ℕ)
45	44	nnrpd 12699	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) ∈ ℝ+)
46	45	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℝ+)
47		rerpdivcl 12689	. . . . . 6 ⊢ ((3 ∈ ℝ ∧ (2↑(𝑘 + 1)) ∈ ℝ+) → (3 / (2↑(𝑘 + 1))) ∈ ℝ)
48	41, 46, 47	sylancr 586	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (3 / (2↑(𝑘 + 1))) ∈ ℝ)
49		nnexpcl 13723	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
50	42, 49	mpan 686	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → (2↑𝑘) ∈ ℕ)
51	50	nnrpd 12699	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 → (2↑𝑘) ∈ ℝ+)
52	51	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℝ+)
53		rerpdivcl 12689	. . . . . 6 ⊢ ((3 ∈ ℝ ∧ (2↑𝑘) ∈ ℝ+) → (3 / (2↑𝑘)) ∈ ℝ)
54	41, 52, 53	sylancr 586	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (3 / (2↑𝑘)) ∈ ℝ)
55		oveq1 7262	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝑆‘𝑘) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑚))))
56		oveq2 7263	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑘 → (2↑𝑚) = (2↑𝑘))
57	56	oveq2d 7271	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑘 → (1 / (2↑𝑚)) = (1 / (2↑𝑘)))
58	57	oveq2d 7271	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑘 → ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑚))) = ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
59		ovex 7288	. . . . . . . . . . . 12 ⊢ ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∈ V
60	55, 58, 19, 59	ovmpo 7411	. . . . . . . . . . 11 ⊢ (((𝑆‘𝑘) ∈ 𝑋 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐵𝑘) = ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
61	40, 60	sylancom 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐵𝑘) = ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
62		df-br 5071	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆‘𝑘)𝐺𝑘 ↔ ⟨(𝑆‘𝑘), 𝑘⟩ ∈ 𝐺)
63		fveq2 6756	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (𝑇‘𝑥) = (𝑇‘⟨(𝑆‘𝑘), 𝑘⟩))
64		df-ov 7258	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆‘𝑘)𝑇𝑘) = (𝑇‘⟨(𝑆‘𝑘), 𝑘⟩)
65	63, 64	eqtr4di 2797	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (𝑇‘𝑥) = ((𝑆‘𝑘)𝑇𝑘))
66	35, 36	op2ndd 7815	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (2nd ‘𝑥) = 𝑘)
67	66	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → ((2nd ‘𝑥) + 1) = (𝑘 + 1))
68	65, 67	breq12d 5083	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ↔ ((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1)))
69		fveq2 6756	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (𝐵‘𝑥) = (𝐵‘⟨(𝑆‘𝑘), 𝑘⟩))
70		df-ov 7258	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆‘𝑘)𝐵𝑘) = (𝐵‘⟨(𝑆‘𝑘), 𝑘⟩)
71	69, 70	eqtr4di 2797	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (𝐵‘𝑥) = ((𝑆‘𝑘)𝐵𝑘))
72	65, 67	oveq12d 7273	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1)) = (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1)))
73	71, 72	ineq12d 4144	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) = (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))))
74	73	eleq1d 2823	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 ↔ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾))
75	68, 74	anbi12d 630	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) ↔ (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
76	75	rspccv 3549	. . . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐺𝑘 → (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
80	34, 79	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾))
81	80	simpld 494	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1))
82		ovex 7288	. . . . . . . . . . . . . . 15 ⊢ ((𝑆‘𝑘)𝑇𝑘) ∈ V
83	16, 17, 18, 82, 27	heiborlem2 35897	. . . . . . . . . . . . . 14 ⊢ (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ↔ ((𝑘 + 1) ∈ ℕ0 ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)) ∧ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1)) ∈ 𝐾))
84	83	simp2bi 1144	. . . . . . . . . . . . 13 ⊢ (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) → ((𝑆‘𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)))
85	81, 84	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)))
86	15, 85	sseldd 3918	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋)
87	12	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℕ0)
88		oveq1 7262	. . . . . . . . . . . 12 ⊢ (𝑧 = ((𝑆‘𝑘)𝑇𝑘) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑𝑚))))
89		oveq2 7263	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑘 + 1) → (2↑𝑚) = (2↑(𝑘 + 1)))
90	89	oveq2d 7271	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑘 + 1) → (1 / (2↑𝑚)) = (1 / (2↑(𝑘 + 1))))
91	90	oveq2d 7271	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑘 + 1) → (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑𝑚))) = (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
92		ovex 7288	. . . . . . . . . . . 12 ⊢ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))) ∈ V
93	88, 91, 19, 92	ovmpo 7411	. . . . . . . . . . 11 ⊢ ((((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋 ∧ (𝑘 + 1) ∈ ℕ0) → (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1)) = (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
94	86, 87, 93	syl2anc 583	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1)) = (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
95	61, 94	ineq12d 4144	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) = (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))))
96	80	simprd 495	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)
97		0elpw 5273	. . . . . . . . . . . . 13 ⊢ ∅ ∈ 𝒫 𝑈
98		0fin 8916	. . . . . . . . . . . . 13 ⊢ ∅ ∈ Fin
99		elin 3899	. . . . . . . . . . . . 13 ⊢ (∅ ∈ (𝒫 𝑈 ∩ Fin) ↔ (∅ ∈ 𝒫 𝑈 ∧ ∅ ∈ Fin))
100	97, 98, 99	mpbir2an 707	. . . . . . . . . . . 12 ⊢ ∅ ∈ (𝒫 𝑈 ∩ Fin)
101		0ss 4327	. . . . . . . . . . . 12 ⊢ ∅ ⊆ ∪ ∅
102		unieq 4847	. . . . . . . . . . . . . 14 ⊢ (𝑣 = ∅ → ∪ 𝑣 = ∪ ∅)
103	102	sseq2d 3949	. . . . . . . . . . . . 13 ⊢ (𝑣 = ∅ → (∅ ⊆ ∪ 𝑣 ↔ ∅ ⊆ ∪ ∅))
104	103	rspcev 3552	. . . . . . . . . . . 12 ⊢ ((∅ ∈ (𝒫 𝑈 ∩ Fin) ∧ ∅ ⊆ ∪ ∅) → ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣)
105	100, 101, 104	mp2an 688	. . . . . . . . . . 11 ⊢ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣
106		0ex 5226	. . . . . . . . . . . . 13 ⊢ ∅ ∈ V
107		sseq1 3942	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = ∅ → (𝑢 ⊆ ∪ 𝑣 ↔ ∅ ⊆ ∪ 𝑣))
108	107	rexbidv 3225	. . . . . . . . . . . . . 14 ⊢ (𝑢 = ∅ → (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣 ↔ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣))
109	108	notbid 317	. . . . . . . . . . . . 13 ⊢ (𝑢 = ∅ → (¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣))
110	106, 109, 17	elab2 3606	. . . . . . . . . . . 12 ⊢ (∅ ∈ 𝐾 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣)
111	110	con2bii 357	. . . . . . . . . . 11 ⊢ (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣 ↔ ¬ ∅ ∈ 𝐾)
112	105, 111	mpbi 229	. . . . . . . . . 10 ⊢ ¬ ∅ ∈ 𝐾
113		nelne2 3041	. . . . . . . . . 10 ⊢ (((((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾 ∧ ¬ ∅ ∈ 𝐾) → (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ≠ ∅)
114	96, 112, 113	sylancl 585	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ≠ ∅)
115	95, 114	eqnetrrd 3011	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) ≠ ∅)
116	51	rpreccld 12711	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 → (1 / (2↑𝑘)) ∈ ℝ+)
117	116	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ+)
118	117	rpred 12701	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ)
119	45	rpreccld 12711	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 → (1 / (2↑(𝑘 + 1))) ∈ ℝ+)
120	119	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ+)
121	120	rpred 12701	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ)
122		rexadd 12895	. . . . . . . . . . . 12 ⊢ (((1 / (2↑𝑘)) ∈ ℝ ∧ (1 / (2↑(𝑘 + 1))) ∈ ℝ) → ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
123	118, 121, 122	syl2anc 583	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
124	123	breq1d 5080	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ↔ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘))))
125	117	rpxrd 12702	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ*)
126	120	rpxrd 12702	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ*)
127		bldisj 23459	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆‘𝑘) ∈ 𝑋 ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋) ∧ ((1 / (2↑𝑘)) ∈ ℝ* ∧ (1 / (2↑(𝑘 + 1))) ∈ ℝ* ∧ ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)))) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅)
128	127	3exp2 1352	. . . . . . . . . . . 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 1376	. . . . . . . . . 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 2955	. . . . . . . 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 12716	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ∈ ℝ+)
135	134	rpred 12701	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ∈ ℝ)
136	4	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐷 ∈ (Met‘𝑋))
137		metcl 23393	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝑆‘𝑘) ∈ 𝑋 ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋) → ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ∈ ℝ)
138	136, 40, 86, 137	syl3anc 1369	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ∈ ℝ)
139	135, 138	letrid 11057	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ∨ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ≤ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1))))))
140	139	ord 860	. . . . . . 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 13664	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ≥‘0) → (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1)) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
143		nn0uz 12549	. . . . . . . . . . . 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 6757	. . . . . . . . . . 11 ⊢ (𝑆‘(𝑘 + 1)) = (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1))
146	23	fveq1i 6757	. . . . . . . . . . . 12 ⊢ (𝑆‘𝑘) = (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)
147	146	oveq1i 7265	. . . . . . . . . . 11 ⊢ ((𝑆‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)))
148	144, 145, 147	3eqtr4g 2804	. . . . . . . . . 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 7262	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑘 + 1) → (𝑚 − 1) = ((𝑘 + 1) − 1))
152	150, 151	ifbieq2d 4482	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑘 + 1) → if(𝑚 = 0, 𝐶, (𝑚 − 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)))
153		nn0p1nn 12202	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ)
154		nnne0 11937	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 + 1) ∈ ℕ → (𝑘 + 1) ≠ 0)
155	154	neneqd 2947	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 + 1) ∈ ℕ → ¬ (𝑘 + 1) = 0)
156	153, 155	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ0 → ¬ (𝑘 + 1) = 0)
157	156	iffalsed 4467	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 → if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)) = ((𝑘 + 1) − 1))
158		ovex 7288	. . . . . . . . . . . . . 14 ⊢ ((𝑘 + 1) − 1) ∈ V
159	157, 158	eqeltrdi 2847	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ0 → if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)) ∈ V)
160	149, 152, 12, 159	fvmptd3 6880	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)))
161		nn0cn 12173	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ)
162		ax-1cn 10860	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
163		pncan 11157	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
164	161, 162, 163	sylancl 585	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 → ((𝑘 + 1) − 1) = 𝑘)
165	160, 157, 164	3eqtrd 2782	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = 𝑘)
166	165	oveq2d 7271	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → ((𝑆‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))) = ((𝑆‘𝑘)𝑇𝑘))
167	148, 166	eqtrd 2778	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 → (𝑆‘(𝑘 + 1)) = ((𝑆‘𝑘)𝑇𝑘))
168	167	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) = ((𝑆‘𝑘)𝑇𝑘))
169	168	oveq1d 7270	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆‘𝑘)) = (((𝑆‘𝑘)𝑇𝑘)𝐷(𝑆‘𝑘)))
170		metsym 23411	. . . . . . . 8 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋 ∧ (𝑆‘𝑘) ∈ 𝑋) → (((𝑆‘𝑘)𝑇𝑘)𝐷(𝑆‘𝑘)) = ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)))
171	136, 86, 40, 170	syl3anc 1369	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝑇𝑘)𝐷(𝑆‘𝑘)) = ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)))
172	169, 171	eqtrd 2778	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆‘𝑘)) = ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)))
173		3cn 11984	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℂ
174	173	2timesi 12041	. . . . . . . . . . . 12 ⊢ (2 · 3) = (3 + 3)
175	174	oveq1i 7265	. . . . . . . . . . 11 ⊢ ((2 · 3) − 3) = ((3 + 3) − 3)
176	173, 173	pncan3oi 11167	. . . . . . . . . . 11 ⊢ ((3 + 3) − 3) = 3
177		df-3 11967	. . . . . . . . . . 11 ⊢ 3 = (2 + 1)
178	175, 176, 177	3eqtri 2770	. . . . . . . . . 10 ⊢ ((2 · 3) − 3) = (2 + 1)
179	178	oveq1i 7265	. . . . . . . . 9 ⊢ (((2 · 3) − 3) / (2↑(𝑘 + 1))) = ((2 + 1) / (2↑(𝑘 + 1)))
180		rpcn 12669	. . . . . . . . . . 11 ⊢ ((2↑(𝑘 + 1)) ∈ ℝ+ → (2↑(𝑘 + 1)) ∈ ℂ)
181		rpne0 12675	. . . . . . . . . . 11 ⊢ ((2↑(𝑘 + 1)) ∈ ℝ+ → (2↑(𝑘 + 1)) ≠ 0)
182		2cn 11978	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℂ
183	182, 173	mulcli 10913	. . . . . . . . . . . 12 ⊢ (2 · 3) ∈ ℂ
184		divsubdir 11599	. . . . . . . . . . . 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 1449	. . . . . . . . . . 11 ⊢ (((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0) → (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
186	180, 181, 185	syl2anc 583	. . . . . . . . . 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 11588	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 1 ∈ ℂ ∧ ((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0)) → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
189	182, 162, 188	mp3an12 1449	. . . . . . . . . . 11 ⊢ (((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0) → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
190	180, 181, 189	syl2anc 583	. . . . . . . . . 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 2803	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
193		rpcn 12669	. . . . . . . . . . . 12 ⊢ ((2↑𝑘) ∈ ℝ+ → (2↑𝑘) ∈ ℂ)
194		rpne0 12675	. . . . . . . . . . . 12 ⊢ ((2↑𝑘) ∈ ℝ+ → (2↑𝑘) ≠ 0)
195		2cnne0 12113	. . . . . . . . . . . . 13 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
196		divcan5 11607	. . . . . . . . . . . . 13 ⊢ ((3 ∈ ℂ ∧ ((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
197	173, 195, 196	mp3an13 1450	. . . . . . . . . . . 12 ⊢ (((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
198	193, 194, 197	syl2anc 583	. . . . . . . . . . 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 10888	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ (2↑𝑘) ∈ ℂ) → (2 · (2↑𝑘)) = ((2↑𝑘) · 2))
202	182, 200, 201	sylancr 586	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 → (2 · (2↑𝑘)) = ((2↑𝑘) · 2))
203		expp1 13717	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (2↑(𝑘 + 1)) = ((2↑𝑘) · 2))
204	182, 203	mpan 686	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) = ((2↑𝑘) · 2))
205	202, 204	eqtr4d 2781	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → (2 · (2↑𝑘)) = (2↑(𝑘 + 1)))
206	205	oveq2d 7271	. . . . . . . . . 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 7270	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
209		divcan5 11607	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℂ ∧ ((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
210	162, 195, 209	mp3an13 1450	. . . . . . . . . . . 12 ⊢ (((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
211	193, 194, 210	syl2anc 583	. . . . . . . . . . 11 ⊢ ((2↑𝑘) ∈ ℝ+ → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
212	51, 211	syl 17	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
213		2t1e2 12066	. . . . . . . . . . . 12 ⊢ (2 · 1) = 2
214	213	a1i 11	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → (2 · 1) = 2)
215	214, 205	oveq12d 7273	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → ((2 · 1) / (2 · (2↑𝑘))) = (2 / (2↑(𝑘 + 1))))
216	212, 215	eqtr3d 2780	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 → (1 / (2↑𝑘)) = (2 / (2↑(𝑘 + 1))))
217	216	oveq1d 7270	. . . . . . . 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 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
220	141, 172, 219	3brtr4d 5102	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆‘𝑘)) ≤ ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))))
221		blss2 23465	. . . . 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 1383	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) ⊆ ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
223	1, 222	sylan2 592	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) ⊆ ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
224		peano2nn 11915	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
225		fveq2 6756	. . . . . . . . 9 ⊢ (𝑛 = (𝑘 + 1) → (𝑆‘𝑛) = (𝑆‘(𝑘 + 1)))
226		oveq2 7263	. . . . . . . . . 10 ⊢ (𝑛 = (𝑘 + 1) → (2↑𝑛) = (2↑(𝑘 + 1)))
227	226	oveq2d 7271	. . . . . . . . 9 ⊢ (𝑛 = (𝑘 + 1) → (3 / (2↑𝑛)) = (3 / (2↑(𝑘 + 1))))
228	225, 227	opeq12d 4809	. . . . . . . 8 ⊢ (𝑛 = (𝑘 + 1) → ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩ = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
229		heibor.12	. . . . . . . 8 ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩)
230		opex 5373	. . . . . . . 8 ⊢ ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩ ∈ V
231	228, 229, 230	fvmpt 6857	. . . . . . 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 6760	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) = ((ball‘𝐷)‘⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩))
235		df-ov 7258	. . . 4 ⊢ ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) = ((ball‘𝐷)‘⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
236	234, 235	eqtr4di 2797	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) = ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))))
237		fveq2 6756	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (𝑆‘𝑛) = (𝑆‘𝑘))
238		oveq2 7263	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (2↑𝑛) = (2↑𝑘))
239	238	oveq2d 7271	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (3 / (2↑𝑛)) = (3 / (2↑𝑘)))
240	237, 239	opeq12d 4809	. . . . . . 7 ⊢ (𝑛 = 𝑘 → ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩ = ⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩)
241		opex 5373	. . . . . . 7 ⊢ ⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩ ∈ V
242	240, 229, 241	fvmpt 6857	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (𝑀‘𝑘) = ⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩)
243	242	fveq2d 6760	. . . . 5 ⊢ (𝑘 ∈ ℕ → ((ball‘𝐷)‘(𝑀‘𝑘)) = ((ball‘𝐷)‘⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩))
244		df-ov 7258	. . . . 5 ⊢ ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))) = ((ball‘𝐷)‘⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩)
245	243, 244	eqtr4di 2797	. . . 4 ⊢ (𝑘 ∈ ℕ → ((ball‘𝐷)‘(𝑀‘𝑘)) = ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
246	245	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘𝑘)) = ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
247	223, 236, 246	3sstr4d 3964	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀‘𝑘)))
248	247	ralrimiva 3107	1 ⊢ (𝜑 → ∀𝑘 ∈ ℕ ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀‘𝑘)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108  {cab 2715   ≠ wne 2942  ∀wral 3063  ∃wrex 3064  Vcvv 3422   ∩ cin 3882   ⊆ wss 3883  ∅c0 4253  ifcif 4456  𝒫 cpw 4530  ⟨cop 4564  ∪ cuni 4836  ∪ ciun 4921   class class class wbr 5070  {copab 5132   ↦ cmpt 5153  ⟶wf 6414  ‘cfv 6418  (class class class)co 7255   ∈ cmpo 7257  2^nd c2nd 7803  Fincfn 8691  ℂcc 10800  ℝcr 10801  0cc0 10802  1c1 10803   + caddc 10805   · cmul 10807  ℝ^*cxr 10939   ≤ cle 10941   − cmin 11135   / cdiv 11562  ℕcn 11903  2c2 11958  3c3 11959  ℕ₀cn0 12163  ℤ_≥cuz 12511  ℝ⁺crp 12659   +_𝑒 cxad 12775  seqcseq 13649  ↑cexp 13710  ∞Metcxmet 20495  Metcmet 20496  ballcbl 20497  MetOpencmopn 20500  CMetccmet 24323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-1st 7804  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-er 8456  df-map 8575  df-en 8692  df-dom 8693  df-sdom 8694  df-fin 8695  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-div 11563  df-nn 11904  df-2 11966  df-3 11967  df-n0 12164  df-z 12250  df-uz 12512  df-rp 12660  df-xneg 12777  df-xadd 12778  df-xmul 12779  df-seq 13650  df-exp 13711  df-psmet 20502  df-xmet 20503  df-met 20504  df-bl 20505  df-cmet 24326

This theorem is referenced by:  heiborlem8  35903  heiborlem9  35904