Metamath Proof Explorer

Theorem limcun

Description: A point is a limit of F on A u. B iff it is the limit of the restriction of F to A and to B . (Contributed by Mario Carneiro, 30-Dec-2016)

Ref Expression
Hypotheses limcun.1 ⊢ φ → A ⊆ ℂ
limcun.2 ⊢ φ → B ⊆ ℂ
limcun.3 ⊢ φ → F : A ∪ B ⟶ ℂ
Assertion limcun ⊢ φ → F lim ℂ C = F ↾ A lim ℂ C ∩ F ↾ B lim ℂ C

Proof

Step Hyp Ref Expression
1 limcun.1 ⊢ φ → A ⊆ ℂ
2 limcun.2 ⊢ φ → B ⊆ ℂ
3 limcun.3 ⊢ φ → F : A ∪ B ⟶ ℂ
4 limcrcl ⊢ x ∈ F lim ℂ C → F : dom ⁡ F ⟶ ℂ ∧ dom ⁡ F ⊆ ℂ ∧ C ∈ ℂ
5 4 simp3d ⊢ x ∈ F lim ℂ C → C ∈ ℂ
6 5 a1i ⊢ φ → x ∈ F lim ℂ C → C ∈ ℂ
7 elinel1 ⊢ x ∈ F ↾ A lim ℂ C ∩ F ↾ B lim ℂ C → x ∈ F ↾ A lim ℂ C
8 limcrcl ⊢ x ∈ F ↾ A lim ℂ C → F ↾ A : dom ⁡ F ↾ A ⟶ ℂ ∧ dom ⁡ F ↾ A ⊆ ℂ ∧ C ∈ ℂ
9 8 simp3d ⊢ x ∈ F ↾ A lim ℂ C → C ∈ ℂ
10 7 9 syl ⊢ x ∈ F ↾ A lim ℂ C ∩ F ↾ B lim ℂ C → C ∈ ℂ
11 10 a1i ⊢ φ → x ∈ F ↾ A lim ℂ C ∩ F ↾ B lim ℂ C → C ∈ ℂ
12 prfi ⊢ A B ∈ Fin
13 12 a1i ⊢ φ ∧ C ∈ ℂ → A B ∈ Fin
14 1 adantr ⊢ φ ∧ C ∈ ℂ → A ⊆ ℂ
15 2 adantr ⊢ φ ∧ C ∈ ℂ → B ⊆ ℂ
16 cnex ⊢ ℂ ∈ V
17 16 ssex ⊢ A ⊆ ℂ → A ∈ V
18 14 17 syl ⊢ φ ∧ C ∈ ℂ → A ∈ V
19 16 ssex ⊢ B ⊆ ℂ → B ∈ V
20 15 19 syl ⊢ φ ∧ C ∈ ℂ → B ∈ V
21 sseq1 ⊢ y = A → y ⊆ ℂ ↔ A ⊆ ℂ
22 sseq1 ⊢ y = B → y ⊆ ℂ ↔ B ⊆ ℂ
23 21 22 ralprg ⊢ A ∈ V ∧ B ∈ V → ∀ y ∈ A B y ⊆ ℂ ↔ A ⊆ ℂ ∧ B ⊆ ℂ
24 18 20 23 syl2anc ⊢ φ ∧ C ∈ ℂ → ∀ y ∈ A B y ⊆ ℂ ↔ A ⊆ ℂ ∧ B ⊆ ℂ
25 14 15 24 mpbir2and ⊢ φ ∧ C ∈ ℂ → ∀ y ∈ A B y ⊆ ℂ
26 3 adantr ⊢ φ ∧ C ∈ ℂ → F : A ∪ B ⟶ ℂ
27 uniiun ⊢ ⋃ A B = ⋃ y ∈ A B y
28 uniprg ⊢ A ∈ V ∧ B ∈ V → ⋃ A B = A ∪ B
29 18 20 28 syl2anc ⊢ φ ∧ C ∈ ℂ → ⋃ A B = A ∪ B
30 27 29 eqtr3id ⊢ φ ∧ C ∈ ℂ → ⋃ y ∈ A B y = A ∪ B
31 30 feq2d ⊢ φ ∧ C ∈ ℂ → F : ⋃ y ∈ A B y ⟶ ℂ ↔ F : A ∪ B ⟶ ℂ
32 26 31 mpbird ⊢ φ ∧ C ∈ ℂ → F : ⋃ y ∈ A B y ⟶ ℂ
33 simpr ⊢ φ ∧ C ∈ ℂ → C ∈ ℂ
34 13 25 32 33 limciun ⊢ φ ∧ C ∈ ℂ → F lim ℂ C = ℂ ∩ ⋂ y ∈ A B F ↾ y lim ℂ C
35 34 eleq2d ⊢ φ ∧ C ∈ ℂ → x ∈ F lim ℂ C ↔ x ∈ ℂ ∩ ⋂ y ∈ A B F ↾ y lim ℂ C
36 reseq2 ⊢ y = A → F ↾ y = F ↾ A
37 36 oveq1d ⊢ y = A → F ↾ y lim ℂ C = F ↾ A lim ℂ C
38 37 eleq2d ⊢ y = A → x ∈ F ↾ y lim ℂ C ↔ x ∈ F ↾ A lim ℂ C
39 reseq2 ⊢ y = B → F ↾ y = F ↾ B
40 39 oveq1d ⊢ y = B → F ↾ y lim ℂ C = F ↾ B lim ℂ C
41 40 eleq2d ⊢ y = B → x ∈ F ↾ y lim ℂ C ↔ x ∈ F ↾ B lim ℂ C
42 38 41 ralprg ⊢ A ∈ V ∧ B ∈ V → ∀ y ∈ A B x ∈ F ↾ y lim ℂ C ↔ x ∈ F ↾ A lim ℂ C ∧ x ∈ F ↾ B lim ℂ C
43 18 20 42 syl2anc ⊢ φ ∧ C ∈ ℂ → ∀ y ∈ A B x ∈ F ↾ y lim ℂ C ↔ x ∈ F ↾ A lim ℂ C ∧ x ∈ F ↾ B lim ℂ C
44 43 anbi2d ⊢ φ ∧ C ∈ ℂ → x ∈ ℂ ∧ ∀ y ∈ A B x ∈ F ↾ y lim ℂ C ↔ x ∈ ℂ ∧ x ∈ F ↾ A lim ℂ C ∧ x ∈ F ↾ B lim ℂ C
45 limccl ⊢ F ↾ A lim ℂ C ⊆ ℂ
46 45 sseli ⊢ x ∈ F ↾ A lim ℂ C → x ∈ ℂ
47 46 adantr ⊢ x ∈ F ↾ A lim ℂ C ∧ x ∈ F ↾ B lim ℂ C → x ∈ ℂ
48 47 pm4.71ri ⊢ x ∈ F ↾ A lim ℂ C ∧ x ∈ F ↾ B lim ℂ C ↔ x ∈ ℂ ∧ x ∈ F ↾ A lim ℂ C ∧ x ∈ F ↾ B lim ℂ C
49 44 48 bitr4di ⊢ φ ∧ C ∈ ℂ → x ∈ ℂ ∧ ∀ y ∈ A B x ∈ F ↾ y lim ℂ C ↔ x ∈ F ↾ A lim ℂ C ∧ x ∈ F ↾ B lim ℂ C
50 elriin ⊢ x ∈ ℂ ∩ ⋂ y ∈ A B F ↾ y lim ℂ C ↔ x ∈ ℂ ∧ ∀ y ∈ A B x ∈ F ↾ y lim ℂ C
51 elin ⊢ x ∈ F ↾ A lim ℂ C ∩ F ↾ B lim ℂ C ↔ x ∈ F ↾ A lim ℂ C ∧ x ∈ F ↾ B lim ℂ C
52 49 50 51 3bitr4g ⊢ φ ∧ C ∈ ℂ → x ∈ ℂ ∩ ⋂ y ∈ A B F ↾ y lim ℂ C ↔ x ∈ F ↾ A lim ℂ C ∩ F ↾ B lim ℂ C
53 35 52 bitrd ⊢ φ ∧ C ∈ ℂ → x ∈ F lim ℂ C ↔ x ∈ F ↾ A lim ℂ C ∩ F ↾ B lim ℂ C
54 53 ex ⊢ φ → C ∈ ℂ → x ∈ F lim ℂ C ↔ x ∈ F ↾ A lim ℂ C ∩ F ↾ B lim ℂ C
55 6 11 54 pm5.21ndd ⊢ φ → x ∈ F lim ℂ C ↔ x ∈ F ↾ A lim ℂ C ∩ F ↾ B lim ℂ C
56 55 eqrdv ⊢ φ → F lim ℂ C = F ↾ A lim ℂ C ∩ F ↾ B lim ℂ C