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 ( ⇝𝑑 β€˜ 𝐽 ) )