Metamath Proof Explorer


Theorem limcresi

Description: Any limit of F is also a limit of the restriction of F . (Contributed by Mario Carneiro, 28-Dec-2016)

Ref Expression
Assertion limcresi FlimBFClimB

Proof

Step Hyp Ref Expression
1 limcrcl xFlimBF:domFdomFB
2 1 simp1d xFlimBF:domF
3 1 simp2d xFlimBdomF
4 1 simp3d xFlimBB
5 eqid TopOpenfld=TopOpenfld
6 2 3 4 5 ellimc2 xFlimBxFlimBxuTopOpenfldxuvTopOpenfldBvFvdomFBu
7 6 ibi xFlimBxuTopOpenfldxuvTopOpenfldBvFvdomFBu
8 inss2 vdomFCBdomFCB
9 difss domFCBdomFC
10 inss2 domFCC
11 9 10 sstri domFCBC
12 8 11 sstri vdomFCBC
13 resima2 vdomFCBCFCvdomFCB=FvdomFCB
14 12 13 ax-mp FCvdomFCB=FvdomFCB
15 inss1 domFCdomF
16 ssdif domFCdomFdomFCBdomFB
17 15 16 ax-mp domFCBdomFB
18 sslin domFCBdomFBvdomFCBvdomFB
19 imass2 vdomFCBvdomFBFvdomFCBFvdomFB
20 17 18 19 mp2b FvdomFCBFvdomFB
21 14 20 eqsstri FCvdomFCBFvdomFB
22 sstr FCvdomFCBFvdomFBFvdomFBuFCvdomFCBu
23 21 22 mpan FvdomFBuFCvdomFCBu
24 23 anim2i BvFvdomFBuBvFCvdomFCBu
25 24 reximi vTopOpenfldBvFvdomFBuvTopOpenfldBvFCvdomFCBu
26 25 imim2i xuvTopOpenfldBvFvdomFBuxuvTopOpenfldBvFCvdomFCBu
27 26 ralimi uTopOpenfldxuvTopOpenfldBvFvdomFBuuTopOpenfldxuvTopOpenfldBvFCvdomFCBu
28 27 anim2i xuTopOpenfldxuvTopOpenfldBvFvdomFBuxuTopOpenfldxuvTopOpenfldBvFCvdomFCBu
29 7 28 syl xFlimBxuTopOpenfldxuvTopOpenfldBvFCvdomFCBu
30 fresin F:domFFC:domFC
31 2 30 syl xFlimBFC:domFC
32 15 3 sstrid xFlimBdomFC
33 31 32 4 5 ellimc2 xFlimBxFClimBxuTopOpenfldxuvTopOpenfldBvFCvdomFCBu
34 29 33 mpbird xFlimBxFClimB
35 34 ssriv FlimBFClimB