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 ( 𝐹 limℂ 𝐵 ) ⊆ ( ( 𝐹 ↾ 𝐶 ) limℂ 𝐵 )

Proof

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