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 36684
Description: Lemma for heibor 36689. 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 12479 . . . 4 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„•0)
2 heibor.6 . . . . . . . 8 (πœ‘ β†’ 𝐷 ∈ (CMetβ€˜π‘‹))
3 cmetmet 24803 . . . . . . . 8 (𝐷 ∈ (CMetβ€˜π‘‹) β†’ 𝐷 ∈ (Metβ€˜π‘‹))
42, 3syl 17 . . . . . . 7 (πœ‘ β†’ 𝐷 ∈ (Metβ€˜π‘‹))
5 metxmet 23840 . . . . . . 7 (𝐷 ∈ (Metβ€˜π‘‹) β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
64, 5syl 17 . . . . . 6 (πœ‘ β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
76adantr 482 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
8 heibor.7 . . . . . . . . 9 (πœ‘ β†’ 𝐹:β„•0⟢(𝒫 𝑋 ∩ Fin))
9 inss1 4229 . . . . . . . . 9 (𝒫 𝑋 ∩ Fin) βŠ† 𝒫 𝑋
10 fss 6735 . . . . . . . . 9 ((𝐹:β„•0⟢(𝒫 𝑋 ∩ Fin) ∧ (𝒫 𝑋 ∩ Fin) βŠ† 𝒫 𝑋) β†’ 𝐹:β„•0βŸΆπ’« 𝑋)
118, 9, 10sylancl 587 . . . . . . . 8 (πœ‘ β†’ 𝐹:β„•0βŸΆπ’« 𝑋)
12 peano2nn0 12512 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ (π‘˜ + 1) ∈ β„•0)
13 ffvelcdm 7084 . . . . . . . 8 ((𝐹:β„•0βŸΆπ’« 𝑋 ∧ (π‘˜ + 1) ∈ β„•0) β†’ (πΉβ€˜(π‘˜ + 1)) ∈ 𝒫 𝑋)
1411, 12, 13syl2an 597 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (πΉβ€˜(π‘˜ + 1)) ∈ 𝒫 𝑋)
1514elpwid 4612 . . . . . 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 36682 . . . . . . . 8 ((πœ‘ ∧ (π‘˜ + 1) ∈ β„•0) β†’ (π‘†β€˜(π‘˜ + 1))𝐺(π‘˜ + 1))
2512, 24sylan2 594 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘†β€˜(π‘˜ + 1))𝐺(π‘˜ + 1))
26 fvex 6905 . . . . . . . . 9 (π‘†β€˜(π‘˜ + 1)) ∈ V
27 ovex 7442 . . . . . . . . 9 (π‘˜ + 1) ∈ V
2816, 17, 18, 26, 27heiborlem2 36680 . . . . . . . 8 ((π‘†β€˜(π‘˜ + 1))𝐺(π‘˜ + 1) ↔ ((π‘˜ + 1) ∈ β„•0 ∧ (π‘†β€˜(π‘˜ + 1)) ∈ (πΉβ€˜(π‘˜ + 1)) ∧ ((π‘†β€˜(π‘˜ + 1))𝐡(π‘˜ + 1)) ∈ 𝐾))
2928simp2bi 1147 . . . . . . 7 ((π‘†β€˜(π‘˜ + 1))𝐺(π‘˜ + 1) β†’ (π‘†β€˜(π‘˜ + 1)) ∈ (πΉβ€˜(π‘˜ + 1)))
3025, 29syl 17 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘†β€˜(π‘˜ + 1)) ∈ (πΉβ€˜(π‘˜ + 1)))
3115, 30sseldd 3984 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘†β€˜(π‘˜ + 1)) ∈ 𝑋)
3211ffvelcdmda 7087 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (πΉβ€˜π‘˜) ∈ 𝒫 𝑋)
3332elpwid 4612 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (πΉβ€˜π‘˜) βŠ† 𝑋)
3416, 17, 18, 19, 2, 8, 20, 21, 22, 23heiborlem4 36682 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘†β€˜π‘˜)πΊπ‘˜)
35 fvex 6905 . . . . . . . . 9 (π‘†β€˜π‘˜) ∈ V
36 vex 3479 . . . . . . . . 9 π‘˜ ∈ V
3716, 17, 18, 35, 36heiborlem2 36680 . . . . . . . 8 ((π‘†β€˜π‘˜)πΊπ‘˜ ↔ (π‘˜ ∈ β„•0 ∧ (π‘†β€˜π‘˜) ∈ (πΉβ€˜π‘˜) ∧ ((π‘†β€˜π‘˜)π΅π‘˜) ∈ 𝐾))
3837simp2bi 1147 . . . . . . 7 ((π‘†β€˜π‘˜)πΊπ‘˜ β†’ (π‘†β€˜π‘˜) ∈ (πΉβ€˜π‘˜))
3934, 38syl 17 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘†β€˜π‘˜) ∈ (πΉβ€˜π‘˜))
4033, 39sseldd 3984 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘†β€˜π‘˜) ∈ 𝑋)
41 3re 12292 . . . . . 6 3 ∈ ℝ
42 2nn 12285 . . . . . . . . 9 2 ∈ β„•
43 nnexpcl 14040 . . . . . . . . 9 ((2 ∈ β„• ∧ (π‘˜ + 1) ∈ β„•0) β†’ (2↑(π‘˜ + 1)) ∈ β„•)
4442, 12, 43sylancr 588 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ (2↑(π‘˜ + 1)) ∈ β„•)
4544nnrpd 13014 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ (2↑(π‘˜ + 1)) ∈ ℝ+)
4645adantl 483 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (2↑(π‘˜ + 1)) ∈ ℝ+)
47 rerpdivcl 13004 . . . . . 6 ((3 ∈ ℝ ∧ (2↑(π‘˜ + 1)) ∈ ℝ+) β†’ (3 / (2↑(π‘˜ + 1))) ∈ ℝ)
4841, 46, 47sylancr 588 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (3 / (2↑(π‘˜ + 1))) ∈ ℝ)
49 nnexpcl 14040 . . . . . . . . 9 ((2 ∈ β„• ∧ π‘˜ ∈ β„•0) β†’ (2β†‘π‘˜) ∈ β„•)
5042, 49mpan 689 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ (2β†‘π‘˜) ∈ β„•)
5150nnrpd 13014 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ (2β†‘π‘˜) ∈ ℝ+)
5251adantl 483 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (2β†‘π‘˜) ∈ ℝ+)
53 rerpdivcl 13004 . . . . . 6 ((3 ∈ ℝ ∧ (2β†‘π‘˜) ∈ ℝ+) β†’ (3 / (2β†‘π‘˜)) ∈ ℝ)
5441, 52, 53sylancr 588 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (3 / (2β†‘π‘˜)) ∈ ℝ)
55 oveq1 7416 . . . . . . . . . . . 12 (𝑧 = (π‘†β€˜π‘˜) β†’ (𝑧(ballβ€˜π·)(1 / (2β†‘π‘š))) = ((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘š))))
56 oveq2 7417 . . . . . . . . . . . . . 14 (π‘š = π‘˜ β†’ (2β†‘π‘š) = (2β†‘π‘˜))
5756oveq2d 7425 . . . . . . . . . . . . 13 (π‘š = π‘˜ β†’ (1 / (2β†‘π‘š)) = (1 / (2β†‘π‘˜)))
5857oveq2d 7425 . . . . . . . . . . . 12 (π‘š = π‘˜ β†’ ((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘š))) = ((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘˜))))
59 ovex 7442 . . . . . . . . . . . 12 ((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘˜))) ∈ V
6055, 58, 19, 59ovmpo 7568 . . . . . . . . . . 11 (((π‘†β€˜π‘˜) ∈ 𝑋 ∧ π‘˜ ∈ β„•0) β†’ ((π‘†β€˜π‘˜)π΅π‘˜) = ((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘˜))))
6140, 60sylancom 589 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘†β€˜π‘˜)π΅π‘˜) = ((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘˜))))
62 df-br 5150 . . . . . . . . . . . . . . . . 17 ((π‘†β€˜π‘˜)πΊπ‘˜ ↔ ⟨(π‘†β€˜π‘˜), π‘˜βŸ© ∈ 𝐺)
63 fveq2 6892 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = ⟨(π‘†β€˜π‘˜), π‘˜βŸ© β†’ (π‘‡β€˜π‘₯) = (π‘‡β€˜βŸ¨(π‘†β€˜π‘˜), π‘˜βŸ©))
64 df-ov 7412 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘†β€˜π‘˜)π‘‡π‘˜) = (π‘‡β€˜βŸ¨(π‘†β€˜π‘˜), π‘˜βŸ©)
6563, 64eqtr4di 2791 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = ⟨(π‘†β€˜π‘˜), π‘˜βŸ© β†’ (π‘‡β€˜π‘₯) = ((π‘†β€˜π‘˜)π‘‡π‘˜))
6635, 36op2ndd 7986 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = ⟨(π‘†β€˜π‘˜), π‘˜βŸ© β†’ (2nd β€˜π‘₯) = π‘˜)
6766oveq1d 7424 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = ⟨(π‘†β€˜π‘˜), π‘˜βŸ© β†’ ((2nd β€˜π‘₯) + 1) = (π‘˜ + 1))
6865, 67breq12d 5162 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = ⟨(π‘†β€˜π‘˜), π‘˜βŸ© β†’ ((π‘‡β€˜π‘₯)𝐺((2nd β€˜π‘₯) + 1) ↔ ((π‘†β€˜π‘˜)π‘‡π‘˜)𝐺(π‘˜ + 1)))
69 fveq2 6892 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ = ⟨(π‘†β€˜π‘˜), π‘˜βŸ© β†’ (π΅β€˜π‘₯) = (π΅β€˜βŸ¨(π‘†β€˜π‘˜), π‘˜βŸ©))
70 df-ov 7412 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘†β€˜π‘˜)π΅π‘˜) = (π΅β€˜βŸ¨(π‘†β€˜π‘˜), π‘˜βŸ©)
7169, 70eqtr4di 2791 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = ⟨(π‘†β€˜π‘˜), π‘˜βŸ© β†’ (π΅β€˜π‘₯) = ((π‘†β€˜π‘˜)π΅π‘˜))
7265, 67oveq12d 7427 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = ⟨(π‘†β€˜π‘˜), π‘˜βŸ© β†’ ((π‘‡β€˜π‘₯)𝐡((2nd β€˜π‘₯) + 1)) = (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1)))
7371, 72ineq12d 4214 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = ⟨(π‘†β€˜π‘˜), π‘˜βŸ© β†’ ((π΅β€˜π‘₯) ∩ ((π‘‡β€˜π‘₯)𝐡((2nd β€˜π‘₯) + 1))) = (((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))))
7473eleq1d 2819 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = ⟨(π‘†β€˜π‘˜), π‘˜βŸ© β†’ (((π΅β€˜π‘₯) ∩ ((π‘‡β€˜π‘₯)𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾 ↔ (((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))) ∈ 𝐾))
7568, 74anbi12d 632 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = ⟨(π‘†β€˜π‘˜), π‘˜βŸ© β†’ (((π‘‡β€˜π‘₯)𝐺((2nd β€˜π‘₯) + 1) ∧ ((π΅β€˜π‘₯) ∩ ((π‘‡β€˜π‘₯)𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾) ↔ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐺(π‘˜ + 1) ∧ (((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))) ∈ 𝐾)))
7675rspccv 3610 . . . . . . . . . . . . . . . . . 18 (βˆ€π‘₯ ∈ 𝐺 ((π‘‡β€˜π‘₯)𝐺((2nd β€˜π‘₯) + 1) ∧ ((π΅β€˜π‘₯) ∩ ((π‘‡β€˜π‘₯)𝐡((2nd β€˜π‘₯) + 1))) ∈ 𝐾) β†’ (⟨(π‘†β€˜π‘˜), π‘˜βŸ© ∈ 𝐺 β†’ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐺(π‘˜ + 1) ∧ (((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))) ∈ 𝐾)))
7721, 76syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (⟨(π‘†β€˜π‘˜), π‘˜βŸ© ∈ 𝐺 β†’ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐺(π‘˜ + 1) ∧ (((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))) ∈ 𝐾)))
7862, 77biimtrid 241 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((π‘†β€˜π‘˜)πΊπ‘˜ β†’ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐺(π‘˜ + 1) ∧ (((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))) ∈ 𝐾)))
7978adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘†β€˜π‘˜)πΊπ‘˜ β†’ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐺(π‘˜ + 1) ∧ (((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))) ∈ 𝐾)))
8034, 79mpd 15 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐺(π‘˜ + 1) ∧ (((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))) ∈ 𝐾))
8180simpld 496 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘†β€˜π‘˜)π‘‡π‘˜)𝐺(π‘˜ + 1))
82 ovex 7442 . . . . . . . . . . . . . . 15 ((π‘†β€˜π‘˜)π‘‡π‘˜) ∈ V
8316, 17, 18, 82, 27heiborlem2 36680 . . . . . . . . . . . . . 14 (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐺(π‘˜ + 1) ↔ ((π‘˜ + 1) ∈ β„•0 ∧ ((π‘†β€˜π‘˜)π‘‡π‘˜) ∈ (πΉβ€˜(π‘˜ + 1)) ∧ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1)) ∈ 𝐾))
8483simp2bi 1147 . . . . . . . . . . . . 13 (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐺(π‘˜ + 1) β†’ ((π‘†β€˜π‘˜)π‘‡π‘˜) ∈ (πΉβ€˜(π‘˜ + 1)))
8581, 84syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘†β€˜π‘˜)π‘‡π‘˜) ∈ (πΉβ€˜(π‘˜ + 1)))
8615, 85sseldd 3984 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘†β€˜π‘˜)π‘‡π‘˜) ∈ 𝑋)
8712adantl 483 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘˜ + 1) ∈ β„•0)
88 oveq1 7416 . . . . . . . . . . . 12 (𝑧 = ((π‘†β€˜π‘˜)π‘‡π‘˜) β†’ (𝑧(ballβ€˜π·)(1 / (2β†‘π‘š))) = (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘š))))
89 oveq2 7417 . . . . . . . . . . . . . 14 (π‘š = (π‘˜ + 1) β†’ (2β†‘π‘š) = (2↑(π‘˜ + 1)))
9089oveq2d 7425 . . . . . . . . . . . . 13 (π‘š = (π‘˜ + 1) β†’ (1 / (2β†‘π‘š)) = (1 / (2↑(π‘˜ + 1))))
9190oveq2d 7425 . . . . . . . . . . . 12 (π‘š = (π‘˜ + 1) β†’ (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘š))) = (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2↑(π‘˜ + 1)))))
92 ovex 7442 . . . . . . . . . . . 12 (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2↑(π‘˜ + 1)))) ∈ V
9388, 91, 19, 92ovmpo 7568 . . . . . . . . . . 11 ((((π‘†β€˜π‘˜)π‘‡π‘˜) ∈ 𝑋 ∧ (π‘˜ + 1) ∈ β„•0) β†’ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1)) = (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2↑(π‘˜ + 1)))))
9486, 87, 93syl2anc 585 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1)) = (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2↑(π‘˜ + 1)))))
9561, 94ineq12d 4214 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))) = (((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘˜))) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2↑(π‘˜ + 1))))))
9680simprd 497 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))) ∈ 𝐾)
97 0elpw 5355 . . . . . . . . . . . . 13 βˆ… ∈ 𝒫 π‘ˆ
98 0fin 9171 . . . . . . . . . . . . 13 βˆ… ∈ Fin
99 elin 3965 . . . . . . . . . . . . 13 (βˆ… ∈ (𝒫 π‘ˆ ∩ Fin) ↔ (βˆ… ∈ 𝒫 π‘ˆ ∧ βˆ… ∈ Fin))
10097, 98, 99mpbir2an 710 . . . . . . . . . . . 12 βˆ… ∈ (𝒫 π‘ˆ ∩ Fin)
101 0ss 4397 . . . . . . . . . . . 12 βˆ… βŠ† βˆͺ βˆ…
102 unieq 4920 . . . . . . . . . . . . . 14 (𝑣 = βˆ… β†’ βˆͺ 𝑣 = βˆͺ βˆ…)
103102sseq2d 4015 . . . . . . . . . . . . 13 (𝑣 = βˆ… β†’ (βˆ… βŠ† βˆͺ 𝑣 ↔ βˆ… βŠ† βˆͺ βˆ…))
104103rspcev 3613 . . . . . . . . . . . 12 ((βˆ… ∈ (𝒫 π‘ˆ ∩ Fin) ∧ βˆ… βŠ† βˆͺ βˆ…) β†’ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)βˆ… βŠ† βˆͺ 𝑣)
105100, 101, 104mp2an 691 . . . . . . . . . . 11 βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)βˆ… βŠ† βˆͺ 𝑣
106 0ex 5308 . . . . . . . . . . . . 13 βˆ… ∈ V
107 sseq1 4008 . . . . . . . . . . . . . . 15 (𝑒 = βˆ… β†’ (𝑒 βŠ† βˆͺ 𝑣 ↔ βˆ… βŠ† βˆͺ 𝑣))
108107rexbidv 3179 . . . . . . . . . . . . . 14 (𝑒 = βˆ… β†’ (βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝑒 βŠ† βˆͺ 𝑣 ↔ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)βˆ… βŠ† βˆͺ 𝑣))
109108notbid 318 . . . . . . . . . . . . 13 (𝑒 = βˆ… β†’ (Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝑒 βŠ† βˆͺ 𝑣 ↔ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)βˆ… βŠ† βˆͺ 𝑣))
110106, 109, 17elab2 3673 . . . . . . . . . . . 12 (βˆ… ∈ 𝐾 ↔ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)βˆ… βŠ† βˆͺ 𝑣)
111110con2bii 358 . . . . . . . . . . 11 (βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)βˆ… βŠ† βˆͺ 𝑣 ↔ Β¬ βˆ… ∈ 𝐾)
112105, 111mpbi 229 . . . . . . . . . 10 Β¬ βˆ… ∈ 𝐾
113 nelne2 3041 . . . . . . . . . 10 (((((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))) ∈ 𝐾 ∧ Β¬ βˆ… ∈ 𝐾) β†’ (((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))) β‰  βˆ…)
11496, 112, 113sylancl 587 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((π‘†β€˜π‘˜)π΅π‘˜) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐡(π‘˜ + 1))) β‰  βˆ…)
11595, 114eqnetrrd 3010 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘˜))) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2↑(π‘˜ + 1))))) β‰  βˆ…)
11651rpreccld 13026 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„•0 β†’ (1 / (2β†‘π‘˜)) ∈ ℝ+)
117116adantl 483 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (1 / (2β†‘π‘˜)) ∈ ℝ+)
118117rpred 13016 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (1 / (2β†‘π‘˜)) ∈ ℝ)
11945rpreccld 13026 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„•0 β†’ (1 / (2↑(π‘˜ + 1))) ∈ ℝ+)
120119adantl 483 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (1 / (2↑(π‘˜ + 1))) ∈ ℝ+)
121120rpred 13016 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (1 / (2↑(π‘˜ + 1))) ∈ ℝ)
122 rexadd 13211 . . . . . . . . . . . 12 (((1 / (2β†‘π‘˜)) ∈ ℝ ∧ (1 / (2↑(π‘˜ + 1))) ∈ ℝ) β†’ ((1 / (2β†‘π‘˜)) +𝑒 (1 / (2↑(π‘˜ + 1)))) = ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))))
123118, 121, 122syl2anc 585 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((1 / (2β†‘π‘˜)) +𝑒 (1 / (2↑(π‘˜ + 1)))) = ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))))
124123breq1d 5159 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((1 / (2β†‘π‘˜)) +𝑒 (1 / (2↑(π‘˜ + 1)))) ≀ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)) ↔ ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))) ≀ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜))))
125117rpxrd 13017 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (1 / (2β†‘π‘˜)) ∈ ℝ*)
126120rpxrd 13017 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (1 / (2↑(π‘˜ + 1))) ∈ ℝ*)
127 bldisj 23904 . . . . . . . . . . . . 13 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ (π‘†β€˜π‘˜) ∈ 𝑋 ∧ ((π‘†β€˜π‘˜)π‘‡π‘˜) ∈ 𝑋) ∧ ((1 / (2β†‘π‘˜)) ∈ ℝ* ∧ (1 / (2↑(π‘˜ + 1))) ∈ ℝ* ∧ ((1 / (2β†‘π‘˜)) +𝑒 (1 / (2↑(π‘˜ + 1)))) ≀ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)))) β†’ (((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘˜))) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2↑(π‘˜ + 1))))) = βˆ…)
1281273exp2 1355 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ (π‘†β€˜π‘˜) ∈ 𝑋 ∧ ((π‘†β€˜π‘˜)π‘‡π‘˜) ∈ 𝑋) β†’ ((1 / (2β†‘π‘˜)) ∈ ℝ* β†’ ((1 / (2↑(π‘˜ + 1))) ∈ ℝ* β†’ (((1 / (2β†‘π‘˜)) +𝑒 (1 / (2↑(π‘˜ + 1)))) ≀ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)) β†’ (((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘˜))) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2↑(π‘˜ + 1))))) = βˆ…))))
129128imp32 420 . . . . . . . . . . 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 1379 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((1 / (2β†‘π‘˜)) +𝑒 (1 / (2↑(π‘˜ + 1)))) ≀ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)) β†’ (((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘˜))) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2↑(π‘˜ + 1))))) = βˆ…))
131124, 130sylbird 260 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))) ≀ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)) β†’ (((π‘†β€˜π‘˜)(ballβ€˜π·)(1 / (2β†‘π‘˜))) ∩ (((π‘†β€˜π‘˜)π‘‡π‘˜)(ballβ€˜π·)(1 / (2↑(π‘˜ + 1))))) = βˆ…))
132131necon3ad 2954 . . . . . . . 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 13031 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))) ∈ ℝ+)
135134rpred 13016 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))) ∈ ℝ)
1364adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 𝐷 ∈ (Metβ€˜π‘‹))
137 metcl 23838 . . . . . . . . . 10 ((𝐷 ∈ (Metβ€˜π‘‹) ∧ (π‘†β€˜π‘˜) ∈ 𝑋 ∧ ((π‘†β€˜π‘˜)π‘‡π‘˜) ∈ 𝑋) β†’ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)) ∈ ℝ)
138136, 40, 86, 137syl3anc 1372 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)) ∈ ℝ)
139135, 138letrid 11366 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))) ≀ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)) ∨ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)) ≀ ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1))))))
140139ord 863 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (Β¬ ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))) ≀ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)) β†’ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)) ≀ ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1))))))
141133, 140mpd 15 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)) ≀ ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))))
142 seqp1 13981 . . . . . . . . . . . 12 (π‘˜ ∈ (β„€β‰₯β€˜0) β†’ (seq0(𝑇, (π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1))))β€˜(π‘˜ + 1)) = ((seq0(𝑇, (π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1))))β€˜π‘˜)𝑇((π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1)))β€˜(π‘˜ + 1))))
143 nn0uz 12864 . . . . . . . . . . . 12 β„•0 = (β„€β‰₯β€˜0)
144142, 143eleq2s 2852 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ (seq0(𝑇, (π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1))))β€˜(π‘˜ + 1)) = ((seq0(𝑇, (π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1))))β€˜π‘˜)𝑇((π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1)))β€˜(π‘˜ + 1))))
14523fveq1i 6893 . . . . . . . . . . 11 (π‘†β€˜(π‘˜ + 1)) = (seq0(𝑇, (π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1))))β€˜(π‘˜ + 1))
14623fveq1i 6893 . . . . . . . . . . . 12 (π‘†β€˜π‘˜) = (seq0(𝑇, (π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1))))β€˜π‘˜)
147146oveq1i 7419 . . . . . . . . . . 11 ((π‘†β€˜π‘˜)𝑇((π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1)))β€˜(π‘˜ + 1))) = ((seq0(𝑇, (π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1))))β€˜π‘˜)𝑇((π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1)))β€˜(π‘˜ + 1)))
148144, 145, 1473eqtr4g 2798 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ (π‘†β€˜(π‘˜ + 1)) = ((π‘†β€˜π‘˜)𝑇((π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1)))β€˜(π‘˜ + 1))))
149 eqid 2733 . . . . . . . . . . . . 13 (π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1))) = (π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1)))
150 eqeq1 2737 . . . . . . . . . . . . . 14 (π‘š = (π‘˜ + 1) β†’ (π‘š = 0 ↔ (π‘˜ + 1) = 0))
151 oveq1 7416 . . . . . . . . . . . . . 14 (π‘š = (π‘˜ + 1) β†’ (π‘š βˆ’ 1) = ((π‘˜ + 1) βˆ’ 1))
152150, 151ifbieq2d 4555 . . . . . . . . . . . . 13 (π‘š = (π‘˜ + 1) β†’ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1)) = if((π‘˜ + 1) = 0, 𝐢, ((π‘˜ + 1) βˆ’ 1)))
153 nn0p1nn 12511 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„•0 β†’ (π‘˜ + 1) ∈ β„•)
154 nnne0 12246 . . . . . . . . . . . . . . . . 17 ((π‘˜ + 1) ∈ β„• β†’ (π‘˜ + 1) β‰  0)
155154neneqd 2946 . . . . . . . . . . . . . . . 16 ((π‘˜ + 1) ∈ β„• β†’ Β¬ (π‘˜ + 1) = 0)
156153, 155syl 17 . . . . . . . . . . . . . . 15 (π‘˜ ∈ β„•0 β†’ Β¬ (π‘˜ + 1) = 0)
157156iffalsed 4540 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„•0 β†’ if((π‘˜ + 1) = 0, 𝐢, ((π‘˜ + 1) βˆ’ 1)) = ((π‘˜ + 1) βˆ’ 1))
158 ovex 7442 . . . . . . . . . . . . . 14 ((π‘˜ + 1) βˆ’ 1) ∈ V
159157, 158eqeltrdi 2842 . . . . . . . . . . . . 13 (π‘˜ ∈ β„•0 β†’ if((π‘˜ + 1) = 0, 𝐢, ((π‘˜ + 1) βˆ’ 1)) ∈ V)
160149, 152, 12, 159fvmptd3 7022 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ ((π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1)))β€˜(π‘˜ + 1)) = if((π‘˜ + 1) = 0, 𝐢, ((π‘˜ + 1) βˆ’ 1)))
161 nn0cn 12482 . . . . . . . . . . . . 13 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„‚)
162 ax-1cn 11168 . . . . . . . . . . . . 13 1 ∈ β„‚
163 pncan 11466 . . . . . . . . . . . . 13 ((π‘˜ ∈ β„‚ ∧ 1 ∈ β„‚) β†’ ((π‘˜ + 1) βˆ’ 1) = π‘˜)
164161, 162, 163sylancl 587 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ ((π‘˜ + 1) βˆ’ 1) = π‘˜)
165160, 157, 1643eqtrd 2777 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ ((π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1)))β€˜(π‘˜ + 1)) = π‘˜)
166165oveq2d 7425 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ ((π‘†β€˜π‘˜)𝑇((π‘š ∈ β„•0 ↦ if(π‘š = 0, 𝐢, (π‘š βˆ’ 1)))β€˜(π‘˜ + 1))) = ((π‘†β€˜π‘˜)π‘‡π‘˜))
167148, 166eqtrd 2773 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ (π‘†β€˜(π‘˜ + 1)) = ((π‘†β€˜π‘˜)π‘‡π‘˜))
168167adantl 483 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π‘†β€˜(π‘˜ + 1)) = ((π‘†β€˜π‘˜)π‘‡π‘˜))
169168oveq1d 7424 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘†β€˜(π‘˜ + 1))𝐷(π‘†β€˜π‘˜)) = (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐷(π‘†β€˜π‘˜)))
170 metsym 23856 . . . . . . . 8 ((𝐷 ∈ (Metβ€˜π‘‹) ∧ ((π‘†β€˜π‘˜)π‘‡π‘˜) ∈ 𝑋 ∧ (π‘†β€˜π‘˜) ∈ 𝑋) β†’ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐷(π‘†β€˜π‘˜)) = ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)))
171136, 86, 40, 170syl3anc 1372 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((π‘†β€˜π‘˜)π‘‡π‘˜)𝐷(π‘†β€˜π‘˜)) = ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)))
172169, 171eqtrd 2773 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘†β€˜(π‘˜ + 1))𝐷(π‘†β€˜π‘˜)) = ((π‘†β€˜π‘˜)𝐷((π‘†β€˜π‘˜)π‘‡π‘˜)))
173 3cn 12293 . . . . . . . . . . . . 13 3 ∈ β„‚
1741732timesi 12350 . . . . . . . . . . . 12 (2 Β· 3) = (3 + 3)
175174oveq1i 7419 . . . . . . . . . . 11 ((2 Β· 3) βˆ’ 3) = ((3 + 3) βˆ’ 3)
176173, 173pncan3oi 11476 . . . . . . . . . . 11 ((3 + 3) βˆ’ 3) = 3
177 df-3 12276 . . . . . . . . . . 11 3 = (2 + 1)
178175, 176, 1773eqtri 2765 . . . . . . . . . 10 ((2 Β· 3) βˆ’ 3) = (2 + 1)
179178oveq1i 7419 . . . . . . . . 9 (((2 Β· 3) βˆ’ 3) / (2↑(π‘˜ + 1))) = ((2 + 1) / (2↑(π‘˜ + 1)))
180 rpcn 12984 . . . . . . . . . . 11 ((2↑(π‘˜ + 1)) ∈ ℝ+ β†’ (2↑(π‘˜ + 1)) ∈ β„‚)
181 rpne0 12990 . . . . . . . . . . 11 ((2↑(π‘˜ + 1)) ∈ ℝ+ β†’ (2↑(π‘˜ + 1)) β‰  0)
182 2cn 12287 . . . . . . . . . . . . 13 2 ∈ β„‚
183182, 173mulcli 11221 . . . . . . . . . . . 12 (2 Β· 3) ∈ β„‚
184 divsubdir 11908 . . . . . . . . . . . 12 (((2 Β· 3) ∈ β„‚ ∧ 3 ∈ β„‚ ∧ ((2↑(π‘˜ + 1)) ∈ β„‚ ∧ (2↑(π‘˜ + 1)) β‰  0)) β†’ (((2 Β· 3) βˆ’ 3) / (2↑(π‘˜ + 1))) = (((2 Β· 3) / (2↑(π‘˜ + 1))) βˆ’ (3 / (2↑(π‘˜ + 1)))))
185183, 173, 184mp3an12 1452 . . . . . . . . . . 11 (((2↑(π‘˜ + 1)) ∈ β„‚ ∧ (2↑(π‘˜ + 1)) β‰  0) β†’ (((2 Β· 3) βˆ’ 3) / (2↑(π‘˜ + 1))) = (((2 Β· 3) / (2↑(π‘˜ + 1))) βˆ’ (3 / (2↑(π‘˜ + 1)))))
186180, 181, 185syl2anc 585 . . . . . . . . . 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 11897 . . . . . . . . . . . 12 ((2 ∈ β„‚ ∧ 1 ∈ β„‚ ∧ ((2↑(π‘˜ + 1)) ∈ β„‚ ∧ (2↑(π‘˜ + 1)) β‰  0)) β†’ ((2 + 1) / (2↑(π‘˜ + 1))) = ((2 / (2↑(π‘˜ + 1))) + (1 / (2↑(π‘˜ + 1)))))
189182, 162, 188mp3an12 1452 . . . . . . . . . . 11 (((2↑(π‘˜ + 1)) ∈ β„‚ ∧ (2↑(π‘˜ + 1)) β‰  0) β†’ ((2 + 1) / (2↑(π‘˜ + 1))) = ((2 / (2↑(π‘˜ + 1))) + (1 / (2↑(π‘˜ + 1)))))
190180, 181, 189syl2anc 585 . . . . . . . . . 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 2797 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ (((2 Β· 3) / (2↑(π‘˜ + 1))) βˆ’ (3 / (2↑(π‘˜ + 1)))) = ((2 / (2↑(π‘˜ + 1))) + (1 / (2↑(π‘˜ + 1)))))
193 rpcn 12984 . . . . . . . . . . . 12 ((2β†‘π‘˜) ∈ ℝ+ β†’ (2β†‘π‘˜) ∈ β„‚)
194 rpne0 12990 . . . . . . . . . . . 12 ((2β†‘π‘˜) ∈ ℝ+ β†’ (2β†‘π‘˜) β‰  0)
195 2cnne0 12422 . . . . . . . . . . . . 13 (2 ∈ β„‚ ∧ 2 β‰  0)
196 divcan5 11916 . . . . . . . . . . . . 13 ((3 ∈ β„‚ ∧ ((2β†‘π‘˜) ∈ β„‚ ∧ (2β†‘π‘˜) β‰  0) ∧ (2 ∈ β„‚ ∧ 2 β‰  0)) β†’ ((2 Β· 3) / (2 Β· (2β†‘π‘˜))) = (3 / (2β†‘π‘˜)))
197173, 195, 196mp3an13 1453 . . . . . . . . . . . 12 (((2β†‘π‘˜) ∈ β„‚ ∧ (2β†‘π‘˜) β‰  0) β†’ ((2 Β· 3) / (2 Β· (2β†‘π‘˜))) = (3 / (2β†‘π‘˜)))
198193, 194, 197syl2anc 585 . . . . . . . . . . 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 11196 . . . . . . . . . . . . 13 ((2 ∈ β„‚ ∧ (2β†‘π‘˜) ∈ β„‚) β†’ (2 Β· (2β†‘π‘˜)) = ((2β†‘π‘˜) Β· 2))
202182, 200, 201sylancr 588 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ (2 Β· (2β†‘π‘˜)) = ((2β†‘π‘˜) Β· 2))
203 expp1 14034 . . . . . . . . . . . . 13 ((2 ∈ β„‚ ∧ π‘˜ ∈ β„•0) β†’ (2↑(π‘˜ + 1)) = ((2β†‘π‘˜) Β· 2))
204182, 203mpan 689 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ (2↑(π‘˜ + 1)) = ((2β†‘π‘˜) Β· 2))
205202, 204eqtr4d 2776 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ (2 Β· (2β†‘π‘˜)) = (2↑(π‘˜ + 1)))
206205oveq2d 7425 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ ((2 Β· 3) / (2 Β· (2β†‘π‘˜))) = ((2 Β· 3) / (2↑(π‘˜ + 1))))
207199, 206eqtr3d 2775 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ (3 / (2β†‘π‘˜)) = ((2 Β· 3) / (2↑(π‘˜ + 1))))
208207oveq1d 7424 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ ((3 / (2β†‘π‘˜)) βˆ’ (3 / (2↑(π‘˜ + 1)))) = (((2 Β· 3) / (2↑(π‘˜ + 1))) βˆ’ (3 / (2↑(π‘˜ + 1)))))
209 divcan5 11916 . . . . . . . . . . . . 13 ((1 ∈ β„‚ ∧ ((2β†‘π‘˜) ∈ β„‚ ∧ (2β†‘π‘˜) β‰  0) ∧ (2 ∈ β„‚ ∧ 2 β‰  0)) β†’ ((2 Β· 1) / (2 Β· (2β†‘π‘˜))) = (1 / (2β†‘π‘˜)))
210162, 195, 209mp3an13 1453 . . . . . . . . . . . 12 (((2β†‘π‘˜) ∈ β„‚ ∧ (2β†‘π‘˜) β‰  0) β†’ ((2 Β· 1) / (2 Β· (2β†‘π‘˜))) = (1 / (2β†‘π‘˜)))
211193, 194, 210syl2anc 585 . . . . . . . . . . 11 ((2β†‘π‘˜) ∈ ℝ+ β†’ ((2 Β· 1) / (2 Β· (2β†‘π‘˜))) = (1 / (2β†‘π‘˜)))
21251, 211syl 17 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ ((2 Β· 1) / (2 Β· (2β†‘π‘˜))) = (1 / (2β†‘π‘˜)))
213 2t1e2 12375 . . . . . . . . . . . 12 (2 Β· 1) = 2
214213a1i 11 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ (2 Β· 1) = 2)
215214, 205oveq12d 7427 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ ((2 Β· 1) / (2 Β· (2β†‘π‘˜))) = (2 / (2↑(π‘˜ + 1))))
216212, 215eqtr3d 2775 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ (1 / (2β†‘π‘˜)) = (2 / (2↑(π‘˜ + 1))))
217216oveq1d 7424 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))) = ((2 / (2↑(π‘˜ + 1))) + (1 / (2↑(π‘˜ + 1)))))
218192, 208, 2173eqtr4d 2783 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ ((3 / (2β†‘π‘˜)) βˆ’ (3 / (2↑(π‘˜ + 1)))) = ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))))
219218adantl 483 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((3 / (2β†‘π‘˜)) βˆ’ (3 / (2↑(π‘˜ + 1)))) = ((1 / (2β†‘π‘˜)) + (1 / (2↑(π‘˜ + 1)))))
220141, 172, 2193brtr4d 5181 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘†β€˜(π‘˜ + 1))𝐷(π‘†β€˜π‘˜)) ≀ ((3 / (2β†‘π‘˜)) βˆ’ (3 / (2↑(π‘˜ + 1)))))
221 blss2 23910 . . . . 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 1386 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((π‘†β€˜(π‘˜ + 1))(ballβ€˜π·)(3 / (2↑(π‘˜ + 1)))) βŠ† ((π‘†β€˜π‘˜)(ballβ€˜π·)(3 / (2β†‘π‘˜))))
2231, 222sylan2 594 . . 3 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((π‘†β€˜(π‘˜ + 1))(ballβ€˜π·)(3 / (2↑(π‘˜ + 1)))) βŠ† ((π‘†β€˜π‘˜)(ballβ€˜π·)(3 / (2β†‘π‘˜))))
224 peano2nn 12224 . . . . . . 7 (π‘˜ ∈ β„• β†’ (π‘˜ + 1) ∈ β„•)
225 fveq2 6892 . . . . . . . . 9 (𝑛 = (π‘˜ + 1) β†’ (π‘†β€˜π‘›) = (π‘†β€˜(π‘˜ + 1)))
226 oveq2 7417 . . . . . . . . . 10 (𝑛 = (π‘˜ + 1) β†’ (2↑𝑛) = (2↑(π‘˜ + 1)))
227226oveq2d 7425 . . . . . . . . 9 (𝑛 = (π‘˜ + 1) β†’ (3 / (2↑𝑛)) = (3 / (2↑(π‘˜ + 1))))
228225, 227opeq12d 4882 . . . . . . . 8 (𝑛 = (π‘˜ + 1) β†’ ⟨(π‘†β€˜π‘›), (3 / (2↑𝑛))⟩ = ⟨(π‘†β€˜(π‘˜ + 1)), (3 / (2↑(π‘˜ + 1)))⟩)
229 heibor.12 . . . . . . . 8 𝑀 = (𝑛 ∈ β„• ↦ ⟨(π‘†β€˜π‘›), (3 / (2↑𝑛))⟩)
230 opex 5465 . . . . . . . 8 ⟨(π‘†β€˜(π‘˜ + 1)), (3 / (2↑(π‘˜ + 1)))⟩ ∈ V
231228, 229, 230fvmpt 6999 . . . . . . 7 ((π‘˜ + 1) ∈ β„• β†’ (π‘€β€˜(π‘˜ + 1)) = ⟨(π‘†β€˜(π‘˜ + 1)), (3 / (2↑(π‘˜ + 1)))⟩)
232224, 231syl 17 . . . . . 6 (π‘˜ ∈ β„• β†’ (π‘€β€˜(π‘˜ + 1)) = ⟨(π‘†β€˜(π‘˜ + 1)), (3 / (2↑(π‘˜ + 1)))⟩)
233232adantl 483 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘€β€˜(π‘˜ + 1)) = ⟨(π‘†β€˜(π‘˜ + 1)), (3 / (2↑(π‘˜ + 1)))⟩)
234233fveq2d 6896 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((ballβ€˜π·)β€˜(π‘€β€˜(π‘˜ + 1))) = ((ballβ€˜π·)β€˜βŸ¨(π‘†β€˜(π‘˜ + 1)), (3 / (2↑(π‘˜ + 1)))⟩))
235 df-ov 7412 . . . 4 ((π‘†β€˜(π‘˜ + 1))(ballβ€˜π·)(3 / (2↑(π‘˜ + 1)))) = ((ballβ€˜π·)β€˜βŸ¨(π‘†β€˜(π‘˜ + 1)), (3 / (2↑(π‘˜ + 1)))⟩)
236234, 235eqtr4di 2791 . . 3 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((ballβ€˜π·)β€˜(π‘€β€˜(π‘˜ + 1))) = ((π‘†β€˜(π‘˜ + 1))(ballβ€˜π·)(3 / (2↑(π‘˜ + 1)))))
237 fveq2 6892 . . . . . . . 8 (𝑛 = π‘˜ β†’ (π‘†β€˜π‘›) = (π‘†β€˜π‘˜))
238 oveq2 7417 . . . . . . . . 9 (𝑛 = π‘˜ β†’ (2↑𝑛) = (2β†‘π‘˜))
239238oveq2d 7425 . . . . . . . 8 (𝑛 = π‘˜ β†’ (3 / (2↑𝑛)) = (3 / (2β†‘π‘˜)))
240237, 239opeq12d 4882 . . . . . . 7 (𝑛 = π‘˜ β†’ ⟨(π‘†β€˜π‘›), (3 / (2↑𝑛))⟩ = ⟨(π‘†β€˜π‘˜), (3 / (2β†‘π‘˜))⟩)
241 opex 5465 . . . . . . 7 ⟨(π‘†β€˜π‘˜), (3 / (2β†‘π‘˜))⟩ ∈ V
242240, 229, 241fvmpt 6999 . . . . . 6 (π‘˜ ∈ β„• β†’ (π‘€β€˜π‘˜) = ⟨(π‘†β€˜π‘˜), (3 / (2β†‘π‘˜))⟩)
243242fveq2d 6896 . . . . 5 (π‘˜ ∈ β„• β†’ ((ballβ€˜π·)β€˜(π‘€β€˜π‘˜)) = ((ballβ€˜π·)β€˜βŸ¨(π‘†β€˜π‘˜), (3 / (2β†‘π‘˜))⟩))
244 df-ov 7412 . . . . 5 ((π‘†β€˜π‘˜)(ballβ€˜π·)(3 / (2β†‘π‘˜))) = ((ballβ€˜π·)β€˜βŸ¨(π‘†β€˜π‘˜), (3 / (2β†‘π‘˜))⟩)
245243, 244eqtr4di 2791 . . . 4 (π‘˜ ∈ β„• β†’ ((ballβ€˜π·)β€˜(π‘€β€˜π‘˜)) = ((π‘†β€˜π‘˜)(ballβ€˜π·)(3 / (2β†‘π‘˜))))
246245adantl 483 . . 3 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((ballβ€˜π·)β€˜(π‘€β€˜π‘˜)) = ((π‘†β€˜π‘˜)(ballβ€˜π·)(3 / (2β†‘π‘˜))))
247223, 236, 2463sstr4d 4030 . 2 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((ballβ€˜π·)β€˜(π‘€β€˜(π‘˜ + 1))) βŠ† ((ballβ€˜π·)β€˜(π‘€β€˜π‘˜)))
248247ralrimiva 3147 1 (πœ‘ β†’ βˆ€π‘˜ ∈ β„• ((ballβ€˜π·)β€˜(π‘€β€˜(π‘˜ + 1))) βŠ† ((ballβ€˜π·)β€˜(π‘€β€˜π‘˜)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  {cab 2710   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3475   ∩ cin 3948   βŠ† wss 3949  βˆ…c0 4323  ifcif 4529  π’« cpw 4603  βŸ¨cop 4635  βˆͺ cuni 4909  βˆͺ ciun 4998   class class class wbr 5149  {copab 5211   ↦ cmpt 5232  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409   ∈ cmpo 7411  2nd c2nd 7974  Fincfn 8939  β„‚cc 11108  β„cr 11109  0cc0 11110  1c1 11111   + caddc 11113   Β· cmul 11115  β„*cxr 11247   ≀ cle 11249   βˆ’ cmin 11444   / cdiv 11871  β„•cn 12212  2c2 12267  3c3 12268  β„•0cn0 12472  β„€β‰₯cuz 12822  β„+crp 12974   +𝑒 cxad 13090  seqcseq 13966  β†‘cexp 14027  βˆžMetcxmet 20929  Metcmet 20930  ballcbl 20931  MetOpencmopn 20934  CMetccmet 24771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-er 8703  df-map 8822  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-n0 12473  df-z 12559  df-uz 12823  df-rp 12975  df-xneg 13092  df-xadd 13093  df-xmul 13094  df-seq 13967  df-exp 14028  df-psmet 20936  df-xmet 20937  df-met 20938  df-bl 20939  df-cmet 24774
This theorem is referenced by:  heiborlem8  36686  heiborlem9  36687
  Copyright terms: Public domain W3C validator