Theorem heiborlem6 32785

Description: Lemma for heibor 32790. 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 11176	. . . 4 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
2		heibor.6	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))
3		cmetmet 22892	. . . . . . . 8 ⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
4	2, 3	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
5		metxmet 21949	. . . . . . 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 3795	. . . . . . . . 9 ⊢ (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋
10		fss 5969	. . . . . . . . 9 ⊢ ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋) → 𝐹:ℕ0⟶𝒫 𝑋)
11	8, 9, 10	sylancl 693	. . . . . . . 8 ⊢ (𝜑 → 𝐹:ℕ0⟶𝒫 𝑋)
12		peano2nn0 11210	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
13		ffvelrn 6265	. . . . . . . 8 ⊢ ((𝐹:ℕ0⟶𝒫 𝑋 ∧ (𝑘 + 1) ∈ ℕ0) → (𝐹‘(𝑘 + 1)) ∈ 𝒫 𝑋)
14	11, 12, 13	syl2an 493	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘(𝑘 + 1)) ∈ 𝒫 𝑋)
15	14	elpwid 4118	. . . . . 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 32783	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑘 + 1) ∈ ℕ0) → (𝑆‘(𝑘 + 1))𝐺(𝑘 + 1))
25	12, 24	sylan2 490	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1))𝐺(𝑘 + 1))
26		fvex 6113	. . . . . . . . 9 ⊢ (𝑆‘(𝑘 + 1)) ∈ V
27		ovex 6577	. . . . . . . . 9 ⊢ (𝑘 + 1) ∈ V
28	16, 17, 18, 26, 27	heiborlem2 32781	. . . . . . . 8 ⊢ ((𝑆‘(𝑘 + 1))𝐺(𝑘 + 1) ↔ ((𝑘 + 1) ∈ ℕ0 ∧ (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)) ∧ ((𝑆‘(𝑘 + 1))𝐵(𝑘 + 1)) ∈ 𝐾))
29	28	simp2bi 1070	. . . . . . 7 ⊢ ((𝑆‘(𝑘 + 1))𝐺(𝑘 + 1) → (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)))
30	25, 29	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)))
31	15, 30	sseldd 3569	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) ∈ 𝑋)
32	11	ffvelrnda 6267	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) ∈ 𝒫 𝑋)
33	32	elpwid 4118	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) ⊆ 𝑋)
34	16, 17, 18, 19, 2, 8, 20, 21, 22, 23	heiborlem4 32783	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘𝑘)𝐺𝑘)
35		fvex 6113	. . . . . . . . 9 ⊢ (𝑆‘𝑘) ∈ V
36		vex 3176	. . . . . . . . 9 ⊢ 𝑘 ∈ V
37	16, 17, 18, 35, 36	heiborlem2 32781	. . . . . . . 8 ⊢ ((𝑆‘𝑘)𝐺𝑘 ↔ (𝑘 ∈ ℕ0 ∧ (𝑆‘𝑘) ∈ (𝐹‘𝑘) ∧ ((𝑆‘𝑘)𝐵𝑘) ∈ 𝐾))
38	37	simp2bi 1070	. . . . . . 7 ⊢ ((𝑆‘𝑘)𝐺𝑘 → (𝑆‘𝑘) ∈ (𝐹‘𝑘))
39	34, 38	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘𝑘) ∈ (𝐹‘𝑘))
40	33, 39	sseldd 3569	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘𝑘) ∈ 𝑋)
41		3re 10971	. . . . . 6 ⊢ 3 ∈ ℝ
42		2nn 11062	. . . . . . . . 9 ⊢ 2 ∈ ℕ
43		nnexpcl 12735	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ (𝑘 + 1) ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℕ)
44	42, 12, 43	sylancr 694	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) ∈ ℕ)
45	44	nnrpd 11746	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) ∈ ℝ+)
46	45	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℝ+)
47		rerpdivcl 11737	. . . . . 6 ⊢ ((3 ∈ ℝ ∧ (2↑(𝑘 + 1)) ∈ ℝ+) → (3 / (2↑(𝑘 + 1))) ∈ ℝ)
48	41, 46, 47	sylancr 694	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (3 / (2↑(𝑘 + 1))) ∈ ℝ)
49		nnexpcl 12735	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
50	42, 49	mpan 702	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → (2↑𝑘) ∈ ℕ)
51	50	nnrpd 11746	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 → (2↑𝑘) ∈ ℝ+)
52	51	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℝ+)
53		rerpdivcl 11737	. . . . . 6 ⊢ ((3 ∈ ℝ ∧ (2↑𝑘) ∈ ℝ+) → (3 / (2↑𝑘)) ∈ ℝ)
54	41, 52, 53	sylancr 694	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (3 / (2↑𝑘)) ∈ ℝ)
55		oveq1 6556	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝑆‘𝑘) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑚))))
56		oveq2 6557	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑘 → (2↑𝑚) = (2↑𝑘))
57	56	oveq2d 6565	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑘 → (1 / (2↑𝑚)) = (1 / (2↑𝑘)))
58	57	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑘 → ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑚))) = ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
59		ovex 6577	. . . . . . . . . . . 12 ⊢ ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∈ V
60	55, 58, 19, 59	ovmpt2 6694	. . . . . . . . . . 11 ⊢ (((𝑆‘𝑘) ∈ 𝑋 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐵𝑘) = ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
61	40, 60	sylancom 698	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐵𝑘) = ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
62		df-br 4584	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆‘𝑘)𝐺𝑘 ↔ ⟨(𝑆‘𝑘), 𝑘⟩ ∈ 𝐺)
63		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (𝑇‘𝑥) = (𝑇‘⟨(𝑆‘𝑘), 𝑘⟩))
64		df-ov 6552	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆‘𝑘)𝑇𝑘) = (𝑇‘⟨(𝑆‘𝑘), 𝑘⟩)
65	63, 64	syl6eqr 2662	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (𝑇‘𝑥) = ((𝑆‘𝑘)𝑇𝑘))
66	35, 36	op2ndd 7070	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (2nd ‘𝑥) = 𝑘)
67	66	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → ((2nd ‘𝑥) + 1) = (𝑘 + 1))
68	65, 67	breq12d 4596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ↔ ((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1)))
69		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (𝐵‘𝑥) = (𝐵‘⟨(𝑆‘𝑘), 𝑘⟩))
70		df-ov 6552	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆‘𝑘)𝐵𝑘) = (𝐵‘⟨(𝑆‘𝑘), 𝑘⟩)
71	69, 70	syl6eqr 2662	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (𝐵‘𝑥) = ((𝑆‘𝑘)𝐵𝑘))
72	65, 67	oveq12d 6567	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1)) = (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1)))
73	71, 72	ineq12d 3777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) = (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))))
74	73	eleq1d 2672	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 ↔ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾))
75	68, 74	anbi12d 743	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = ⟨(𝑆‘𝑘), 𝑘⟩ → (((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) ↔ (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
76	75	rspccv 3279	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) → (⟨(𝑆‘𝑘), 𝑘⟩ ∈ 𝐺 → (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
77	21, 76	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (⟨(𝑆‘𝑘), 𝑘⟩ ∈ 𝐺 → (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
78	62, 77	syl5bi 231	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑆‘𝑘)𝐺𝑘 → (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
79	78	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐺𝑘 → (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
80	34, 79	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾))
81	80	simpld 474	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1))
82		ovex 6577	. . . . . . . . . . . . . . 15 ⊢ ((𝑆‘𝑘)𝑇𝑘) ∈ V
83	16, 17, 18, 82, 27	heiborlem2 32781	. . . . . . . . . . . . . 14 ⊢ (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ↔ ((𝑘 + 1) ∈ ℕ0 ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)) ∧ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1)) ∈ 𝐾))
84	83	simp2bi 1070	. . . . . . . . . . . . 13 ⊢ (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) → ((𝑆‘𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)))
85	81, 84	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)))
86	15, 85	sseldd 3569	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋)
87	12	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℕ0)
88		oveq1 6556	. . . . . . . . . . . 12 ⊢ (𝑧 = ((𝑆‘𝑘)𝑇𝑘) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑𝑚))))
89		oveq2 6557	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑘 + 1) → (2↑𝑚) = (2↑(𝑘 + 1)))
90	89	oveq2d 6565	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑘 + 1) → (1 / (2↑𝑚)) = (1 / (2↑(𝑘 + 1))))
91	90	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑘 + 1) → (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑𝑚))) = (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
92		ovex 6577	. . . . . . . . . . . 12 ⊢ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))) ∈ V
93	88, 91, 19, 92	ovmpt2 6694	. . . . . . . . . . 11 ⊢ ((((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋 ∧ (𝑘 + 1) ∈ ℕ0) → (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1)) = (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
94	86, 87, 93	syl2anc 691	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1)) = (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
95	61, 94	ineq12d 3777	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) = (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))))
96	80	simprd 478	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)
97		0elpw 4760	. . . . . . . . . . . . 13 ⊢ ∅ ∈ 𝒫 𝑈
98		0fin 8073	. . . . . . . . . . . . 13 ⊢ ∅ ∈ Fin
99		elin 3758	. . . . . . . . . . . . 13 ⊢ (∅ ∈ (𝒫 𝑈 ∩ Fin) ↔ (∅ ∈ 𝒫 𝑈 ∧ ∅ ∈ Fin))
100	97, 98, 99	mpbir2an 957	. . . . . . . . . . . 12 ⊢ ∅ ∈ (𝒫 𝑈 ∩ Fin)
101		0ss 3924	. . . . . . . . . . . 12 ⊢ ∅ ⊆ ∪ ∅
102		unieq 4380	. . . . . . . . . . . . . 14 ⊢ (𝑣 = ∅ → ∪ 𝑣 = ∪ ∅)
103	102	sseq2d 3596	. . . . . . . . . . . . 13 ⊢ (𝑣 = ∅ → (∅ ⊆ ∪ 𝑣 ↔ ∅ ⊆ ∪ ∅))
104	103	rspcev 3282	. . . . . . . . . . . 12 ⊢ ((∅ ∈ (𝒫 𝑈 ∩ Fin) ∧ ∅ ⊆ ∪ ∅) → ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣)
105	100, 101, 104	mp2an 704	. . . . . . . . . . 11 ⊢ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣
106		0ex 4718	. . . . . . . . . . . . 13 ⊢ ∅ ∈ V
107		sseq1 3589	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = ∅ → (𝑢 ⊆ ∪ 𝑣 ↔ ∅ ⊆ ∪ 𝑣))
108	107	rexbidv 3034	. . . . . . . . . . . . . 14 ⊢ (𝑢 = ∅ → (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣 ↔ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣))
109	108	notbid 307	. . . . . . . . . . . . 13 ⊢ (𝑢 = ∅ → (¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣))
110	106, 109, 17	elab2 3323	. . . . . . . . . . . 12 ⊢ (∅ ∈ 𝐾 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣)
111	110	con2bii 346	. . . . . . . . . . 11 ⊢ (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣 ↔ ¬ ∅ ∈ 𝐾)
112	105, 111	mpbi 219	. . . . . . . . . 10 ⊢ ¬ ∅ ∈ 𝐾
113		nelne2 2879	. . . . . . . . . 10 ⊢ (((((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾 ∧ ¬ ∅ ∈ 𝐾) → (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ≠ ∅)
114	96, 112, 113	sylancl 693	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ≠ ∅)
115	95, 114	eqnetrrd 2850	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) ≠ ∅)
116	51	rpreccld 11758	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 → (1 / (2↑𝑘)) ∈ ℝ+)
117	116	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ+)
118	117	rpred 11748	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ)
119	45	rpreccld 11758	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 → (1 / (2↑(𝑘 + 1))) ∈ ℝ+)
120	119	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ+)
121	120	rpred 11748	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ)
122		rexadd 11937	. . . . . . . . . . . 12 ⊢ (((1 / (2↑𝑘)) ∈ ℝ ∧ (1 / (2↑(𝑘 + 1))) ∈ ℝ) → ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
123	118, 121, 122	syl2anc 691	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
124	123	breq1d 4593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ↔ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘))))
125	117	rpxrd 11749	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ*)
126	120	rpxrd 11749	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ*)
127		bldisj 22013	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆‘𝑘) ∈ 𝑋 ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋) ∧ ((1 / (2↑𝑘)) ∈ ℝ* ∧ (1 / (2↑(𝑘 + 1))) ∈ ℝ* ∧ ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)))) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅)
128	127	3exp2 1277	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆‘𝑘) ∈ 𝑋 ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋) → ((1 / (2↑𝑘)) ∈ ℝ* → ((1 / (2↑(𝑘 + 1))) ∈ ℝ* → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))))
129	128	imp32 448	. . . . . . . . . . 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 1326	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))
131	124, 130	sylbird 249	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))
132	131	necon3ad 2795	. . . . . . . 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 11763	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ∈ ℝ+)
135	134	rpred 11748	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ∈ ℝ)
136	4	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐷 ∈ (Met‘𝑋))
137		metcl 21947	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝑆‘𝑘) ∈ 𝑋 ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋) → ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ∈ ℝ)
138	136, 40, 86, 137	syl3anc 1318	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ∈ ℝ)
139	135, 138	letrid 10068	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ∨ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ≤ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1))))))
140	139	ord 391	. . . . . . 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 12678	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ≥‘0) → (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1)) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
143		nn0uz 11598	. . . . . . . . . . . 12 ⊢ ℕ0 = (ℤ≥‘0)
144	142, 143	eleq2s 2706	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1)) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
145	23	fveq1i 6104	. . . . . . . . . . 11 ⊢ (𝑆‘(𝑘 + 1)) = (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1))
146	23	fveq1i 6104	. . . . . . . . . . . 12 ⊢ (𝑆‘𝑘) = (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)
147	146	oveq1i 6559	. . . . . . . . . . 11 ⊢ ((𝑆‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)))
148	144, 145, 147	3eqtr4g 2669	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → (𝑆‘(𝑘 + 1)) = ((𝑆‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
149		nn0p1nn 11209	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ)
150		nnne0 10930	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 + 1) ∈ ℕ → (𝑘 + 1) ≠ 0)
151	150	neneqd 2787	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 + 1) ∈ ℕ → ¬ (𝑘 + 1) = 0)
152	149, 151	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ0 → ¬ (𝑘 + 1) = 0)
153	152	iffalsed 4047	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 → if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)) = ((𝑘 + 1) − 1))
154		ovex 6577	. . . . . . . . . . . . . 14 ⊢ ((𝑘 + 1) − 1) ∈ V
155	153, 154	syl6eqel 2696	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ0 → if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)) ∈ V)
156		eqeq1 2614	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝑘 + 1) → (𝑚 = 0 ↔ (𝑘 + 1) = 0))
157		oveq1 6556	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝑘 + 1) → (𝑚 − 1) = ((𝑘 + 1) − 1))
158	156, 157	ifbieq2d 4061	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑘 + 1) → if(𝑚 = 0, 𝐶, (𝑚 − 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)))
159		eqid 2610	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))) = (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))
160	158, 159	fvmptg 6189	. . . . . . . . . . . . 13 ⊢ (((𝑘 + 1) ∈ ℕ0 ∧ if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)) ∈ V) → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)))
161	12, 155, 160	syl2anc 691	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)))
162		nn0cn 11179	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ)
163		ax-1cn 9873	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
164		pncan 10166	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
165	162, 163, 164	sylancl 693	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 → ((𝑘 + 1) − 1) = 𝑘)
166	161, 153, 165	3eqtrd 2648	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = 𝑘)
167	166	oveq2d 6565	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → ((𝑆‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))) = ((𝑆‘𝑘)𝑇𝑘))
168	148, 167	eqtrd 2644	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 → (𝑆‘(𝑘 + 1)) = ((𝑆‘𝑘)𝑇𝑘))
169	168	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) = ((𝑆‘𝑘)𝑇𝑘))
170	169	oveq1d 6564	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆‘𝑘)) = (((𝑆‘𝑘)𝑇𝑘)𝐷(𝑆‘𝑘)))
171		metsym 21965	. . . . . . . 8 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋 ∧ (𝑆‘𝑘) ∈ 𝑋) → (((𝑆‘𝑘)𝑇𝑘)𝐷(𝑆‘𝑘)) = ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)))
172	136, 86, 40, 171	syl3anc 1318	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝑇𝑘)𝐷(𝑆‘𝑘)) = ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)))
173	170, 172	eqtrd 2644	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆‘𝑘)) = ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)))
174		3cn 10972	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℂ
175	174	2timesi 11024	. . . . . . . . . . . 12 ⊢ (2 · 3) = (3 + 3)
176	175	oveq1i 6559	. . . . . . . . . . 11 ⊢ ((2 · 3) − 3) = ((3 + 3) − 3)
177	174, 174	pncan3oi 10176	. . . . . . . . . . 11 ⊢ ((3 + 3) − 3) = 3
178		df-3 10957	. . . . . . . . . . 11 ⊢ 3 = (2 + 1)
179	176, 177, 178	3eqtri 2636	. . . . . . . . . 10 ⊢ ((2 · 3) − 3) = (2 + 1)
180	179	oveq1i 6559	. . . . . . . . 9 ⊢ (((2 · 3) − 3) / (2↑(𝑘 + 1))) = ((2 + 1) / (2↑(𝑘 + 1)))
181		rpcn 11717	. . . . . . . . . . 11 ⊢ ((2↑(𝑘 + 1)) ∈ ℝ+ → (2↑(𝑘 + 1)) ∈ ℂ)
182		rpne0 11724	. . . . . . . . . . 11 ⊢ ((2↑(𝑘 + 1)) ∈ ℝ+ → (2↑(𝑘 + 1)) ≠ 0)
183		2cn 10968	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℂ
184	183, 174	mulcli 9924	. . . . . . . . . . . 12 ⊢ (2 · 3) ∈ ℂ
185		divsubdir 10600	. . . . . . . . . . . 12 ⊢ (((2 · 3) ∈ ℂ ∧ 3 ∈ ℂ ∧ ((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0)) → (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
186	184, 174, 185	mp3an12 1406	. . . . . . . . . . 11 ⊢ (((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0) → (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
187	181, 182, 186	syl2anc 691	. . . . . . . . . 10 ⊢ ((2↑(𝑘 + 1)) ∈ ℝ+ → (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
188	45, 187	syl 17	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 → (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
189		divdir 10589	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 1 ∈ ℂ ∧ ((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0)) → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
190	183, 163, 189	mp3an12 1406	. . . . . . . . . . 11 ⊢ (((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0) → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
191	181, 182, 190	syl2anc 691	. . . . . . . . . 10 ⊢ ((2↑(𝑘 + 1)) ∈ ℝ+ → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
192	45, 191	syl 17	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
193	180, 188, 192	3eqtr3a 2668	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
194		rpcn 11717	. . . . . . . . . . . 12 ⊢ ((2↑𝑘) ∈ ℝ+ → (2↑𝑘) ∈ ℂ)
195		rpne0 11724	. . . . . . . . . . . 12 ⊢ ((2↑𝑘) ∈ ℝ+ → (2↑𝑘) ≠ 0)
196		2cnne0 11119	. . . . . . . . . . . . 13 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
197		divcan5 10606	. . . . . . . . . . . . 13 ⊢ ((3 ∈ ℂ ∧ ((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
198	174, 196, 197	mp3an13 1407	. . . . . . . . . . . 12 ⊢ (((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
199	194, 195, 198	syl2anc 691	. . . . . . . . . . 11 ⊢ ((2↑𝑘) ∈ ℝ+ → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
200	51, 199	syl 17	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
201	51, 194	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ0 → (2↑𝑘) ∈ ℂ)
202		mulcom 9901	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ (2↑𝑘) ∈ ℂ) → (2 · (2↑𝑘)) = ((2↑𝑘) · 2))
203	183, 201, 202	sylancr 694	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 → (2 · (2↑𝑘)) = ((2↑𝑘) · 2))
204		expp1 12729	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (2↑(𝑘 + 1)) = ((2↑𝑘) · 2))
205	183, 204	mpan 702	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) = ((2↑𝑘) · 2))
206	203, 205	eqtr4d 2647	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → (2 · (2↑𝑘)) = (2↑(𝑘 + 1)))
207	206	oveq2d 6565	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → ((2 · 3) / (2 · (2↑𝑘))) = ((2 · 3) / (2↑(𝑘 + 1))))
208	200, 207	eqtr3d 2646	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 → (3 / (2↑𝑘)) = ((2 · 3) / (2↑(𝑘 + 1))))
209	208	oveq1d 6564	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
210		divcan5 10606	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℂ ∧ ((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
211	163, 196, 210	mp3an13 1407	. . . . . . . . . . . 12 ⊢ (((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
212	194, 195, 211	syl2anc 691	. . . . . . . . . . 11 ⊢ ((2↑𝑘) ∈ ℝ+ → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
213	51, 212	syl 17	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
214		2t1e2 11053	. . . . . . . . . . . 12 ⊢ (2 · 1) = 2
215	214	a1i 11	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → (2 · 1) = 2)
216	215, 206	oveq12d 6567	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → ((2 · 1) / (2 · (2↑𝑘))) = (2 / (2↑(𝑘 + 1))))
217	213, 216	eqtr3d 2646	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 → (1 / (2↑𝑘)) = (2 / (2↑(𝑘 + 1))))
218	217	oveq1d 6564	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
219	193, 209, 218	3eqtr4d 2654	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
220	219	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
221	141, 173, 220	3brtr4d 4615	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆‘𝑘)) ≤ ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))))
222		blss2 22019	. . . . 5 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆‘(𝑘 + 1)) ∈ 𝑋 ∧ (𝑆‘𝑘) ∈ 𝑋) ∧ ((3 / (2↑(𝑘 + 1))) ∈ ℝ ∧ (3 / (2↑𝑘)) ∈ ℝ ∧ ((𝑆‘(𝑘 + 1))𝐷(𝑆‘𝑘)) ≤ ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))))) → ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) ⊆ ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
223	7, 31, 40, 48, 54, 221, 222	syl33anc 1333	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) ⊆ ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
224	1, 223	sylan2 490	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) ⊆ ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
225		peano2nn 10909	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
226		fveq2 6103	. . . . . . . . 9 ⊢ (𝑛 = (𝑘 + 1) → (𝑆‘𝑛) = (𝑆‘(𝑘 + 1)))
227		oveq2 6557	. . . . . . . . . 10 ⊢ (𝑛 = (𝑘 + 1) → (2↑𝑛) = (2↑(𝑘 + 1)))
228	227	oveq2d 6565	. . . . . . . . 9 ⊢ (𝑛 = (𝑘 + 1) → (3 / (2↑𝑛)) = (3 / (2↑(𝑘 + 1))))
229	226, 228	opeq12d 4348	. . . . . . . 8 ⊢ (𝑛 = (𝑘 + 1) → ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩ = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
230		heibor.12	. . . . . . . 8 ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩)
231		opex 4859	. . . . . . . 8 ⊢ ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩ ∈ V
232	229, 230, 231	fvmpt 6191	. . . . . . 7 ⊢ ((𝑘 + 1) ∈ ℕ → (𝑀‘(𝑘 + 1)) = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
233	225, 232	syl 17	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (𝑀‘(𝑘 + 1)) = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
234	233	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑀‘(𝑘 + 1)) = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
235	234	fveq2d 6107	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) = ((ball‘𝐷)‘⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩))
236		df-ov 6552	. . . 4 ⊢ ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) = ((ball‘𝐷)‘⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
237	235, 236	syl6eqr 2662	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) = ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))))
238		fveq2 6103	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (𝑆‘𝑛) = (𝑆‘𝑘))
239		oveq2 6557	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (2↑𝑛) = (2↑𝑘))
240	239	oveq2d 6565	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (3 / (2↑𝑛)) = (3 / (2↑𝑘)))
241	238, 240	opeq12d 4348	. . . . . . 7 ⊢ (𝑛 = 𝑘 → ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩ = ⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩)
242		opex 4859	. . . . . . 7 ⊢ ⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩ ∈ V
243	241, 230, 242	fvmpt 6191	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (𝑀‘𝑘) = ⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩)
244	243	fveq2d 6107	. . . . 5 ⊢ (𝑘 ∈ ℕ → ((ball‘𝐷)‘(𝑀‘𝑘)) = ((ball‘𝐷)‘⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩))
245		df-ov 6552	. . . . 5 ⊢ ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))) = ((ball‘𝐷)‘⟨(𝑆‘𝑘), (3 / (2↑𝑘))⟩)
246	244, 245	syl6eqr 2662	. . . 4 ⊢ (𝑘 ∈ ℕ → ((ball‘𝐷)‘(𝑀‘𝑘)) = ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
247	246	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘𝑘)) = ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
248	224, 237, 247	3sstr4d 3611	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀‘𝑘)))
249	248	ralrimiva 2949	1 ⊢ (𝜑 → ∀𝑘 ∈ ℕ ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀‘𝑘)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  ifcif 4036  𝒫 cpw 4108  ⟨cop 4131  ∪ cuni 4372  ∪ ciun 4455   class class class wbr 4583  {copab 4642   ↦ cmpt 4643  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  2^nd c2nd 7058  Fincfn 7841  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820  ℝ^*cxr 9952   ≤ cle 9954   − cmin 10145   / cdiv 10563  ℕcn 10897  2c2 10947  3c3 10948  ℕ₀cn0 11169  ℤ_≥cuz 11563  ℝ⁺crp 11708   +_𝑒 cxad 11820  seqcseq 12663  ↑cexp 12722  ∞Metcxmt 19552  Metcme 19553  ballcbl 19554  MetOpencmopn 19557  CMetcms 22860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-seq 12664  df-exp 12723  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-cmet 22863

This theorem is referenced by:  heiborlem8  32787  heiborlem9  32788