Metamath Proof Explorer


Theorem cnpflf2

Description: F is continuous at point A iff a limit of F when x tends to A is ( FA ) . Proposition 9 of BourbakiTop1 p. TG I.50. (Contributed by FL, 29-May-2011) (Revised by Mario Carneiro, 9-Apr-2015)

Ref Expression
Hypothesis cnpflf2.3 L = nei J A
Assertion cnpflf2 J TopOn X K TopOn Y A X F J CnP K A F : X Y F A K fLimf L F

Proof

Step Hyp Ref Expression
1 cnpflf2.3 L = nei J A
2 cnpf2 J TopOn X K TopOn Y F J CnP K A F : X Y
3 2 3expa J TopOn X K TopOn Y F J CnP K A F : X Y
4 3 3adantl3 J TopOn X K TopOn Y A X F J CnP K A F : X Y
5 simpl1 J TopOn X K TopOn Y A X F J CnP K A J TopOn X
6 simpl3 J TopOn X K TopOn Y A X F J CnP K A A X
7 neiflim J TopOn X A X A J fLim nei J A
8 1 oveq2i J fLim L = J fLim nei J A
9 7 8 eleqtrrdi J TopOn X A X A J fLim L
10 5 6 9 syl2anc J TopOn X K TopOn Y A X F J CnP K A A J fLim L
11 simpr J TopOn X K TopOn Y A X F J CnP K A F J CnP K A
12 cnpflfi A J fLim L F J CnP K A F A K fLimf L F
13 10 11 12 syl2anc J TopOn X K TopOn Y A X F J CnP K A F A K fLimf L F
14 4 13 jca J TopOn X K TopOn Y A X F J CnP K A F : X Y F A K fLimf L F
15 simpl1 J TopOn X K TopOn Y A X F : X Y J TopOn X
16 topontop J TopOn X J Top
17 15 16 syl J TopOn X K TopOn Y A X F : X Y J Top
18 simpl3 J TopOn X K TopOn Y A X F : X Y A X
19 toponuni J TopOn X X = J
20 15 19 syl J TopOn X K TopOn Y A X F : X Y X = J
21 18 20 eleqtrd J TopOn X K TopOn Y A X F : X Y A J
22 1 eleq2i z L z nei J A
23 eqid J = J
24 23 isneip J Top A J z nei J A z J v J A v v z
25 22 24 syl5bb J Top A J z L z J v J A v v z
26 17 21 25 syl2anc J TopOn X K TopOn Y A X F : X Y z L z J v J A v v z
27 sstr2 F v F z F z u F v u
28 imass2 v z F v F z
29 27 28 syl11 F z u v z F v u
30 29 anim2d F z u A v v z A v F v u
31 30 reximdv F z u v J A v v z v J A v F v u
32 31 com12 v J A v v z F z u v J A v F v u
33 32 adantl z J v J A v v z F z u v J A v F v u
34 26 33 syl6bi J TopOn X K TopOn Y A X F : X Y z L F z u v J A v F v u
35 34 rexlimdv J TopOn X K TopOn Y A X F : X Y z L F z u v J A v F v u
36 35 imim2d J TopOn X K TopOn Y A X F : X Y F A u z L F z u F A u v J A v F v u
37 36 ralimdv J TopOn X K TopOn Y A X F : X Y u K F A u z L F z u u K F A u v J A v F v u
38 simpr J TopOn X K TopOn Y A X F : X Y F : X Y
39 37 38 jctild J TopOn X K TopOn Y A X F : X Y u K F A u z L F z u F : X Y u K F A u v J A v F v u
40 39 adantld J TopOn X K TopOn Y A X F : X Y F A Y u K F A u z L F z u F : X Y u K F A u v J A v F v u
41 simpl2 J TopOn X K TopOn Y A X F : X Y K TopOn Y
42 18 snssd J TopOn X K TopOn Y A X F : X Y A X
43 18 snn0d J TopOn X K TopOn Y A X F : X Y A
44 neifil J TopOn X A X A nei J A Fil X
45 15 42 43 44 syl3anc J TopOn X K TopOn Y A X F : X Y nei J A Fil X
46 1 45 eqeltrid J TopOn X K TopOn Y A X F : X Y L Fil X
47 isflf K TopOn Y L Fil X F : X Y F A K fLimf L F F A Y u K F A u z L F z u
48 41 46 38 47 syl3anc J TopOn X K TopOn Y A X F : X Y F A K fLimf L F F A Y u K F A u z L F z u
49 iscnp J TopOn X K TopOn Y A X F J CnP K A F : X Y u K F A u v J A v F v u
50 49 adantr J TopOn X K TopOn Y A X F : X Y F J CnP K A F : X Y u K F A u v J A v F v u
51 40 48 50 3imtr4d J TopOn X K TopOn Y A X F : X Y F A K fLimf L F F J CnP K A
52 51 impr J TopOn X K TopOn Y A X F : X Y F A K fLimf L F F J CnP K A
53 14 52 impbida J TopOn X K TopOn Y A X F J CnP K A F : X Y F A K fLimf L F