Metamath Proof Explorer

Theorem cmetcaulem

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

Ref Expression
Hypotheses cmetcau.1 
|- J = ( MetOpen ` D )
cmetcau.3 
|- ( ph -> D e. ( CMet ` X ) )
cmetcau.4 
|- ( ph -> P e. X )
cmetcau.5 
|- ( ph -> F e. ( Cau ` D ) )
cmetcau.6 
|- G = ( x e. NN |-> if ( x e. dom F , ( F ` x ) , P ) )
Assertion cmetcaulem 
|- ( ph -> F e. dom ( ~~>t ` J ) )

Proof

Step Hyp Ref Expression
1 cmetcau.1 
 |-  J = ( MetOpen ` D )
2 cmetcau.3 
 |-  ( ph -> D e. ( CMet ` X ) )
3 cmetcau.4 
 |-  ( ph -> P e. X )
4 cmetcau.5 
 |-  ( ph -> F e. ( Cau ` D ) )
5 cmetcau.6 
 |-  G = ( x e. NN |-> if ( x e. dom F , ( F ` x ) , P ) )
6 cmetmet 
 |-  ( D e. ( CMet ` X ) -> D e. ( Met ` X ) )
7 2 6 syl 
 |-  ( ph -> D e. ( Met ` X ) )
8 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
9 7 8 syl 
 |-  ( ph -> D e. ( *Met ` X ) )
10 1 mopntopon 
 |-  ( D e. ( *Met ` X ) -> J e. ( TopOn ` X ) )
11 9 10 syl 
 |-  ( ph -> J e. ( TopOn ` X ) )
12 1z 
 |-  1 e. ZZ
13 nnuz 
 |-  NN = ( ZZ>= ` 1 )
14 13 uzfbas 
 |-  ( 1 e. ZZ -> ( ZZ>= " NN ) e. ( fBas ` NN ) )
15 12 14 mp1i 
 |-  ( ph -> ( ZZ>= " NN ) e. ( fBas ` NN ) )
16 fgcl 
 |-  ( ( ZZ>= " NN ) e. ( fBas ` NN ) -> ( NN filGen ( ZZ>= " NN ) ) e. ( Fil ` NN ) )
17 15 16 syl 
 |-  ( ph -> ( NN filGen ( ZZ>= " NN ) ) e. ( Fil ` NN ) )
18 elfvdm 
 |-  ( D e. ( CMet ` X ) -> X e. dom CMet )
19 2 18 syl 
 |-  ( ph -> X e. dom CMet )
20 cnex 
 |-  CC e. _V
21 20 a1i 
 |-  ( ph -> CC e. _V )
22 caufpm 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Cau ` D ) ) -> F e. ( X ^pm CC ) )
23 9 4 22 syl2anc 
 |-  ( ph -> F e. ( X ^pm CC ) )
24 elpm2g 
 |-  ( ( X e. dom CMet /\ CC e. _V ) -> ( F e. ( X ^pm CC ) <-> ( F : dom F --> X /\ dom F C_ CC ) ) )
25 24 simprbda 
 |-  ( ( ( X e. dom CMet /\ CC e. _V ) /\ F e. ( X ^pm CC ) ) -> F : dom F --> X )
26 19 21 23 25 syl21anc 
 |-  ( ph -> F : dom F --> X )
27 26 adantr 
 |-  ( ( ph /\ x e. NN ) -> F : dom F --> X )
28 27 ffvelcdmda 
 |-  ( ( ( ph /\ x e. NN ) /\ x e. dom F ) -> ( F ` x ) e. X )
29 3 ad2antrr 
 |-  ( ( ( ph /\ x e. NN ) /\ -. x e. dom F ) -> P e. X )
30 28 29 ifclda 
 |-  ( ( ph /\ x e. NN ) -> if ( x e. dom F , ( F ` x ) , P ) e. X )
31 30 5 fmptd 
 |-  ( ph -> G : NN --> X )
32 flfval 
 |-  ( ( J e. ( TopOn ` X ) /\ ( NN filGen ( ZZ>= " NN ) ) e. ( Fil ` NN ) /\ G : NN --> X ) -> ( ( J fLimf ( NN filGen ( ZZ>= " NN ) ) ) ` G ) = ( J fLim ( ( X FilMap G ) ` ( NN filGen ( ZZ>= " NN ) ) ) ) )
33 11 17 31 32 syl3anc 
 |-  ( ph -> ( ( J fLimf ( NN filGen ( ZZ>= " NN ) ) ) ` G ) = ( J fLim ( ( X FilMap G ) ` ( NN filGen ( ZZ>= " NN ) ) ) ) )
34 eqid 
 |-  ( NN filGen ( ZZ>= " NN ) ) = ( NN filGen ( ZZ>= " NN ) )
35 34 fmfg 
 |-  ( ( X e. dom CMet /\ ( ZZ>= " NN ) e. ( fBas ` NN ) /\ G : NN --> X ) -> ( ( X FilMap G ) ` ( ZZ>= " NN ) ) = ( ( X FilMap G ) ` ( NN filGen ( ZZ>= " NN ) ) ) )
36 19 15 31 35 syl3anc 
 |-  ( ph -> ( ( X FilMap G ) ` ( ZZ>= " NN ) ) = ( ( X FilMap G ) ` ( NN filGen ( ZZ>= " NN ) ) ) )
37 36 oveq2d 
 |-  ( ph -> ( J fLim ( ( X FilMap G ) ` ( ZZ>= " NN ) ) ) = ( J fLim ( ( X FilMap G ) ` ( NN filGen ( ZZ>= " NN ) ) ) ) )
38 33 37 eqtr4d 
 |-  ( ph -> ( ( J fLimf ( NN filGen ( ZZ>= " NN ) ) ) ` G ) = ( J fLim ( ( X FilMap G ) ` ( ZZ>= " NN ) ) ) )
39 biidd 
 |-  ( z = 1 -> ( E. j e. NN A. k e. ( ZZ>= ` j ) k e. dom F <-> E. j e. NN A. k e. ( ZZ>= ` j ) k e. dom F ) )
40 1zzd 
 |-  ( ph -> 1 e. ZZ )
41 13 9 40 iscau3 
 |-  ( ph -> ( F e. ( Cau ` D ) <-> ( F e. ( X ^pm CC ) /\ A. z e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. w e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` w ) ) < z ) ) ) )
42 41 simplbda 
 |-  ( ( ph /\ F e. ( Cau ` D ) ) -> A. z e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. w e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` w ) ) < z ) )
43 4 42 mpdan 
 |-  ( ph -> A. z e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. w e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` w ) ) < z ) )
44 simp1 
 |-  ( ( k e. dom F /\ ( F ` k ) e. X /\ A. w e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` w ) ) < z ) -> k e. dom F )
45 44 ralimi 
 |-  ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. w e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` w ) ) < z ) -> A. k e. ( ZZ>= ` j ) k e. dom F )
46 45 reximi 
 |-  ( E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. w e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` w ) ) < z ) -> E. j e. NN A. k e. ( ZZ>= ` j ) k e. dom F )
47 46 ralimi 
 |-  ( A. z e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. w e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` w ) ) < z ) -> A. z e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) k e. dom F )
48 43 47 syl 
 |-  ( ph -> A. z e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) k e. dom F )
49 1rp 
 |-  1 e. RR+
50 49 a1i 
 |-  ( ph -> 1 e. RR+ )
51 39 48 50 rspcdva 
 |-  ( ph -> E. j e. NN A. k e. ( ZZ>= ` j ) k e. dom F )
52 dfss3 
 |-  ( ( ZZ>= ` j ) C_ dom F <-> A. k e. ( ZZ>= ` j ) k e. dom F )
53 nnsscn 
 |-  NN C_ CC
54 31 53 jctir 
 |-  ( ph -> ( G : NN --> X /\ NN C_ CC ) )
55 elpm2r 
 |-  ( ( ( X e. dom CMet /\ CC e. _V ) /\ ( G : NN --> X /\ NN C_ CC ) ) -> G e. ( X ^pm CC ) )
56 19 21 54 55 syl21anc 
 |-  ( ph -> G e. ( X ^pm CC ) )
57 56 adantr 
 |-  ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) -> G e. ( X ^pm CC ) )
58 eqid 
 |-  ( ZZ>= ` j ) = ( ZZ>= ` j )
59 9 adantr 
 |-  ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) -> D e. ( *Met ` X ) )
60 nnz 
 |-  ( j e. NN -> j e. ZZ )
61 60 ad2antrl 
 |-  ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) -> j e. ZZ )
62 eqidd 
 |-  ( ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) = ( F ` k ) )
63 eqidd 
 |-  ( ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) /\ m e. ( ZZ>= ` j ) ) -> ( F ` m ) = ( F ` m ) )
64 58 59 61 62 63 iscau4 
 |-  ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) -> ( F e. ( Cau ` D ) <-> ( F e. ( X ^pm CC ) /\ A. z e. RR+ E. m e. ( ZZ>= ` j ) A. k e. ( ZZ>= ` m ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` m ) ) < z ) ) ) )
65 64 simplbda 
 |-  ( ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) /\ F e. ( Cau ` D ) ) -> A. z e. RR+ E. m e. ( ZZ>= ` j ) A. k e. ( ZZ>= ` m ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` m ) ) < z ) )
66 4 65 mpidan 
 |-  ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) -> A. z e. RR+ E. m e. ( ZZ>= ` j ) A. k e. ( ZZ>= ` m ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` m ) ) < z ) )
67 simprl 
 |-  ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) -> j e. NN )
68 eluznn 
 |-  ( ( j e. NN /\ m e. ( ZZ>= ` j ) ) -> m e. NN )
69 67 68 sylan 
 |-  ( ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) /\ m e. ( ZZ>= ` j ) ) -> m e. NN )
70 eluznn 
 |-  ( ( m e. NN /\ k e. ( ZZ>= ` m ) ) -> k e. NN )
71 5 30 dmmptd 
 |-  ( ph -> dom G = NN )
72 71 adantr 
 |-  ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) -> dom G = NN )
73 72 eleq2d 
 |-  ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) -> ( k e. dom G <-> k e. NN ) )
74 73 biimpar 
 |-  ( ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) /\ k e. NN ) -> k e. dom G )
75 74 a1d 
 |-  ( ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) /\ k e. NN ) -> ( k e. dom F -> k e. dom G ) )
76 idd 
 |-  ( ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) /\ k e. NN ) -> ( ( F ` k ) e. X -> ( F ` k ) e. X ) )
77 idd 
 |-  ( ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) /\ k e. NN ) -> ( ( ( F ` k ) D ( F ` m ) ) < z -> ( ( F ` k ) D ( F ` m ) ) < z ) )
78 75 76 77 3anim123d 
 |-  ( ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) /\ k e. NN ) -> ( ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` m ) ) < z ) -> ( k e. dom G /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` m ) ) < z ) ) )
79 70 78 sylan2 
 |-  ( ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) /\ ( m e. NN /\ k e. ( ZZ>= ` m ) ) ) -> ( ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` m ) ) < z ) -> ( k e. dom G /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` m ) ) < z ) ) )
80 79 anassrs 
 |-  ( ( ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) /\ m e. NN ) /\ k e. ( ZZ>= ` m ) ) -> ( ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` m ) ) < z ) -> ( k e. dom G /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` m ) ) < z ) ) )
81 80 ralimdva 
 |-  ( ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) /\ m e. NN ) -> ( A. k e. ( ZZ>= ` m ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` m ) ) < z ) -> A. k e. ( ZZ>= ` m ) ( k e. dom G /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` m ) ) < z ) ) )
82 69 81 syldan 
 |-  ( ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) /\ m e. ( ZZ>= ` j ) ) -> ( A. k e. ( ZZ>= ` m ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` m ) ) < z ) -> A. k e. ( ZZ>= ` m ) ( k e. dom G /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` m ) ) < z ) ) )
83 82 reximdva 
 |-  ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) -> ( E. m e. ( ZZ>= ` j ) A. k e. ( ZZ>= ` m ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` m ) ) < z ) -> E. m e. ( ZZ>= ` j ) A. k e. ( ZZ>= ` m ) ( k e. dom G /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` m ) ) < z ) ) )
84 83 ralimdv 
 |-  ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) -> ( A. z e. RR+ E. m e. ( ZZ>= ` j ) A. k e. ( ZZ>= ` m ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` m ) ) < z ) -> A. z e. RR+ E. m e. ( ZZ>= ` j ) A. k e. ( ZZ>= ` m ) ( k e. dom G /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` m ) ) < z ) ) )
85 66 84 mpd 
 |-  ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) -> A. z e. RR+ E. m e. ( ZZ>= ` j ) A. k e. ( ZZ>= ` m ) ( k e. dom G /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` m ) ) < z ) )
86 eluznn 
 |-  ( ( j e. NN /\ k e. ( ZZ>= ` j ) ) -> k e. NN )
87 67 86 sylan 
 |-  ( ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) /\ k e. ( ZZ>= ` j ) ) -> k e. NN )
88 simprr 
 |-  ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) -> ( ZZ>= ` j ) C_ dom F )
89 88 sselda 
 |-  ( ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) /\ k e. ( ZZ>= ` j ) ) -> k e. dom F )
90 iftrue 
 |-  ( k e. dom F -> if ( k e. dom F , ( F ` k ) , P ) = ( F ` k ) )
91 90 adantl 
 |-  ( ( k e. NN /\ k e. dom F ) -> if ( k e. dom F , ( F ` k ) , P ) = ( F ` k ) )
92 fvex 
 |-  ( F ` k ) e. _V
93 91 92 eqeltrdi 
 |-  ( ( k e. NN /\ k e. dom F ) -> if ( k e. dom F , ( F ` k ) , P ) e. _V )
94 eleq1w 
 |-  ( x = k -> ( x e. dom F <-> k e. dom F ) )
95 fveq2 
 |-  ( x = k -> ( F ` x ) = ( F ` k ) )
96 94 95 ifbieq1d 
 |-  ( x = k -> if ( x e. dom F , ( F ` x ) , P ) = if ( k e. dom F , ( F ` k ) , P ) )
97 96 5 fvmptg 
 |-  ( ( k e. NN /\ if ( k e. dom F , ( F ` k ) , P ) e. _V ) -> ( G ` k ) = if ( k e. dom F , ( F ` k ) , P ) )
98 93 97 syldan 
 |-  ( ( k e. NN /\ k e. dom F ) -> ( G ` k ) = if ( k e. dom F , ( F ` k ) , P ) )
99 98 91 eqtrd 
 |-  ( ( k e. NN /\ k e. dom F ) -> ( G ` k ) = ( F ` k ) )
100 87 89 99 syl2anc 
 |-  ( ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) /\ k e. ( ZZ>= ` j ) ) -> ( G ` k ) = ( F ` k ) )
101 88 sselda 
 |-  ( ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) /\ m e. ( ZZ>= ` j ) ) -> m e. dom F )
102 69 101 elind 
 |-  ( ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) /\ m e. ( ZZ>= ` j ) ) -> m e. ( NN i^i dom F ) )
103 fveq2 
 |-  ( k = m -> ( G ` k ) = ( G ` m ) )
104 fveq2 
 |-  ( k = m -> ( F ` k ) = ( F ` m ) )
105 103 104 eqeq12d 
 |-  ( k = m -> ( ( G ` k ) = ( F ` k ) <-> ( G ` m ) = ( F ` m ) ) )
106 elin 
 |-  ( k e. ( NN i^i dom F ) <-> ( k e. NN /\ k e. dom F ) )
107 106 99 sylbi 
 |-  ( k e. ( NN i^i dom F ) -> ( G ` k ) = ( F ` k ) )
108 105 107 vtoclga 
 |-  ( m e. ( NN i^i dom F ) -> ( G ` m ) = ( F ` m ) )
109 102 108 syl 
 |-  ( ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) /\ m e. ( ZZ>= ` j ) ) -> ( G ` m ) = ( F ` m ) )
110 58 59 61 100 109 iscau4 
 |-  ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) -> ( G e. ( Cau ` D ) <-> ( G e. ( X ^pm CC ) /\ A. z e. RR+ E. m e. ( ZZ>= ` j ) A. k e. ( ZZ>= ` m ) ( k e. dom G /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` m ) ) < z ) ) ) )
111 57 85 110 mpbir2and 
 |-  ( ( ph /\ ( j e. NN /\ ( ZZ>= ` j ) C_ dom F ) ) -> G e. ( Cau ` D ) )
112 111 expr 
 |-  ( ( ph /\ j e. NN ) -> ( ( ZZ>= ` j ) C_ dom F -> G e. ( Cau ` D ) ) )
113 52 112 biimtrrid 
 |-  ( ( ph /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) k e. dom F -> G e. ( Cau ` D ) ) )
114 113 rexlimdva 
 |-  ( ph -> ( E. j e. NN A. k e. ( ZZ>= ` j ) k e. dom F -> G e. ( Cau ` D ) ) )
115 51 114 mpd 
 |-  ( ph -> G e. ( Cau ` D ) )
116 eqid 
 |-  ( ( X FilMap G ) ` ( ZZ>= " NN ) ) = ( ( X FilMap G ) ` ( ZZ>= " NN ) )
117 13 116 caucfil 
 |-  ( ( D e. ( *Met ` X ) /\ 1 e. ZZ /\ G : NN --> X ) -> ( G e. ( Cau ` D ) <-> ( ( X FilMap G ) ` ( ZZ>= " NN ) ) e. ( CauFil ` D ) ) )
118 9 40 31 117 syl3anc 
 |-  ( ph -> ( G e. ( Cau ` D ) <-> ( ( X FilMap G ) ` ( ZZ>= " NN ) ) e. ( CauFil ` D ) ) )
119 115 118 mpbid 
 |-  ( ph -> ( ( X FilMap G ) ` ( ZZ>= " NN ) ) e. ( CauFil ` D ) )
120 1 cmetcvg 
 |-  ( ( D e. ( CMet ` X ) /\ ( ( X FilMap G ) ` ( ZZ>= " NN ) ) e. ( CauFil ` D ) ) -> ( J fLim ( ( X FilMap G ) ` ( ZZ>= " NN ) ) ) =/= (/) )
121 2 119 120 syl2anc 
 |-  ( ph -> ( J fLim ( ( X FilMap G ) ` ( ZZ>= " NN ) ) ) =/= (/) )
122 38 121 eqnetrd 
 |-  ( ph -> ( ( J fLimf ( NN filGen ( ZZ>= " NN ) ) ) ` G ) =/= (/) )
123 n0 
 |-  ( ( ( J fLimf ( NN filGen ( ZZ>= " NN ) ) ) ` G ) =/= (/) <-> E. y y e. ( ( J fLimf ( NN filGen ( ZZ>= " NN ) ) ) ` G ) )
124 122 123 sylib 
 |-  ( ph -> E. y y e. ( ( J fLimf ( NN filGen ( ZZ>= " NN ) ) ) ` G ) )
125 13 34 lmflf 
 |-  ( ( J e. ( TopOn ` X ) /\ 1 e. ZZ /\ G : NN --> X ) -> ( G ( ~~>t ` J ) y <-> y e. ( ( J fLimf ( NN filGen ( ZZ>= " NN ) ) ) ` G ) ) )
126 11 40 31 125 syl3anc 
 |-  ( ph -> ( G ( ~~>t ` J ) y <-> y e. ( ( J fLimf ( NN filGen ( ZZ>= " NN ) ) ) ` G ) ) )
127 23 adantr 
 |-  ( ( ph /\ G ( ~~>t ` J ) y ) -> F e. ( X ^pm CC ) )
128 lmcl 
 |-  ( ( J e. ( TopOn ` X ) /\ G ( ~~>t ` J ) y ) -> y e. X )
129 11 128 sylan 
 |-  ( ( ph /\ G ( ~~>t ` J ) y ) -> y e. X )
130 1 9 13 40 lmmbr3 
 |-  ( ph -> ( G ( ~~>t ` J ) y <-> ( G e. ( X ^pm CC ) /\ y e. X /\ A. z e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) ) ) )
131 130 biimpa 
 |-  ( ( ph /\ G ( ~~>t ` J ) y ) -> ( G e. ( X ^pm CC ) /\ y e. X /\ A. z e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) ) )
132 131 simp3d 
 |-  ( ( ph /\ G ( ~~>t ` J ) y ) -> A. z e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) )
133 r19.26 
 |-  ( A. z e. RR+ ( E. j e. NN A. k e. ( ZZ>= ` j ) k e. dom F /\ E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) ) <-> ( A. z e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) k e. dom F /\ A. z e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) ) )
134 13 rexanuz2 
 |-  ( E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) ) <-> ( E. j e. NN A. k e. ( ZZ>= ` j ) k e. dom F /\ E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) ) )
135 simprl 
 |-  ( ( ( ph /\ k e. NN ) /\ ( k e. dom F /\ ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) ) ) -> k e. dom F )
136 99 ad2ant2lr 
 |-  ( ( ( ph /\ k e. NN ) /\ ( k e. dom F /\ ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) ) ) -> ( G ` k ) = ( F ` k ) )
137 simprr2 
 |-  ( ( ( ph /\ k e. NN ) /\ ( k e. dom F /\ ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) ) ) -> ( G ` k ) e. X )
138 136 137 eqeltrrd 
 |-  ( ( ( ph /\ k e. NN ) /\ ( k e. dom F /\ ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) ) ) -> ( F ` k ) e. X )
139 136 oveq1d 
 |-  ( ( ( ph /\ k e. NN ) /\ ( k e. dom F /\ ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) ) ) -> ( ( G ` k ) D y ) = ( ( F ` k ) D y ) )
140 simprr3 
 |-  ( ( ( ph /\ k e. NN ) /\ ( k e. dom F /\ ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) ) ) -> ( ( G ` k ) D y ) < z )
141 139 140 eqbrtrrd 
 |-  ( ( ( ph /\ k e. NN ) /\ ( k e. dom F /\ ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) ) ) -> ( ( F ` k ) D y ) < z )
142 135 138 141 3jca 
 |-  ( ( ( ph /\ k e. NN ) /\ ( k e. dom F /\ ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) ) ) -> ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D y ) < z ) )
143 142 ex 
 |-  ( ( ph /\ k e. NN ) -> ( ( k e. dom F /\ ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) ) -> ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D y ) < z ) ) )
144 86 143 sylan2 
 |-  ( ( ph /\ ( j e. NN /\ k e. ( ZZ>= ` j ) ) ) -> ( ( k e. dom F /\ ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) ) -> ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D y ) < z ) ) )
145 144 anassrs 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( k e. dom F /\ ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) ) -> ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D y ) < z ) ) )
146 145 ralimdva 
 |-  ( ( ph /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) ) -> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D y ) < z ) ) )
147 146 reximdva 
 |-  ( ph -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D y ) < z ) ) )
148 134 147 biimtrrid 
 |-  ( ph -> ( ( E. j e. NN A. k e. ( ZZ>= ` j ) k e. dom F /\ E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D y ) < z ) ) )
149 148 ralimdv 
 |-  ( ph -> ( A. z e. RR+ ( E. j e. NN A. k e. ( ZZ>= ` j ) k e. dom F /\ E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) ) -> A. z e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D y ) < z ) ) )
150 133 149 biimtrrid 
 |-  ( ph -> ( ( A. z e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) k e. dom F /\ A. z e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) ) -> A. z e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D y ) < z ) ) )
151 48 150 mpand 
 |-  ( ph -> ( A. z e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) -> A. z e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D y ) < z ) ) )
152 151 adantr 
 |-  ( ( ph /\ G ( ~~>t ` J ) y ) -> ( A. z e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom G /\ ( G ` k ) e. X /\ ( ( G ` k ) D y ) < z ) -> A. z e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D y ) < z ) ) )
153 132 152 mpd 
 |-  ( ( ph /\ G ( ~~>t ` J ) y ) -> A. z e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D y ) < z ) )
154 9 adantr 
 |-  ( ( ph /\ G ( ~~>t ` J ) y ) -> D e. ( *Met ` X ) )
155 1zzd 
 |-  ( ( ph /\ G ( ~~>t ` J ) y ) -> 1 e. ZZ )
156 1 154 13 155 lmmbr3 
 |-  ( ( ph /\ G ( ~~>t ` J ) y ) -> ( F ( ~~>t ` J ) y <-> ( F e. ( X ^pm CC ) /\ y e. X /\ A. z e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D y ) < z ) ) ) )
157 127 129 153 156 mpbir3and 
 |-  ( ( ph /\ G ( ~~>t ` J ) y ) -> F ( ~~>t ` J ) y )
158 lmrel 
 |-  Rel ( ~~>t ` J )
159 158 releldmi 
 |-  ( F ( ~~>t ` J ) y -> F e. dom ( ~~>t ` J ) )
160 157 159 syl 
 |-  ( ( ph /\ G ( ~~>t ` J ) y ) -> F e. dom ( ~~>t ` J ) )
161 160 ex 
 |-  ( ph -> ( G ( ~~>t ` J ) y -> F e. dom ( ~~>t ` J ) ) )
162 126 161 sylbird 
 |-  ( ph -> ( y e. ( ( J fLimf ( NN filGen ( ZZ>= " NN ) ) ) ` G ) -> F e. dom ( ~~>t ` J ) ) )
163 162 exlimdv 
 |-  ( ph -> ( E. y y e. ( ( J fLimf ( NN filGen ( ZZ>= " NN ) ) ) ` G ) -> F e. dom ( ~~>t ` J ) ) )
164 124 163 mpd 
 |-  ( ph -> F e. dom ( ~~>t ` J ) )