Theorem heiborlem9 34539

Description: Lemma for heibor 34541. Discharge the hypotheses of heiborlem8 34538 by applying caubl 23617 to get a convergent point and adding the open cover assumption. (Contributed by Jeff Madsen, 20-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↑𝑛))⟩)
heibor.13	⊢ (𝜑 → 𝑈 ⊆ 𝐽)
heiborlem9.14	⊢ (𝜑 → ∪ 𝑈 = 𝑋)

Assertion

Ref	Expression
heiborlem9	⊢ (𝜑 → 𝜓)

Distinct variable groups:   𝑥,𝑛,𝑦,𝑢,𝐹   𝑥,𝐺   𝜑,𝑥   𝑚,𝑛,𝑢,𝑣,𝑥,𝑦,𝑧,𝐷   𝑚,𝑀,𝑢,𝑥,𝑦,𝑧   𝑇,𝑚,𝑛,𝑥,𝑦,𝑧   𝐵,𝑛,𝑢,𝑣,𝑦   𝑚,𝐽,𝑛,𝑢,𝑣,𝑥,𝑦,𝑧   𝑈,𝑛,𝑢,𝑣,𝑥,𝑦,𝑧   𝜓,𝑦,𝑧   𝑆,𝑚,𝑛,𝑢,𝑣,𝑥,𝑦,𝑧   𝑚,𝑋,𝑛,𝑢,𝑣,𝑥,𝑦,𝑧   𝐶,𝑚,𝑛,𝑢,𝑣,𝑦   𝑛,𝐾,𝑥,𝑦,𝑧   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑦,𝑧,𝑣,𝑢,𝑚,𝑛)   𝜓(𝑥,𝑣,𝑢,𝑚,𝑛)   𝐵(𝑧,𝑚)   𝐶(𝑥,𝑧)   𝑇(𝑣,𝑢)   𝑈(𝑚)   𝐹(𝑧,𝑣,𝑚)   𝐺(𝑦,𝑧,𝑣,𝑢,𝑚,𝑛)   𝐾(𝑣,𝑢,𝑚)   𝑀(𝑣,𝑛)

Proof of Theorem heiborlem9

Dummy variables 𝑡 𝑘 𝑟 are mutually distinct and distinct from all other variables.

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 387   ∧ w3a 1068   = wceq 1507   ∈ wcel 2050  {cab 2758  ∀wral 3088  ∃wrex 3089   ∩ cin 3830   ⊆ wss 3831  ifcif 4351  𝒫 cpw 4423  ⟨cop 4448  ∪ cuni 4713  ∪ ciun 4793   class class class wbr 4930  {copab 4992   ↦ cmpt 5009  dom cdm 5408   ∘ ccom 5412  Fun wfun 6184  ⟶wf 6186  ‘cfv 6190  (class class class)co 6978   ∈ cmpo 6980  1^st c1st 7501  2^nd c2nd 7502  Fincfn 8308  0cc0 10337  1c1 10338   + caddc 10340   < clt 10476   − cmin 10672   / cdiv 11100  ℕcn 11441  2c2 11498  3c3 11499  ℕ₀cn0 11710  ℝ⁺crp 12207  seqcseq 13187  ↑cexp 13247  ∞Metcxmet 20235  Metcmet 20236  ballcbl 20237  MetOpencmopn 20240  TopOnctopon 21225  ⇝_𝑡clm 21541  Hauscha 21623  Cauccau 23562  CMetccmet 23563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-rep 5050  ax-sep 5061  ax-nul 5068  ax-pow 5120  ax-pr 5187  ax-un 7281  ax-cnex 10393  ax-resscn 10394  ax-1cn 10395  ax-icn 10396  ax-addcl 10397  ax-addrcl 10398  ax-mulcl 10399  ax-mulrcl 10400  ax-mulcom 10401  ax-addass 10402  ax-mulass 10403  ax-distr 10404  ax-i2m1 10405  ax-1ne0 10406  ax-1rid 10407  ax-rnegex 10408  ax-rrecex 10409  ax-cnre 10410  ax-pre-lttri 10411  ax-pre-lttrn 10412  ax-pre-ltadd 10413  ax-pre-mulgt0 10414  ax-pre-sup 10415

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rmo 3096  df-rab 3097  df-v 3417  df-sbc 3684  df-csb 3789  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-pss 3847  df-nul 4181  df-if 4352  df-pw 4425  df-sn 4443  df-pr 4445  df-tp 4447  df-op 4449  df-uni 4714  df-int 4751  df-iun 4795  df-iin 4796  df-br 4931  df-opab 4993  df-mpt 5010  df-tr 5032  df-id 5313  df-eprel 5318  df-po 5327  df-so 5328  df-fr 5367  df-we 5369  df-xp 5414  df-rel 5415  df-cnv 5416  df-co 5417  df-dm 5418  df-rn 5419  df-res 5420  df-ima 5421  df-pred 5988  df-ord 6034  df-on 6035  df-lim 6036  df-suc 6037  df-iota 6154  df-fun 6192  df-fn 6193  df-f 6194  df-f1 6195  df-fo 6196  df-f1o 6197  df-fv 6198  df-riota 6939  df-ov 6981  df-oprab 6982  df-mpo 6983  df-om 7399  df-1st 7503  df-2nd 7504  df-wrecs 7752  df-recs 7814  df-rdg 7852  df-1o 7907  df-er 8091  df-map 8210  df-pm 8211  df-en 8309  df-dom 8310  df-sdom 8311  df-fin 8312  df-sup 8703  df-inf 8704  df-pnf 10478  df-mnf 10479  df-xr 10480  df-ltxr 10481  df-le 10482  df-sub 10674  df-neg 10675  df-div 11101  df-nn 11442  df-2 11506  df-3 11507  df-n0 11711  df-z 11797  df-uz 12062  df-q 12166  df-rp 12208  df-xneg 12327  df-xadd 12328  df-xmul 12329  df-ico 12563  df-icc 12564  df-fl 12980  df-seq 13188  df-exp 13248  df-rest 16555  df-topgen 16576  df-psmet 20242  df-xmet 20243  df-met 20244  df-bl 20245  df-mopn 20246  df-fbas 20247  df-fg 20248  df-top 21209  df-topon 21226  df-bases 21261  df-cld 21334  df-ntr 21335  df-cls 21336  df-nei 21413  df-lm 21544  df-haus 21630  df-fil 22161  df-fm 22253  df-flim 22254  df-flf 22255  df-cfil 23564  df-cau 23565  df-cmet 23566

This theorem is referenced by:  heiborlem10  34540