heiborlem9

Description: Lemma for heibor . Discharge the hypotheses of heiborlem8 by applying caubl to get a convergent point and adding the open cover assumption. (Contributed by Jeff Madsen, 20-Jan-2014)

	Ref	Expression
Hypotheses	heibor.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	heibor.3	⊢ 𝐾 = { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 }
	heibor.4	⊢ 𝐺 = { ⟨ 𝑦 , 𝑛 ⟩ ∣ ( 𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ∧ ( 𝑦 𝐵 𝑛 ) ∈ 𝐾 ) }
	heibor.5	⊢ 𝐵 = ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ₀ ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) )
	heibor.6	⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
	heibor.7	⊢ ( 𝜑 → 𝐹 : ℕ₀ ⟶ ( 𝒫 𝑋 ∩ Fin ) )
	heibor.8	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ₀ 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) )
	heibor.9	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐺 ( ( 𝑇 ‘ 𝑥 ) 𝐺 ( ( 2^nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )
	heibor.10	⊢ ( 𝜑 → 𝐶 𝐺 0 )
	heibor.11	⊢ 𝑆 = seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ₀ ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) )
	heibor.12	⊢ 𝑀 = ( 𝑛 ∈ ℕ ↦ ⟨ ( 𝑆 ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) ⟩ )
	heibor.13	⊢ ( 𝜑 → 𝑈 ⊆ 𝐽 )
	heiborlem9.14	⊢ ( 𝜑 → ∪ 𝑈 = 𝑋 )
Assertion	heiborlem9	⊢ ( 𝜑 → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		heibor.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2		heibor.3	⊢ 𝐾 = { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 }
3		heibor.4	⊢ 𝐺 = { ⟨ 𝑦 , 𝑛 ⟩ ∣ ( 𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ∧ ( 𝑦 𝐵 𝑛 ) ∈ 𝐾 ) }
4		heibor.5	⊢ 𝐵 = ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ₀ ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) )
5		heibor.6	⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
6		heibor.7	⊢ ( 𝜑 → 𝐹 : ℕ₀ ⟶ ( 𝒫 𝑋 ∩ Fin ) )
7		heibor.8	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ₀ 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) )
8		heibor.9	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐺 ( ( 𝑇 ‘ 𝑥 ) 𝐺 ( ( 2^nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )
9		heibor.10	⊢ ( 𝜑 → 𝐶 𝐺 0 )
10		heibor.11	⊢ 𝑆 = seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ₀ ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) )
11		heibor.12	⊢ 𝑀 = ( 𝑛 ∈ ℕ ↦ ⟨ ( 𝑆 ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) ⟩ )
12		heibor.13	⊢ ( 𝜑 → 𝑈 ⊆ 𝐽 )
13		heiborlem9.14	⊢ ( 𝜑 → ∪ 𝑈 = 𝑋 )
14		cmetmet	⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
15		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
16	5 14 15	3syl	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
17	1	mopntopon	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
18	16 17	syl	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
19	1 2 3 4 5 6 7 8 9 10 11	heiborlem5	⊢ ( 𝜑 → 𝑀 : ℕ ⟶ ( 𝑋 × ℝ⁺ ) )
20	1 2 3 4 5 6 7 8 9 10 11	heiborlem6	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ ( 𝑘 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) )
21	1 2 3 4 5 6 7 8 9 10 11	heiborlem7	⊢ ∀ 𝑟 ∈ ℝ⁺ ∃ 𝑘 ∈ ℕ ( 2^nd ‘ ( 𝑀 ‘ 𝑘 ) ) < 𝑟
22	21	a1i	⊢ ( 𝜑 → ∀ 𝑟 ∈ ℝ⁺ ∃ 𝑘 ∈ ℕ ( 2^nd ‘ ( 𝑀 ‘ 𝑘 ) ) < 𝑟 )
23	16 19 20 22	caubl	⊢ ( 𝜑 → ( 1^st ∘ 𝑀 ) ∈ ( Cau ‘ 𝐷 ) )
24	1	cmetcau	⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ ( 1^st ∘ 𝑀 ) ∈ ( Cau ‘ 𝐷 ) ) → ( 1^st ∘ 𝑀 ) ∈ dom ( ⇝_𝑡 ‘ 𝐽 ) )
25	5 23 24	syl2anc	⊢ ( 𝜑 → ( 1^st ∘ 𝑀 ) ∈ dom ( ⇝_𝑡 ‘ 𝐽 ) )
26	1	methaus	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Haus )
27	16 26	syl	⊢ ( 𝜑 → 𝐽 ∈ Haus )
28		lmfun	⊢ ( 𝐽 ∈ Haus → Fun ( ⇝_𝑡 ‘ 𝐽 ) )
29		funfvbrb	⊢ ( Fun ( ⇝_𝑡 ‘ 𝐽 ) → ( ( 1^st ∘ 𝑀 ) ∈ dom ( ⇝_𝑡 ‘ 𝐽 ) ↔ ( 1^st ∘ 𝑀 ) ( ⇝_𝑡 ‘ 𝐽 ) ( ( ⇝_𝑡 ‘ 𝐽 ) ‘ ( 1^st ∘ 𝑀 ) ) ) )
30	27 28 29	3syl	⊢ ( 𝜑 → ( ( 1^st ∘ 𝑀 ) ∈ dom ( ⇝_𝑡 ‘ 𝐽 ) ↔ ( 1^st ∘ 𝑀 ) ( ⇝_𝑡 ‘ 𝐽 ) ( ( ⇝_𝑡 ‘ 𝐽 ) ‘ ( 1^st ∘ 𝑀 ) ) ) )
31	25 30	mpbid	⊢ ( 𝜑 → ( 1^st ∘ 𝑀 ) ( ⇝_𝑡 ‘ 𝐽 ) ( ( ⇝_𝑡 ‘ 𝐽 ) ‘ ( 1^st ∘ 𝑀 ) ) )
32		lmcl	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 1^st ∘ 𝑀 ) ( ⇝_𝑡 ‘ 𝐽 ) ( ( ⇝_𝑡 ‘ 𝐽 ) ‘ ( 1^st ∘ 𝑀 ) ) ) → ( ( ⇝_𝑡 ‘ 𝐽 ) ‘ ( 1^st ∘ 𝑀 ) ) ∈ 𝑋 )
33	18 31 32	syl2anc	⊢ ( 𝜑 → ( ( ⇝_𝑡 ‘ 𝐽 ) ‘ ( 1^st ∘ 𝑀 ) ) ∈ 𝑋 )
34	33 13	eleqtrrd	⊢ ( 𝜑 → ( ( ⇝_𝑡 ‘ 𝐽 ) ‘ ( 1^st ∘ 𝑀 ) ) ∈ ∪ 𝑈 )
35		eluni2	⊢ ( ( ( ⇝_𝑡 ‘ 𝐽 ) ‘ ( 1^st ∘ 𝑀 ) ) ∈ ∪ 𝑈 ↔ ∃ 𝑡 ∈ 𝑈 ( ( ⇝_𝑡 ‘ 𝐽 ) ‘ ( 1^st ∘ 𝑀 ) ) ∈ 𝑡 )
36	34 35	sylib	⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝑈 ( ( ⇝_𝑡 ‘ 𝐽 ) ‘ ( 1^st ∘ 𝑀 ) ) ∈ 𝑡 )
37	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑈 ∧ ( ( ⇝_𝑡 ‘ 𝐽 ) ‘ ( 1^st ∘ 𝑀 ) ) ∈ 𝑡 ) ) → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
38	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑈 ∧ ( ( ⇝_𝑡 ‘ 𝐽 ) ‘ ( 1^st ∘ 𝑀 ) ) ∈ 𝑡 ) ) → 𝐹 : ℕ₀ ⟶ ( 𝒫 𝑋 ∩ Fin ) )
39	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑈 ∧ ( ( ⇝_𝑡 ‘ 𝐽 ) ‘ ( 1^st ∘ 𝑀 ) ) ∈ 𝑡 ) ) → ∀ 𝑛 ∈ ℕ₀ 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) )
40	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑈 ∧ ( ( ⇝_𝑡 ‘ 𝐽 ) ‘ ( 1^st ∘ 𝑀 ) ) ∈ 𝑡 ) ) → ∀ 𝑥 ∈ 𝐺 ( ( 𝑇 ‘ 𝑥 ) 𝐺 ( ( 2^nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )
41	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑈 ∧ ( ( ⇝_𝑡 ‘ 𝐽 ) ‘ ( 1^st ∘ 𝑀 ) ) ∈ 𝑡 ) ) → 𝐶 𝐺 0 )
42	12	adantr	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑈 ∧ ( ( ⇝_𝑡 ‘ 𝐽 ) ‘ ( 1^st ∘ 𝑀 ) ) ∈ 𝑡 ) ) → 𝑈 ⊆ 𝐽 )
43		fvex	⊢ ( ( ⇝_𝑡 ‘ 𝐽 ) ‘ ( 1^st ∘ 𝑀 ) ) ∈ V
44		simprr	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑈 ∧ ( ( ⇝_𝑡 ‘ 𝐽 ) ‘ ( 1^st ∘ 𝑀 ) ) ∈ 𝑡 ) ) → ( ( ⇝_𝑡 ‘ 𝐽 ) ‘ ( 1^st ∘ 𝑀 ) ) ∈ 𝑡 )
45		simprl	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑈 ∧ ( ( ⇝_𝑡 ‘ 𝐽 ) ‘ ( 1^st ∘ 𝑀 ) ) ∈ 𝑡 ) ) → 𝑡 ∈ 𝑈 )
46	31	adantr	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑈 ∧ ( ( ⇝_𝑡 ‘ 𝐽 ) ‘ ( 1^st ∘ 𝑀 ) ) ∈ 𝑡 ) ) → ( 1^st ∘ 𝑀 ) ( ⇝_𝑡 ‘ 𝐽 ) ( ( ⇝_𝑡 ‘ 𝐽 ) ‘ ( 1^st ∘ 𝑀 ) ) )
47	1 2 3 4 37 38 39 40 41 10 11 42 43 44 45 46	heiborlem8	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑈 ∧ ( ( ⇝_𝑡 ‘ 𝐽 ) ‘ ( 1^st ∘ 𝑀 ) ) ∈ 𝑡 ) ) → 𝜓 )
48	36 47	rexlimddv	⊢ ( 𝜑 → 𝜓 )

Metamath Proof Explorer

Theorem heiborlem9

Proof