Metamath Proof Explorer

Theorem heiborlem5

Description: Lemma for heibor . The function M is a set of point-and-radius pairs suitable for application to caubl . (Contributed by Jeff Madsen, 23-Jan-2014)

Ref Expression
Hypotheses 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 ⊢ 𝑆 = seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) )
heibor.12 ⊢ 𝑀 = ( 𝑛 ∈ ℕ ↦ ⟨ ( 𝑆 ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) ⟩ )
Assertion heiborlem5 ( 𝜑 → 𝑀 : ℕ ⟶ ( 𝑋 × ℝ+ ) )

Proof

Step Hyp Ref Expression
1 heibor.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 heibor.3 ⊢ 𝐾 = { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 }
3 heibor.4 ⊢ 𝐺 = { ⟨ 𝑦 , 𝑛 ⟩ ∣ ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ∧ ( 𝑦 𝐵 𝑛 ) ∈ 𝐾 ) }
4 heibor.5 ⊢ 𝐵 = ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) )
5 heibor.6 ⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
6 heibor.7 ⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ ( 𝒫 𝑋 ∩ Fin ) )
7 heibor.8 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) )
8 heibor.9 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐺 ( ( 𝑇 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )
9 heibor.10 ⊢ ( 𝜑 → 𝐶 𝐺 0 )
10 heibor.11 ⊢ 𝑆 = seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) )
11 heibor.12 ⊢ 𝑀 = ( 𝑛 ∈ ℕ ↦ ⟨ ( 𝑆 ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) ⟩ )
12 nnnn0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
13 inss1 ⊢ ( 𝒫 𝑋 ∩ Fin ) ⊆ 𝒫 𝑋
14 6 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝒫 𝑋 ∩ Fin ) )
15 13 14 sseldi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝒫 𝑋 )
16 15 elpwid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ⊆ 𝑋 )
17 1 2 3 4 5 6 7 8 9 10 heiborlem4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑆 ‘ 𝑘 ) 𝐺 𝑘 )
18 fvex ⊢ ( 𝑆 ‘ 𝑘 ) ∈ V
19 vex ⊢ 𝑘 ∈ V
20 1 2 3 18 19 heiborlem2 ⊢ ( ( 𝑆 ‘ 𝑘 ) 𝐺 𝑘 ↔ ( 𝑘 ∈ ℕ0 ∧ ( 𝑆 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) ∧ ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∈ 𝐾 ) )
21 20 simp2bi ⊢ ( ( 𝑆 ‘ 𝑘 ) 𝐺 𝑘 → ( 𝑆 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) )
22 17 21 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑆 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) )
23 16 22 sseldd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑆 ‘ 𝑘 ) ∈ 𝑋 )
24 12 23 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ‘ 𝑘 ) ∈ 𝑋 )
25 24 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ∈ 𝑋 )
26 fveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝑆 ‘ 𝑘 ) = ( 𝑆 ‘ 𝑛 ) )
27 26 eleq1d ⊢ ( 𝑘 = 𝑛 → ( ( 𝑆 ‘ 𝑘 ) ∈ 𝑋 ↔ ( 𝑆 ‘ 𝑛 ) ∈ 𝑋 ) )
28 27 cbvralvw ⊢ ( ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ∈ 𝑋 ↔ ∀ 𝑛 ∈ ℕ ( 𝑆 ‘ 𝑛 ) ∈ 𝑋 )
29 25 28 sylib ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝑆 ‘ 𝑛 ) ∈ 𝑋 )
30 3re ⊢ 3 ∈ ℝ
31 3pos ⊢ 0 < 3
32 30 31 elrpii ⊢ 3 ∈ ℝ+
33 2nn ⊢ 2 ∈ ℕ
34 nnnn0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
35 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
36 33 34 35 sylancr ⊢ ( 𝑛 ∈ ℕ → ( 2 ↑ 𝑛 ) ∈ ℕ )
37 36 nnrpd ⊢ ( 𝑛 ∈ ℕ → ( 2 ↑ 𝑛 ) ∈ ℝ+ )
38 rpdivcl ⊢ ( ( 3 ∈ ℝ+ ∧ ( 2 ↑ 𝑛 ) ∈ ℝ+ ) → ( 3 / ( 2 ↑ 𝑛 ) ) ∈ ℝ+ )
39 32 37 38 sylancr ⊢ ( 𝑛 ∈ ℕ → ( 3 / ( 2 ↑ 𝑛 ) ) ∈ ℝ+ )
40 opelxpi ⊢ ( ( ( 𝑆 ‘ 𝑛 ) ∈ 𝑋 ∧ ( 3 / ( 2 ↑ 𝑛 ) ) ∈ ℝ+ ) → ⟨ ( 𝑆 ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) ⟩ ∈ ( 𝑋 × ℝ+ ) )
41 40 expcom ⊢ ( ( 3 / ( 2 ↑ 𝑛 ) ) ∈ ℝ+ → ( ( 𝑆 ‘ 𝑛 ) ∈ 𝑋 → ⟨ ( 𝑆 ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) ⟩ ∈ ( 𝑋 × ℝ+ ) ) )
42 39 41 syl ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑆 ‘ 𝑛 ) ∈ 𝑋 → ⟨ ( 𝑆 ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) ⟩ ∈ ( 𝑋 × ℝ+ ) ) )
43 42 ralimia ⊢ ( ∀ 𝑛 ∈ ℕ ( 𝑆 ‘ 𝑛 ) ∈ 𝑋 → ∀ 𝑛 ∈ ℕ ⟨ ( 𝑆 ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) ⟩ ∈ ( 𝑋 × ℝ+ ) )
44 29 43 syl ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ⟨ ( 𝑆 ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) ⟩ ∈ ( 𝑋 × ℝ+ ) )
45 11 fmpt ⊢ ( ∀ 𝑛 ∈ ℕ ⟨ ( 𝑆 ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) ⟩ ∈ ( 𝑋 × ℝ+ ) ↔ 𝑀 : ℕ ⟶ ( 𝑋 × ℝ+ ) )
46 44 45 sylib ⊢ ( 𝜑 → 𝑀 : ℕ ⟶ ( 𝑋 × ℝ+ ) )