This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem limciun

Description: A point is a limit of F on the finite union U_ x e. A B ( x ) iff it is the limit of the restriction of F to each B ( x ) . (Contributed by Mario Carneiro, 30-Dec-2016)

Ref Expression
Hypotheses limciun.1 
|- ( ph -> A e. Fin )
limciun.2 
|- ( ph -> A. x e. A B C_ CC )
limciun.3 
|- ( ph -> F : U_ x e. A B --> CC )
limciun.4 
|- ( ph -> C e. CC )
Assertion limciun 
|- ( ph -> ( F limCC C ) = ( CC i^i |^|_ x e. A ( ( F |` B ) limCC C ) ) )

Proof

Step Hyp Ref Expression
1 limciun.1 
 |-  ( ph -> A e. Fin )
2 limciun.2 
 |-  ( ph -> A. x e. A B C_ CC )
3 limciun.3 
 |-  ( ph -> F : U_ x e. A B --> CC )
4 limciun.4 
 |-  ( ph -> C e. CC )
5 limccl 
 |-  ( F limCC C ) C_ CC
6 limcresi 
 |-  ( F limCC C ) C_ ( ( F |` B ) limCC C )
7 6 rgenw 
 |-  A. x e. A ( F limCC C ) C_ ( ( F |` B ) limCC C )
8 ssiin 
 |-  ( ( F limCC C ) C_ |^|_ x e. A ( ( F |` B ) limCC C ) <-> A. x e. A ( F limCC C ) C_ ( ( F |` B ) limCC C ) )
9 7 8 mpbir 
 |-  ( F limCC C ) C_ |^|_ x e. A ( ( F |` B ) limCC C )
10 5 9 ssini 
 |-  ( F limCC C ) C_ ( CC i^i |^|_ x e. A ( ( F |` B ) limCC C ) )
11 10 a1i 
 |-  ( ph -> ( F limCC C ) C_ ( CC i^i |^|_ x e. A ( ( F |` B ) limCC C ) ) )
12 elriin 
 |-  ( y e. ( CC i^i |^|_ x e. A ( ( F |` B ) limCC C ) ) <-> ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) )
13 simprl 
 |-  ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) -> y e. CC )
14 1 ad2antrr 
 |-  ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) -> A e. Fin )
15 simplrr 
 |-  ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) -> A. x e. A y e. ( ( F |` B ) limCC C ) )
16 nfcv 
 |-  F/_ x F
17 nfcsb1v 
 |-  F/_ x [_ a / x ]_ B
18 16 17 nfres 
 |-  F/_ x ( F |` [_ a / x ]_ B )
19 nfcv 
 |-  F/_ x limCC
20 nfcv 
 |-  F/_ x C
21 18 19 20 nfov 
 |-  F/_ x ( ( F |` [_ a / x ]_ B ) limCC C )
22 21 nfcri 
 |-  F/ x y e. ( ( F |` [_ a / x ]_ B ) limCC C )
23 csbeq1a 
 |-  ( x = a -> B = [_ a / x ]_ B )
24 23 reseq2d 
 |-  ( x = a -> ( F |` B ) = ( F |` [_ a / x ]_ B ) )
25 24 oveq1d 
 |-  ( x = a -> ( ( F |` B ) limCC C ) = ( ( F |` [_ a / x ]_ B ) limCC C ) )
26 25 eleq2d 
 |-  ( x = a -> ( y e. ( ( F |` B ) limCC C ) <-> y e. ( ( F |` [_ a / x ]_ B ) limCC C ) ) )
27 22 26 rspc 
 |-  ( a e. A -> ( A. x e. A y e. ( ( F |` B ) limCC C ) -> y e. ( ( F |` [_ a / x ]_ B ) limCC C ) ) )
28 15 27 mpan9 
 |-  ( ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) /\ a e. A ) -> y e. ( ( F |` [_ a / x ]_ B ) limCC C ) )
29 3 ad2antrr 
 |-  ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ a e. A ) -> F : U_ x e. A B --> CC )
30 ssiun2 
 |-  ( a e. A -> [_ a / x ]_ B C_ U_ a e. A [_ a / x ]_ B )
31 nfcv 
 |-  F/_ a B
32 31 17 23 cbviun 
 |-  U_ x e. A B = U_ a e. A [_ a / x ]_ B
33 30 32 sseqtrrdi 
 |-  ( a e. A -> [_ a / x ]_ B C_ U_ x e. A B )
34 33 adantl 
 |-  ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ a e. A ) -> [_ a / x ]_ B C_ U_ x e. A B )
35 29 34 fssresd 
 |-  ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ a e. A ) -> ( F |` [_ a / x ]_ B ) : [_ a / x ]_ B --> CC )
36 simpr 
 |-  ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ a e. A ) -> a e. A )
37 2 ad2antrr 
 |-  ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ a e. A ) -> A. x e. A B C_ CC )
38 nfcv 
 |-  F/_ x CC
39 17 38 nfss 
 |-  F/ x [_ a / x ]_ B C_ CC
40 23 sseq1d 
 |-  ( x = a -> ( B C_ CC <-> [_ a / x ]_ B C_ CC ) )
41 39 40 rspc 
 |-  ( a e. A -> ( A. x e. A B C_ CC -> [_ a / x ]_ B C_ CC ) )
42 36 37 41 sylc 
 |-  ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ a e. A ) -> [_ a / x ]_ B C_ CC )
43 4 ad2antrr 
 |-  ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ a e. A ) -> C e. CC )
44 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
45 35 42 43 44 ellimc2 
 |-  ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ a e. A ) -> ( y e. ( ( F |` [_ a / x ]_ B ) limCC C ) <-> ( y e. CC /\ A. u e. ( TopOpen ` CCfld ) ( y e. u -> E. k e. ( TopOpen ` CCfld ) ( C e. k /\ ( ( F |` [_ a / x ]_ B ) " ( k i^i ( [_ a / x ]_ B \ { C } ) ) ) C_ u ) ) ) ) )
46 45 adantlr 
 |-  ( ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) /\ a e. A ) -> ( y e. ( ( F |` [_ a / x ]_ B ) limCC C ) <-> ( y e. CC /\ A. u e. ( TopOpen ` CCfld ) ( y e. u -> E. k e. ( TopOpen ` CCfld ) ( C e. k /\ ( ( F |` [_ a / x ]_ B ) " ( k i^i ( [_ a / x ]_ B \ { C } ) ) ) C_ u ) ) ) ) )
47 28 46 mpbid 
 |-  ( ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) /\ a e. A ) -> ( y e. CC /\ A. u e. ( TopOpen ` CCfld ) ( y e. u -> E. k e. ( TopOpen ` CCfld ) ( C e. k /\ ( ( F |` [_ a / x ]_ B ) " ( k i^i ( [_ a / x ]_ B \ { C } ) ) ) C_ u ) ) ) )
48 47 simprd 
 |-  ( ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) /\ a e. A ) -> A. u e. ( TopOpen ` CCfld ) ( y e. u -> E. k e. ( TopOpen ` CCfld ) ( C e. k /\ ( ( F |` [_ a / x ]_ B ) " ( k i^i ( [_ a / x ]_ B \ { C } ) ) ) C_ u ) ) )
49 simplrl 
 |-  ( ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) /\ a e. A ) -> u e. ( TopOpen ` CCfld ) )
50 simplrr 
 |-  ( ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) /\ a e. A ) -> y e. u )
51 rsp 
 |-  ( A. u e. ( TopOpen ` CCfld ) ( y e. u -> E. k e. ( TopOpen ` CCfld ) ( C e. k /\ ( ( F |` [_ a / x ]_ B ) " ( k i^i ( [_ a / x ]_ B \ { C } ) ) ) C_ u ) ) -> ( u e. ( TopOpen ` CCfld ) -> ( y e. u -> E. k e. ( TopOpen ` CCfld ) ( C e. k /\ ( ( F |` [_ a / x ]_ B ) " ( k i^i ( [_ a / x ]_ B \ { C } ) ) ) C_ u ) ) ) )
52 48 49 50 51 syl3c 
 |-  ( ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) /\ a e. A ) -> E. k e. ( TopOpen ` CCfld ) ( C e. k /\ ( ( F |` [_ a / x ]_ B ) " ( k i^i ( [_ a / x ]_ B \ { C } ) ) ) C_ u ) )
53 52 ralrimiva 
 |-  ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) -> A. a e. A E. k e. ( TopOpen ` CCfld ) ( C e. k /\ ( ( F |` [_ a / x ]_ B ) " ( k i^i ( [_ a / x ]_ B \ { C } ) ) ) C_ u ) )
54 nfv 
 |-  F/ a E. k e. ( TopOpen ` CCfld ) ( C e. k /\ ( ( F |` B ) " ( k i^i ( B \ { C } ) ) ) C_ u )
55 nfcv 
 |-  F/_ x ( TopOpen ` CCfld )
56 nfv 
 |-  F/ x C e. k
57 nfcv 
 |-  F/_ x k
58 nfcv 
 |-  F/_ x { C }
59 17 58 nfdif 
 |-  F/_ x ( [_ a / x ]_ B \ { C } )
60 57 59 nfin 
 |-  F/_ x ( k i^i ( [_ a / x ]_ B \ { C } ) )
61 18 60 nfima 
 |-  F/_ x ( ( F |` [_ a / x ]_ B ) " ( k i^i ( [_ a / x ]_ B \ { C } ) ) )
62 nfcv 
 |-  F/_ x u
63 61 62 nfss 
 |-  F/ x ( ( F |` [_ a / x ]_ B ) " ( k i^i ( [_ a / x ]_ B \ { C } ) ) ) C_ u
64 56 63 nfan 
 |-  F/ x ( C e. k /\ ( ( F |` [_ a / x ]_ B ) " ( k i^i ( [_ a / x ]_ B \ { C } ) ) ) C_ u )
65 55 64 nfrexw 
 |-  F/ x E. k e. ( TopOpen ` CCfld ) ( C e. k /\ ( ( F |` [_ a / x ]_ B ) " ( k i^i ( [_ a / x ]_ B \ { C } ) ) ) C_ u )
66 23 difeq1d 
 |-  ( x = a -> ( B \ { C } ) = ( [_ a / x ]_ B \ { C } ) )
67 66 ineq2d 
 |-  ( x = a -> ( k i^i ( B \ { C } ) ) = ( k i^i ( [_ a / x ]_ B \ { C } ) ) )
68 24 67 imaeq12d 
 |-  ( x = a -> ( ( F |` B ) " ( k i^i ( B \ { C } ) ) ) = ( ( F |` [_ a / x ]_ B ) " ( k i^i ( [_ a / x ]_ B \ { C } ) ) ) )
69 68 sseq1d 
 |-  ( x = a -> ( ( ( F |` B ) " ( k i^i ( B \ { C } ) ) ) C_ u <-> ( ( F |` [_ a / x ]_ B ) " ( k i^i ( [_ a / x ]_ B \ { C } ) ) ) C_ u ) )
70 69 anbi2d 
 |-  ( x = a -> ( ( C e. k /\ ( ( F |` B ) " ( k i^i ( B \ { C } ) ) ) C_ u ) <-> ( C e. k /\ ( ( F |` [_ a / x ]_ B ) " ( k i^i ( [_ a / x ]_ B \ { C } ) ) ) C_ u ) ) )
71 70 rexbidv 
 |-  ( x = a -> ( E. k e. ( TopOpen ` CCfld ) ( C e. k /\ ( ( F |` B ) " ( k i^i ( B \ { C } ) ) ) C_ u ) <-> E. k e. ( TopOpen ` CCfld ) ( C e. k /\ ( ( F |` [_ a / x ]_ B ) " ( k i^i ( [_ a / x ]_ B \ { C } ) ) ) C_ u ) ) )
72 54 65 71 cbvralw 
 |-  ( A. x e. A E. k e. ( TopOpen ` CCfld ) ( C e. k /\ ( ( F |` B ) " ( k i^i ( B \ { C } ) ) ) C_ u ) <-> A. a e. A E. k e. ( TopOpen ` CCfld ) ( C e. k /\ ( ( F |` [_ a / x ]_ B ) " ( k i^i ( [_ a / x ]_ B \ { C } ) ) ) C_ u ) )
73 53 72 sylibr 
 |-  ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) -> A. x e. A E. k e. ( TopOpen ` CCfld ) ( C e. k /\ ( ( F |` B ) " ( k i^i ( B \ { C } ) ) ) C_ u ) )
74 eleq2 
 |-  ( k = ( g ` x ) -> ( C e. k <-> C e. ( g ` x ) ) )
75 ineq1 
 |-  ( k = ( g ` x ) -> ( k i^i ( B \ { C } ) ) = ( ( g ` x ) i^i ( B \ { C } ) ) )
76 75 imaeq2d 
 |-  ( k = ( g ` x ) -> ( ( F |` B ) " ( k i^i ( B \ { C } ) ) ) = ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) )
77 76 sseq1d 
 |-  ( k = ( g ` x ) -> ( ( ( F |` B ) " ( k i^i ( B \ { C } ) ) ) C_ u <-> ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u ) )
78 74 77 anbi12d 
 |-  ( k = ( g ` x ) -> ( ( C e. k /\ ( ( F |` B ) " ( k i^i ( B \ { C } ) ) ) C_ u ) <-> ( C e. ( g ` x ) /\ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u ) ) )
79 78 ac6sfi 
 |-  ( ( A e. Fin /\ A. x e. A E. k e. ( TopOpen ` CCfld ) ( C e. k /\ ( ( F |` B ) " ( k i^i ( B \ { C } ) ) ) C_ u ) ) -> E. g ( g : A --> ( TopOpen ` CCfld ) /\ A. x e. A ( C e. ( g ` x ) /\ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u ) ) )
80 14 73 79 syl2anc 
 |-  ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) -> E. g ( g : A --> ( TopOpen ` CCfld ) /\ A. x e. A ( C e. ( g ` x ) /\ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u ) ) )
81 44 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
82 frn 
 |-  ( g : A --> ( TopOpen ` CCfld ) -> ran g C_ ( TopOpen ` CCfld ) )
83 82 ad2antrl 
 |-  ( ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) /\ ( g : A --> ( TopOpen ` CCfld ) /\ A. x e. A ( C e. ( g ` x ) /\ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u ) ) ) -> ran g C_ ( TopOpen ` CCfld ) )
84 14 adantr 
 |-  ( ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) /\ ( g : A --> ( TopOpen ` CCfld ) /\ A. x e. A ( C e. ( g ` x ) /\ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u ) ) ) -> A e. Fin )
85 ffn 
 |-  ( g : A --> ( TopOpen ` CCfld ) -> g Fn A )
86 85 ad2antrl 
 |-  ( ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) /\ ( g : A --> ( TopOpen ` CCfld ) /\ A. x e. A ( C e. ( g ` x ) /\ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u ) ) ) -> g Fn A )
87 dffn4 
 |-  ( g Fn A <-> g : A -onto-> ran g )
88 86 87 sylib 
 |-  ( ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) /\ ( g : A --> ( TopOpen ` CCfld ) /\ A. x e. A ( C e. ( g ` x ) /\ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u ) ) ) -> g : A -onto-> ran g )
89 fofi 
 |-  ( ( A e. Fin /\ g : A -onto-> ran g ) -> ran g e. Fin )
90 84 88 89 syl2anc 
 |-  ( ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) /\ ( g : A --> ( TopOpen ` CCfld ) /\ A. x e. A ( C e. ( g ` x ) /\ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u ) ) ) -> ran g e. Fin )
91 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
92 91 rintopn 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ran g C_ ( TopOpen ` CCfld ) /\ ran g e. Fin ) -> ( CC i^i |^| ran g ) e. ( TopOpen ` CCfld ) )
93 81 83 90 92 mp3an2i 
 |-  ( ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) /\ ( g : A --> ( TopOpen ` CCfld ) /\ A. x e. A ( C e. ( g ` x ) /\ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u ) ) ) -> ( CC i^i |^| ran g ) e. ( TopOpen ` CCfld ) )
94 4 adantr 
 |-  ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) -> C e. CC )
95 94 ad2antrr 
 |-  ( ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) /\ ( g : A --> ( TopOpen ` CCfld ) /\ A. x e. A ( C e. ( g ` x ) /\ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u ) ) ) -> C e. CC )
96 simpl 
 |-  ( ( C e. ( g ` x ) /\ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u ) -> C e. ( g ` x ) )
97 96 ralimi 
 |-  ( A. x e. A ( C e. ( g ` x ) /\ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u ) -> A. x e. A C e. ( g ` x ) )
98 97 ad2antll 
 |-  ( ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) /\ ( g : A --> ( TopOpen ` CCfld ) /\ A. x e. A ( C e. ( g ` x ) /\ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u ) ) ) -> A. x e. A C e. ( g ` x ) )
99 eleq2 
 |-  ( z = ( g ` x ) -> ( C e. z <-> C e. ( g ` x ) ) )
100 99 ralrn 
 |-  ( g Fn A -> ( A. z e. ran g C e. z <-> A. x e. A C e. ( g ` x ) ) )
101 86 100 syl 
 |-  ( ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) /\ ( g : A --> ( TopOpen ` CCfld ) /\ A. x e. A ( C e. ( g ` x ) /\ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u ) ) ) -> ( A. z e. ran g C e. z <-> A. x e. A C e. ( g ` x ) ) )
102 98 101 mpbird 
 |-  ( ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) /\ ( g : A --> ( TopOpen ` CCfld ) /\ A. x e. A ( C e. ( g ` x ) /\ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u ) ) ) -> A. z e. ran g C e. z )
103 elrint 
 |-  ( C e. ( CC i^i |^| ran g ) <-> ( C e. CC /\ A. z e. ran g C e. z ) )
104 95 102 103 sylanbrc 
 |-  ( ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) /\ ( g : A --> ( TopOpen ` CCfld ) /\ A. x e. A ( C e. ( g ` x ) /\ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u ) ) ) -> C e. ( CC i^i |^| ran g ) )
105 indifcom 
 |-  ( ( CC i^i |^| ran g ) i^i ( U_ x e. A B \ { C } ) ) = ( U_ x e. A B i^i ( ( CC i^i |^| ran g ) \ { C } ) )
106 iunin1 
 |-  U_ x e. A ( B i^i ( ( CC i^i |^| ran g ) \ { C } ) ) = ( U_ x e. A B i^i ( ( CC i^i |^| ran g ) \ { C } ) )
107 105 106 eqtr4i 
 |-  ( ( CC i^i |^| ran g ) i^i ( U_ x e. A B \ { C } ) ) = U_ x e. A ( B i^i ( ( CC i^i |^| ran g ) \ { C } ) )
108 107 imaeq2i 
 |-  ( F " ( ( CC i^i |^| ran g ) i^i ( U_ x e. A B \ { C } ) ) ) = ( F " U_ x e. A ( B i^i ( ( CC i^i |^| ran g ) \ { C } ) ) )
109 imaiun 
 |-  ( F " U_ x e. A ( B i^i ( ( CC i^i |^| ran g ) \ { C } ) ) ) = U_ x e. A ( F " ( B i^i ( ( CC i^i |^| ran g ) \ { C } ) ) )
110 108 109 eqtri 
 |-  ( F " ( ( CC i^i |^| ran g ) i^i ( U_ x e. A B \ { C } ) ) ) = U_ x e. A ( F " ( B i^i ( ( CC i^i |^| ran g ) \ { C } ) ) )
111 inss2 
 |-  ( CC i^i |^| ran g ) C_ |^| ran g
112 fnfvelrn 
 |-  ( ( g Fn A /\ x e. A ) -> ( g ` x ) e. ran g )
113 85 112 sylan 
 |-  ( ( g : A --> ( TopOpen ` CCfld ) /\ x e. A ) -> ( g ` x ) e. ran g )
114 intss1 
 |-  ( ( g ` x ) e. ran g -> |^| ran g C_ ( g ` x ) )
115 113 114 syl 
 |-  ( ( g : A --> ( TopOpen ` CCfld ) /\ x e. A ) -> |^| ran g C_ ( g ` x ) )
116 111 115 sstrid 
 |-  ( ( g : A --> ( TopOpen ` CCfld ) /\ x e. A ) -> ( CC i^i |^| ran g ) C_ ( g ` x ) )
117 116 ssdifd 
 |-  ( ( g : A --> ( TopOpen ` CCfld ) /\ x e. A ) -> ( ( CC i^i |^| ran g ) \ { C } ) C_ ( ( g ` x ) \ { C } ) )
118 sslin 
 |-  ( ( ( CC i^i |^| ran g ) \ { C } ) C_ ( ( g ` x ) \ { C } ) -> ( B i^i ( ( CC i^i |^| ran g ) \ { C } ) ) C_ ( B i^i ( ( g ` x ) \ { C } ) ) )
119 imass2 
 |-  ( ( B i^i ( ( CC i^i |^| ran g ) \ { C } ) ) C_ ( B i^i ( ( g ` x ) \ { C } ) ) -> ( F " ( B i^i ( ( CC i^i |^| ran g ) \ { C } ) ) ) C_ ( F " ( B i^i ( ( g ` x ) \ { C } ) ) ) )
120 117 118 119 3syl 
 |-  ( ( g : A --> ( TopOpen ` CCfld ) /\ x e. A ) -> ( F " ( B i^i ( ( CC i^i |^| ran g ) \ { C } ) ) ) C_ ( F " ( B i^i ( ( g ` x ) \ { C } ) ) ) )
121 indifcom 
 |-  ( ( g ` x ) i^i ( B \ { C } ) ) = ( B i^i ( ( g ` x ) \ { C } ) )
122 121 imaeq2i 
 |-  ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) = ( ( F |` B ) " ( B i^i ( ( g ` x ) \ { C } ) ) )
123 inss1 
 |-  ( B i^i ( ( g ` x ) \ { C } ) ) C_ B
124 resima2 
 |-  ( ( B i^i ( ( g ` x ) \ { C } ) ) C_ B -> ( ( F |` B ) " ( B i^i ( ( g ` x ) \ { C } ) ) ) = ( F " ( B i^i ( ( g ` x ) \ { C } ) ) ) )
125 123 124 ax-mp 
 |-  ( ( F |` B ) " ( B i^i ( ( g ` x ) \ { C } ) ) ) = ( F " ( B i^i ( ( g ` x ) \ { C } ) ) )
126 122 125 eqtri 
 |-  ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) = ( F " ( B i^i ( ( g ` x ) \ { C } ) ) )
127 120 126 sseqtrrdi 
 |-  ( ( g : A --> ( TopOpen ` CCfld ) /\ x e. A ) -> ( F " ( B i^i ( ( CC i^i |^| ran g ) \ { C } ) ) ) C_ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) )
128 sstr2 
 |-  ( ( F " ( B i^i ( ( CC i^i |^| ran g ) \ { C } ) ) ) C_ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) -> ( ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u -> ( F " ( B i^i ( ( CC i^i |^| ran g ) \ { C } ) ) ) C_ u ) )
129 127 128 syl 
 |-  ( ( g : A --> ( TopOpen ` CCfld ) /\ x e. A ) -> ( ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u -> ( F " ( B i^i ( ( CC i^i |^| ran g ) \ { C } ) ) ) C_ u ) )
130 129 adantld 
 |-  ( ( g : A --> ( TopOpen ` CCfld ) /\ x e. A ) -> ( ( C e. ( g ` x ) /\ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u ) -> ( F " ( B i^i ( ( CC i^i |^| ran g ) \ { C } ) ) ) C_ u ) )
131 130 ralimdva 
 |-  ( g : A --> ( TopOpen ` CCfld ) -> ( A. x e. A ( C e. ( g ` x ) /\ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u ) -> A. x e. A ( F " ( B i^i ( ( CC i^i |^| ran g ) \ { C } ) ) ) C_ u ) )
132 131 imp 
 |-  ( ( g : A --> ( TopOpen ` CCfld ) /\ A. x e. A ( C e. ( g ` x ) /\ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u ) ) -> A. x e. A ( F " ( B i^i ( ( CC i^i |^| ran g ) \ { C } ) ) ) C_ u )
133 132 adantl 
 |-  ( ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) /\ ( g : A --> ( TopOpen ` CCfld ) /\ A. x e. A ( C e. ( g ` x ) /\ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u ) ) ) -> A. x e. A ( F " ( B i^i ( ( CC i^i |^| ran g ) \ { C } ) ) ) C_ u )
134 iunss 
 |-  ( U_ x e. A ( F " ( B i^i ( ( CC i^i |^| ran g ) \ { C } ) ) ) C_ u <-> A. x e. A ( F " ( B i^i ( ( CC i^i |^| ran g ) \ { C } ) ) ) C_ u )
135 133 134 sylibr 
 |-  ( ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) /\ ( g : A --> ( TopOpen ` CCfld ) /\ A. x e. A ( C e. ( g ` x ) /\ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u ) ) ) -> U_ x e. A ( F " ( B i^i ( ( CC i^i |^| ran g ) \ { C } ) ) ) C_ u )
136 110 135 eqsstrid 
 |-  ( ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) /\ ( g : A --> ( TopOpen ` CCfld ) /\ A. x e. A ( C e. ( g ` x ) /\ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u ) ) ) -> ( F " ( ( CC i^i |^| ran g ) i^i ( U_ x e. A B \ { C } ) ) ) C_ u )
137 eleq2 
 |-  ( v = ( CC i^i |^| ran g ) -> ( C e. v <-> C e. ( CC i^i |^| ran g ) ) )
138 ineq1 
 |-  ( v = ( CC i^i |^| ran g ) -> ( v i^i ( U_ x e. A B \ { C } ) ) = ( ( CC i^i |^| ran g ) i^i ( U_ x e. A B \ { C } ) ) )
139 138 imaeq2d 
 |-  ( v = ( CC i^i |^| ran g ) -> ( F " ( v i^i ( U_ x e. A B \ { C } ) ) ) = ( F " ( ( CC i^i |^| ran g ) i^i ( U_ x e. A B \ { C } ) ) ) )
140 139 sseq1d 
 |-  ( v = ( CC i^i |^| ran g ) -> ( ( F " ( v i^i ( U_ x e. A B \ { C } ) ) ) C_ u <-> ( F " ( ( CC i^i |^| ran g ) i^i ( U_ x e. A B \ { C } ) ) ) C_ u ) )
141 137 140 anbi12d 
 |-  ( v = ( CC i^i |^| ran g ) -> ( ( C e. v /\ ( F " ( v i^i ( U_ x e. A B \ { C } ) ) ) C_ u ) <-> ( C e. ( CC i^i |^| ran g ) /\ ( F " ( ( CC i^i |^| ran g ) i^i ( U_ x e. A B \ { C } ) ) ) C_ u ) ) )
142 141 rspcev 
 |-  ( ( ( CC i^i |^| ran g ) e. ( TopOpen ` CCfld ) /\ ( C e. ( CC i^i |^| ran g ) /\ ( F " ( ( CC i^i |^| ran g ) i^i ( U_ x e. A B \ { C } ) ) ) C_ u ) ) -> E. v e. ( TopOpen ` CCfld ) ( C e. v /\ ( F " ( v i^i ( U_ x e. A B \ { C } ) ) ) C_ u ) )
143 93 104 136 142 syl12anc 
 |-  ( ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) /\ ( g : A --> ( TopOpen ` CCfld ) /\ A. x e. A ( C e. ( g ` x ) /\ ( ( F |` B ) " ( ( g ` x ) i^i ( B \ { C } ) ) ) C_ u ) ) ) -> E. v e. ( TopOpen ` CCfld ) ( C e. v /\ ( F " ( v i^i ( U_ x e. A B \ { C } ) ) ) C_ u ) )
144 80 143 exlimddv 
 |-  ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ ( u e. ( TopOpen ` CCfld ) /\ y e. u ) ) -> E. v e. ( TopOpen ` CCfld ) ( C e. v /\ ( F " ( v i^i ( U_ x e. A B \ { C } ) ) ) C_ u ) )
145 144 expr 
 |-  ( ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) /\ u e. ( TopOpen ` CCfld ) ) -> ( y e. u -> E. v e. ( TopOpen ` CCfld ) ( C e. v /\ ( F " ( v i^i ( U_ x e. A B \ { C } ) ) ) C_ u ) ) )
146 145 ralrimiva 
 |-  ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) -> A. u e. ( TopOpen ` CCfld ) ( y e. u -> E. v e. ( TopOpen ` CCfld ) ( C e. v /\ ( F " ( v i^i ( U_ x e. A B \ { C } ) ) ) C_ u ) ) )
147 3 adantr 
 |-  ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) -> F : U_ x e. A B --> CC )
148 iunss 
 |-  ( U_ x e. A B C_ CC <-> A. x e. A B C_ CC )
149 2 148 sylibr 
 |-  ( ph -> U_ x e. A B C_ CC )
150 149 adantr 
 |-  ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) -> U_ x e. A B C_ CC )
151 147 150 94 44 ellimc2 
 |-  ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) -> ( y e. ( F limCC C ) <-> ( y e. CC /\ A. u e. ( TopOpen ` CCfld ) ( y e. u -> E. v e. ( TopOpen ` CCfld ) ( C e. v /\ ( F " ( v i^i ( U_ x e. A B \ { C } ) ) ) C_ u ) ) ) ) )
152 13 146 151 mpbir2and 
 |-  ( ( ph /\ ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) ) -> y e. ( F limCC C ) )
153 152 ex 
 |-  ( ph -> ( ( y e. CC /\ A. x e. A y e. ( ( F |` B ) limCC C ) ) -> y e. ( F limCC C ) ) )
154 12 153 biimtrid 
 |-  ( ph -> ( y e. ( CC i^i |^|_ x e. A ( ( F |` B ) limCC C ) ) -> y e. ( F limCC C ) ) )
155 154 ssrdv 
 |-  ( ph -> ( CC i^i |^|_ x e. A ( ( F |` B ) limCC C ) ) C_ ( F limCC C ) )
156 11 155 eqssd 
 |-  ( ph -> ( F limCC C ) = ( CC i^i |^|_ x e. A ( ( F |` B ) limCC C ) ) )