Metamath Proof Explorer

Theorem dvcnp2

Description: A function is continuous at each point for which it is differentiable. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016)

Ref Expression
Hypotheses dvcnp.j 
|- J = ( K |`t A )
dvcnp.k 
|- K = ( TopOpen ` CCfld )
Assertion dvcnp2 
|- ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B e. dom ( S _D F ) ) -> F e. ( ( J CnP K ) ` B ) )

Proof

Step Hyp Ref Expression
1 dvcnp.j 
 |-  J = ( K |`t A )
2 dvcnp.k 
 |-  K = ( TopOpen ` CCfld )
3 simpl2 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> F : A --> CC )
4 3 ffvelrnda 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. A ) -> ( F ` z ) e. CC )
5 2 cnfldtop 
 |-  K e. Top
6 simpl1 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> S C_ CC )
7 cnex 
 |-  CC e. _V
8 ssexg 
 |-  ( ( S C_ CC /\ CC e. _V ) -> S e. _V )
9 6 7 8 sylancl 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> S e. _V )
10 resttop 
 |-  ( ( K e. Top /\ S e. _V ) -> ( K |`t S ) e. Top )
11 5 9 10 sylancr 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( K |`t S ) e. Top )
12 simpl3 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> A C_ S )
13 2 cnfldtopon 
 |-  K e. ( TopOn ` CC )
14 resttopon 
 |-  ( ( K e. ( TopOn ` CC ) /\ S C_ CC ) -> ( K |`t S ) e. ( TopOn ` S ) )
15 13 6 14 sylancr 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( K |`t S ) e. ( TopOn ` S ) )
16 toponuni 
 |-  ( ( K |`t S ) e. ( TopOn ` S ) -> S = U. ( K |`t S ) )
17 15 16 syl 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> S = U. ( K |`t S ) )
18 12 17 sseqtrd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> A C_ U. ( K |`t S ) )
19 eqid 
 |-  U. ( K |`t S ) = U. ( K |`t S )
20 19 ntrss2 
 |-  ( ( ( K |`t S ) e. Top /\ A C_ U. ( K |`t S ) ) -> ( ( int ` ( K |`t S ) ) ` A ) C_ A )
21 11 18 20 syl2anc 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( ( int ` ( K |`t S ) ) ` A ) C_ A )
22 eqid 
 |-  ( K |`t S ) = ( K |`t S )
23 eqid 
 |-  ( z e. ( A \ { B } ) |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ) = ( z e. ( A \ { B } ) |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) )
24 simp1 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> S C_ CC )
25 simp2 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> F : A --> CC )
26 simp3 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> A C_ S )
27 22 2 23 24 25 26 eldv 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> ( B ( S _D F ) y <-> ( B e. ( ( int ` ( K |`t S ) ) ` A ) /\ y e. ( ( z e. ( A \ { B } ) |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ) limCC B ) ) ) )
28 27 simprbda 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> B e. ( ( int ` ( K |`t S ) ) ` A ) )
29 21 28 sseldd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> B e. A )
30 3 29 ffvelrnd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( F ` B ) e. CC )
31 30 adantr 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. A ) -> ( F ` B ) e. CC )
32 4 31 subcld 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. A ) -> ( ( F ` z ) - ( F ` B ) ) e. CC )
33 ssid 
 |-  CC C_ CC
34 33 a1i 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> CC C_ CC )
35 txtopon 
 |-  ( ( K e. ( TopOn ` CC ) /\ K e. ( TopOn ` CC ) ) -> ( K tX K ) e. ( TopOn ` ( CC X. CC ) ) )
36 13 13 35 mp2an 
 |-  ( K tX K ) e. ( TopOn ` ( CC X. CC ) )
37 36 toponrestid 
 |-  ( K tX K ) = ( ( K tX K ) |`t ( CC X. CC ) )
38 12 6 sstrd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> A C_ CC )
39 3 38 29 dvlem 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) e. CC )
40 38 ssdifssd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( A \ { B } ) C_ CC )
41 40 sselda 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> z e. CC )
42 38 29 sseldd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> B e. CC )
43 42 adantr 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> B e. CC )
44 41 43 subcld 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> ( z - B ) e. CC )
45 27 simplbda 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> y e. ( ( z e. ( A \ { B } ) |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ) limCC B ) )
46 limcresi 
 |-  ( ( z e. A |-> ( z - B ) ) limCC B ) C_ ( ( ( z e. A |-> ( z - B ) ) |` ( A \ { B } ) ) limCC B )
47 difss 
 |-  ( A \ { B } ) C_ A
48 resmpt 
 |-  ( ( A \ { B } ) C_ A -> ( ( z e. A |-> ( z - B ) ) |` ( A \ { B } ) ) = ( z e. ( A \ { B } ) |-> ( z - B ) ) )
49 47 48 ax-mp 
 |-  ( ( z e. A |-> ( z - B ) ) |` ( A \ { B } ) ) = ( z e. ( A \ { B } ) |-> ( z - B ) )
50 49 oveq1i 
 |-  ( ( ( z e. A |-> ( z - B ) ) |` ( A \ { B } ) ) limCC B ) = ( ( z e. ( A \ { B } ) |-> ( z - B ) ) limCC B )
51 46 50 sseqtri 
 |-  ( ( z e. A |-> ( z - B ) ) limCC B ) C_ ( ( z e. ( A \ { B } ) |-> ( z - B ) ) limCC B )
52 42 subidd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( B - B ) = 0 )
53 2 subcn 
 |-  - e. ( ( K tX K ) Cn K )
54 53 a1i 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> - e. ( ( K tX K ) Cn K ) )
55 cncfmptid 
 |-  ( ( A C_ CC /\ CC C_ CC ) -> ( z e. A |-> z ) e. ( A -cn-> CC ) )
56 38 33 55 sylancl 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( z e. A |-> z ) e. ( A -cn-> CC ) )
57 cncfmptc 
 |-  ( ( B e. CC /\ A C_ CC /\ CC C_ CC ) -> ( z e. A |-> B ) e. ( A -cn-> CC ) )
58 42 38 34 57 syl3anc 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( z e. A |-> B ) e. ( A -cn-> CC ) )
59 2 54 56 58 cncfmpt2f 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( z e. A |-> ( z - B ) ) e. ( A -cn-> CC ) )
60 oveq1 
 |-  ( z = B -> ( z - B ) = ( B - B ) )
61 59 29 60 cnmptlimc 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( B - B ) e. ( ( z e. A |-> ( z - B ) ) limCC B ) )
62 52 61 eqeltrrd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> 0 e. ( ( z e. A |-> ( z - B ) ) limCC B ) )
63 51 62 sselid 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> 0 e. ( ( z e. ( A \ { B } ) |-> ( z - B ) ) limCC B ) )
64 2 mulcn 
 |-  x. e. ( ( K tX K ) Cn K )
65 24 25 26 dvcl 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> y e. CC )
66 0cn 
 |-  0 e. CC
67 opelxpi 
 |-  ( ( y e. CC /\ 0 e. CC ) -> <. y , 0 >. e. ( CC X. CC ) )
68 65 66 67 sylancl 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> <. y , 0 >. e. ( CC X. CC ) )
69 36 toponunii 
 |-  ( CC X. CC ) = U. ( K tX K )
70 69 cncnpi 
 |-  ( ( x. e. ( ( K tX K ) Cn K ) /\ <. y , 0 >. e. ( CC X. CC ) ) -> x. e. ( ( ( K tX K ) CnP K ) ` <. y , 0 >. ) )
71 64 68 70 sylancr 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> x. e. ( ( ( K tX K ) CnP K ) ` <. y , 0 >. ) )
72 39 44 34 34 2 37 45 63 71 limccnp2 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( y x. 0 ) e. ( ( z e. ( A \ { B } ) |-> ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) x. ( z - B ) ) ) limCC B ) )
73 65 mul01d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( y x. 0 ) = 0 )
74 3 adantr 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> F : A --> CC )
75 simpr 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> z e. ( A \ { B } ) )
76 47 75 sselid 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> z e. A )
77 74 76 ffvelrnd 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> ( F ` z ) e. CC )
78 30 adantr 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> ( F ` B ) e. CC )
79 77 78 subcld 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> ( ( F ` z ) - ( F ` B ) ) e. CC )
80 eldifsni 
 |-  ( z e. ( A \ { B } ) -> z =/= B )
81 80 adantl 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> z =/= B )
82 41 43 81 subne0d 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> ( z - B ) =/= 0 )
83 79 44 82 divcan1d 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) x. ( z - B ) ) = ( ( F ` z ) - ( F ` B ) ) )
84 83 mpteq2dva 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( z e. ( A \ { B } ) |-> ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) x. ( z - B ) ) ) = ( z e. ( A \ { B } ) |-> ( ( F ` z ) - ( F ` B ) ) ) )
85 84 oveq1d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( ( z e. ( A \ { B } ) |-> ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) x. ( z - B ) ) ) limCC B ) = ( ( z e. ( A \ { B } ) |-> ( ( F ` z ) - ( F ` B ) ) ) limCC B ) )
86 72 73 85 3eltr3d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> 0 e. ( ( z e. ( A \ { B } ) |-> ( ( F ` z ) - ( F ` B ) ) ) limCC B ) )
87 32 fmpttd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( z e. A |-> ( ( F ` z ) - ( F ` B ) ) ) : A --> CC )
88 87 limcdif 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( ( z e. A |-> ( ( F ` z ) - ( F ` B ) ) ) limCC B ) = ( ( ( z e. A |-> ( ( F ` z ) - ( F ` B ) ) ) |` ( A \ { B } ) ) limCC B ) )
89 resmpt 
 |-  ( ( A \ { B } ) C_ A -> ( ( z e. A |-> ( ( F ` z ) - ( F ` B ) ) ) |` ( A \ { B } ) ) = ( z e. ( A \ { B } ) |-> ( ( F ` z ) - ( F ` B ) ) ) )
90 47 89 ax-mp 
 |-  ( ( z e. A |-> ( ( F ` z ) - ( F ` B ) ) ) |` ( A \ { B } ) ) = ( z e. ( A \ { B } ) |-> ( ( F ` z ) - ( F ` B ) ) )
91 90 oveq1i 
 |-  ( ( ( z e. A |-> ( ( F ` z ) - ( F ` B ) ) ) |` ( A \ { B } ) ) limCC B ) = ( ( z e. ( A \ { B } ) |-> ( ( F ` z ) - ( F ` B ) ) ) limCC B )
92 88 91 eqtrdi 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( ( z e. A |-> ( ( F ` z ) - ( F ` B ) ) ) limCC B ) = ( ( z e. ( A \ { B } ) |-> ( ( F ` z ) - ( F ` B ) ) ) limCC B ) )
93 86 92 eleqtrrd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> 0 e. ( ( z e. A |-> ( ( F ` z ) - ( F ` B ) ) ) limCC B ) )
94 cncfmptc 
 |-  ( ( ( F ` B ) e. CC /\ A C_ CC /\ CC C_ CC ) -> ( z e. A |-> ( F ` B ) ) e. ( A -cn-> CC ) )
95 30 38 34 94 syl3anc 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( z e. A |-> ( F ` B ) ) e. ( A -cn-> CC ) )
96 eqidd 
 |-  ( z = B -> ( F ` B ) = ( F ` B ) )
97 95 29 96 cnmptlimc 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( F ` B ) e. ( ( z e. A |-> ( F ` B ) ) limCC B ) )
98 2 addcn 
 |-  + e. ( ( K tX K ) Cn K )
99 opelxpi 
 |-  ( ( 0 e. CC /\ ( F ` B ) e. CC ) -> <. 0 , ( F ` B ) >. e. ( CC X. CC ) )
100 66 30 99 sylancr 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> <. 0 , ( F ` B ) >. e. ( CC X. CC ) )
101 69 cncnpi 
 |-  ( ( + e. ( ( K tX K ) Cn K ) /\ <. 0 , ( F ` B ) >. e. ( CC X. CC ) ) -> + e. ( ( ( K tX K ) CnP K ) ` <. 0 , ( F ` B ) >. ) )
102 98 100 101 sylancr 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> + e. ( ( ( K tX K ) CnP K ) ` <. 0 , ( F ` B ) >. ) )
103 32 31 34 34 2 37 93 97 102 limccnp2 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( 0 + ( F ` B ) ) e. ( ( z e. A |-> ( ( ( F ` z ) - ( F ` B ) ) + ( F ` B ) ) ) limCC B ) )
104 30 addid2d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( 0 + ( F ` B ) ) = ( F ` B ) )
105 4 31 npcand 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. A ) -> ( ( ( F ` z ) - ( F ` B ) ) + ( F ` B ) ) = ( F ` z ) )
106 105 mpteq2dva 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( z e. A |-> ( ( ( F ` z ) - ( F ` B ) ) + ( F ` B ) ) ) = ( z e. A |-> ( F ` z ) ) )
107 3 feqmptd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> F = ( z e. A |-> ( F ` z ) ) )
108 106 107 eqtr4d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( z e. A |-> ( ( ( F ` z ) - ( F ` B ) ) + ( F ` B ) ) ) = F )
109 108 oveq1d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( ( z e. A |-> ( ( ( F ` z ) - ( F ` B ) ) + ( F ` B ) ) ) limCC B ) = ( F limCC B ) )
110 103 104 109 3eltr3d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( F ` B ) e. ( F limCC B ) )
111 2 1 cnplimc 
 |-  ( ( A C_ CC /\ B e. A ) -> ( F e. ( ( J CnP K ) ` B ) <-> ( F : A --> CC /\ ( F ` B ) e. ( F limCC B ) ) ) )
112 38 29 111 syl2anc 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( F e. ( ( J CnP K ) ` B ) <-> ( F : A --> CC /\ ( F ` B ) e. ( F limCC B ) ) ) )
113 3 110 112 mpbir2and 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> F e. ( ( J CnP K ) ` B ) )
114 113 ex 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> ( B ( S _D F ) y -> F e. ( ( J CnP K ) ` B ) ) )
115 114 exlimdv 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> ( E. y B ( S _D F ) y -> F e. ( ( J CnP K ) ` B ) ) )
116 eldmg 
 |-  ( B e. dom ( S _D F ) -> ( B e. dom ( S _D F ) <-> E. y B ( S _D F ) y ) )
117 116 ibi 
 |-  ( B e. dom ( S _D F ) -> E. y B ( S _D F ) y )
118 115 117 impel 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B e. dom ( S _D F ) ) -> F e. ( ( J CnP K ) ` B ) )