Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  islimrs4 Unicode version

Theorem islimrs4 25582
 Description: The limits of at point relatively to is a limit of at point relatively to . (Contributed by FL, 13-Dec-2013.)
Hypotheses
Ref Expression
islimrs.1 t
islimrs.2
islimrs.3
Assertion
Ref Expression
islimrs4

Proof of Theorem islimrs4
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp11 985 . . 3
2 simp12 986 . . 3
3 inss1 3389 . . . 4
43a1i 10 . . 3
5 simp2l 981 . . 3
6 incom 3361 . . . . . 6
7 inass 3379 . . . . . 6
8 eqtr 2300 . . . . . . 7
9 innei 16862 . . . . . . . . . . . . 13
1093expia 1153 . . . . . . . . . . . 12
11103adant1 973 . . . . . . . . . . 11
12113ad2ant1 976 . . . . . . . . . 10
1312imp 418 . . . . . . . . 9
14 incom 3361 . . . . . . . . . 10
152, 5jca 518 . . . . . . . . . . . . 13
1615ad2antrl 708 . . . . . . . . . . . 12
17 simpl2r 1009 . . . . . . . . . . . . 13
1817adantl 452 . . . . . . . . . . . 12
19 simpl 443 . . . . . . . . . . . 12
20 islimrs.3 . . . . . . . . . . . . 13
2120neindisj 16854 . . . . . . . . . . . 12
2216, 18, 19, 21syl12anc 1180 . . . . . . . . . . 11
23 neeq1 2454 . . . . . . . . . . 11
2422, 23syl5ibr 212 . . . . . . . . . 10
2514, 24ax-mp 8 . . . . . . . . 9
2613, 25mpancom 650 . . . . . . . 8
27 neeq1 2454 . . . . . . . 8
2826, 27syl5ibr 212 . . . . . . 7
298, 28syl 15 . . . . . 6
306, 7, 29mp2an 653 . . . . 5
3130ralrimiva 2626 . . . 4
32 ssinss1 3397 . . . . . . 7
3332ad2antrl 708 . . . . . 6
34333adant3 975 . . . . 5
3520clsss3 16796 . . . . . . . . . 10
3635sseld 3179 . . . . . . . . 9
3736ex 423 . . . . . . . 8
38373ad2ant2 977 . . . . . . 7
3938imp32 422 . . . . . 6
40393adant3 975 . . . . 5
4120neindisj2 16860 . . . . 5
422, 34, 40, 41syl3anc 1182 . . . 4
4331, 42mpbird 223 . . 3
44 simp3 957 . . 3
45 islimrs.1 . . . 4 t
46 islimrs.2 . . . 4
4745, 46, 20islimrs3 25581 . . 3
481, 2, 4, 5, 43, 44, 47syl321anc 1204 . 2
49 ineq1 3363 . . . . . . . . . . . 12
5049eqeq2d 2294 . . . . . . . . . . 11
5150cbvrexv 2765 . . . . . . . . . 10
52 incom 3361 . . . . . . . . . . . . . . 15
5352ineq2i 3367 . . . . . . . . . . . . . 14
54 inass 3379 . . . . . . . . . . . . . 14
5553, 54eqtr4i 2306 . . . . . . . . . . . . 13
56 eqtr 2300 . . . . . . . . . . . . . 14
57 cnvresima 5162 . . . . . . . . . . . . . . . 16
58 inass 3379 . . . . . . . . . . . . . . . . . . . 20
59 eqtr 2300 . . . . . . . . . . . . . . . . . . . 20
60 eqtr 2300 . . . . . . . . . . . . . . . . . . . . 21
61 cnvimass 5033 . . . . . . . . . . . . . . . . . . . . . . . 24
62 uniexg 4517 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
6346, 62syl5eqel 2367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
64 uniexg 4517 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
6520, 64syl5eqel 2367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
66 ssexg 4160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
6766ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
68 elmapg 6785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
6968biimpd 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
7069expcom 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7167, 70syl6 29 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
7271com13 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
7372imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
7463, 65, 73syl2an 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
75743adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7675adantrd 454 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
77763imp 1145 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7877ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . 25
79 fdm 5393 . . . . . . . . . . . . . . . . . . . . . . . . 25
8078, 79syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24
8161, 80syl5sseq 3226 . . . . . . . . . . . . . . . . . . . . . . 23
82 df-ss 3166 . . . . . . . . . . . . . . . . . . . . . . . 24
83 ineq1 3363 . . . . . . . . . . . . . . . . . . . . . . . . 25
84 eqtr 2300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
85 inundif 3532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
86 uneq1 3322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
87 eqtr 2300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
88 undir 3418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
89 difss 3303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
90 eqtr 2300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
91 sstr 3187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
92 ssequn1 3345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
93 uncom 3319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
94 eqtr 2300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
9594ineq2d 3370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
96 eqtr 2300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
97 simpl12 1031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
9897ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
99 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
100 simpl13 1032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
101100ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
102 innei 16862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
10398, 99, 101, 102syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
10497adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
10520neii1 16843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
106104, 105sylan 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
107 ssinss1 3397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
108106, 107syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
10981adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
110 simpl2l 1008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
111110ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
112109, 111sstrd 3189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
113 ssdifss 3307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
114112, 113syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
115108, 114unssd 3351 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
116 ssun1 3338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
117115, 116jctil 523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
11898, 103, 117jca31 520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
119118ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
12020ssnei2 16853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
121119, 120syl6 29 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
122 ineq1 3363 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
123122eqeq2d 2294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
124123rspcev 2884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
125124ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
126121, 125syl6 29 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
127126com3r 73 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
12896, 127syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
129128ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
130129com3l 75 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
13195, 130syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
13293, 131mpan 651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
13392, 132sylbi 187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
13491, 133syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
135134ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
136135com3l 75 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
13781, 136mpcom 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
138137com3l 75 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
13989, 90, 138mpsyl 59 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
14087, 88, 139sylancl 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
141140ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
142141eqcoms 2286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
14385, 86, 142mpsyl 59 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
14484, 143syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
145144ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
146145com23 72 . . . . . . . . . . . . . . . . . . . . . . . . . 26
147146eqcoms 2286 . . . . . . . . . . . . . . . . . . . . . . . . 25
14883, 147syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24
14982, 148sylbi 187 . . . . . . . . . . . . . . . . . . . . . . 23
15081, 149mpcom 32 . . . . . . . . . . . . . . . . . . . . . 22
151150com3l 75 . . . . . . . . . . . . . . . . . . . . 21
15260, 151syl 15 . . . . . . . . . . . . . . . . . . . 20
15358, 59, 152sylancr 644 . . . . . . . . . . . . . . . . . . 19
154153ex 423 . . . . . . . . . . . . . . . . . 18
1551543impd 1165 . . . . . . . . . . . . . . . . 17
156155eqcoms 2286 . . . . . . . . . . . . . . . 16
15757, 156ax-mp 8 . . . . . . . . . . . . . . 15
1581573exp 1150 . . . . . . . . . . . . . 14
15956, 158syl 15 . . . . . . . . . . . . 13
16055, 159mpan2 652 . . . . . . . . . . . 12
161160com12 27 . . . . . . . . . . 11
162161rexlimiv 2661 . . . . . . . . . 10
16351, 162sylbi 187 . . . . . . . . 9
164163com12 27 . . . . . . . 8
165 fvex 5539 . . . . . . . . 9
166110adantr 451 . . . . . . . . . . 11
16720topopn 16652 . . . . . . . . . . . 12
168104, 167syl 15 . . . . . . . . . . 11
169 ssexg 4160 . . . . . . . . . . 11
170166, 168, 169syl2anc 642 . . . . . . . . . 10
171 inex1g 4157 . . . . . . . . . 10
172170, 171syl 15 . . . . . . . . 9
173 elrest 13332 . . . . . . . . 9 t
174165, 172, 173sylancr 644 . . . . . . . 8 t
17545eleq2i 2347 . . . . . . . . 9 t
176 elrest 13332 . . . . . . . . . 10 t
177165, 170, 176sylancr 644 . . . . . . . . 9 t
178175, 177syl5bb 248 . . . . . . . 8
179164, 174, 1783imtr4d 259 . . . . . . 7 t
180179ralimdva 2621 . . . . . 6 t
181180imdistanda 674 . . . . 5 t
18220toptopon 16671 . . . . . . . . 9 TopOn
1832, 182sylib 188 . . . . . . . 8 TopOn
184 trnei 17587 . . . . . . . 8 TopOn t
185183, 34, 40, 184syl3anc 1182 . . . . . . 7 t
18643, 185mpbid 201 . . . . . 6 t
187633ad2ant1 976 . . . . . . . . . 10
188187adantr 451 . . . . . . . . 9
18920eqcomi 2287 . . . . . . . . . . . . . . . 16
190189eleq1i 2346 . . . . . . . . . . . . . . 15
19166expcom 424 . . . . . . . . . . . . . . 15
192190, 191sylbi 187 . . . . . . . . . . . . . 14
19364, 192syl 15 . . . . . . . . . . . . 13
1941933ad2ant2 977 . . . . . . . . . . . 12
195194com12 27 . . . . . . . . . . 11
196195adantr 451 . . . . . . . . . 10