Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  heiborlem6 Structured version   Visualization version   GIF version
Theorem heiborlem6 36770
Description: Lemma for heibor 36775. 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
StepHypRef Expression
1 nnnn0 12481 . . . 4 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„•0)
2 heibor.6 . . . . . . . 8 (πœ‘ β†’ 𝐷 ∈ (CMetβ€˜π‘‹))
3 cmetmet 24810 . . . . . . . 8 (𝐷 ∈ (CMetβ€˜π‘‹) β†’ 𝐷 ∈ (Metβ€˜π‘‹))
42, 3syl 17 . . . . . . 7 (πœ‘ β†’ 𝐷 ∈ (Metβ€˜π‘‹))
5 metxmet 23847 . . . . . . 7 (𝐷 ∈ (Metβ€˜π‘‹) β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
64, 5syl 17 . . . . . 6 (πœ‘ β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
76adantr 481 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
8 heibor.7 . . . . . . . . 9 (πœ‘ β†’ 𝐹:β„•0⟢(𝒫 𝑋 ∩ Fin))
9 inss1 4228 . . . . . . . . 9 (𝒫 𝑋 ∩ Fin) βŠ† 𝒫 𝑋
10 fss 6734 . . . . . . . . 9 ((𝐹:β„•0⟢(𝒫 𝑋 ∩ Fin) ∧ (𝒫 𝑋 ∩ Fin) βŠ† 𝒫 𝑋) β†’ 𝐹:β„•0βŸΆπ’« 𝑋)
118, 9, 10sylancl 586 . . . . . . . 8 (πœ‘ β†’ 𝐹:β„•0βŸΆπ’« 𝑋)
12 peano2nn0 12514 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ (π‘˜ + 1) ∈ β„•0)
13 ffvelcdm 7083 . . . . . . . 8 ((𝐹:β„•0βŸΆπ’« 𝑋 ∧ (π‘˜ + 1) ∈ β„•0) β†’ (πΉβ€˜(π‘˜ + 1)) ∈ 𝒫 𝑋)
1411, 12, 13syl2an 596 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (πΉβ€˜(π‘˜ + 1)) ∈ 𝒫 𝑋)
1514elpwid 4611 . . . . . 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))))
2416, 17, 18, 19, 2, 8, 20, 21, 22, 23heiborlem4 36768 . . . . . . . 8 ((πœ‘ ∧ (π‘˜ + 1) ∈ β„•0) β†’ (π‘†β€˜(π‘˜ + 1))𝐺(π‘˜ + 1))
2512, 24sylan2 593 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘†β€˜(π‘˜ + 1))𝐺(π‘˜ + 1))
26 fvex 6904 . . . . . . . . 9 (π‘†β€˜(π‘˜ + 1)) ∈ V
27 ovex 7444 . . . . . . . . 9 (π‘˜ + 1) ∈ V
2816, 17, 18, 26, 27heiborlem2 36766 . . . . . . . 8 ((π‘†β€˜(π‘˜ + 1))𝐺(π‘˜ + 1) ↔ ((π‘˜ + 1) ∈ β„•0 ∧ (π‘†β€˜(π‘˜ + 1)) ∈ (πΉβ€˜(π‘˜ + 1)) ∧ ((π‘†β€˜(π‘˜ + 1))𝐡(π‘˜ + 1)) ∈ 𝐾))
2928simp2bi 1146 . . . . . . 7 ((π‘†β€˜(π‘˜ + 1))𝐺(π‘˜ + 1) β†’ (π‘†β€˜(π‘˜ + 1)) ∈ (πΉβ€˜(π‘˜ + 1)))
3025, 29syl 17 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘†β€˜(π‘˜ + 1)) ∈ (πΉβ€˜(π‘˜ + 1)))
3115, 30sseldd 3983 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘†β€˜(π‘˜ + 1)) ∈ 𝑋)
3211ffvelcdmda 7086 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (πΉβ€˜π‘˜) ∈ 𝒫 𝑋)
3332elpwid 4611 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (πΉβ€˜π‘˜) βŠ† 𝑋)
3416, 17, 18, 19, 2, 8, 20, 21, 22, 23heiborlem4 36768 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘†β€˜π‘˜)πΊπ‘˜)
35 fvex 6904 . . . . . . . . 9 (π‘†β€˜π‘˜) ∈ V
36 vex 3478 . . . . . . . . 9 π‘˜ ∈ V
3716, 17, 18, 35, 36heiborlem2 36766 . . . . . . . 8 ((π‘†β€˜π‘˜)πΊπ‘˜ ↔ (π‘˜ ∈ β„•0 ∧ (π‘†β€˜π‘˜) ∈ (πΉβ€˜π‘˜) ∧ ((π‘†β€˜π‘˜)π΅π‘˜) ∈ 𝐾))
3837simp2bi 1146 . . . . . . 7 ((π‘†β€˜π‘˜)πΊπ‘˜ β†’ (π‘†β€˜π‘˜) ∈ (πΉβ€˜π‘˜))
3934, 38syl 17 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘†β€˜π‘˜) ∈ (πΉβ€˜π‘˜))
4033, 39sseldd 3983 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘†β€˜π‘˜) ∈ 𝑋)
41 3re 12294 . . . . . 6 3 ∈ ℝ
42 2nn 12287 . . . . . . . . 9 2 ∈ β„•
43 nnexpcl 14042 . . . . . . . . 9 ((2 ∈ β„• ∧ (π‘˜ + 1) ∈ β„•0) β†’ (2↑(π‘˜ + 1)) ∈ β„•)
4442, 12, 43sylancr 587 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ (2↑(π‘˜ + 1)) ∈ β„•)
4544nnrpd 13016 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ (2↑(π‘˜ + 1)) ∈ ℝ+)
4645adantl 482 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (2↑(π‘˜ + 1)) ∈ ℝ+)
47 rerpdivcl 13006 . . . . . 6 ((3 ∈ ℝ ∧ (2↑(π‘˜ + 1)) ∈ ℝ+) β†’ (3 / (2↑(π‘˜ + 1))) ∈ ℝ)
4841, 46, 47sylancr 587 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (3 / (2↑(π‘˜ + 1))) ∈ ℝ)
49 nnexpcl 14042 . . . . . . . . 9 ((2 ∈ β„• ∧ π‘˜ ∈ β„•0) β†’ (2β†‘π‘˜) ∈ β„•)
5042, 49mpan 688 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ (2β†‘π‘˜) ∈ β„•)
5150nnrpd 13016 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ (2β†‘π‘˜) ∈ ℝ+)
5251adantl 482 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (2β†‘π‘˜) ∈ ℝ+)
53 rerpdivcl 13006 . . . . . 6 ((3 ∈ ℝ ∧ (2β†‘π‘˜) ∈ ℝ+) β†’ (3 / (2β†‘π‘˜)) ∈ ℝ)
5441, 52, 53sylancr 587 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (3 / (2β†‘π‘˜)) ∈ ℝ)
55 oveq1 7418 . . . . . . . . . . . 12 (𝑧 = (π‘†β€˜π‘˜) β†’ (𝑧(ballβ€˜π·)(1 / (2β†‘π‘š))) = ((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘š))))
56 oveq2 7419 . . . . . . . . . . . . . 14 (π‘š = π‘˜ β†’ (2β†‘π‘š) = (2β†‘π‘˜))
5756oveq2d 7427 . . . . . . . . . . . . 13 (π‘š = π‘˜ β†’ (1 / (2β†‘π‘š)) = (1 / (2β†‘π‘˜)))
5857oveq2d 7427 . . . . . . . . . . . 12 (π‘š = π‘˜ β†’ ((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘š))) = ((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘˜))))
59 ovex 7444 . . . . . . . . . . . 12 ((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘˜))) ∈ V
6055, 58, 19, 59ovmpo 7570 . . . . . . . . . . 11 (((π‘†β€˜π‘˜) ∈ 𝑋 ∧ π‘˜ ∈ β„•0) β†’ ((π‘†β€˜π‘˜)π΅π‘˜) = ((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘˜))))
6140, 60sylancom 588 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘†β€˜π‘˜)π΅π‘˜) = ((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘˜))))
62 df-br 5149 . . . . . . . . . . . . . . . . 17 ((π‘†β€˜π‘˜)πΊπ‘˜ ↔ ⟨(π‘†β€˜π‘˜), π‘˜βŸ© ∈ 𝐺)
63 fveq2 6891 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = ⟨(π‘†β€˜π‘˜), π‘˜βŸ© β†’ (π‘‡β€˜π‘₯) = (π‘‡β€˜βŸ¨(π‘†β€˜π‘˜), π‘˜βŸ©))
64 df-ov 7414 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘†β€˜π‘˜)π‘‡π‘˜) = (π‘‡β€˜βŸ¨(π‘†β€˜π‘˜), π‘˜βŸ©)
6563, 64eqtr4di 2790 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = ⟨(π‘†β€˜π‘˜), π‘˜βŸ© β†’ (π‘‡β€˜π‘₯) = ((π‘†β€˜π‘˜)π‘‡π‘˜))
6635, 36op2ndd 7988 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = ⟨(π‘†β€˜π‘˜), π‘˜βŸ© β†’ (2nd β€˜π‘₯) = π‘˜)
6766oveq1d 7426 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = ⟨(π‘†β€˜π‘˜), π‘˜βŸ© β†’ ((2nd β€˜π‘₯) + 1) = (π‘˜ + 1))
6865, 67breq12d 5161 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = ⟨(π‘†β€˜π‘˜), π‘˜βŸ© β†’ ((π‘‡β€˜π‘₯)𝐺((2nd β€˜π‘₯) + 1) ↔ ((π‘†β€˜π‘˜)π‘‡π‘˜)𝐺(π‘˜ + 1)))
69 fveq2 6891 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ = ⟨(π‘†β€˜π‘˜), π‘˜βŸ© β†’ (π΅β€˜π‘₯) = (π΅β€˜βŸ¨(π‘†β€˜π‘˜), π‘˜βŸ©))
70 df-ov 7414 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘†β€˜π‘˜)π΅π‘˜) = (π΅β€˜βŸ¨(π‘†β€˜π‘˜), π‘˜βŸ©)
7169, 70eqtr4di 2790 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = ⟨(π‘†β€˜π‘˜), π‘˜βŸ© β†’ (π΅β€˜π‘₯) = ((π‘†β€˜π‘˜)π΅π‘˜))
7265, 67oveq12d 7429 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = ⟨(π‘†β€˜π‘˜), π‘˜βŸ© β†’ ((π‘‡β€˜π‘₯)𝐡((2nd β€˜π‘₯) + 1)) = (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1)))
7371, 72ineq12d 4213 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = ⟨(π‘†β€˜π‘˜), π‘˜βŸ© β†’ ((π΅β€˜π‘₯) ∩ ((π‘‡β€˜π‘₯)𝐡((2nd β€˜π‘₯) + 1))) = (((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))))
7473eleq1d 2818 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = ⟨(π‘†β€˜π‘˜), π‘˜βŸ© β†’ (((π΅β€˜π‘₯) ∩ ((π‘‡β€˜π‘₯)𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾 ↔ (((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))) ∈ 𝐾))
7568, 74anbi12d 631 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = ⟨(π‘†β€˜π‘˜), π‘˜βŸ© β†’ (((π‘‡β€˜π‘₯)𝐺((2nd β€˜π‘₯) + 1) ∧ ((π΅β€˜π‘₯) ∩ ((π‘‡β€˜π‘₯)𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾) ↔ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐺(π‘˜ + 1) ∧ (((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))) ∈ 𝐾)))
7675rspccv 3609 . . . . . . . . . . . . . . . . . 18 (βˆ€π‘₯ ∈ 𝐺 ((π‘‡β€˜π‘₯)𝐺((2nd β€˜π‘₯) + 1) ∧ ((π΅β€˜π‘₯) ∩ ((π‘‡β€˜π‘₯)𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾) β†’ (⟨(π‘†β€˜π‘˜), π‘˜βŸ© ∈ 𝐺 β†’ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐺(π‘˜ + 1) ∧ (((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))) ∈ 𝐾)))
7721, 76syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (⟨(π‘†β€˜π‘˜), π‘˜βŸ© ∈ 𝐺 β†’ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐺(π‘˜ + 1) ∧ (((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))) ∈ 𝐾)))
7862, 77biimtrid 241 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((π‘†β€˜π‘˜)πΊπ‘˜ β†’ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐺(π‘˜ + 1) ∧ (((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))) ∈ 𝐾)))
7978adantr 481 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘†β€˜π‘˜)πΊπ‘˜ β†’ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐺(π‘˜ + 1) ∧ (((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))) ∈ 𝐾)))
8034, 79mpd 15 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐺(π‘˜ + 1) ∧ (((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))) ∈ 𝐾))
8180simpld 495 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘†β€˜π‘˜)π‘‡π‘˜)𝐺(π‘˜ + 1))
82 ovex 7444 . . . . . . . . . . . . . . 15 ((π‘†β€˜π‘˜)π‘‡π‘˜) ∈ V
8316, 17, 18, 82, 27heiborlem2 36766 . . . . . . . . . . . . . 14 (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐺(π‘˜ + 1) ↔ ((π‘˜ + 1) ∈ β„•0 ∧ ((π‘†β€˜π‘˜)π‘‡π‘˜) ∈ (πΉβ€˜(π‘˜ + 1)) ∧ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1)) ∈ 𝐾))
8483simp2bi 1146 . . . . . . . . . . . . 13 (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐺(π‘˜ + 1) β†’ ((π‘†β€˜π‘˜)π‘‡π‘˜) ∈ (πΉβ€˜(π‘˜ + 1)))
8581, 84syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘†β€˜π‘˜)π‘‡π‘˜) ∈ (πΉβ€˜(π‘˜ + 1)))
8615, 85sseldd 3983 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘†β€˜π‘˜)π‘‡π‘˜) ∈ 𝑋)
8712adantl 482 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘˜ + 1) ∈ β„•0)
88 oveq1 7418 . . . . . . . . . . . 12 (𝑧 = ((π‘†β€˜π‘˜)π‘‡π‘˜) β†’ (𝑧(ballβ€˜π·)(1 / (2β†‘π‘š))) = (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘š))))
89 oveq2 7419 . . . . . . . . . . . . . 14 (π‘š = (π‘˜ + 1) β†’ (2β†‘π‘š) = (2↑(π‘˜ + 1)))
9089oveq2d 7427 . . . . . . . . . . . . 13 (π‘š = (π‘˜ + 1) β†’ (1 / (2β†‘π‘š)) = (1 / (2↑(π‘˜ + 1))))
9190oveq2d 7427 . . . . . . . . . . . 12 (π‘š = (π‘˜ + 1) β†’ (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘š))) = (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2↑(π‘˜ + 1)))))
92 ovex 7444 . . . . . . . . . . . 12 (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2↑(π‘˜ + 1)))) ∈ V
9388, 91, 19, 92ovmpo 7570 . . . . . . . . . . 11 ((((π‘†β€˜π‘˜)π‘‡π‘˜) ∈ 𝑋 ∧ (π‘˜ + 1) ∈ β„•0) β†’ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1)) = (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2↑(π‘˜ + 1)))))
9486, 87, 93syl2anc 584 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1)) = (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2↑(π‘˜ + 1)))))
9561, 94ineq12d 4213 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))) = (((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘˜))) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2↑(π‘˜ + 1))))))
9680simprd 496 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))) ∈ 𝐾)
97 0elpw 5354 . . . . . . . . . . . . 13 βˆ… ∈ 𝒫 π‘ˆ
98 0fin 9173 . . . . . . . . . . . . 13 βˆ… ∈ Fin
99 elin 3964 . . . . . . . . . . . . 13 (βˆ… ∈ (𝒫 π‘ˆ ∩ Fin) ↔ (βˆ… ∈ 𝒫 π‘ˆ ∧ βˆ… ∈ Fin))
10097, 98, 99mpbir2an 709 . . . . . . . . . . . 12 βˆ… ∈ (𝒫 π‘ˆ ∩ Fin)
101 0ss 4396 . . . . . . . . . . . 12 βˆ… βŠ† βˆͺ βˆ…
102 unieq 4919 . . . . . . . . . . . . . 14 (𝑣 = βˆ… β†’ βˆͺ 𝑣 = βˆͺ βˆ…)
103102sseq2d 4014 . . . . . . . . . . . . 13 (𝑣 = βˆ… β†’ (βˆ… βŠ† βˆͺ 𝑣 ↔ βˆ… βŠ† βˆͺ βˆ…))
104103rspcev 3612 . . . . . . . . . . . 12 ((βˆ… ∈ (𝒫 π‘ˆ ∩ Fin) ∧ βˆ… βŠ† βˆͺ βˆ…) β†’ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)βˆ… βŠ† βˆͺ 𝑣)
105100, 101, 104mp2an 690 . . . . . . . . . . 11 βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)βˆ… βŠ† βˆͺ 𝑣
106 0ex 5307 . . . . . . . . . . . . 13 βˆ… ∈ V
107 sseq1 4007 . . . . . . . . . . . . . . 15 (𝑒 = βˆ… β†’ (𝑒 βŠ† βˆͺ 𝑣 ↔ βˆ… βŠ† βˆͺ 𝑣))
108107rexbidv 3178 . . . . . . . . . . . . . 14 (𝑒 = βˆ… β†’ (βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝑒 βŠ† βˆͺ 𝑣 ↔ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)βˆ… βŠ† βˆͺ 𝑣))
109108notbid 317 . . . . . . . . . . . . 13 (𝑒 = βˆ… β†’ (Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝑒 βŠ† βˆͺ 𝑣 ↔ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)βˆ… βŠ† βˆͺ 𝑣))
110106, 109, 17elab2 3672 . . . . . . . . . . . 12 (βˆ… ∈ 𝐾 ↔ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)βˆ… βŠ† βˆͺ 𝑣)
111110con2bii 357 . . . . . . . . . . 11 (βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)βˆ… βŠ† βˆͺ 𝑣 ↔ Β¬ βˆ… ∈ 𝐾)
112105, 111mpbi 229 . . . . . . . . . 10 Β¬ βˆ… ∈ 𝐾
113 nelne2 3040 . . . . . . . . . 10 (((((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))) ∈ 𝐾 ∧ Β¬ βˆ… ∈ 𝐾) β†’ (((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))) β‰  βˆ…)
11496, 112, 113sylancl 586 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))) β‰  βˆ…)
11595, 114eqnetrrd 3009 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘˜))) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2↑(π‘˜ + 1))))) β‰  βˆ…)
11651rpreccld 13028 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„•0 β†’ (1 / (2β†‘π‘˜)) ∈ ℝ+)
117116adantl 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (1 / (2β†‘π‘˜)) ∈ ℝ+)
118117rpred 13018 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (1 / (2β†‘π‘˜)) ∈ ℝ)
11945rpreccld 13028 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„•0 β†’ (1 / (2↑(π‘˜ + 1))) ∈ ℝ+)
120119adantl 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (1 / (2↑(π‘˜ + 1))) ∈ ℝ+)
121120rpred 13018 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (1 / (2↑(π‘˜ + 1))) ∈ ℝ)
122 rexadd 13213 . . . . . . . . . . . 12 (((1 / (2β†‘π‘˜)) ∈ ℝ ∧ (1 / (2↑(π‘˜ + 1))) ∈ ℝ) β†’ ((1 / (2β†‘π‘˜)) +𝑒 (1 / (2↑(π‘˜ + 1)))) = ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))))
123118, 121, 122syl2anc 584 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((1 / (2β†‘π‘˜)) +𝑒 (1 / (2↑(π‘˜ + 1)))) = ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))))
124123breq1d 5158 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((1 / (2β†‘π‘˜)) +𝑒 (1 / (2↑(π‘˜ + 1)))) ≀ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)) ↔ ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))) ≀ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜))))
125117rpxrd 13019 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (1 / (2β†‘π‘˜)) ∈ ℝ*)
126120rpxrd 13019 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (1 / (2↑(π‘˜ + 1))) ∈ ℝ*)
127 bldisj 23911 . . . . . . . . . . . . 13 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ (π‘†β€˜π‘˜) ∈ 𝑋 ∧ ((π‘†β€˜π‘˜)π‘‡π‘˜) ∈ 𝑋) ∧ ((1 / (2β†‘π‘˜)) ∈ ℝ* ∧ (1 / (2↑(π‘˜ + 1))) ∈ ℝ* ∧ ((1 / (2β†‘π‘˜)) +𝑒 (1 / (2↑(π‘˜ + 1)))) ≀ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)))) β†’ (((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘˜))) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2↑(π‘˜ + 1))))) = βˆ…)
1281273exp2 1354 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ (π‘†β€˜π‘˜) ∈ 𝑋 ∧ ((π‘†β€˜π‘˜)π‘‡π‘˜) ∈ 𝑋) β†’ ((1 / (2β†‘π‘˜)) ∈ ℝ* β†’ ((1 / (2↑(π‘˜ + 1))) ∈ ℝ* β†’ (((1 / (2β†‘π‘˜)) +𝑒 (1 / (2↑(π‘˜ + 1)))) ≀ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)) β†’ (((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘˜))) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2↑(π‘˜ + 1))))) = βˆ…))))
129128imp32 419 . . . . . . . . . . 11 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ (π‘†β€˜π‘˜) ∈ 𝑋 ∧ ((π‘†β€˜π‘˜)π‘‡π‘˜) ∈ 𝑋) ∧ ((1 / (2β†‘π‘˜)) ∈ ℝ* ∧ (1 / (2↑(π‘˜ + 1))) ∈ ℝ*)) β†’ (((1 / (2β†‘π‘˜)) +𝑒 (1 / (2↑(π‘˜ + 1)))) ≀ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)) β†’ (((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘˜))) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2↑(π‘˜ + 1))))) = βˆ…))
1307, 40, 86, 125, 126, 129syl32anc 1378 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((1 / (2β†‘π‘˜)) +𝑒 (1 / (2↑(π‘˜ + 1)))) ≀ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)) β†’ (((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘˜))) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2↑(π‘˜ + 1))))) = βˆ…))
131124, 130sylbird 259 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))) ≀ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)) β†’ (((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘˜))) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2↑(π‘˜ + 1))))) = βˆ…))
132131necon3ad 2953 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘˜))) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2↑(π‘˜ + 1))))) β‰  βˆ… β†’ Β¬ ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))) ≀ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜))))
133115, 132mpd 15 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ Β¬ ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))) ≀ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)))
134117, 120rpaddcld 13033 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))) ∈ ℝ+)
135134rpred 13018 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))) ∈ ℝ)
1364adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 𝐷 ∈ (Metβ€˜π‘‹))
137 metcl 23845 . . . . . . . . . 10 ((𝐷 ∈ (Metβ€˜π‘‹) ∧ (π‘†β€˜π‘˜) ∈ 𝑋 ∧ ((π‘†β€˜π‘˜)π‘‡π‘˜) ∈ 𝑋) β†’ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)) ∈ ℝ)
138136, 40, 86, 137syl3anc 1371 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)) ∈ ℝ)
139135, 138letrid 11368 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))) ≀ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)) ∨ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)) ≀ ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1))))))
140139ord 862 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (Β¬ ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))) ≀ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)) β†’ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)) ≀ ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1))))))
141133, 140mpd 15 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)) ≀ ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))))
142 seqp1 13983 . . . . . . . . . . . 12 (π‘˜ ∈ (β„€β‰₯β€˜0) β†’ (seq0(𝑇, (π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1))))β€˜(π‘˜ + 1)) = ((seq0(𝑇, (π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1))))β€˜π‘˜)𝑇((π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1)))β€˜(π‘˜ + 1))))
143 nn0uz 12866 . . . . . . . . . . . 12 β„•0 = (β„€β‰₯β€˜0)
144142, 143eleq2s 2851 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ (seq0(𝑇, (π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1))))β€˜(π‘˜ + 1)) = ((seq0(𝑇, (π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1))))β€˜π‘˜)𝑇((π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1)))β€˜(π‘˜ + 1))))
14523fveq1i 6892 . . . . . . . . . . 11 (π‘†β€˜(π‘˜ + 1)) = (seq0(𝑇, (π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1))))β€˜(π‘˜ + 1))
14623fveq1i 6892 . . . . . . . . . . . 12 (π‘†β€˜π‘˜) = (seq0(𝑇, (π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1))))β€˜π‘˜)
147146oveq1i 7421 . . . . . . . . . . 11 ((π‘†β€˜π‘˜)𝑇((π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1)))β€˜(π‘˜ + 1))) = ((seq0(𝑇, (π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1))))β€˜π‘˜)𝑇((π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1)))β€˜(π‘˜ + 1)))
148144, 145, 1473eqtr4g 2797 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ (π‘†β€˜(π‘˜ + 1)) = ((π‘†β€˜π‘˜)𝑇((π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1)))β€˜(π‘˜ + 1))))
149 eqid 2732 . . . . . . . . . . . . 13 (π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1))) = (π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1)))
150 eqeq1 2736 . . . . . . . . . . . . . 14 (π‘š = (π‘˜ + 1) β†’ (π‘š = 0 ↔ (π‘˜ + 1) = 0))
151 oveq1 7418 . . . . . . . . . . . . . 14 (π‘š = (π‘˜ + 1) β†’ (π‘š βˆ’ 1) = ((π‘˜ + 1) βˆ’ 1))
152150, 151ifbieq2d 4554 . . . . . . . . . . . . 13 (π‘š = (π‘˜ + 1) β†’ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1)) = if((π‘˜ + 1) = 0, 𝐢, ((π‘˜ + 1) βˆ’ 1)))
153 nn0p1nn 12513 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„•0 β†’ (π‘˜ + 1) ∈ β„•)
154 nnne0 12248 . . . . . . . . . . . . . . . . 17 ((π‘˜ + 1) ∈ β„• β†’ (π‘˜ + 1) β‰  0)
155154neneqd 2945 . . . . . . . . . . . . . . . 16 ((π‘˜ + 1) ∈ β„• β†’ Β¬ (π‘˜ + 1) = 0)
156153, 155syl 17 . . . . . . . . . . . . . . 15 (π‘˜ ∈ β„•0 β†’ Β¬ (π‘˜ + 1) = 0)
157156iffalsed 4539 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„•0 β†’ if((π‘˜ + 1) = 0, 𝐢, ((π‘˜ + 1) βˆ’ 1)) = ((π‘˜ + 1) βˆ’ 1))
158 ovex 7444 . . . . . . . . . . . . . 14 ((π‘˜ + 1) βˆ’ 1) ∈ V
159157, 158eqeltrdi 2841 . . . . . . . . . . . . 13 (π‘˜ ∈ β„•0 β†’ if((π‘˜ + 1) = 0, 𝐢, ((π‘˜ + 1) βˆ’ 1)) ∈ V)
160149, 152, 12, 159fvmptd3 7021 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ ((π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1)))β€˜(π‘˜ + 1)) = if((π‘˜ + 1) = 0, 𝐢, ((π‘˜ + 1) βˆ’ 1)))
161 nn0cn 12484 . . . . . . . . . . . . 13 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„‚)
162 ax-1cn 11170 . . . . . . . . . . . . 13 1 ∈ β„‚
163 pncan 11468 . . . . . . . . . . . . 13 ((π‘˜ ∈ β„‚ ∧ 1 ∈ β„‚) β†’ ((π‘˜ + 1) βˆ’ 1) = π‘˜)
164161, 162, 163sylancl 586 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ ((π‘˜ + 1) βˆ’ 1) = π‘˜)
165160, 157, 1643eqtrd 2776 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ ((π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1)))β€˜(π‘˜ + 1)) = π‘˜)
166165oveq2d 7427 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ ((π‘†β€˜π‘˜)𝑇((π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1)))β€˜(π‘˜ + 1))) = ((π‘†β€˜π‘˜)π‘‡π‘˜))
167148, 166eqtrd 2772 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ (π‘†β€˜(π‘˜ + 1)) = ((π‘†β€˜π‘˜)π‘‡π‘˜))
168167adantl 482 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘†β€˜(π‘˜ + 1)) = ((π‘†β€˜π‘˜)π‘‡π‘˜))
169168oveq1d 7426 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘†β€˜(π‘˜ + 1))𝐷(π‘†β€˜π‘˜)) = (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐷(π‘†β€˜π‘˜)))
170 metsym 23863 . . . . . . . 8 ((𝐷 ∈ (Metβ€˜π‘‹) ∧ ((π‘†β€˜π‘˜)π‘‡π‘˜) ∈ 𝑋 ∧ (π‘†β€˜π‘˜) ∈ 𝑋) β†’ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐷(π‘†β€˜π‘˜)) = ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)))
171136, 86, 40, 170syl3anc 1371 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐷(π‘†β€˜π‘˜)) = ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)))
172169, 171eqtrd 2772 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘†β€˜(π‘˜ + 1))𝐷(π‘†β€˜π‘˜)) = ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)))
173 3cn 12295 . . . . . . . . . . . . 13 3 ∈ β„‚
1741732timesi 12352 . . . . . . . . . . . 12 (2 Β· 3) = (3 + 3)
175174oveq1i 7421 . . . . . . . . . . 11 ((2 Β· 3) βˆ’ 3) = ((3 + 3) βˆ’ 3)
176173, 173pncan3oi 11478 . . . . . . . . . . 11 ((3 + 3) βˆ’ 3) = 3
177 df-3 12278 . . . . . . . . . . 11 3 = (2 + 1)
178175, 176, 1773eqtri 2764 . . . . . . . . . 10 ((2 Β· 3) βˆ’ 3) = (2 + 1)
179178oveq1i 7421 . . . . . . . . 9 (((2 Β· 3) βˆ’ 3) / (2↑(π‘˜ + 1))) = ((2 + 1) / (2↑(π‘˜ + 1)))
180 rpcn 12986 . . . . . . . . . . 11 ((2↑(π‘˜ + 1)) ∈ ℝ+ β†’ (2↑(π‘˜ + 1)) ∈ β„‚)
181 rpne0 12992 . . . . . . . . . . 11 ((2↑(π‘˜ + 1)) ∈ ℝ+ β†’ (2↑(π‘˜ + 1)) β‰  0)
182 2cn 12289 . . . . . . . . . . . . 13 2 ∈ β„‚
183182, 173mulcli 11223 . . . . . . . . . . . 12 (2 Β· 3) ∈ β„‚
184 divsubdir 11910 . . . . . . . . . . . 12 (((2 Β· 3) ∈ β„‚ ∧ 3 ∈ β„‚ ∧ ((2↑(π‘˜ + 1)) ∈ β„‚ ∧ (2↑(π‘˜ + 1)) β‰  0)) β†’ (((2 Β· 3) βˆ’ 3) / (2↑(π‘˜ + 1))) = (((2 Β· 3) / (2↑(π‘˜ + 1))) βˆ’ (3 / (2↑(π‘˜ + 1)))))
185183, 173, 184mp3an12 1451 . . . . . . . . . . 11 (((2↑(π‘˜ + 1)) ∈ β„‚ ∧ (2↑(π‘˜ + 1)) β‰  0) β†’ (((2 Β· 3) βˆ’ 3) / (2↑(π‘˜ + 1))) = (((2 Β· 3) / (2↑(π‘˜ + 1))) βˆ’ (3 / (2↑(π‘˜ + 1)))))
186180, 181, 185syl2anc 584 . . . . . . . . . 10 ((2↑(π‘˜ + 1)) ∈ ℝ+ β†’ (((2 Β· 3) βˆ’ 3) / (2↑(π‘˜ + 1))) = (((2 Β· 3) / (2↑(π‘˜ + 1))) βˆ’ (3 / (2↑(π‘˜ + 1)))))
18745, 186syl 17 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ (((2 Β· 3) βˆ’ 3) / (2↑(π‘˜ + 1))) = (((2 Β· 3) / (2↑(π‘˜ + 1))) βˆ’ (3 / (2↑(π‘˜ + 1)))))
188 divdir 11899 . . . . . . . . . . . 12 ((2 ∈ β„‚ ∧ 1 ∈ β„‚ ∧ ((2↑(π‘˜ + 1)) ∈ β„‚ ∧ (2↑(π‘˜ + 1)) β‰  0)) β†’ ((2 + 1) / (2↑(π‘˜ + 1))) = ((2 / (2↑(π‘˜ + 1))) + (1 / (2↑(π‘˜ + 1)))))
189182, 162, 188mp3an12 1451 . . . . . . . . . . 11 (((2↑(π‘˜ + 1)) ∈ β„‚ ∧ (2↑(π‘˜ + 1)) β‰  0) β†’ ((2 + 1) / (2↑(π‘˜ + 1))) = ((2 / (2↑(π‘˜ + 1))) + (1 / (2↑(π‘˜ + 1)))))
190180, 181, 189syl2anc 584 . . . . . . . . . 10 ((2↑(π‘˜ + 1)) ∈ ℝ+ β†’ ((2 + 1) / (2↑(π‘˜ + 1))) = ((2 / (2↑(π‘˜ + 1))) + (1 / (2↑(π‘˜ + 1)))))
19145, 190syl 17 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ ((2 + 1) / (2↑(π‘˜ + 1))) = ((2 / (2↑(π‘˜ + 1))) + (1 / (2↑(π‘˜ + 1)))))
192179, 187, 1913eqtr3a 2796 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ (((2 Β· 3) / (2↑(π‘˜ + 1))) βˆ’ (3 / (2↑(π‘˜ + 1)))) = ((2 / (2↑(π‘˜ + 1))) + (1 / (2↑(π‘˜ + 1)))))
193 rpcn 12986 . . . . . . . . . . . 12 ((2β†‘π‘˜) ∈ ℝ+ β†’ (2β†‘π‘˜) ∈ β„‚)
194 rpne0 12992 . . . . . . . . . . . 12 ((2β†‘π‘˜) ∈ ℝ+ β†’ (2β†‘π‘˜) β‰  0)
195 2cnne0 12424 . . . . . . . . . . . . 13 (2 ∈ β„‚ ∧ 2 β‰  0)
196 divcan5 11918 . . . . . . . . . . . . 13 ((3 ∈ β„‚ ∧ ((2β†‘π‘˜) ∈ β„‚ ∧ (2β†‘π‘˜) β‰  0) ∧ (2 ∈ β„‚ ∧ 2 β‰  0)) β†’ ((2 Β· 3) / (2 Β· (2β†‘π‘˜))) = (3 / (2β†‘π‘˜)))
197173, 195, 196mp3an13 1452 . . . . . . . . . . . 12 (((2β†‘π‘˜) ∈ β„‚ ∧ (2β†‘π‘˜) β‰  0) β†’ ((2 Β· 3) / (2 Β· (2β†‘π‘˜))) = (3 / (2β†‘π‘˜)))
198193, 194, 197syl2anc 584 . . . . . . . . . . 11 ((2β†‘π‘˜) ∈ ℝ+ β†’ ((2 Β· 3) / (2 Β· (2β†‘π‘˜))) = (3 / (2β†‘π‘˜)))
19951, 198syl 17 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ ((2 Β· 3) / (2 Β· (2β†‘π‘˜))) = (3 / (2β†‘π‘˜)))
20051, 193syl 17 . . . . . . . . . . . . 13 (π‘˜ ∈ β„•0 β†’ (2β†‘π‘˜) ∈ β„‚)
201 mulcom 11198 . . . . . . . . . . . . 13 ((2 ∈ β„‚ ∧ (2β†‘π‘˜) ∈ β„‚) β†’ (2 Β· (2β†‘π‘˜)) = ((2β†‘π‘˜) Β· 2))
202182, 200, 201sylancr 587 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ (2 Β· (2β†‘π‘˜)) = ((2β†‘π‘˜) Β· 2))
203 expp1 14036 . . . . . . . . . . . . 13 ((2 ∈ β„‚ ∧ π‘˜ ∈ β„•0) β†’ (2↑(π‘˜ + 1)) = ((2β†‘π‘˜) Β· 2))
204182, 203mpan 688 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ (2↑(π‘˜ + 1)) = ((2β†‘π‘˜) Β· 2))
205202, 204eqtr4d 2775 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ (2 Β· (2β†‘π‘˜)) = (2↑(π‘˜ + 1)))
206205oveq2d 7427 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ ((2 Β· 3) / (2 Β· (2β†‘π‘˜))) = ((2 Β· 3) / (2↑(π‘˜ + 1))))
207199, 206eqtr3d 2774 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ (3 / (2β†‘π‘˜)) = ((2 Β· 3) / (2↑(π‘˜ + 1))))
208207oveq1d 7426 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ ((3 / (2β†‘π‘˜)) βˆ’ (3 / (2↑(π‘˜ + 1)))) = (((2 Β· 3) / (2↑(π‘˜ + 1))) βˆ’ (3 / (2↑(π‘˜ + 1)))))
209 divcan5 11918 . . . . . . . . . . . . 13 ((1 ∈ β„‚ ∧ ((2β†‘π‘˜) ∈ β„‚ ∧ (2β†‘π‘˜) β‰  0) ∧ (2 ∈ β„‚ ∧ 2 β‰  0)) β†’ ((2 Β· 1) / (2 Β· (2β†‘π‘˜))) = (1 / (2β†‘π‘˜)))
210162, 195, 209mp3an13 1452 . . . . . . . . . . . 12 (((2β†‘π‘˜) ∈ β„‚ ∧ (2β†‘π‘˜) β‰  0) β†’ ((2 Β· 1) / (2 Β· (2β†‘π‘˜))) = (1 / (2β†‘π‘˜)))
211193, 194, 210syl2anc 584 . . . . . . . . . . 11 ((2β†‘π‘˜) ∈ ℝ+ β†’ ((2 Β· 1) / (2 Β· (2β†‘π‘˜))) = (1 / (2β†‘π‘˜)))
21251, 211syl 17 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ ((2 Β· 1) / (2 Β· (2β†‘π‘˜))) = (1 / (2β†‘π‘˜)))
213 2t1e2 12377 . . . . . . . . . . . 12 (2 Β· 1) = 2
214213a1i 11 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ (2 Β· 1) = 2)
215214, 205oveq12d 7429 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ ((2 Β· 1) / (2 Β· (2β†‘π‘˜))) = (2 / (2↑(π‘˜ + 1))))
216212, 215eqtr3d 2774 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ (1 / (2β†‘π‘˜)) = (2 / (2↑(π‘˜ + 1))))
217216oveq1d 7426 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))) = ((2 / (2↑(π‘˜ + 1))) + (1 / (2↑(π‘˜ + 1)))))
218192, 208, 2173eqtr4d 2782 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ ((3 / (2β†‘π‘˜)) βˆ’ (3 / (2↑(π‘˜ + 1)))) = ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))))
219218adantl 482 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((3 / (2β†‘π‘˜)) βˆ’ (3 / (2↑(π‘˜ + 1)))) = ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))))
220141, 172, 2193brtr4d 5180 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘†β€˜(π‘˜ + 1))𝐷(π‘†β€˜π‘˜)) ≀ ((3 / (2β†‘π‘˜)) βˆ’ (3 / (2↑(π‘˜ + 1)))))
221 blss2 23917 . . . . 5 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ (π‘†β€˜(π‘˜ + 1)) ∈ 𝑋 ∧ (π‘†β€˜π‘˜) ∈ 𝑋) ∧ ((3 / (2↑(π‘˜ + 1))) ∈ ℝ ∧ (3 / (2β†‘π‘˜)) ∈ ℝ ∧ ((π‘†β€˜(π‘˜ + 1))𝐷(π‘†β€˜π‘˜)) ≀ ((3 / (2β†‘π‘˜)) βˆ’ (3 / (2↑(π‘˜ + 1)))))) β†’ ((π‘†β€˜(π‘˜ + 1))(ballβ€˜π·)(3 / (2↑(π‘˜ + 1)))) βŠ† ((π‘†β€˜π‘˜)(ballβ€˜π·)(3 / (2β†‘π‘˜))))
2227, 31, 40, 48, 54, 220, 221syl33anc 1385 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘†β€˜(π‘˜ + 1))(ballβ€˜π·)(3 / (2↑(π‘˜ + 1)))) βŠ† ((π‘†β€˜π‘˜)(ballβ€˜π·)(3 / (2β†‘π‘˜))))
2231, 222sylan2 593 . . 3 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((π‘†β€˜(π‘˜ + 1))(ballβ€˜π·)(3 / (2↑(π‘˜ + 1)))) βŠ† ((π‘†β€˜π‘˜)(ballβ€˜π·)(3 / (2β†‘π‘˜))))
224 peano2nn 12226 . . . . . . 7 (π‘˜ ∈ β„• β†’ (π‘˜ + 1) ∈ β„•)
225 fveq2 6891 . . . . . . . . 9 (𝑛 = (π‘˜ + 1) β†’ (π‘†β€˜π‘›) = (π‘†β€˜(π‘˜ + 1)))
226 oveq2 7419 . . . . . . . . . 10 (𝑛 = (π‘˜ + 1) β†’ (2↑𝑛) = (2↑(π‘˜ + 1)))
227226oveq2d 7427 . . . . . . . . 9 (𝑛 = (π‘˜ + 1) β†’ (3 / (2↑𝑛)) = (3 / (2↑(π‘˜ + 1))))
228225, 227opeq12d 4881 . . . . . . . 8 (𝑛 = (π‘˜ + 1) β†’ ⟨(π‘†β€˜π‘›), (3 / (2↑𝑛))⟩ = ⟨(π‘†β€˜(π‘˜ + 1)), (3 / (2↑(π‘˜ + 1)))⟩)
229 heibor.12 . . . . . . . 8 𝑀 = (𝑛 ∈ β„• ↦ ⟨(π‘†β€˜π‘›), (3 / (2↑𝑛))⟩)
230 opex 5464 . . . . . . . 8 ⟨(π‘†β€˜(π‘˜ + 1)), (3 / (2↑(π‘˜ + 1)))⟩ ∈ V
231228, 229, 230fvmpt 6998 . . . . . . 7 ((π‘˜ + 1) ∈ β„• β†’ (π‘€β€˜(π‘˜ + 1)) = ⟨(π‘†β€˜(π‘˜ + 1)), (3 / (2↑(π‘˜ + 1)))⟩)
232224, 231syl 17 . . . . . 6 (π‘˜ ∈ β„• β†’ (π‘€β€˜(π‘˜ + 1)) = ⟨(π‘†β€˜(π‘˜ + 1)), (3 / (2↑(π‘˜ + 1)))⟩)
233232adantl 482 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘€β€˜(π‘˜ + 1)) = ⟨(π‘†β€˜(π‘˜ + 1)), (3 / (2↑(π‘˜ + 1)))⟩)
234233fveq2d 6895 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((ballβ€˜π·)β€˜(π‘€β€˜(π‘˜ + 1))) = ((ballβ€˜π·)β€˜βŸ¨(π‘†β€˜(π‘˜ + 1)), (3 / (2↑(π‘˜ + 1)))⟩))
235 df-ov 7414 . . . 4 ((π‘†β€˜(π‘˜ + 1))(ballβ€˜π·)(3 / (2↑(π‘˜ + 1)))) = ((ballβ€˜π·)β€˜βŸ¨(π‘†β€˜(π‘˜ + 1)), (3 / (2↑(π‘˜ + 1)))⟩)
236234, 235eqtr4di 2790 . . 3 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((ballβ€˜π·)β€˜(π‘€β€˜(π‘˜ + 1))) = ((π‘†β€˜(π‘˜ + 1))(ballβ€˜π·)(3 / (2↑(π‘˜ + 1)))))
237 fveq2 6891 . . . . . . . 8 (𝑛 = π‘˜ β†’ (π‘†β€˜π‘›) = (π‘†β€˜π‘˜))
238 oveq2 7419 . . . . . . . . 9 (𝑛 = π‘˜ β†’ (2↑𝑛) = (2β†‘π‘˜))
239238oveq2d 7427 . . . . . . . 8 (𝑛 = π‘˜ β†’ (3 / (2↑𝑛)) = (3 / (2β†‘π‘˜)))
240237, 239opeq12d 4881 . . . . . . 7 (𝑛 = π‘˜ β†’ ⟨(π‘†β€˜π‘›), (3 / (2↑𝑛))⟩ = ⟨(π‘†β€˜π‘˜), (3 / (2β†‘π‘˜))⟩)
241 opex 5464 . . . . . . 7 ⟨(π‘†β€˜π‘˜), (3 / (2β†‘π‘˜))⟩ ∈ V
242240, 229, 241fvmpt 6998 . . . . . 6 (π‘˜ ∈ β„• β†’ (π‘€β€˜π‘˜) = ⟨(π‘†β€˜π‘˜), (3 / (2β†‘π‘˜))⟩)
243242fveq2d 6895 . . . . 5 (π‘˜ ∈ β„• β†’ ((ballβ€˜π·)β€˜(π‘€β€˜π‘˜)) = ((ballβ€˜π·)β€˜βŸ¨(π‘†β€˜π‘˜), (3 / (2β†‘π‘˜))⟩))
244 df-ov 7414 . . . . 5 ((π‘†β€˜π‘˜)(ballβ€˜π·)(3 / (2β†‘π‘˜))) = ((ballβ€˜π·)β€˜βŸ¨(π‘†β€˜π‘˜), (3 / (2β†‘π‘˜))⟩)
245243, 244eqtr4di 2790 . . . 4 (π‘˜ ∈ β„• β†’ ((ballβ€˜π·)β€˜(π‘€β€˜π‘˜)) = ((π‘†β€˜π‘˜)(ballβ€˜π·)(3 / (2β†‘π‘˜))))
246245adantl 482 . . 3 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((ballβ€˜π·)β€˜(π‘€β€˜π‘˜)) = ((π‘†β€˜π‘˜)(ballβ€˜π·)(3 / (2β†‘π‘˜))))
247223, 236, 2463sstr4d 4029 . 2 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((ballβ€˜π·)β€˜(π‘€β€˜(π‘˜ + 1))) βŠ† ((ballβ€˜π·)β€˜(π‘€β€˜π‘˜)))
248247ralrimiva 3146 1 (πœ‘ β†’ βˆ€π‘˜ ∈ β„• ((ballβ€˜π·)β€˜(π‘€β€˜(π‘˜ + 1))) βŠ† ((ballβ€˜π·)β€˜(π‘€β€˜π‘˜)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  {cab 2709   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3474   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  ifcif 4528  π’« cpw 4602  βŸ¨cop 4634  βˆͺ cuni 4908  βˆͺ ciun 4997   class class class wbr 5148  {copab 5210   ↦ cmpt 5231  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7411   ∈ cmpo 7413  2nd c2nd 7976  Fincfn 8941  β„‚cc 11110  β„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   Β· cmul 11117  β„*cxr 11249   ≀ cle 11251   βˆ’ cmin 11446   / cdiv 11873  β„•cn 12214  2c2 12269  3c3 12270  β„•0cn0 12474  β„€β‰₯cuz 12824  β„+crp 12976   +𝑒 cxad 13092  seqcseq 13968  β†‘cexp 14029  βˆžMetcxmet 20935  Metcmet 20936  ballcbl 20937  MetOpencmopn 20940  CMetccmet 24778
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-div 11874  df-nn 12215  df-2 12277  df-3 12278  df-n0 12475  df-z 12561  df-uz 12825  df-rp 12977  df-xneg 13094  df-xadd 13095  df-xmul 13096  df-seq 13969  df-exp 14030  df-psmet 20942  df-xmet 20943  df-met 20944  df-bl 20945  df-cmet 24781
This theorem is referenced by:  heiborlem8  36772  heiborlem9  36773
  Copyright terms: Public domain W3C validator