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

Theorem cmetcaulem 24524
Description: Lemma for cmetcau 24525. (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 24522 . . . . . . . . 9 (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
31, 2syl 17 . . . . . . . 8 (𝜑𝐷 ∈ (Met‘𝑋))
4 metxmet 23559 . . . . . . . 8 (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
53, 4syl 17 . . . . . . 7 (𝜑𝐷 ∈ (∞Met‘𝑋))
6 cmetcau.1 . . . . . . . 8 𝐽 = (MetOpen‘𝐷)
76mopntopon 23664 . . . . . . 7 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋))
85, 7syl 17 . . . . . 6 (𝜑𝐽 ∈ (TopOn‘𝑋))
9 1z 12423 . . . . . . . 8 1 ∈ ℤ
10 nnuz 12694 . . . . . . . . 9 ℕ = (ℤ‘1)
1110uzfbas 23121 . . . . . . . 8 (1 ∈ ℤ → (ℤ “ ℕ) ∈ (fBas‘ℕ))
129, 11mp1i 13 . . . . . . 7 (𝜑 → (ℤ “ ℕ) ∈ (fBas‘ℕ))
13 fgcl 23101 . . . . . . 7 ((ℤ “ ℕ) ∈ (fBas‘ℕ) → (ℕfilGen(ℤ “ ℕ)) ∈ (Fil‘ℕ))
1412, 13syl 17 . . . . . 6 (𝜑 → (ℕfilGen(ℤ “ ℕ)) ∈ (Fil‘ℕ))
15 elfvdm 6845 . . . . . . . . . . . 12 (𝐷 ∈ (CMet‘𝑋) → 𝑋 ∈ dom CMet)
161, 15syl 17 . . . . . . . . . . 11 (𝜑𝑋 ∈ dom CMet)
17 cnex 11025 . . . . . . . . . . . 12 ℂ ∈ V
1817a1i 11 . . . . . . . . . . 11 (𝜑 → ℂ ∈ V)
19 cmetcau.5 . . . . . . . . . . . 12 (𝜑𝐹 ∈ (Cau‘𝐷))
20 caufpm 24518 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘𝐷)) → 𝐹 ∈ (𝑋pm ℂ))
215, 19, 20syl2anc 584 . . . . . . . . . . 11 (𝜑𝐹 ∈ (𝑋pm ℂ))
22 elpm2g 8680 . . . . . . . . . . . 12 ((𝑋 ∈ dom CMet ∧ ℂ ∈ V) → (𝐹 ∈ (𝑋pm ℂ) ↔ (𝐹:dom 𝐹𝑋 ∧ dom 𝐹 ⊆ ℂ)))
2322simprbda 499 . . . . . . . . . . 11 (((𝑋 ∈ dom CMet ∧ ℂ ∈ V) ∧ 𝐹 ∈ (𝑋pm ℂ)) → 𝐹:dom 𝐹𝑋)
2416, 18, 21, 23syl21anc 835 . . . . . . . . . 10 (𝜑𝐹:dom 𝐹𝑋)
2524adantr 481 . . . . . . . . 9 ((𝜑𝑥 ∈ ℕ) → 𝐹:dom 𝐹𝑋)
2625ffvelcdmda 7000 . . . . . . . 8 (((𝜑𝑥 ∈ ℕ) ∧ 𝑥 ∈ dom 𝐹) → (𝐹𝑥) ∈ 𝑋)
27 cmetcau.4 . . . . . . . . 9 (𝜑𝑃𝑋)
2827ad2antrr 723 . . . . . . . 8 (((𝜑𝑥 ∈ ℕ) ∧ ¬ 𝑥 ∈ dom 𝐹) → 𝑃𝑋)
2926, 28ifclda 4506 . . . . . . 7 ((𝜑𝑥 ∈ ℕ) → if(𝑥 ∈ dom 𝐹, (𝐹𝑥), 𝑃) ∈ 𝑋)
30 cmetcau.6 . . . . . . 7 𝐺 = (𝑥 ∈ ℕ ↦ if(𝑥 ∈ dom 𝐹, (𝐹𝑥), 𝑃))
3129, 30fmptd 7027 . . . . . 6 (𝜑𝐺:ℕ⟶𝑋)
32 flfval 23213 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ (ℕfilGen(ℤ “ ℕ)) ∈ (Fil‘ℕ) ∧ 𝐺:ℕ⟶𝑋) → ((𝐽 fLimf (ℕfilGen(ℤ “ ℕ)))‘𝐺) = (𝐽 fLim ((𝑋 FilMap 𝐺)‘(ℕfilGen(ℤ “ ℕ)))))
338, 14, 31, 32syl3anc 1370 . . . . 5 (𝜑 → ((𝐽 fLimf (ℕfilGen(ℤ “ ℕ)))‘𝐺) = (𝐽 fLim ((𝑋 FilMap 𝐺)‘(ℕfilGen(ℤ “ ℕ)))))
34 eqid 2737 . . . . . . . 8 (ℕfilGen(ℤ “ ℕ)) = (ℕfilGen(ℤ “ ℕ))
3534fmfg 23172 . . . . . . 7 ((𝑋 ∈ dom CMet ∧ (ℤ “ ℕ) ∈ (fBas‘ℕ) ∧ 𝐺:ℕ⟶𝑋) → ((𝑋 FilMap 𝐺)‘(ℤ “ ℕ)) = ((𝑋 FilMap 𝐺)‘(ℕfilGen(ℤ “ ℕ))))
3616, 12, 31, 35syl3anc 1370 . . . . . 6 (𝜑 → ((𝑋 FilMap 𝐺)‘(ℤ “ ℕ)) = ((𝑋 FilMap 𝐺)‘(ℕfilGen(ℤ “ ℕ))))
3736oveq2d 7331 . . . . 5 (𝜑 → (𝐽 fLim ((𝑋 FilMap 𝐺)‘(ℤ “ ℕ))) = (𝐽 fLim ((𝑋 FilMap 𝐺)‘(ℕfilGen(ℤ “ ℕ)))))
3833, 37eqtr4d 2780 . . . 4 (𝜑 → ((𝐽 fLimf (ℕfilGen(ℤ “ ℕ)))‘𝐺) = (𝐽 fLim ((𝑋 FilMap 𝐺)‘(ℤ “ ℕ))))
39 biidd 261 . . . . . . . 8 (𝑧 = 1 → (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹 ↔ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹))
40 1zzd 12424 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℤ)
4110, 5, 40iscau3 24514 . . . . . . . . . . 11 (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋pm ℂ) ∧ ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑤 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑤)) < 𝑧))))
4241simplbda 500 . . . . . . . . . 10 ((𝜑𝐹 ∈ (Cau‘𝐷)) → ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑤 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑤)) < 𝑧))
4319, 42mpdan 684 . . . . . . . . 9 (𝜑 → ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑤 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑤)) < 𝑧))
44 simp1 1135 . . . . . . . . . . . 12 ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑤 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑤)) < 𝑧) → 𝑘 ∈ dom 𝐹)
4544ralimi 3083 . . . . . . . . . . 11 (∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑤 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑤)) < 𝑧) → ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹)
4645reximi 3084 . . . . . . . . . 10 (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑤 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑤)) < 𝑧) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹)
4746ralimi 3083 . . . . . . . . 9 (∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑤 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑤)) < 𝑧) → ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹)
4843, 47syl 17 . . . . . . . 8 (𝜑 → ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹)
49 1rp 12807 . . . . . . . . 9 1 ∈ ℝ+
5049a1i 11 . . . . . . . 8 (𝜑 → 1 ∈ ℝ+)
5139, 48, 50rspcdva 3571 . . . . . . 7 (𝜑 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹)
52 dfss3 3919 . . . . . . . . 9 ((ℤ𝑗) ⊆ dom 𝐹 ↔ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹)
53 nnsscn 12051 . . . . . . . . . . . . . 14 ℕ ⊆ ℂ
5431, 53jctir 521 . . . . . . . . . . . . 13 (𝜑 → (𝐺:ℕ⟶𝑋 ∧ ℕ ⊆ ℂ))
55 elpm2r 8681 . . . . . . . . . . . . 13 (((𝑋 ∈ dom CMet ∧ ℂ ∈ V) ∧ (𝐺:ℕ⟶𝑋 ∧ ℕ ⊆ ℂ)) → 𝐺 ∈ (𝑋pm ℂ))
5616, 18, 54, 55syl21anc 835 . . . . . . . . . . . 12 (𝜑𝐺 ∈ (𝑋pm ℂ))
5756adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → 𝐺 ∈ (𝑋pm ℂ))
58 eqid 2737 . . . . . . . . . . . . . . 15 (ℤ𝑗) = (ℤ𝑗)
595adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → 𝐷 ∈ (∞Met‘𝑋))
60 nnz 12415 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ → 𝑗 ∈ ℤ)
6160ad2antrl 725 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → 𝑗 ∈ ℤ)
62 eqidd 2738 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) = (𝐹𝑘))
63 eqidd 2738 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑚 ∈ (ℤ𝑗)) → (𝐹𝑚) = (𝐹𝑚))
6458, 59, 61, 62, 63iscau4 24515 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋pm ℂ) ∧ ∀𝑧 ∈ ℝ+𝑚 ∈ (ℤ𝑗)∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧))))
6564simplbda 500 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝐹 ∈ (Cau‘𝐷)) → ∀𝑧 ∈ ℝ+𝑚 ∈ (ℤ𝑗)∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧))
6619, 65mpidan 686 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → ∀𝑧 ∈ ℝ+𝑚 ∈ (ℤ𝑗)∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧))
67 simprl 768 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → 𝑗 ∈ ℕ)
68 eluznn 12731 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ℕ ∧ 𝑚 ∈ (ℤ𝑗)) → 𝑚 ∈ ℕ)
6967, 68sylan 580 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑚 ∈ (ℤ𝑗)) → 𝑚 ∈ ℕ)
70 eluznn 12731 . . . . . . . . . . . . . . . . . 18 ((𝑚 ∈ ℕ ∧ 𝑘 ∈ (ℤ𝑚)) → 𝑘 ∈ ℕ)
7130, 29dmmptd 6615 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → dom 𝐺 = ℕ)
7271adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → dom 𝐺 = ℕ)
7372eleq2d 2823 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → (𝑘 ∈ dom 𝐺𝑘 ∈ ℕ))
7473biimpar 478 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ dom 𝐺)
7574a1d 25 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑘 ∈ ℕ) → (𝑘 ∈ dom 𝐹𝑘 ∈ dom 𝐺))
76 idd 24 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑘 ∈ ℕ) → ((𝐹𝑘) ∈ 𝑋 → (𝐹𝑘) ∈ 𝑋))
77 idd 24 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑘 ∈ ℕ) → (((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧 → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧))
7875, 76, 773anim123d 1442 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑘 ∈ ℕ) → ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧) → (𝑘 ∈ dom 𝐺 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧)))
7970, 78sylan2 593 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ (𝑚 ∈ ℕ ∧ 𝑘 ∈ (ℤ𝑚))) → ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧) → (𝑘 ∈ dom 𝐺 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧)))
8079anassrs 468 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑚)) → ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧) → (𝑘 ∈ dom 𝐺 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧)))
8180ralimdva 3161 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑚 ∈ ℕ) → (∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧) → ∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐺 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧)))
8269, 81syldan 591 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑚 ∈ (ℤ𝑗)) → (∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧) → ∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐺 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧)))
8382reximdva 3162 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → (∃𝑚 ∈ (ℤ𝑗)∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧) → ∃𝑚 ∈ (ℤ𝑗)∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐺 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧)))
8483ralimdv 3163 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → (∀𝑧 ∈ ℝ+𝑚 ∈ (ℤ𝑗)∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧) → ∀𝑧 ∈ ℝ+𝑚 ∈ (ℤ𝑗)∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐺 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧)))
8566, 84mpd 15 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → ∀𝑧 ∈ ℝ+𝑚 ∈ (ℤ𝑗)∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐺 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧))
86 eluznn 12731 . . . . . . . . . . . . . 14 ((𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘 ∈ ℕ)
8767, 86sylan 580 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘 ∈ ℕ)
88 simprr 770 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → (ℤ𝑗) ⊆ dom 𝐹)
8988sselda 3931 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘 ∈ dom 𝐹)
90 iftrue 4477 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ dom 𝐹 → if(𝑘 ∈ dom 𝐹, (𝐹𝑘), 𝑃) = (𝐹𝑘))
9190adantl 482 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑘 ∈ dom 𝐹) → if(𝑘 ∈ dom 𝐹, (𝐹𝑘), 𝑃) = (𝐹𝑘))
92 fvex 6824 . . . . . . . . . . . . . . . 16 (𝐹𝑘) ∈ V
9391, 92eqeltrdi 2846 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ 𝑘 ∈ dom 𝐹) → if(𝑘 ∈ dom 𝐹, (𝐹𝑘), 𝑃) ∈ V)
94 eleq1w 2820 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑘 → (𝑥 ∈ dom 𝐹𝑘 ∈ dom 𝐹))
95 fveq2 6811 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑘 → (𝐹𝑥) = (𝐹𝑘))
9694, 95ifbieq1d 4495 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑘 → if(𝑥 ∈ dom 𝐹, (𝐹𝑥), 𝑃) = if(𝑘 ∈ dom 𝐹, (𝐹𝑘), 𝑃))
9796, 30fvmptg 6912 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ ∧ if(𝑘 ∈ dom 𝐹, (𝐹𝑘), 𝑃) ∈ V) → (𝐺𝑘) = if(𝑘 ∈ dom 𝐹, (𝐹𝑘), 𝑃))
9893, 97syldan 591 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ ∧ 𝑘 ∈ dom 𝐹) → (𝐺𝑘) = if(𝑘 ∈ dom 𝐹, (𝐹𝑘), 𝑃))
9998, 91eqtrd 2777 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ 𝑘 ∈ dom 𝐹) → (𝐺𝑘) = (𝐹𝑘))
10087, 89, 99syl2anc 584 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐺𝑘) = (𝐹𝑘))
10188sselda 3931 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑚 ∈ (ℤ𝑗)) → 𝑚 ∈ dom 𝐹)
10269, 101elind 4139 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑚 ∈ (ℤ𝑗)) → 𝑚 ∈ (ℕ ∩ dom 𝐹))
103 fveq2 6811 . . . . . . . . . . . . . . 15 (𝑘 = 𝑚 → (𝐺𝑘) = (𝐺𝑚))
104 fveq2 6811 . . . . . . . . . . . . . . 15 (𝑘 = 𝑚 → (𝐹𝑘) = (𝐹𝑚))
105103, 104eqeq12d 2753 . . . . . . . . . . . . . 14 (𝑘 = 𝑚 → ((𝐺𝑘) = (𝐹𝑘) ↔ (𝐺𝑚) = (𝐹𝑚)))
106 elin 3913 . . . . . . . . . . . . . . 15 (𝑘 ∈ (ℕ ∩ dom 𝐹) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ∈ dom 𝐹))
107106, 99sylbi 216 . . . . . . . . . . . . . 14 (𝑘 ∈ (ℕ ∩ dom 𝐹) → (𝐺𝑘) = (𝐹𝑘))
108105, 107vtoclga 3522 . . . . . . . . . . . . 13 (𝑚 ∈ (ℕ ∩ dom 𝐹) → (𝐺𝑚) = (𝐹𝑚))
109102, 108syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) ∧ 𝑚 ∈ (ℤ𝑗)) → (𝐺𝑚) = (𝐹𝑚))
11058, 59, 61, 100, 109iscau4 24515 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → (𝐺 ∈ (Cau‘𝐷) ↔ (𝐺 ∈ (𝑋pm ℂ) ∧ ∀𝑧 ∈ ℝ+𝑚 ∈ (ℤ𝑗)∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐺 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑧))))
11157, 85, 110mpbir2and 710 . . . . . . . . . 10 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ (ℤ𝑗) ⊆ dom 𝐹)) → 𝐺 ∈ (Cau‘𝐷))
112111expr 457 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((ℤ𝑗) ⊆ dom 𝐹𝐺 ∈ (Cau‘𝐷)))
11352, 112syl5bir 242 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹𝐺 ∈ (Cau‘𝐷)))
114113rexlimdva 3149 . . . . . . 7 (𝜑 → (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹𝐺 ∈ (Cau‘𝐷)))
11551, 114mpd 15 . . . . . 6 (𝜑𝐺 ∈ (Cau‘𝐷))
116 eqid 2737 . . . . . . . 8 ((𝑋 FilMap 𝐺)‘(ℤ “ ℕ)) = ((𝑋 FilMap 𝐺)‘(ℤ “ ℕ))
11710, 116caucfil 24519 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ 1 ∈ ℤ ∧ 𝐺:ℕ⟶𝑋) → (𝐺 ∈ (Cau‘𝐷) ↔ ((𝑋 FilMap 𝐺)‘(ℤ “ ℕ)) ∈ (CauFil‘𝐷)))
1185, 40, 31, 117syl3anc 1370 . . . . . 6 (𝜑 → (𝐺 ∈ (Cau‘𝐷) ↔ ((𝑋 FilMap 𝐺)‘(ℤ “ ℕ)) ∈ (CauFil‘𝐷)))
119115, 118mpbid 231 . . . . 5 (𝜑 → ((𝑋 FilMap 𝐺)‘(ℤ “ ℕ)) ∈ (CauFil‘𝐷))
1206cmetcvg 24521 . . . . 5 ((𝐷 ∈ (CMet‘𝑋) ∧ ((𝑋 FilMap 𝐺)‘(ℤ “ ℕ)) ∈ (CauFil‘𝐷)) → (𝐽 fLim ((𝑋 FilMap 𝐺)‘(ℤ “ ℕ))) ≠ ∅)
1211, 119, 120syl2anc 584 . . . 4 (𝜑 → (𝐽 fLim ((𝑋 FilMap 𝐺)‘(ℤ “ ℕ))) ≠ ∅)
12238, 121eqnetrd 3009 . . 3 (𝜑 → ((𝐽 fLimf (ℕfilGen(ℤ “ ℕ)))‘𝐺) ≠ ∅)
123 n0 4291 . . 3 (((𝐽 fLimf (ℕfilGen(ℤ “ ℕ)))‘𝐺) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ ((𝐽 fLimf (ℕfilGen(ℤ “ ℕ)))‘𝐺))
124122, 123sylib 217 . 2 (𝜑 → ∃𝑦 𝑦 ∈ ((𝐽 fLimf (ℕfilGen(ℤ “ ℕ)))‘𝐺))
12510, 34lmflf 23228 . . . . 5 ((𝐽 ∈ (TopOn‘𝑋) ∧ 1 ∈ ℤ ∧ 𝐺:ℕ⟶𝑋) → (𝐺(⇝𝑡𝐽)𝑦𝑦 ∈ ((𝐽 fLimf (ℕfilGen(ℤ “ ℕ)))‘𝐺)))
1268, 40, 31, 125syl3anc 1370 . . . 4 (𝜑 → (𝐺(⇝𝑡𝐽)𝑦𝑦 ∈ ((𝐽 fLimf (ℕfilGen(ℤ “ ℕ)))‘𝐺)))
12721adantr 481 . . . . . . 7 ((𝜑𝐺(⇝𝑡𝐽)𝑦) → 𝐹 ∈ (𝑋pm ℂ))
128 lmcl 22520 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐺(⇝𝑡𝐽)𝑦) → 𝑦𝑋)
1298, 128sylan 580 . . . . . . 7 ((𝜑𝐺(⇝𝑡𝐽)𝑦) → 𝑦𝑋)
1306, 5, 10, 40lmmbr3 24496 . . . . . . . . . 10 (𝜑 → (𝐺(⇝𝑡𝐽)𝑦 ↔ (𝐺 ∈ (𝑋pm ℂ) ∧ 𝑦𝑋 ∧ ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧))))
131130biimpa 477 . . . . . . . . 9 ((𝜑𝐺(⇝𝑡𝐽)𝑦) → (𝐺 ∈ (𝑋pm ℂ) ∧ 𝑦𝑋 ∧ ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)))
132131simp3d 1143 . . . . . . . 8 ((𝜑𝐺(⇝𝑡𝐽)𝑦) → ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧))
133 r19.26 3111 . . . . . . . . . . 11 (∀𝑧 ∈ ℝ+ (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹 ∧ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)) ↔ (∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹 ∧ ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)))
13410rexanuz2 15133 . . . . . . . . . . . . 13 (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)) ↔ (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹 ∧ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)))
135 simprl 768 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧))) → 𝑘 ∈ dom 𝐹)
13699ad2ant2lr 745 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧))) → (𝐺𝑘) = (𝐹𝑘))
137 simprr2 1221 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧))) → (𝐺𝑘) ∈ 𝑋)
138136, 137eqeltrrd 2839 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧))) → (𝐹𝑘) ∈ 𝑋)
139136oveq1d 7330 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧))) → ((𝐺𝑘)𝐷𝑦) = ((𝐹𝑘)𝐷𝑦))
140 simprr3 1222 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧))) → ((𝐺𝑘)𝐷𝑦) < 𝑧)
141139, 140eqbrtrrd 5111 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧))) → ((𝐹𝑘)𝐷𝑦) < 𝑧)
142135, 138, 1413jca 1127 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ℕ) ∧ (𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧))) → (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧))
143142ex 413 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → ((𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)) → (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧)))
14486, 143sylan2 593 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ𝑗))) → ((𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)) → (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧)))
145144anassrs 468 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)) → (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧)))
146145ralimdva 3161 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → (∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)) → ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧)))
147146reximdva 3162 . . . . . . . . . . . . 13 (𝜑 → (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧)))
148134, 147syl5bir 242 . . . . . . . . . . . 12 (𝜑 → ((∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹 ∧ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧)))
149148ralimdv 3163 . . . . . . . . . . 11 (𝜑 → (∀𝑧 ∈ ℝ+ (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹 ∧ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)) → ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧)))
150133, 149syl5bir 242 . . . . . . . . . 10 (𝜑 → ((∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)𝑘 ∈ dom 𝐹 ∧ ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧)) → ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧)))
15148, 150mpand 692 . . . . . . . . 9 (𝜑 → (∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧) → ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧)))
152151adantr 481 . . . . . . . 8 ((𝜑𝐺(⇝𝑡𝐽)𝑦) → (∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐺 ∧ (𝐺𝑘) ∈ 𝑋 ∧ ((𝐺𝑘)𝐷𝑦) < 𝑧) → ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧)))
153132, 152mpd 15 . . . . . . 7 ((𝜑𝐺(⇝𝑡𝐽)𝑦) → ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧))
1545adantr 481 . . . . . . . 8 ((𝜑𝐺(⇝𝑡𝐽)𝑦) → 𝐷 ∈ (∞Met‘𝑋))
155 1zzd 12424 . . . . . . . 8 ((𝜑𝐺(⇝𝑡𝐽)𝑦) → 1 ∈ ℤ)
1566, 154, 10, 155lmmbr3 24496 . . . . . . 7 ((𝜑𝐺(⇝𝑡𝐽)𝑦) → (𝐹(⇝𝑡𝐽)𝑦 ↔ (𝐹 ∈ (𝑋pm ℂ) ∧ 𝑦𝑋 ∧ ∀𝑧 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ((𝐹𝑘)𝐷𝑦) < 𝑧))))
157127, 129, 153, 156mpbir3and 1341 . . . . . 6 ((𝜑𝐺(⇝𝑡𝐽)𝑦) → 𝐹(⇝𝑡𝐽)𝑦)
158 lmrel 22453 . . . . . . 7 Rel (⇝𝑡𝐽)
159158releldmi 5876 . . . . . 6 (𝐹(⇝𝑡𝐽)𝑦𝐹 ∈ dom (⇝𝑡𝐽))
160157, 159syl 17 . . . . 5 ((𝜑𝐺(⇝𝑡𝐽)𝑦) → 𝐹 ∈ dom (⇝𝑡𝐽))
161160ex 413 . . . 4 (𝜑 → (𝐺(⇝𝑡𝐽)𝑦𝐹 ∈ dom (⇝𝑡𝐽)))
162126, 161sylbird 259 . . 3 (𝜑 → (𝑦 ∈ ((𝐽 fLimf (ℕfilGen(ℤ “ ℕ)))‘𝐺) → 𝐹 ∈ dom (⇝𝑡𝐽)))
163162exlimdv 1935 . 2 (𝜑 → (∃𝑦 𝑦 ∈ ((𝐽 fLimf (ℕfilGen(ℤ “ ℕ)))‘𝐺) → 𝐹 ∈ dom (⇝𝑡𝐽)))
164124, 163mpd 15 1 (𝜑𝐹 ∈ dom (⇝𝑡𝐽))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1086   = wceq 1540  wex 1780  wcel 2105  wne 2941  wral 3062  wrex 3071  Vcvv 3441  cin 3896  wss 3897  c0 4267  ifcif 4471   class class class wbr 5087  cmpt 5170  dom cdm 5607  cima 5610  wf 6461  cfv 6465  (class class class)co 7315  pm cpm 8664  cc 10942  1c1 10945   < clt 11082  cn 12046  cz 12392  cuz 12655  +crp 12803  ∞Metcxmet 20654  Metcmet 20655  fBascfbas 20657  filGencfg 20658  MetOpencmopn 20659  TopOnctopon 22131  𝑡clm 22449  Filcfil 23068   FilMap cfm 23156   fLim cflim 23157   fLimf cflf 23158  CauFilccfil 24488  Cauccau 24489  CMetccmet 24490
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5224  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7628  ax-cnex 11000  ax-resscn 11001  ax-1cn 11002  ax-icn 11003  ax-addcl 11004  ax-addrcl 11005  ax-mulcl 11006  ax-mulrcl 11007  ax-mulcom 11008  ax-addass 11009  ax-mulass 11010  ax-distr 11011  ax-i2m1 11012  ax-1ne0 11013  ax-1rid 11014  ax-rnegex 11015  ax-rrecex 11016  ax-cnre 11017  ax-pre-lttri 11018  ax-pre-lttrn 11019  ax-pre-ltadd 11020  ax-pre-mulgt0 11021  ax-pre-sup 11022
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-iun 4939  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5562  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-riota 7272  df-ov 7318  df-oprab 7319  df-mpo 7320  df-om 7758  df-1st 7876  df-2nd 7877  df-frecs 8144  df-wrecs 8175  df-recs 8249  df-rdg 8288  df-er 8546  df-map 8665  df-pm 8666  df-en 8782  df-dom 8783  df-sdom 8784  df-sup 9271  df-inf 9272  df-pnf 11084  df-mnf 11085  df-xr 11086  df-ltxr 11087  df-le 11088  df-sub 11280  df-neg 11281  df-div 11706  df-nn 12047  df-2 12109  df-n0 12307  df-z 12393  df-uz 12656  df-q 12762  df-rp 12804  df-xneg 12921  df-xadd 12922  df-xmul 12923  df-ico 13158  df-rest 17203  df-topgen 17224  df-psmet 20661  df-xmet 20662  df-met 20663  df-bl 20664  df-mopn 20665  df-fbas 20666  df-fg 20667  df-top 22115  df-topon 22132  df-bases 22168  df-ntr 22243  df-nei 22321  df-lm 22452  df-fil 23069  df-fm 23161  df-flim 23162  df-flf 23163  df-cfil 24491  df-cau 24492  df-cmet 24493
This theorem is referenced by:  cmetcau  24525
  Copyright terms: Public domain W3C validator