Metamath Proof Explorer

Theorem cmetcaulem

Description: Lemma for cmetcau . (Contributed by Mario Carneiro, 14-Oct-2015)

Ref Expression
Hypotheses cmetcau.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
cmetcau.3 ⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
cmetcau.4 ⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
cmetcau.5 ⊢ ( 𝜑 → 𝐹 ∈ ( Cau ‘ 𝐷 ) )
cmetcau.6 ⊢ 𝐺 = ( 𝑥 ∈ ℕ ↦ if ( 𝑥 ∈ dom 𝐹 , ( 𝐹 ‘ 𝑥 ) , 𝑃 ) )
Assertion cmetcaulem ( 𝜑 → 𝐹 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 cmetcau.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 cmetcau.3 ⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
3 cmetcau.4 ⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
4 cmetcau.5 ⊢ ( 𝜑 → 𝐹 ∈ ( Cau ‘ 𝐷 ) )
5 cmetcau.6 ⊢ 𝐺 = ( 𝑥 ∈ ℕ ↦ if ( 𝑥 ∈ dom 𝐹 , ( 𝐹 ‘ 𝑥 ) , 𝑃 ) )
6 cmetmet ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
7 2 6 syl ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
8 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
9 7 8 syl ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
10 1 mopntopon ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
11 9 10 syl ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
12 1z ⊢ 1 ∈ ℤ
13 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
14 13 uzfbas ⊢ ( 1 ∈ ℤ → ( ℤ≥ “ ℕ ) ∈ ( fBas ‘ ℕ ) )
15 12 14 mp1i ⊢ ( 𝜑 → ( ℤ≥ “ ℕ ) ∈ ( fBas ‘ ℕ ) )
16 fgcl ⊢ ( ( ℤ≥ “ ℕ ) ∈ ( fBas ‘ ℕ ) → ( ℕ filGen ( ℤ≥ “ ℕ ) ) ∈ ( Fil ‘ ℕ ) )
17 15 16 syl ⊢ ( 𝜑 → ( ℕ filGen ( ℤ≥ “ ℕ ) ) ∈ ( Fil ‘ ℕ ) )
18 elfvdm ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝑋 ∈ dom CMet )
19 2 18 syl ⊢ ( 𝜑 → 𝑋 ∈ dom CMet )
20 cnex ⊢ ℂ ∈ V
21 20 a1i ⊢ ( 𝜑 → ℂ ∈ V )
22 caufpm ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → 𝐹 ∈ ( 𝑋 ↑pm ℂ ) )
23 9 4 22 syl2anc ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 ↑pm ℂ ) )
24 elpm2g ⊢ ( ( 𝑋 ∈ dom CMet ∧ ℂ ∈ V ) → ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ↔ ( 𝐹 : dom 𝐹 ⟶ 𝑋 ∧ dom 𝐹 ⊆ ℂ ) ) )
25 24 simprbda ⊢ ( ( ( 𝑋 ∈ dom CMet ∧ ℂ ∈ V ) ∧ 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ) → 𝐹 : dom 𝐹 ⟶ 𝑋 )
26 19 21 23 25 syl21anc ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ 𝑋 )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → 𝐹 : dom 𝐹 ⟶ 𝑋 )
28 27 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑋 )
29 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) ∧ ¬ 𝑥 ∈ dom 𝐹 ) → 𝑃 ∈ 𝑋 )
30 28 29 ifclda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → if ( 𝑥 ∈ dom 𝐹 , ( 𝐹 ‘ 𝑥 ) , 𝑃 ) ∈ 𝑋 )
31 30 5 fmptd ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ 𝑋 )
32 flfval ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( ℕ filGen ( ℤ≥ “ ℕ ) ) ∈ ( Fil ‘ ℕ ) ∧ 𝐺 : ℕ ⟶ 𝑋 ) → ( ( 𝐽 fLimf ( ℕ filGen ( ℤ≥ “ ℕ ) ) ) ‘ 𝐺 ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝐺 ) ‘ ( ℕ filGen ( ℤ≥ “ ℕ ) ) ) ) )
33 11 17 31 32 syl3anc ⊢ ( 𝜑 → ( ( 𝐽 fLimf ( ℕ filGen ( ℤ≥ “ ℕ ) ) ) ‘ 𝐺 ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝐺 ) ‘ ( ℕ filGen ( ℤ≥ “ ℕ ) ) ) ) )
34 eqid ⊢ ( ℕ filGen ( ℤ≥ “ ℕ ) ) = ( ℕ filGen ( ℤ≥ “ ℕ ) )
35 34 fmfg ⊢ ( ( 𝑋 ∈ dom CMet ∧ ( ℤ≥ “ ℕ ) ∈ ( fBas ‘ ℕ ) ∧ 𝐺 : ℕ ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐺 ) ‘ ( ℤ≥ “ ℕ ) ) = ( ( 𝑋 FilMap 𝐺 ) ‘ ( ℕ filGen ( ℤ≥ “ ℕ ) ) ) )
36 19 15 31 35 syl3anc ⊢ ( 𝜑 → ( ( 𝑋 FilMap 𝐺 ) ‘ ( ℤ≥ “ ℕ ) ) = ( ( 𝑋 FilMap 𝐺 ) ‘ ( ℕ filGen ( ℤ≥ “ ℕ ) ) ) )
37 36 oveq2d ⊢ ( 𝜑 → ( 𝐽 fLim ( ( 𝑋 FilMap 𝐺 ) ‘ ( ℤ≥ “ ℕ ) ) ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝐺 ) ‘ ( ℕ filGen ( ℤ≥ “ ℕ ) ) ) ) )
38 33 37 eqtr4d ⊢ ( 𝜑 → ( ( 𝐽 fLimf ( ℕ filGen ( ℤ≥ “ ℕ ) ) ) ‘ 𝐺 ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝐺 ) ‘ ( ℤ≥ “ ℕ ) ) ) )
39 biidd ⊢ ( 𝑧 = 1 → ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑘 ∈ dom 𝐹 ↔ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑘 ∈ dom 𝐹 ) )
40 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
41 13 9 40 iscau3 ⊢ ( 𝜑 → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑤 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑧 ) ) ) )
42 41 simplbda ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑤 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑧 ) )
43 4 42 mpdan ⊢ ( 𝜑 → ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑤 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑧 ) )
44 simp1 ⊢ ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑤 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑧 ) → 𝑘 ∈ dom 𝐹 )
45 44 ralimi ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑤 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑧 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑘 ∈ dom 𝐹 )
46 45 reximi ⊢ ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑤 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑧 ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑘 ∈ dom 𝐹 )
47 46 ralimi ⊢ ( ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑤 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑧 ) → ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑘 ∈ dom 𝐹 )
48 43 47 syl ⊢ ( 𝜑 → ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑘 ∈ dom 𝐹 )
49 1rp ⊢ 1 ∈ ℝ+
50 49 a1i ⊢ ( 𝜑 → 1 ∈ ℝ+ )
51 39 48 50 rspcdva ⊢ ( 𝜑 → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑘 ∈ dom 𝐹 )
52 dfss3 ⊢ ( ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑘 ∈ dom 𝐹 )
53 nnsscn ⊢ ℕ ⊆ ℂ
54 31 53 jctir ⊢ ( 𝜑 → ( 𝐺 : ℕ ⟶ 𝑋 ∧ ℕ ⊆ ℂ ) )
55 elpm2r ⊢ ( ( ( 𝑋 ∈ dom CMet ∧ ℂ ∈ V ) ∧ ( 𝐺 : ℕ ⟶ 𝑋 ∧ ℕ ⊆ ℂ ) ) → 𝐺 ∈ ( 𝑋 ↑pm ℂ ) )
56 19 21 54 55 syl21anc ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 ↑pm ℂ ) )
57 56 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) → 𝐺 ∈ ( 𝑋 ↑pm ℂ ) )
58 eqid ⊢ ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ 𝑗 )
59 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
60 nnz ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℤ )
61 60 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) → 𝑗 ∈ ℤ )
62 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
63 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑚 ) )
64 58 59 61 62 63 iscau4 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ) ) ) )
65 64 simplbda ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → ∀ 𝑧 ∈ ℝ+ ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ) )
66 4 65 mpidan ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) → ∀ 𝑧 ∈ ℝ+ ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ) )
67 simprl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) → 𝑗 ∈ ℕ )
68 eluznn ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑚 ∈ ℕ )
69 67 68 sylan ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑚 ∈ ℕ )
70 eluznn ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ) → 𝑘 ∈ ℕ )
71 5 30 dmmptd ⊢ ( 𝜑 → dom 𝐺 = ℕ )
72 71 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) → dom 𝐺 = ℕ )
73 72 eleq2d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) → ( 𝑘 ∈ dom 𝐺 ↔ 𝑘 ∈ ℕ ) )
74 73 biimpar ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ dom 𝐺 )
75 74 a1d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑘 ∈ dom 𝐹 → 𝑘 ∈ dom 𝐺 ) )
76 idd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 → ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) )
77 idd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑧 → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ) )
78 75 76 77 3anim123d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ) → ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ) ) )
79 70 78 sylan2 ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ) ) → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ) → ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ) ) )
80 79 anassrs ⊢ ( ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ) → ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ) ) )
81 80 ralimdva ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) ∧ 𝑚 ∈ ℕ ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ) ) )
82 69 81 syldan ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ) ) )
83 82 reximdva ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) → ( ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ) → ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ) ) )
84 83 ralimdv ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) → ( ∀ 𝑧 ∈ ℝ+ ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ) → ∀ 𝑧 ∈ ℝ+ ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ) ) )
85 66 84 mpd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) → ∀ 𝑧 ∈ ℝ+ ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ) )
86 eluznn ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ ℕ )
87 67 86 sylan ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ ℕ )
88 simprr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) → ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 )
89 88 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ dom 𝐹 )
90 iftrue ⊢ ( 𝑘 ∈ dom 𝐹 → if ( 𝑘 ∈ dom 𝐹 , ( 𝐹 ‘ 𝑘 ) , 𝑃 ) = ( 𝐹 ‘ 𝑘 ) )
91 90 adantl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑘 ∈ dom 𝐹 ) → if ( 𝑘 ∈ dom 𝐹 , ( 𝐹 ‘ 𝑘 ) , 𝑃 ) = ( 𝐹 ‘ 𝑘 ) )
92 fvex ⊢ ( 𝐹 ‘ 𝑘 ) ∈ V
93 91 92 eqeltrdi ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑘 ∈ dom 𝐹 ) → if ( 𝑘 ∈ dom 𝐹 , ( 𝐹 ‘ 𝑘 ) , 𝑃 ) ∈ V )
94 eleq1w ⊢ ( 𝑥 = 𝑘 → ( 𝑥 ∈ dom 𝐹 ↔ 𝑘 ∈ dom 𝐹 ) )
95 fveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑘 ) )
96 94 95 ifbieq1d ⊢ ( 𝑥 = 𝑘 → if ( 𝑥 ∈ dom 𝐹 , ( 𝐹 ‘ 𝑥 ) , 𝑃 ) = if ( 𝑘 ∈ dom 𝐹 , ( 𝐹 ‘ 𝑘 ) , 𝑃 ) )
97 96 5 fvmptg ⊢ ( ( 𝑘 ∈ ℕ ∧ if ( 𝑘 ∈ dom 𝐹 , ( 𝐹 ‘ 𝑘 ) , 𝑃 ) ∈ V ) → ( 𝐺 ‘ 𝑘 ) = if ( 𝑘 ∈ dom 𝐹 , ( 𝐹 ‘ 𝑘 ) , 𝑃 ) )
98 93 97 syldan ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑘 ∈ dom 𝐹 ) → ( 𝐺 ‘ 𝑘 ) = if ( 𝑘 ∈ dom 𝐹 , ( 𝐹 ‘ 𝑘 ) , 𝑃 ) )
99 98 91 eqtrd ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑘 ∈ dom 𝐹 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
100 87 89 99 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
101 88 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑚 ∈ dom 𝐹 )
102 69 101 elind ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑚 ∈ ( ℕ ∩ dom 𝐹 ) )
103 fveq2 ⊢ ( 𝑘 = 𝑚 → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑚 ) )
104 fveq2 ⊢ ( 𝑘 = 𝑚 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) )
105 103 104 eqeq12d ⊢ ( 𝑘 = 𝑚 → ( ( 𝐺 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) ↔ ( 𝐺 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑚 ) ) )
106 elin ⊢ ( 𝑘 ∈ ( ℕ ∩ dom 𝐹 ) ↔ ( 𝑘 ∈ ℕ ∧ 𝑘 ∈ dom 𝐹 ) )
107 106 99 sylbi ⊢ ( 𝑘 ∈ ( ℕ ∩ dom 𝐹 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
108 105 107 vtoclga ⊢ ( 𝑚 ∈ ( ℕ ∩ dom 𝐹 ) → ( 𝐺 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑚 ) )
109 102 108 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐺 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑚 ) )
110 58 59 61 100 109 iscau4 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) → ( 𝐺 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝐺 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑧 ) ) ) )
111 57 85 110 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) ) → 𝐺 ∈ ( Cau ‘ 𝐷 ) )
112 111 expr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 → 𝐺 ∈ ( Cau ‘ 𝐷 ) ) )
113 52 112 syl5bir ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑘 ∈ dom 𝐹 → 𝐺 ∈ ( Cau ‘ 𝐷 ) ) )
114 113 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑘 ∈ dom 𝐹 → 𝐺 ∈ ( Cau ‘ 𝐷 ) ) )
115 51 114 mpd ⊢ ( 𝜑 → 𝐺 ∈ ( Cau ‘ 𝐷 ) )
116 eqid ⊢ ( ( 𝑋 FilMap 𝐺 ) ‘ ( ℤ≥ “ ℕ ) ) = ( ( 𝑋 FilMap 𝐺 ) ‘ ( ℤ≥ “ ℕ ) )
117 13 116 caucfil ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 1 ∈ ℤ ∧ 𝐺 : ℕ ⟶ 𝑋 ) → ( 𝐺 ∈ ( Cau ‘ 𝐷 ) ↔ ( ( 𝑋 FilMap 𝐺 ) ‘ ( ℤ≥ “ ℕ ) ) ∈ ( CauFil ‘ 𝐷 ) ) )
118 9 40 31 117 syl3anc ⊢ ( 𝜑 → ( 𝐺 ∈ ( Cau ‘ 𝐷 ) ↔ ( ( 𝑋 FilMap 𝐺 ) ‘ ( ℤ≥ “ ℕ ) ) ∈ ( CauFil ‘ 𝐷 ) ) )
119 115 118 mpbid ⊢ ( 𝜑 → ( ( 𝑋 FilMap 𝐺 ) ‘ ( ℤ≥ “ ℕ ) ) ∈ ( CauFil ‘ 𝐷 ) )
120 1 cmetcvg ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ ( ( 𝑋 FilMap 𝐺 ) ‘ ( ℤ≥ “ ℕ ) ) ∈ ( CauFil ‘ 𝐷 ) ) → ( 𝐽 fLim ( ( 𝑋 FilMap 𝐺 ) ‘ ( ℤ≥ “ ℕ ) ) ) ≠ ∅ )
121 2 119 120 syl2anc ⊢ ( 𝜑 → ( 𝐽 fLim ( ( 𝑋 FilMap 𝐺 ) ‘ ( ℤ≥ “ ℕ ) ) ) ≠ ∅ )
122 38 121 eqnetrd ⊢ ( 𝜑 → ( ( 𝐽 fLimf ( ℕ filGen ( ℤ≥ “ ℕ ) ) ) ‘ 𝐺 ) ≠ ∅ )
123 n0 ⊢ ( ( ( 𝐽 fLimf ( ℕ filGen ( ℤ≥ “ ℕ ) ) ) ‘ 𝐺 ) ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ ( ( 𝐽 fLimf ( ℕ filGen ( ℤ≥ “ ℕ ) ) ) ‘ 𝐺 ) )
124 122 123 sylib ⊢ ( 𝜑 → ∃ 𝑦 𝑦 ∈ ( ( 𝐽 fLimf ( ℕ filGen ( ℤ≥ “ ℕ ) ) ) ‘ 𝐺 ) )
125 13 34 lmflf ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 1 ∈ ℤ ∧ 𝐺 : ℕ ⟶ 𝑋 ) → ( 𝐺 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ↔ 𝑦 ∈ ( ( 𝐽 fLimf ( ℕ filGen ( ℤ≥ “ ℕ ) ) ) ‘ 𝐺 ) ) )
126 11 40 31 125 syl3anc ⊢ ( 𝜑 → ( 𝐺 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ↔ 𝑦 ∈ ( ( 𝐽 fLimf ( ℕ filGen ( ℤ≥ “ ℕ ) ) ) ‘ 𝐺 ) ) )
127 23 adantr ⊢ ( ( 𝜑 ∧ 𝐺 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ) → 𝐹 ∈ ( 𝑋 ↑pm ℂ ) )
128 lmcl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐺 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ) → 𝑦 ∈ 𝑋 )
129 11 128 sylan ⊢ ( ( 𝜑 ∧ 𝐺 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ) → 𝑦 ∈ 𝑋 )
130 1 9 13 40 lmmbr3 ⊢ ( 𝜑 → ( 𝐺 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ↔ ( 𝐺 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑦 ∈ 𝑋 ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) ) )
131 130 biimpa ⊢ ( ( 𝜑 ∧ 𝐺 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ) → ( 𝐺 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑦 ∈ 𝑋 ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) )
132 131 simp3d ⊢ ( ( 𝜑 ∧ 𝐺 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ) → ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) )
133 r19.26 ⊢ ( ∀ 𝑧 ∈ ℝ+ ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑘 ∈ dom 𝐹 ∧ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) ↔ ( ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑘 ∈ dom 𝐹 ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) )
134 13 rexanuz2 ⊢ ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) ↔ ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑘 ∈ dom 𝐹 ∧ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) )
135 simprl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) ) → 𝑘 ∈ dom 𝐹 )
136 99 ad2ant2lr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
137 simprr2 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) ) → ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 )
138 136 137 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
139 136 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) ) → ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) = ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) )
140 simprr3 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) ) → ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 )
141 139 140 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 )
142 135 138 141 3jca ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) ) → ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) )
143 142 ex ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) → ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) )
144 86 143 sylan2 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) → ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) )
145 144 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) → ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) )
146 145 ralimdva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) )
147 146 reximdva ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) )
148 134 147 syl5bir ⊢ ( 𝜑 → ( ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑘 ∈ dom 𝐹 ∧ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) )
149 148 ralimdv ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ℝ+ ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑘 ∈ dom 𝐹 ∧ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) → ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) )
150 133 149 syl5bir ⊢ ( 𝜑 → ( ( ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑘 ∈ dom 𝐹 ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) → ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) )
151 48 150 mpand ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) → ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) )
152 151 adantr ⊢ ( ( 𝜑 ∧ 𝐺 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ) → ( ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) → ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) )
153 132 152 mpd ⊢ ( ( 𝜑 ∧ 𝐺 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ) → ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) )
154 9 adantr ⊢ ( ( 𝜑 ∧ 𝐺 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
155 1zzd ⊢ ( ( 𝜑 ∧ 𝐺 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ) → 1 ∈ ℤ )
156 1 154 13 155 lmmbr3 ⊢ ( ( 𝜑 ∧ 𝐺 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ) → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑦 ∈ 𝑋 ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) < 𝑧 ) ) ) )
157 127 129 153 156 mpbir3and ⊢ ( ( 𝜑 ∧ 𝐺 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ) → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 )
158 lmrel ⊢ Rel ( ⇝𝑡 ‘ 𝐽 )
159 158 releldmi ⊢ ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 → 𝐹 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) )
160 157 159 syl ⊢ ( ( 𝜑 ∧ 𝐺 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ) → 𝐹 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) )
161 160 ex ⊢ ( 𝜑 → ( 𝐺 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 → 𝐹 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) ) )
162 126 161 sylbird ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 𝐽 fLimf ( ℕ filGen ( ℤ≥ “ ℕ ) ) ) ‘ 𝐺 ) → 𝐹 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) ) )
163 162 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑦 𝑦 ∈ ( ( 𝐽 fLimf ( ℕ filGen ( ℤ≥ “ ℕ ) ) ) ‘ 𝐺 ) → 𝐹 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) ) )
164 124 163 mpd ⊢ ( 𝜑 → 𝐹 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) )