Theorem heiborlem6 34647

Description: Lemma for heibor 34652. 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 11758	. . . 4 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
2		heibor.6	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))
3		cmetmet 23576	. . . . . . . 8 ⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
4	2, 3	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
5		metxmet 22631	. . . . . . 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 4131	. . . . . . . . 9 ⊢ (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋
10		fss 6402	. . . . . . . . 9 ⊢ ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋) → 𝐹:ℕ0⟶𝒫 𝑋)
11	8, 9, 10	sylancl 586	. . . . . . . 8 ⊢ (𝜑 → 𝐹:ℕ0⟶𝒫 𝑋)
12		peano2nn0 11791	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
13		ffvelrn 6721	. . . . . . . 8 ⊢ ((𝐹:ℕ0⟶𝒫 𝑋 ∧ (𝑘 + 1) ∈ ℕ0) → (𝐹‘(𝑘 + 1)) ∈ 𝒫 𝑋)
14	11, 12, 13	syl2an 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘(𝑘 + 1)) ∈ 𝒫 𝑋)
15	14	elpwid 4471	. . . . . 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 34645	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ ℕ0) → (𝑆‘(𝑘 + 1))𝐺(𝑘 + 1))
25	12, 24	sylan2 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1))𝐺(𝑘 + 1))
26		fvex 6558	. . . . . . . . 9 ⊢ (𝑆‘(𝑘 + 1)) ∈ V
27		ovex 7055	. . . . . . . . 9 ⊢ (𝑘 + 1) ∈ V
28	16, 17, 18, 26, 27	heiborlem2 34643	. . . . . . . 8 ⊢ ((𝑆‘(𝑘 + 1))𝐺(𝑘 + 1) ↔ ((𝑘 + 1) ∈ ℕ0 ∧ (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)) ∧ ((𝑆‘(𝑘 + 1))𝐵(𝑘 + 1)) ∈ 𝐾))
29	28	simp2bi 1139	. . . . . . 7 ⊢ ((𝑆‘(𝑘 + 1))𝐺(𝑘 + 1) → (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)))
30	25, 29	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)))
31	15, 30	sseldd 3896	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) ∈ 𝑋)
32	11	ffvelrnda 6723	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) ∈ 𝒫 𝑋)
33	32	elpwid 4471	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) ⊆ 𝑋)
34	16, 17, 18, 19, 2, 8, 20, 21, 22, 23	heiborlem4 34645	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘𝑘)𝐺𝑘)
35		fvex 6558	. . . . . . . . 9 ⊢ (𝑆‘𝑘) ∈ V
36		vex 3443	. . . . . . . . 9 ⊢ 𝑘 ∈ V
37	16, 17, 18, 35, 36	heiborlem2 34643	. . . . . . . 8 ⊢ ((𝑆‘𝑘)𝐺𝑘 ↔ (𝑘 ∈ ℕ0 ∧ (𝑆‘𝑘) ∈ (𝐹‘𝑘) ∧ ((𝑆‘𝑘)𝐵𝑘) ∈ 𝐾))
38	37	simp2bi 1139	. . . . . . 7 ⊢ ((𝑆‘𝑘)𝐺𝑘 → (𝑆‘𝑘) ∈ (𝐹‘𝑘))
39	34, 38	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘𝑘) ∈ (𝐹‘𝑘))
40	33, 39	sseldd 3896	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘𝑘) ∈ 𝑋)
41		3re 11571	. . . . . 6 ⊢ 3 ∈ ℝ
42		2nn 11564	. . . . . . . . 9 ⊢ 2 ∈ ℕ
43		nnexpcl 13296	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ (𝑘 + 1) ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℕ)
44	42, 12, 43	sylancr 587	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) ∈ ℕ)
45	44	nnrpd 12283	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) ∈ ℝ+)
46	45	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℝ+)
47		rerpdivcl 12273	. . . . . 6 ⊢ ((3 ∈ ℝ ∧ (2↑(𝑘 + 1)) ∈ ℝ+) → (3 / (2↑(𝑘 + 1))) ∈ ℝ)
48	41, 46, 47	sylancr 587	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (3 / (2↑(𝑘 + 1))) ∈ ℝ)
49		nnexpcl 13296	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
50	42, 49	mpan 686	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → (2↑𝑘) ∈ ℕ)
51	50	nnrpd 12283	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 → (2↑𝑘) ∈ ℝ+)
52	51	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℝ+)
53		rerpdivcl 12273	. . . . . 6 ⊢ ((3 ∈ ℝ ∧ (2↑𝑘) ∈ ℝ+) → (3 / (2↑𝑘)) ∈ ℝ)
54	41, 52, 53	sylancr 587	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (3 / (2↑𝑘)) ∈ ℝ)
55		oveq1 7030	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝑆‘𝑘) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑚))))
56		oveq2 7031	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑘 → (2↑𝑚) = (2↑𝑘))
57	56	oveq2d 7039	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑘 → (1 / (2↑𝑚)) = (1 / (2↑𝑘)))
58	57	oveq2d 7039	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑘 → ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑚))) = ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
59		ovex 7055	. . . . . . . . . . . 12 ⊢ ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∈ V
60	55, 58, 19, 59	ovmpo 7173	. . . . . . . . . . 11 ⊢ (((𝑆‘𝑘) ∈ 𝑋 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐵𝑘) = ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
61	40, 60	sylancom 588	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐵𝑘) = ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
62		df-br 4969	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆‘𝑘)𝐺𝑘 ↔ ⟨(𝑆‘𝑘), 𝑘⟩ ∈ 𝐺)
63		fveq2 6545	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (𝑇‘𝑥) = (𝑇‘⟨(𝑆‘𝑘), 𝑘⟩))
64		df-ov 7026	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆‘𝑘)𝑇𝑘) = (𝑇‘⟨(𝑆‘𝑘), 𝑘⟩)
65	63, 64	syl6eqr 2851	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (𝑇‘𝑥) = ((𝑆‘𝑘)𝑇𝑘))
66	35, 36	op2ndd 7563	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (2nd ‘𝑥) = 𝑘)
67	66	oveq1d 7038	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → ((2nd ‘𝑥) + 1) = (𝑘 + 1))
68	65, 67	breq12d 4981	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ↔ ((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1)))
69		fveq2 6545	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (𝐵‘𝑥) = (𝐵‘⟨(𝑆‘𝑘), 𝑘⟩))
70		df-ov 7026	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆‘𝑘)𝐵𝑘) = (𝐵‘⟨(𝑆‘𝑘), 𝑘⟩)
71	69, 70	syl6eqr 2851	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (𝐵‘𝑥) = ((𝑆‘𝑘)𝐵𝑘))
72	65, 67	oveq12d 7041	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1)) = (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1)))
73	71, 72	ineq12d 4116	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) = (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))))
74	73	eleq1d 2869	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 ↔ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾))
75	68, 74	anbi12d 630	. . . . . . . . . . . . . . . . . . 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 243	. . . . . . . . . . . . . . . 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 7055	. . . . . . . . . . . . . . 15 ⊢ ((𝑆‘𝑘)𝑇𝑘) ∈ V
83	16, 17, 18, 82, 27	heiborlem2 34643	. . . . . . . . . . . . . 14 ⊢ (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ↔ ((𝑘 + 1) ∈ ℕ0 ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)) ∧ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1)) ∈ 𝐾))
84	83	simp2bi 1139	. . . . . . . . . . . . 13 ⊢ (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) → ((𝑆‘𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)))
85	81, 84	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)))
86	15, 85	sseldd 3896	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋)
87	12	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℕ0)
88		oveq1 7030	. . . . . . . . . . . 12 ⊢ (𝑧 = ((𝑆‘𝑘)𝑇𝑘) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑𝑚))))
89		oveq2 7031	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑘 + 1) → (2↑𝑚) = (2↑(𝑘 + 1)))
90	89	oveq2d 7039	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑘 + 1) → (1 / (2↑𝑚)) = (1 / (2↑(𝑘 + 1))))
91	90	oveq2d 7039	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑘 + 1) → (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑𝑚))) = (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
92		ovex 7055	. . . . . . . . . . . 12 ⊢ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))) ∈ V
93	88, 91, 19, 92	ovmpo 7173	. . . . . . . . . . 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 4116	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) = (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))))
96	80	simprd 496	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)
97		0elpw 5154	. . . . . . . . . . . . 13 ⊢ ∅ ∈ 𝒫 𝑈
98		0fin 8599	. . . . . . . . . . . . 13 ⊢ ∅ ∈ Fin
99		elin 4096	. . . . . . . . . . . . 13 ⊢ (∅ ∈ (𝒫 𝑈 ∩ Fin) ↔ (∅ ∈ 𝒫 𝑈 ∧ ∅ ∈ Fin))
100	97, 98, 99	mpbir2an 707	. . . . . . . . . . . 12 ⊢ ∅ ∈ (𝒫 𝑈 ∩ Fin)
101		0ss 4276	. . . . . . . . . . . 12 ⊢ ∅ ⊆ ∪ ∅
102		unieq 4759	. . . . . . . . . . . . . 14 ⊢ (𝑣 = ∅ → ∪ 𝑣 = ∪ ∅)
103	102	sseq2d 3926	. . . . . . . . . . . . 13 ⊢ (𝑣 = ∅ → (∅ ⊆ ∪ 𝑣 ↔ ∅ ⊆ ∪ ∅))
104	103	rspcev 3561	. . . . . . . . . . . 12 ⊢ ((∅ ∈ (𝒫 𝑈 ∩ Fin) ∧ ∅ ⊆ ∪ ∅) → ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣)
105	100, 101, 104	mp2an 688	. . . . . . . . . . 11 ⊢ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣
106		0ex 5109	. . . . . . . . . . . . 13 ⊢ ∅ ∈ V
107		sseq1 3919	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = ∅ → (𝑢 ⊆ ∪ 𝑣 ↔ ∅ ⊆ ∪ 𝑣))
108	107	rexbidv 3262	. . . . . . . . . . . . . 14 ⊢ (𝑢 = ∅ → (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣 ↔ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣))
109	108	notbid 319	. . . . . . . . . . . . 13 ⊢ (𝑢 = ∅ → (¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣))
110	106, 109, 17	elab2 3611	. . . . . . . . . . . 12 ⊢ (∅ ∈ 𝐾 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣)
111	110	con2bii 359	. . . . . . . . . . 11 ⊢ (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣 ↔ ¬ ∅ ∈ 𝐾)
112	105, 111	mpbi 231	. . . . . . . . . 10 ⊢ ¬ ∅ ∈ 𝐾
113		nelne2 3085	. . . . . . . . . 10 ⊢ (((((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾 ∧ ¬ ∅ ∈ 𝐾) → (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ≠ ∅)
114	96, 112, 113	sylancl 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ≠ ∅)
115	95, 114	eqnetrrd 3054	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) ≠ ∅)
116	51	rpreccld 12295	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 → (1 / (2↑𝑘)) ∈ ℝ+)
117	116	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ+)
118	117	rpred 12285	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ)
119	45	rpreccld 12295	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 → (1 / (2↑(𝑘 + 1))) ∈ ℝ+)
120	119	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ+)
121	120	rpred 12285	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ)
122		rexadd 12479	. . . . . . . . . . . 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 4978	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ↔ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘))))
125	117	rpxrd 12286	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ*)
126	120	rpxrd 12286	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ*)
127		bldisj 22695	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆‘𝑘) ∈ 𝑋 ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋) ∧ ((1 / (2↑𝑘)) ∈ ℝ* ∧ (1 / (2↑(𝑘 + 1))) ∈ ℝ* ∧ ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)))) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅)
128	127	3exp2 1347	. . . . . . . . . . . 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 1371	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))
131	124, 130	sylbird 261	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))
132	131	necon3ad 2999	. . . . . . . 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 12300	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ∈ ℝ+)
135	134	rpred 12285	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ∈ ℝ)
136	4	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐷 ∈ (Met‘𝑋))
137		metcl 22629	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝑆‘𝑘) ∈ 𝑋 ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋) → ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ∈ ℝ)
138	136, 40, 86, 137	syl3anc 1364	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ∈ ℝ)
139	135, 138	letrid 10645	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ∨ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ≤ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1))))))
140	139	ord 859	. . . . . . 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 13238	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ≥‘0) → (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1)) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
143		nn0uz 12133	. . . . . . . . . . . 12 ⊢ ℕ0 = (ℤ≥‘0)
144	142, 143	eleq2s 2903	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1)) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
145	23	fveq1i 6546	. . . . . . . . . . 11 ⊢ (𝑆‘(𝑘 + 1)) = (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1))
146	23	fveq1i 6546	. . . . . . . . . . . 12 ⊢ (𝑆‘𝑘) = (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)
147	146	oveq1i 7033	. . . . . . . . . . 11 ⊢ ((𝑆‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)))
148	144, 145, 147	3eqtr4g 2858	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → (𝑆‘(𝑘 + 1)) = ((𝑆‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
149		eqid 2797	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))) = (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))
150		eqeq1 2801	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑘 + 1) → (𝑚 = 0 ↔ (𝑘 + 1) = 0))
151		oveq1 7030	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑘 + 1) → (𝑚 − 1) = ((𝑘 + 1) − 1))
152	150, 151	ifbieq2d 4412	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑘 + 1) → if(𝑚 = 0, 𝐶, (𝑚 − 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)))
153		nn0p1nn 11790	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ)
154		nnne0 11525	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 + 1) ∈ ℕ → (𝑘 + 1) ≠ 0)
155	154	neneqd 2991	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 + 1) ∈ ℕ → ¬ (𝑘 + 1) = 0)
156	153, 155	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ0 → ¬ (𝑘 + 1) = 0)
157	156	iffalsed 4398	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 → if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)) = ((𝑘 + 1) − 1))
158		ovex 7055	. . . . . . . . . . . . . 14 ⊢ ((𝑘 + 1) − 1) ∈ V
159	157, 158	syl6eqel 2893	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ0 → if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)) ∈ V)
160	149, 152, 12, 159	fvmptd3 6664	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)))
161		nn0cn 11761	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ)
162		ax-1cn 10448	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
163		pncan 10745	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
164	161, 162, 163	sylancl 586	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 → ((𝑘 + 1) − 1) = 𝑘)
165	160, 157, 164	3eqtrd 2837	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = 𝑘)
166	165	oveq2d 7039	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → ((𝑆‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))) = ((𝑆‘𝑘)𝑇𝑘))
167	148, 166	eqtrd 2833	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 → (𝑆‘(𝑘 + 1)) = ((𝑆‘𝑘)𝑇𝑘))
168	167	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) = ((𝑆‘𝑘)𝑇𝑘))
169	168	oveq1d 7038	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆‘𝑘)) = (((𝑆‘𝑘)𝑇𝑘)𝐷(𝑆‘𝑘)))
170		metsym 22647	. . . . . . . 8 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋 ∧ (𝑆‘𝑘) ∈ 𝑋) → (((𝑆‘𝑘)𝑇𝑘)𝐷(𝑆‘𝑘)) = ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)))
171	136, 86, 40, 170	syl3anc 1364	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝑇𝑘)𝐷(𝑆‘𝑘)) = ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)))
172	169, 171	eqtrd 2833	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆‘𝑘)) = ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)))
173		3cn 11572	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℂ
174	173	2timesi 11629	. . . . . . . . . . . 12 ⊢ (2 · 3) = (3 + 3)
175	174	oveq1i 7033	. . . . . . . . . . 11 ⊢ ((2 · 3) − 3) = ((3 + 3) − 3)
176	173, 173	pncan3oi 10756	. . . . . . . . . . 11 ⊢ ((3 + 3) − 3) = 3
177		df-3 11555	. . . . . . . . . . 11 ⊢ 3 = (2 + 1)
178	175, 176, 177	3eqtri 2825	. . . . . . . . . 10 ⊢ ((2 · 3) − 3) = (2 + 1)
179	178	oveq1i 7033	. . . . . . . . 9 ⊢ (((2 · 3) − 3) / (2↑(𝑘 + 1))) = ((2 + 1) / (2↑(𝑘 + 1)))
180		rpcn 12253	. . . . . . . . . . 11 ⊢ ((2↑(𝑘 + 1)) ∈ ℝ+ → (2↑(𝑘 + 1)) ∈ ℂ)
181		rpne0 12259	. . . . . . . . . . 11 ⊢ ((2↑(𝑘 + 1)) ∈ ℝ+ → (2↑(𝑘 + 1)) ≠ 0)
182		2cn 11566	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℂ
183	182, 173	mulcli 10501	. . . . . . . . . . . 12 ⊢ (2 · 3) ∈ ℂ
184		divsubdir 11188	. . . . . . . . . . . 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 1443	. . . . . . . . . . 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 11177	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 1 ∈ ℂ ∧ ((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0)) → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
189	182, 162, 188	mp3an12 1443	. . . . . . . . . . 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 2857	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
193		rpcn 12253	. . . . . . . . . . . 12 ⊢ ((2↑𝑘) ∈ ℝ+ → (2↑𝑘) ∈ ℂ)
194		rpne0 12259	. . . . . . . . . . . 12 ⊢ ((2↑𝑘) ∈ ℝ+ → (2↑𝑘) ≠ 0)
195		2cnne0 11701	. . . . . . . . . . . . 13 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
196		divcan5 11196	. . . . . . . . . . . . 13 ⊢ ((3 ∈ ℂ ∧ ((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
197	173, 195, 196	mp3an13 1444	. . . . . . . . . . . 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 10476	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ (2↑𝑘) ∈ ℂ) → (2 · (2↑𝑘)) = ((2↑𝑘) · 2))
202	182, 200, 201	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 → (2 · (2↑𝑘)) = ((2↑𝑘) · 2))
203		expp1 13290	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (2↑(𝑘 + 1)) = ((2↑𝑘) · 2))
204	182, 203	mpan 686	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) = ((2↑𝑘) · 2))
205	202, 204	eqtr4d 2836	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → (2 · (2↑𝑘)) = (2↑(𝑘 + 1)))
206	205	oveq2d 7039	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → ((2 · 3) / (2 · (2↑𝑘))) = ((2 · 3) / (2↑(𝑘 + 1))))
207	199, 206	eqtr3d 2835	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 → (3 / (2↑𝑘)) = ((2 · 3) / (2↑(𝑘 + 1))))
208	207	oveq1d 7038	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
209		divcan5 11196	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℂ ∧ ((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
210	162, 195, 209	mp3an13 1444	. . . . . . . . . . . 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 11654	. . . . . . . . . . . 12 ⊢ (2 · 1) = 2
214	213	a1i 11	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → (2 · 1) = 2)
215	214, 205	oveq12d 7041	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → ((2 · 1) / (2 · (2↑𝑘))) = (2 / (2↑(𝑘 + 1))))
216	212, 215	eqtr3d 2835	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 → (1 / (2↑𝑘)) = (2 / (2↑(𝑘 + 1))))
217	216	oveq1d 7038	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
218	192, 208, 217	3eqtr4d 2843	. . . . . . 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 5000	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆‘𝑘)) ≤ ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))))
221		blss2 22701	. . . . 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 1378	. . . 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 11504	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
225		fveq2 6545	. . . . . . . . 9 ⊢ (𝑛 = (𝑘 + 1) → (𝑆‘𝑛) = (𝑆‘(𝑘 + 1)))
226		oveq2 7031	. . . . . . . . . 10 ⊢ (𝑛 = (𝑘 + 1) → (2↑𝑛) = (2↑(𝑘 + 1)))
227	226	oveq2d 7039	. . . . . . . . 9 ⊢ (𝑛 = (𝑘 + 1) → (3 / (2↑𝑛)) = (3 / (2↑(𝑘 + 1))))
228	225, 227	opeq12d 4724	. . . . . . . 8 ⊢ (𝑛 = (𝑘 + 1) → ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩ = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
229		heibor.12	. . . . . . . 8 ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩)
230		opex 5255	. . . . . . . 8 ⊢ ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩ ∈ V
231	228, 229, 230	fvmpt 6642	. . . . . . 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 6549	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) = ((ball‘𝐷)‘⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩))
235		df-ov 7026	. . . 4 ⊢ ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) = ((ball‘𝐷)‘⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
236	234, 235	syl6eqr 2851	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) = ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))))
237		fveq2 6545	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (𝑆‘𝑛) = (𝑆‘𝑘))
238		oveq2 7031	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (2↑𝑛) = (2↑𝑘))
239	238	oveq2d 7039	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (3 / (2↑𝑛)) = (3 / (2↑𝑘)))
240	237, 239	opeq12d 4724	. . . . . . 7 ⊢ (𝑛 = 𝑘 → ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩ = ⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩)
241		opex 5255	. . . . . . 7 ⊢ ⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩ ∈ V
242	240, 229, 241	fvmpt 6642	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (𝑀‘𝑘) = ⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩)
243	242	fveq2d 6549	. . . . 5 ⊢ (𝑘 ∈ ℕ → ((ball‘𝐷)‘(𝑀‘𝑘)) = ((ball‘𝐷)‘⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩))
244		df-ov 7026	. . . . 5 ⊢ ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))) = ((ball‘𝐷)‘⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩)
245	243, 244	syl6eqr 2851	. . . 4 ⊢ (𝑘 ∈ ℕ → ((ball‘𝐷)‘(𝑀‘𝑘)) = ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
246	245	adantl 482	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘𝑘)) = ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
247	223, 236, 246	3sstr4d 3941	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀‘𝑘)))
248	247	ralrimiva 3151	1 ⊢ (𝜑 → ∀𝑘 ∈ ℕ ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀‘𝑘)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∧ w3a 1080   = wceq 1525   ∈ wcel 2083  {cab 2777   ≠ wne 2986  ∀wral 3107  ∃wrex 3108  Vcvv 3440   ∩ cin 3864   ⊆ wss 3865  ∅c0 4217  ifcif 4387  𝒫 cpw 4459  ⟨cop 4484  ∪ cuni 4751  ∪ ciun 4831   class class class wbr 4968  {copab 5030   ↦ cmpt 5047  ⟶wf 6228  ‘cfv 6232  (class class class)co 7023   ∈ cmpo 7025  2^nd c2nd 7551  Fincfn 8364  ℂcc 10388  ℝcr 10389  0cc0 10390  1c1 10391   + caddc 10393   · cmul 10395  ℝ^*cxr 10527   ≤ cle 10529   − cmin 10723   / cdiv 11151  ℕcn 11492  2c2 11546  3c3 11547  ℕ₀cn0 11751  ℤ_≥cuz 12097  ℝ⁺crp 12243   +_𝑒 cxad 12359  seqcseq 13223  ↑cexp 13283  ∞Metcxmet 20216  Metcmet 20217  ballcbl 20218  MetOpencmopn 20221  CMetccmet 23544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-cnex 10446  ax-resscn 10447  ax-1cn 10448  ax-icn 10449  ax-addcl 10450  ax-addrcl 10451  ax-mulcl 10452  ax-mulrcl 10453  ax-mulcom 10454  ax-addass 10455  ax-mulass 10456  ax-distr 10457  ax-i2m1 10458  ax-1ne0 10459  ax-1rid 10460  ax-rnegex 10461  ax-rrecex 10462  ax-cnre 10463  ax-pre-lttri 10464  ax-pre-lttrn 10465  ax-pre-ltadd 10466  ax-pre-mulgt0 10467

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-iun 4833  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-riota 6984  df-ov 7026  df-oprab 7027  df-mpo 7028  df-om 7444  df-1st 7552  df-2nd 7553  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-er 8146  df-map 8265  df-en 8365  df-dom 8366  df-sdom 8367  df-fin 8368  df-pnf 10530  df-mnf 10531  df-xr 10532  df-ltxr 10533  df-le 10534  df-sub 10725  df-neg 10726  df-div 11152  df-nn 11493  df-2 11554  df-3 11555  df-n0 11752  df-z 11836  df-uz 12098  df-rp 12244  df-xneg 12361  df-xadd 12362  df-xmul 12363  df-seq 13224  df-exp 13284  df-psmet 20223  df-xmet 20224  df-met 20225  df-bl 20226  df-cmet 23547

This theorem is referenced by:  heiborlem8  34649  heiborlem9  34650