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 eqtr3id ( ( 𝜑𝐶 ∈ ℂ ) → 𝑦 ∈ { 𝐴 , 𝐵 } 𝑦 = ( 𝐴𝐵 ) )
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 𝐶 ) ) )