Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cmetcaulem Structured version   Visualization version   GIF version

Theorem cmetcaulem 23305
 Description: Lemma for cmetcau 23306. (Contributed by Mario Carneiro, 14-Oct-2015.)
Hypotheses
Ref Expression
cmetcau.1 𝐽 = (MetOpen‘𝐷)
cmetcau.3 (𝜑𝐷 ∈ (CMet‘𝑋))
cmetcau.4 (𝜑𝑃𝑋)
cmetcau.5 (𝜑𝐹 ∈ (Cau‘𝐷))
cmetcau.6 𝐺 = (𝑥 ∈ ℕ ↦ if(𝑥 ∈ dom 𝐹, (𝐹𝑥), 𝑃))
Assertion
Ref Expression
cmetcaulem (𝜑𝐹 ∈ dom (⇝𝑡𝐽))
Distinct variable groups:   𝑥,𝐷   𝑥,𝐹   𝑥,𝑃   𝑥,𝐽   𝜑,𝑥   𝑥,𝑋
Allowed substitution hint:   𝐺(𝑥)

Proof of Theorem cmetcaulem
Dummy variables 𝑗 𝑘 𝑚 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cmetcau.3 . . . . . . . . 9 (𝜑𝐷 ∈ (CMet‘𝑋))
2 cmetmet 23303 . . . . . . . . 9 (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
31, 2syl 17 . . . . . . . 8 (𝜑𝐷 ∈ (Met‘𝑋))
4 metxmet 22359 . . . . . . . 8 (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
53, 4syl 17 . . . . . . 7 (𝜑𝐷 ∈ (∞Met‘𝑋))
6 cmetcau.1 . . . . . . . 8 𝐽 = (MetOpen‘𝐷)
76mopntopon 22464 . . . . . . 7 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋))
85, 7syl 17 . . . . . 6 (𝜑𝐽 ∈ (TopOn‘𝑋))
9 1z 11614 . . . . . . . 8 1 ∈ ℤ
10 nnuz 11930 . . . . . . . . 9 ℕ = (ℤ‘1)
1110uzfbas 21922 . . . . . . . 8 (1 ∈ ℤ → (ℤ “ ℕ) ∈ (fBas‘ℕ))
129, 11mp1i 13 . . . . . . 7 (𝜑 → (ℤ “ ℕ) ∈ (fBas‘ℕ))
13 fgcl 21902 . . . . . . 7 ((ℤ “ ℕ) ∈ (fBas‘ℕ) → (ℕfilGen(ℤ “ ℕ)) ∈ (Fil‘ℕ))
1412, 13syl 17 . . . . . 6 (𝜑 → (ℕfilGen(ℤ “ ℕ)) ∈ (Fil‘ℕ))
15 elfvdm 6363 . . . . . . . . . . . 12 (𝐷 ∈ (CMet‘𝑋) → 𝑋 ∈ dom CMet)
161, 15syl 17 . . . . . . . . . . 11 (𝜑𝑋 ∈ dom CMet)
17 cnex 10223 . . . . . . . . . . . 12 ℂ ∈ V
1817a1i 11 . . . . . . . . . . 11 (𝜑 → ℂ ∈ V)
19 cmetcau.5 . . . . . . . . . . . 12 (𝜑𝐹 ∈ (Cau‘𝐷))
20 caufpm 23299 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘𝐷)) → 𝐹 ∈ (𝑋pm ℂ))
215, 19, 20syl2anc 573 . . . . . . . . . . 11 (𝜑𝐹 ∈ (𝑋pm ℂ))
22 elpm2g 8030 . . . . . . . . . . . 12 ((𝑋 ∈ dom CMet ∧ ℂ ∈ V) → (𝐹 ∈ (𝑋pm ℂ) ↔ (𝐹:dom 𝐹𝑋 ∧ dom 𝐹 ⊆ ℂ)))
2322simprbda 486 . . . . . . . . . . 11 (((𝑋 ∈ dom CMet ∧ ℂ ∈ V) ∧ 𝐹 ∈ (𝑋pm ℂ)) → 𝐹:dom 𝐹𝑋)
2416, 18, 21, 23syl21anc 1475 . . . . . . . . . 10 (𝜑𝐹:dom 𝐹𝑋)
2524adantr 466 . . . . . . . . 9 ((𝜑𝑥 ∈ ℕ) → 𝐹:dom 𝐹𝑋)
2625ffvelrnda 6504 . . . . . . . 8 (((𝜑𝑥 ∈ ℕ) ∧ 𝑥 ∈ dom 𝐹) → (𝐹𝑥) ∈ 𝑋)
27 cmetcau.4 . . . . . . . . 9 (𝜑𝑃𝑋)
2827ad2antrr 705 . . . . . . . 8 (((𝜑𝑥 ∈ ℕ) ∧ ¬ 𝑥 ∈ dom 𝐹) → 𝑃𝑋)
2926, 28ifclda 4260 . . . . . . 7 ((𝜑𝑥 ∈ ℕ) → if(𝑥 ∈ dom 𝐹, (𝐹𝑥), 𝑃) ∈ 𝑋)
30 cmetcau.6 . . . . . . 7 𝐺 = (𝑥 ∈ ℕ ↦ if(𝑥 ∈ dom 𝐹, (𝐹𝑥), 𝑃))
3129, 30fmptd 6529 . . . . . 6 (𝜑𝐺:ℕ⟶𝑋)
32 flfval 22014 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ (ℕfilGen(ℤ “ ℕ)) ∈ (Fil‘ℕ) ∧ 𝐺:ℕ⟶𝑋) → ((𝐽 fLimf (ℕfilGen(ℤ “ ℕ)))‘𝐺) = (𝐽 fLim ((𝑋 FilMap 𝐺)‘(ℕfilGen(ℤ “ ℕ)))))
338, 14, 31, 32syl3anc 1476 . . . . 5 (𝜑 → ((𝐽 fLimf (ℕfilGen(ℤ “ ℕ)))‘𝐺) = (𝐽 fLim ((𝑋 FilMap 𝐺)‘(ℕfilGen(ℤ “ ℕ)))))
34 eqid 2771 . . . . . . . 8 (ℕfilGen(ℤ “ ℕ)) = (ℕfilGen(ℤ “ ℕ))
3534fmfg 21973 . . . . . . 7 ((𝑋 ∈ dom CMet ∧ (ℤ “ ℕ) ∈ (fBas‘ℕ) ∧ 𝐺:ℕ⟶𝑋) → ((𝑋 FilMap 𝐺)‘(ℤ “ ℕ)) = ((𝑋 FilMap 𝐺)‘(ℕfilGen(ℤ “ ℕ))))
3616, 12, 31, 35syl3anc 1476 . . . . . 6 (𝜑 → ((𝑋 FilMap 𝐺)‘(ℤ “ ℕ)) = ((𝑋 FilMap 𝐺)‘(ℕfilGen(ℤ “ ℕ))))
3736oveq2d 6812 . . . . 5 (𝜑 → (𝐽 fLim ((𝑋 FilMap 𝐺)‘(ℤ “ ℕ))) = (𝐽 fLim ((𝑋 FilMap 𝐺)‘(ℕfilGen(ℤ “ ℕ)))))
3833, 37eqtr4d 2808 . . . 4 (𝜑 → ((𝐽 fLimf (ℕfilGen(ℤ “ ℕ)))‘𝐺) = (𝐽 fLim ((𝑋 FilMap 𝐺)‘(ℤ “ ℕ))))
39 biidd 252 . . . . . . . 8 (𝑧 = 1 → (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹 ↔ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹))
40 1zzd 11615 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℤ)
4110, 5, 40iscau3 23295 . . . . . . . . . . 11 (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋pm ℂ) ∧ ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑤 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑤)) < 𝑧))))
4241simplbda 487 . . . . . . . . . 10 ((𝜑𝐹 ∈ (Cau‘𝐷)) → ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑤 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑤)) < 𝑧))
4319, 42mpdan 667 . . . . . . . . 9 (𝜑 → ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑤 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑤)) < 𝑧))
44 simp1 1130 . . . . . . . . . . . 12 ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑤 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑤)) < 𝑧) → 𝑘 ∈ dom 𝐹)
4544ralimi 3101 . . . . . . . . . . 11 (∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑤 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑤)) < 𝑧) → ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹)
4645reximi 3159 . . . . . . . . . 10 (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑤 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑤)) < 𝑧) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹)
4746ralimi 3101 . . . . . . . . 9 (∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑤 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑤)) < 𝑧) → ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹)
4843, 47syl 17 . . . . . . . 8 (𝜑 → ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹)
49 1rp 12039 . . . . . . . . 9 1 ∈ ℝ+
5049a1i 11 . . . . . . . 8 (𝜑 → 1 ∈ ℝ+)
5139, 48, 50rspcdva 3466 . . . . . . 7 (𝜑 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹)
52 dfss3 3741 . . . . . . . . 9 ((ℤ𝑗) ⊆ dom 𝐹 ↔ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹)
53 nnsscn 11231 . . . . . . . . . . . . . 14 ℕ ⊆ ℂ
5431, 53jctir 510 . . . . . . . . . . . . 13 (𝜑 → (𝐺:ℕ⟶𝑋 ∧ ℕ ⊆ ℂ))
55 elpm2r 8031 . . . . . . . . . . . . 13 (((𝑋 ∈ dom CMet ∧ ℂ ∈ V) ∧ (𝐺:ℕ⟶𝑋 ∧ ℕ ⊆ ℂ)) → 𝐺 ∈ (𝑋pm ℂ))
5616, 18, 54, 55syl21anc 1475 . . . . . . . . . . . 12 (𝜑𝐺 ∈ (𝑋pm ℂ))
5756adantr 466 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → 𝐺 ∈ (𝑋pm ℂ))
58 eqid 2771 . . . . . . . . . . . . . . 15 (ℤ𝑗) = (ℤ𝑗)
595adantr 466 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → 𝐷 ∈ (∞Met‘𝑋))
60 nnz 11606 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ → 𝑗 ∈ ℤ)
6160ad2antrl 707 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → 𝑗 ∈ ℤ)
62 eqidd 2772 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) = (𝐹𝑘))
63 eqidd 2772 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑚 ∈ (ℤ𝑗)) → (𝐹𝑚) = (𝐹𝑚))
6458, 59, 61, 62, 63iscau4 23296 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋pm ℂ) ∧ ∀𝑧 ∈ ℝ+𝑚 ∈ (ℤ𝑗)∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧))))
6564simplbda 487 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝐹 ∈ (Cau‘𝐷)) → ∀𝑧 ∈ ℝ+𝑚 ∈ (ℤ𝑗)∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧))
6619, 65mpidan 669 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → ∀𝑧 ∈ ℝ+𝑚 ∈ (ℤ𝑗)∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧))
67 simprl 754 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → 𝑗 ∈ ℕ)
68 eluznn 11966 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ℕ ∧ 𝑚 ∈ (ℤ𝑗)) → 𝑚 ∈ ℕ)
6967, 68sylan 569 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑚 ∈ (ℤ𝑗)) → 𝑚 ∈ ℕ)
70 eluznn 11966 . . . . . . . . . . . . . . . . . 18 ((𝑚 ∈ ℕ ∧ 𝑘 ∈ (ℤ𝑚)) → 𝑘 ∈ ℕ)
7130, 29dmmptd 6163 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → dom 𝐺 = ℕ)
7271adantr 466 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → dom 𝐺 = ℕ)
7372eleq2d 2836 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → (𝑘 ∈ dom 𝐺𝑘 ∈ ℕ))
7473biimpar 463 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ dom 𝐺)
7574a1d 25 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑘 ∈ ℕ) → (𝑘 ∈ dom 𝐹𝑘 ∈ dom 𝐺))
76 idd 24 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑘 ∈ ℕ) → ((𝐹𝑘) ∈ 𝑋 → (𝐹𝑘) ∈ 𝑋))
77 idd 24 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑘 ∈ ℕ) → (((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧 → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧))
7875, 76, 773anim123d 1554 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑘 ∈ ℕ) → ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧) → (𝑘 ∈ dom 𝐺 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧)))
7970, 78sylan2 580 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ (𝑚 ∈ ℕ ∧ 𝑘 ∈ (ℤ𝑚))) → ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧) → (𝑘 ∈ dom 𝐺 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧)))
8079anassrs 453 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑚)) → ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧) → (𝑘 ∈ dom 𝐺 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧)))
8180ralimdva 3111 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑚 ∈ ℕ) → (∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧) → ∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐺 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧)))
8269, 81syldan 579 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑚 ∈ (ℤ𝑗)) → (∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧) → ∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐺 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧)))
8382reximdva 3165 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → (∃𝑚 ∈ (ℤ𝑗)∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧) → ∃𝑚 ∈ (ℤ𝑗)∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐺 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧)))
8483ralimdv 3112 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → (∀𝑧 ∈ ℝ+𝑚 ∈ (ℤ𝑗)∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧) → ∀𝑧 ∈ ℝ+𝑚 ∈ (ℤ𝑗)∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐺 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧)))
8566, 84mpd 15 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → ∀𝑧 ∈ ℝ+𝑚 ∈ (ℤ𝑗)∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐺 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧))
86 eluznn 11966 . . . . . . . . . . . . . 14 ((𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘 ∈ ℕ)
8767, 86sylan 569 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘 ∈ ℕ)
88 simprr 756 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → (ℤ𝑗) ⊆ dom 𝐹)
8988sselda 3752 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘 ∈ dom 𝐹)
90 iftrue 4232 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ dom 𝐹 → if(𝑘 ∈ dom 𝐹, (𝐹𝑘), 𝑃) = (𝐹𝑘))
9190adantl 467 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑘 ∈ dom 𝐹) → if(𝑘 ∈ dom 𝐹, (𝐹𝑘), 𝑃) = (𝐹𝑘))
92 fvex 6344 . . . . . . . . . . . . . . . 16 (𝐹𝑘) ∈ V
9391, 92syl6eqel 2858 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ 𝑘 ∈ dom 𝐹) → if(𝑘 ∈ dom 𝐹, (𝐹𝑘), 𝑃) ∈ V)
94 eleq1w 2833 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑘 → (𝑥 ∈ dom 𝐹𝑘 ∈ dom 𝐹))
95 fveq2 6333 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑘 → (𝐹𝑥) = (𝐹𝑘))
9694, 95ifbieq1d 4249 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑘 → if(𝑥 ∈ dom 𝐹, (𝐹𝑥), 𝑃) = if(𝑘 ∈ dom 𝐹, (𝐹𝑘), 𝑃))
9796, 30fvmptg 6424 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ if(𝑘 ∈ dom 𝐹, (𝐹𝑘), 𝑃) ∈ V) → (𝐺𝑘) = if(𝑘 ∈ dom 𝐹, (𝐹𝑘), 𝑃))
9893, 97syldan 579 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ 𝑘 ∈ dom 𝐹) → (𝐺𝑘) = if(𝑘 ∈ dom 𝐹, (𝐹𝑘), 𝑃))
9998, 91eqtrd 2805 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ 𝑘 ∈ dom 𝐹) → (𝐺𝑘) = (𝐹𝑘))
10087, 89, 99syl2anc 573 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐺𝑘) = (𝐹𝑘))
10188sselda 3752 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑚 ∈ (ℤ𝑗)) → 𝑚 ∈ dom 𝐹)
10269, 101elind 3949 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑚 ∈ (ℤ𝑗)) → 𝑚 ∈ (ℕ ∩ dom 𝐹))
103 fveq2 6333 . . . . . . . . . . . . . . 15 (𝑘 = 𝑚 → (𝐺𝑘) = (𝐺𝑚))
104 fveq2 6333 . . . . . . . . . . . . . . 15 (𝑘 = 𝑚 → (𝐹𝑘) = (𝐹𝑚))
105103, 104eqeq12d 2786 . . . . . . . . . . . . . 14 (𝑘 = 𝑚 → ((𝐺𝑘) = (𝐹𝑘) ↔ (𝐺𝑚) = (𝐹𝑚)))
106 elin 3947 . . . . . . . . . . . . . . 15 (𝑘 ∈ (ℕ ∩ dom 𝐹) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ∈ dom 𝐹))
107106, 99sylbi 207 . . . . . . . . . . . . . 14 (𝑘 ∈ (ℕ ∩ dom 𝐹) → (𝐺𝑘) = (𝐹𝑘))
108105, 107vtoclga 3423 . . . . . . . . . . . . 13 (𝑚 ∈ (ℕ ∩ dom 𝐹) → (𝐺𝑚) = (𝐹𝑚))
109102, 108syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑚 ∈ (ℤ𝑗)) → (𝐺𝑚) = (𝐹𝑚))
11058, 59, 61, 100, 109iscau4 23296 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → (𝐺 ∈ (Cau‘𝐷) ↔ (𝐺 ∈ (𝑋pm ℂ) ∧ ∀𝑧 ∈ ℝ+𝑚 ∈ (ℤ𝑗)∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐺 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧))))
11157, 85, 110mpbir2and 692 . . . . . . . . . 10 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → 𝐺 ∈ (Cau‘𝐷))
112111expr 444 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((ℤ𝑗) ⊆ dom 𝐹𝐺 ∈ (Cau‘𝐷)))
11352, 112syl5bir 233 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹𝐺 ∈ (Cau‘𝐷)))
114113rexlimdva 3179 . . . . . . 7 (𝜑 → (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹𝐺 ∈ (Cau‘𝐷)))
11551, 114mpd 15 . . . . . 6 (𝜑𝐺 ∈ (Cau‘𝐷))
116 eqid 2771 . . . . . . . 8 ((𝑋 FilMap 𝐺)‘(ℤ “ ℕ)) = ((𝑋 FilMap 𝐺)‘(ℤ “ ℕ))
11710, 116caucfil 23300 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ 1 ∈ ℤ ∧ 𝐺:ℕ⟶𝑋) → (𝐺 ∈ (Cau‘𝐷) ↔ ((𝑋 FilMap 𝐺)‘(ℤ “ ℕ)) ∈ (CauFil‘𝐷)))
1185, 40, 31, 117syl3anc 1476 . . . . . 6 (𝜑 → (𝐺 ∈ (Cau‘𝐷) ↔ ((𝑋 FilMap 𝐺)‘(ℤ “ ℕ)) ∈ (CauFil‘𝐷)))
119115, 118mpbid 222 . . . . 5 (𝜑 → ((𝑋 FilMap 𝐺)‘(ℤ “ ℕ)) ∈ (CauFil‘𝐷))
1206cmetcvg 23302 . . . . 5 ((𝐷 ∈ (CMet‘𝑋) ∧ ((𝑋 FilMap 𝐺)‘(ℤ “ ℕ)) ∈ (CauFil‘𝐷)) → (𝐽 fLim ((𝑋 FilMap 𝐺)‘(ℤ “ ℕ))) ≠ ∅)
1211, 119, 120syl2anc 573 . . . 4 (𝜑 → (𝐽 fLim ((𝑋 FilMap 𝐺)‘(ℤ “ ℕ))) ≠ ∅)
12238, 121eqnetrd 3010 . . 3 (𝜑 → ((𝐽 fLimf (ℕfilGen(ℤ “ ℕ)))‘𝐺) ≠ ∅)
123 n0 4079 . . 3 (((𝐽 fLimf (ℕfilGen(ℤ “ ℕ)))‘𝐺) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ ((𝐽 fLimf (ℕfilGen(ℤ “ ℕ)))‘𝐺))
124122, 123sylib 208 . 2 (𝜑 → ∃𝑦 𝑦 ∈ ((𝐽 fLimf (ℕfilGen(ℤ “ ℕ)))‘𝐺))
12510, 34lmflf 22029 . . . . 5 ((𝐽 ∈ (TopOn‘𝑋) ∧ 1 ∈ ℤ ∧ 𝐺:ℕ⟶𝑋) → (𝐺(⇝𝑡𝐽)𝑦𝑦 ∈ ((𝐽 fLimf (ℕfilGen(ℤ “ ℕ)))‘𝐺)))
1268, 40, 31, 125syl3anc 1476 . . . 4 (𝜑 → (𝐺(⇝𝑡𝐽)𝑦𝑦 ∈ ((𝐽 fLimf (ℕfilGen(ℤ “ ℕ)))‘𝐺)))
12721adantr 466 . . . . . . 7 ((𝜑𝐺(⇝𝑡𝐽)𝑦) → 𝐹 ∈ (𝑋pm ℂ))
128 lmcl 21322 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐺(⇝𝑡𝐽)𝑦) → 𝑦𝑋)
1298, 128sylan 569 . . . . . . 7 ((𝜑𝐺(⇝𝑡𝐽)𝑦) → 𝑦𝑋)
1306, 5, 10, 40lmmbr3 23277 . . . . . . . . . 10 (𝜑 → (𝐺(⇝𝑡𝐽)𝑦 ↔ (𝐺 ∈ (𝑋pm ℂ) ∧ 𝑦𝑋 ∧ ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧))))
131130biimpa 462 . . . . . . . . 9 ((𝜑𝐺(⇝𝑡𝐽)𝑦) → (𝐺 ∈ (𝑋pm ℂ) ∧ 𝑦𝑋 ∧ ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)))
132131simp3d 1138 . . . . . . . 8 ((𝜑𝐺(⇝𝑡𝐽)𝑦) → ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧))
133 r19.26 3212 . . . . . . . . . . 11 (∀𝑧 ∈ ℝ+ (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹 ∧ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)) ↔ (∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹 ∧ ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)))
13410rexanuz2 14297 . . . . . . . . . . . . 13 (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)) ↔ (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹 ∧ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)))
135 simprl 754 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧))) → 𝑘 ∈ dom 𝐹)
13699ad2ant2lr 742 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧))) → (𝐺𝑘) = (𝐹𝑘))
137 simprr2 1274 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧))) → (𝐺𝑘) ∈ 𝑋)
138136, 137eqeltrrd 2851 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧))) → (𝐹𝑘) ∈ 𝑋)
139136oveq1d 6811 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧))) → ((𝐺𝑘)𝐷𝑦) = ((𝐹𝑘)𝐷𝑦))
140 simprr3 1276 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧))) → ((𝐺𝑘)𝐷𝑦) < 𝑧)
141139, 140eqbrtrrd 4811 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧))) → ((𝐹𝑘)𝐷𝑦) < 𝑧)
142135, 138, 1413jca 1122 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧))) → (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧))
143142ex 397 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → ((𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)) → (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧)))
14486, 143sylan2 580 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ𝑗))) → ((𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)) → (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧)))
145144anassrs 453 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)) → (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧)))
146145ralimdva 3111 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → (∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)) → ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧)))
147146reximdva 3165 . . . . . . . . . . . . 13 (𝜑 → (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧)))
148134, 147syl5bir 233 . . . . . . . . . . . 12 (𝜑 → ((∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹 ∧ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧)))
149148ralimdv 3112 . . . . . . . . . . 11 (𝜑 → (∀𝑧 ∈ ℝ+ (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹 ∧ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)) → ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧)))
150133, 149syl5bir 233 . . . . . . . . . 10 (𝜑 → ((∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹 ∧ ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)) → ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧)))
15148, 150mpand 675 . . . . . . . . 9 (𝜑 → (∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧) → ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧)))
152151adantr 466 . . . . . . . 8 ((𝜑𝐺(⇝𝑡𝐽)𝑦) → (∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧) → ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧)))
153132, 152mpd 15 . . . . . . 7 ((𝜑𝐺(⇝𝑡𝐽)𝑦) → ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧))
1545adantr 466 . . . . . . . 8 ((𝜑𝐺(⇝𝑡𝐽)𝑦) → 𝐷 ∈ (∞Met‘𝑋))
155 1zzd 11615 . . . . . . . 8 ((𝜑𝐺(⇝𝑡𝐽)𝑦) → 1 ∈ ℤ)
1566, 154, 10, 155lmmbr3 23277 . . . . . . 7 ((𝜑𝐺(⇝𝑡𝐽)𝑦) → (𝐹(⇝𝑡𝐽)𝑦 ↔ (𝐹 ∈ (𝑋pm ℂ) ∧ 𝑦𝑋 ∧ ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧))))
157127, 129, 153, 156mpbir3and 1427 . . . . . 6 ((𝜑𝐺(⇝𝑡𝐽)𝑦) → 𝐹(⇝𝑡𝐽)𝑦)
158 lmrel 21255 . . . . . . 7 Rel (⇝𝑡𝐽)
159158releldmi 5499 . . . . . 6 (𝐹(⇝𝑡𝐽)𝑦𝐹 ∈ dom (⇝𝑡𝐽))
160157, 159syl 17 . . . . 5 ((𝜑𝐺(⇝𝑡𝐽)𝑦) → 𝐹 ∈ dom (⇝𝑡𝐽))
161160ex 397 . . . 4 (𝜑 → (𝐺(⇝𝑡𝐽)𝑦𝐹 ∈ dom (⇝𝑡𝐽)))
162126, 161sylbird 250 . . 3 (𝜑 → (𝑦 ∈ ((𝐽 fLimf (ℕfilGen(ℤ “ ℕ)))‘𝐺) → 𝐹 ∈ dom (⇝𝑡𝐽)))
163162exlimdv 2013 . 2 (𝜑 → (∃𝑦 𝑦 ∈ ((𝐽 fLimf (ℕfilGen(ℤ “ ℕ)))‘𝐺) → 𝐹 ∈ dom (⇝𝑡𝐽)))
164124, 163mpd 15 1 (𝜑𝐹 ∈ dom (⇝𝑡𝐽))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 382   ∧ w3a 1071   = wceq 1631  ∃wex 1852   ∈ wcel 2145   ≠ wne 2943  ∀wral 3061  ∃wrex 3062  Vcvv 3351   ∩ cin 3722   ⊆ wss 3723  ∅c0 4063  ifcif 4226   class class class wbr 4787   ↦ cmpt 4864  dom cdm 5250   “ cima 5253  ⟶wf 6026  ‘cfv 6030  (class class class)co 6796   ↑pm cpm 8014  ℂcc 10140  1c1 10143   < clt 10280  ℕcn 11226  ℤcz 11584  ℤ≥cuz 11893  ℝ+crp 12035  ∞Metcxmt 19946  Metcme 19947  fBascfbas 19949  filGencfg 19950  MetOpencmopn 19951  TopOnctopon 20935  ⇝𝑡clm 21251  Filcfil 21869   FilMap cfm 21957   fLim cflim 21958   fLimf cflf 21959  CauFilccfil 23269  Caucca 23270  CMetcms 23271 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7100  ax-cnex 10198  ax-resscn 10199  ax-1cn 10200  ax-icn 10201  ax-addcl 10202  ax-addrcl 10203  ax-mulcl 10204  ax-mulrcl 10205  ax-mulcom 10206  ax-addass 10207  ax-mulass 10208  ax-distr 10209  ax-i2m1 10210  ax-1ne0 10211  ax-1rid 10212  ax-rnegex 10213  ax-rrecex 10214  ax-cnre 10215  ax-pre-lttri 10216  ax-pre-lttrn 10217  ax-pre-ltadd 10218  ax-pre-mulgt0 10219  ax-pre-sup 10220 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5822  df-ord 5868  df-on 5869  df-lim 5870  df-suc 5871  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-riota 6757  df-ov 6799  df-oprab 6800  df-mpt2 6801  df-om 7217  df-1st 7319  df-2nd 7320  df-wrecs 7563  df-recs 7625  df-rdg 7663  df-er 7900  df-map 8015  df-pm 8016  df-en 8114  df-dom 8115  df-sdom 8116  df-sup 8508  df-inf 8509  df-pnf 10282  df-mnf 10283  df-xr 10284  df-ltxr 10285  df-le 10286  df-sub 10474  df-neg 10475  df-div 10891  df-nn 11227  df-2 11285  df-n0 11500  df-z 11585  df-uz 11894  df-q 11997  df-rp 12036  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-ico 12386  df-rest 16291  df-topgen 16312  df-psmet 19953  df-xmet 19954  df-met 19955  df-bl 19956  df-mopn 19957  df-fbas 19958  df-fg 19959  df-top 20919  df-topon 20936  df-bases 20971  df-ntr 21045  df-nei 21123  df-lm 21254  df-fil 21870  df-fm 21962  df-flim 21963  df-flf 21964  df-cfil 23272  df-cau 23273  df-cmet 23274 This theorem is referenced by:  cmetcau  23306
 Copyright terms: Public domain W3C validator