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 
|- ( ph -> A C_ CC )
limcun.2 
|- ( ph -> B C_ CC )
limcun.3 
|- ( ph -> F : ( A u. B ) --> CC )
Assertion limcun 
|- ( ph -> ( F limCC C ) = ( ( ( F |` A ) limCC C ) i^i ( ( F |` B ) limCC C ) ) )

Proof

Step Hyp Ref Expression
1 limcun.1 
 |-  ( ph -> A C_ CC )
2 limcun.2 
 |-  ( ph -> B C_ CC )
3 limcun.3 
 |-  ( ph -> F : ( A u. B ) --> CC )
4 limcrcl 
 |-  ( x e. ( F limCC C ) -> ( F : dom F --> CC /\ dom F C_ CC /\ C e. CC ) )
5 4 simp3d 
 |-  ( x e. ( F limCC C ) -> C e. CC )
6 5 a1i 
 |-  ( ph -> ( x e. ( F limCC C ) -> C e. CC ) )
7 elinel1 
 |-  ( x e. ( ( ( F |` A ) limCC C ) i^i ( ( F |` B ) limCC C ) ) -> x e. ( ( F |` A ) limCC C ) )
8 limcrcl 
 |-  ( x e. ( ( F |` A ) limCC C ) -> ( ( F |` A ) : dom ( F |` A ) --> CC /\ dom ( F |` A ) C_ CC /\ C e. CC ) )
9 8 simp3d 
 |-  ( x e. ( ( F |` A ) limCC C ) -> C e. CC )
10 7 9 syl 
 |-  ( x e. ( ( ( F |` A ) limCC C ) i^i ( ( F |` B ) limCC C ) ) -> C e. CC )
11 10 a1i 
 |-  ( ph -> ( x e. ( ( ( F |` A ) limCC C ) i^i ( ( F |` B ) limCC C ) ) -> C e. CC ) )
12 prfi 
 |-  { A , B } e. Fin
13 12 a1i 
 |-  ( ( ph /\ C e. CC ) -> { A , B } e. Fin )
14 1 adantr 
 |-  ( ( ph /\ C e. CC ) -> A C_ CC )
15 2 adantr 
 |-  ( ( ph /\ C e. CC ) -> B C_ CC )
16 cnex 
 |-  CC e. _V
17 16 ssex 
 |-  ( A C_ CC -> A e. _V )
18 14 17 syl 
 |-  ( ( ph /\ C e. CC ) -> A e. _V )
19 16 ssex 
 |-  ( B C_ CC -> B e. _V )
20 15 19 syl 
 |-  ( ( ph /\ C e. CC ) -> B e. _V )
21 sseq1 
 |-  ( y = A -> ( y C_ CC <-> A C_ CC ) )
22 sseq1 
 |-  ( y = B -> ( y C_ CC <-> B C_ CC ) )
23 21 22 ralprg 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A. y e. { A , B } y C_ CC <-> ( A C_ CC /\ B C_ CC ) ) )
24 18 20 23 syl2anc 
 |-  ( ( ph /\ C e. CC ) -> ( A. y e. { A , B } y C_ CC <-> ( A C_ CC /\ B C_ CC ) ) )
25 14 15 24 mpbir2and 
 |-  ( ( ph /\ C e. CC ) -> A. y e. { A , B } y C_ CC )
26 3 adantr 
 |-  ( ( ph /\ C e. CC ) -> F : ( A u. B ) --> CC )
27 uniiun 
 |-  U. { A , B } = U_ y e. { A , B } y
28 uniprg 
 |-  ( ( A e. _V /\ B e. _V ) -> U. { A , B } = ( A u. B ) )
29 18 20 28 syl2anc 
 |-  ( ( ph /\ C e. CC ) -> U. { A , B } = ( A u. B ) )
30 27 29 eqtr3id 
 |-  ( ( ph /\ C e. CC ) -> U_ y e. { A , B } y = ( A u. B ) )
31 30 feq2d 
 |-  ( ( ph /\ C e. CC ) -> ( F : U_ y e. { A , B } y --> CC <-> F : ( A u. B ) --> CC ) )
32 26 31 mpbird 
 |-  ( ( ph /\ C e. CC ) -> F : U_ y e. { A , B } y --> CC )
33 simpr 
 |-  ( ( ph /\ C e. CC ) -> C e. CC )
34 13 25 32 33 limciun 
 |-  ( ( ph /\ C e. CC ) -> ( F limCC C ) = ( CC i^i |^|_ y e. { A , B } ( ( F |` y ) limCC C ) ) )
35 34 eleq2d 
 |-  ( ( ph /\ C e. CC ) -> ( x e. ( F limCC C ) <-> x e. ( CC i^i |^|_ y e. { A , B } ( ( F |` y ) limCC C ) ) ) )
36 reseq2 
 |-  ( y = A -> ( F |` y ) = ( F |` A ) )
37 36 oveq1d 
 |-  ( y = A -> ( ( F |` y ) limCC C ) = ( ( F |` A ) limCC C ) )
38 37 eleq2d 
 |-  ( y = A -> ( x e. ( ( F |` y ) limCC C ) <-> x e. ( ( F |` A ) limCC C ) ) )
39 reseq2 
 |-  ( y = B -> ( F |` y ) = ( F |` B ) )
40 39 oveq1d 
 |-  ( y = B -> ( ( F |` y ) limCC C ) = ( ( F |` B ) limCC C ) )
41 40 eleq2d 
 |-  ( y = B -> ( x e. ( ( F |` y ) limCC C ) <-> x e. ( ( F |` B ) limCC C ) ) )
42 38 41 ralprg 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A. y e. { A , B } x e. ( ( F |` y ) limCC C ) <-> ( x e. ( ( F |` A ) limCC C ) /\ x e. ( ( F |` B ) limCC C ) ) ) )
43 18 20 42 syl2anc 
 |-  ( ( ph /\ C e. CC ) -> ( A. y e. { A , B } x e. ( ( F |` y ) limCC C ) <-> ( x e. ( ( F |` A ) limCC C ) /\ x e. ( ( F |` B ) limCC C ) ) ) )
44 43 anbi2d 
 |-  ( ( ph /\ C e. CC ) -> ( ( x e. CC /\ A. y e. { A , B } x e. ( ( F |` y ) limCC C ) ) <-> ( x e. CC /\ ( x e. ( ( F |` A ) limCC C ) /\ x e. ( ( F |` B ) limCC C ) ) ) ) )
45 limccl 
 |-  ( ( F |` A ) limCC C ) C_ CC
46 45 sseli 
 |-  ( x e. ( ( F |` A ) limCC C ) -> x e. CC )
47 46 adantr 
 |-  ( ( x e. ( ( F |` A ) limCC C ) /\ x e. ( ( F |` B ) limCC C ) ) -> x e. CC )
48 47 pm4.71ri 
 |-  ( ( x e. ( ( F |` A ) limCC C ) /\ x e. ( ( F |` B ) limCC C ) ) <-> ( x e. CC /\ ( x e. ( ( F |` A ) limCC C ) /\ x e. ( ( F |` B ) limCC C ) ) ) )
49 44 48 bitr4di 
 |-  ( ( ph /\ C e. CC ) -> ( ( x e. CC /\ A. y e. { A , B } x e. ( ( F |` y ) limCC C ) ) <-> ( x e. ( ( F |` A ) limCC C ) /\ x e. ( ( F |` B ) limCC C ) ) ) )
50 elriin 
 |-  ( x e. ( CC i^i |^|_ y e. { A , B } ( ( F |` y ) limCC C ) ) <-> ( x e. CC /\ A. y e. { A , B } x e. ( ( F |` y ) limCC C ) ) )
51 elin 
 |-  ( x e. ( ( ( F |` A ) limCC C ) i^i ( ( F |` B ) limCC C ) ) <-> ( x e. ( ( F |` A ) limCC C ) /\ x e. ( ( F |` B ) limCC C ) ) )
52 49 50 51 3bitr4g 
 |-  ( ( ph /\ C e. CC ) -> ( x e. ( CC i^i |^|_ y e. { A , B } ( ( F |` y ) limCC C ) ) <-> x e. ( ( ( F |` A ) limCC C ) i^i ( ( F |` B ) limCC C ) ) ) )
53 35 52 bitrd 
 |-  ( ( ph /\ C e. CC ) -> ( x e. ( F limCC C ) <-> x e. ( ( ( F |` A ) limCC C ) i^i ( ( F |` B ) limCC C ) ) ) )
54 53 ex 
 |-  ( ph -> ( C e. CC -> ( x e. ( F limCC C ) <-> x e. ( ( ( F |` A ) limCC C ) i^i ( ( F |` B ) limCC C ) ) ) ) )
55 6 11 54 pm5.21ndd 
 |-  ( ph -> ( x e. ( F limCC C ) <-> x e. ( ( ( F |` A ) limCC C ) i^i ( ( F |` B ) limCC C ) ) ) )
56 55 eqrdv 
 |-  ( ph -> ( F limCC C ) = ( ( ( F |` A ) limCC C ) i^i ( ( F |` B ) limCC C ) ) )