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 ⊢ F lim ℂ B ⊆ F ↾ C lim ℂ B

Proof

Step Hyp Ref Expression
1 limcrcl ⊢ x ∈ F lim ℂ B → F : dom ⁡ F ⟶ ℂ ∧ dom ⁡ F ⊆ ℂ ∧ B ∈ ℂ
2 1 simp1d ⊢ x ∈ F lim ℂ B → F : dom ⁡ F ⟶ ℂ
3 1 simp2d ⊢ x ∈ F lim ℂ B → dom ⁡ F ⊆ ℂ
4 1 simp3d ⊢ x ∈ F lim ℂ B → B ∈ ℂ
5 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
6 2 3 4 5 ellimc2 ⊢ x ∈ F lim ℂ B → x ∈ F lim ℂ B ↔ x ∈ ℂ ∧ ∀ u ∈ TopOpen ⁡ ℂ fld x ∈ u → ∃ v ∈ TopOpen ⁡ ℂ fld B ∈ v ∧ F v ∩ dom ⁡ F ∖ B ⊆ u
7 6 ibi ⊢ x ∈ F lim ℂ B → x ∈ ℂ ∧ ∀ u ∈ TopOpen ⁡ ℂ fld x ∈ u → ∃ v ∈ TopOpen ⁡ ℂ fld B ∈ v ∧ F v ∩ dom ⁡ F ∖ B ⊆ u
8 inss2 ⊢ v ∩ dom ⁡ F ∩ C ∖ B ⊆ dom ⁡ F ∩ C ∖ B
9 difss ⊢ dom ⁡ F ∩ C ∖ B ⊆ dom ⁡ F ∩ C
10 inss2 ⊢ dom ⁡ F ∩ C ⊆ C
11 9 10 sstri ⊢ dom ⁡ F ∩ C ∖ B ⊆ C
12 8 11 sstri ⊢ v ∩ dom ⁡ F ∩ C ∖ B ⊆ C
13 resima2 ⊢ v ∩ dom ⁡ F ∩ C ∖ B ⊆ C → F ↾ C v ∩ dom ⁡ F ∩ C ∖ B = F v ∩ dom ⁡ F ∩ C ∖ B
14 12 13 ax-mp ⊢ F ↾ C v ∩ dom ⁡ F ∩ C ∖ B = F v ∩ dom ⁡ F ∩ C ∖ B
15 inss1 ⊢ dom ⁡ F ∩ C ⊆ dom ⁡ F
16 ssdif ⊢ dom ⁡ F ∩ C ⊆ dom ⁡ F → dom ⁡ F ∩ C ∖ B ⊆ dom ⁡ F ∖ B
17 15 16 ax-mp ⊢ dom ⁡ F ∩ C ∖ B ⊆ dom ⁡ F ∖ B
18 sslin ⊢ dom ⁡ F ∩ C ∖ B ⊆ dom ⁡ F ∖ B → v ∩ dom ⁡ F ∩ C ∖ B ⊆ v ∩ dom ⁡ F ∖ B
19 imass2 ⊢ v ∩ dom ⁡ F ∩ C ∖ B ⊆ v ∩ dom ⁡ F ∖ B → F v ∩ dom ⁡ F ∩ C ∖ B ⊆ F v ∩ dom ⁡ F ∖ B
20 17 18 19 mp2b ⊢ F v ∩ dom ⁡ F ∩ C ∖ B ⊆ F v ∩ dom ⁡ F ∖ B
21 14 20 eqsstri ⊢ F ↾ C v ∩ dom ⁡ F ∩ C ∖ B ⊆ F v ∩ dom ⁡ F ∖ B
22 sstr ⊢ F ↾ C v ∩ dom ⁡ F ∩ C ∖ B ⊆ F v ∩ dom ⁡ F ∖ B ∧ F v ∩ dom ⁡ F ∖ B ⊆ u → F ↾ C v ∩ dom ⁡ F ∩ C ∖ B ⊆ u
23 21 22 mpan ⊢ F v ∩ dom ⁡ F ∖ B ⊆ u → F ↾ C v ∩ dom ⁡ F ∩ C ∖ B ⊆ u
24 23 anim2i ⊢ B ∈ v ∧ F v ∩ dom ⁡ F ∖ B ⊆ u → B ∈ v ∧ F ↾ C v ∩ dom ⁡ F ∩ C ∖ B ⊆ u
25 24 reximi ⊢ ∃ v ∈ TopOpen ⁡ ℂ fld B ∈ v ∧ F v ∩ dom ⁡ F ∖ B ⊆ u → ∃ v ∈ TopOpen ⁡ ℂ fld B ∈ v ∧ F ↾ C v ∩ dom ⁡ F ∩ C ∖ B ⊆ u
26 25 imim2i ⊢ x ∈ u → ∃ v ∈ TopOpen ⁡ ℂ fld B ∈ v ∧ F v ∩ dom ⁡ F ∖ B ⊆ u → x ∈ u → ∃ v ∈ TopOpen ⁡ ℂ fld B ∈ v ∧ F ↾ C v ∩ dom ⁡ F ∩ C ∖ B ⊆ u
27 26 ralimi ⊢ ∀ u ∈ TopOpen ⁡ ℂ fld x ∈ u → ∃ v ∈ TopOpen ⁡ ℂ fld B ∈ v ∧ F v ∩ dom ⁡ F ∖ B ⊆ u → ∀ u ∈ TopOpen ⁡ ℂ fld x ∈ u → ∃ v ∈ TopOpen ⁡ ℂ fld B ∈ v ∧ F ↾ C v ∩ dom ⁡ F ∩ C ∖ B ⊆ u
28 27 anim2i ⊢ x ∈ ℂ ∧ ∀ u ∈ TopOpen ⁡ ℂ fld x ∈ u → ∃ v ∈ TopOpen ⁡ ℂ fld B ∈ v ∧ F v ∩ dom ⁡ F ∖ B ⊆ u → x ∈ ℂ ∧ ∀ u ∈ TopOpen ⁡ ℂ fld x ∈ u → ∃ v ∈ TopOpen ⁡ ℂ fld B ∈ v ∧ F ↾ C v ∩ dom ⁡ F ∩ C ∖ B ⊆ u
29 7 28 syl ⊢ x ∈ F lim ℂ B → x ∈ ℂ ∧ ∀ u ∈ TopOpen ⁡ ℂ fld x ∈ u → ∃ v ∈ TopOpen ⁡ ℂ fld B ∈ v ∧ F ↾ C v ∩ dom ⁡ F ∩ C ∖ B ⊆ u
30 fresin ⊢ F : dom ⁡ F ⟶ ℂ → F ↾ C : dom ⁡ F ∩ C ⟶ ℂ
31 2 30 syl ⊢ x ∈ F lim ℂ B → F ↾ C : dom ⁡ F ∩ C ⟶ ℂ
32 15 3 sstrid ⊢ x ∈ F lim ℂ B → dom ⁡ F ∩ C ⊆ ℂ
33 31 32 4 5 ellimc2 ⊢ x ∈ F lim ℂ B → x ∈ F ↾ C lim ℂ B ↔ x ∈ ℂ ∧ ∀ u ∈ TopOpen ⁡ ℂ fld x ∈ u → ∃ v ∈ TopOpen ⁡ ℂ fld B ∈ v ∧ F ↾ C v ∩ dom ⁡ F ∩ C ∖ B ⊆ u
34 29 33 mpbird ⊢ x ∈ F lim ℂ B → x ∈ F ↾ C lim ℂ B
35 34 ssriv ⊢ F lim ℂ B ⊆ F ↾ C lim ℂ B