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 ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
limcun.2 ⊢ ( 𝜑 → 𝐵 ⊆ ℂ )
limcun.3 ⊢ ( 𝜑 → 𝐹 : ( 𝐴 ∪ 𝐵 ) ⟶ ℂ )
Assertion limcun ( 𝜑 → ( 𝐹 limℂ 𝐶 ) = ( ( ( 𝐹 ↾ 𝐴 ) limℂ 𝐶 ) ∩ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) )

Proof

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