Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnpflf2 Structured version   Unicode version

Theorem cnpflf2 21007
 Description: is continuous at point iff a limit of when tends to is . Proposition 9 of [BourbakiTop1] p. TG I.50. (Contributed by FL, 29-May-2011.) (Revised by Mario Carneiro, 9-Apr-2015.)
Hypothesis
Ref Expression
cnpflf2.3
Assertion
Ref Expression
cnpflf2 TopOn TopOn

Proof of Theorem cnpflf2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnpf2 20258 . . . . 5 TopOn TopOn
213expa 1206 . . . 4 TopOn TopOn
323adantl3 1164 . . 3 TopOn TopOn
4 simpl1 1009 . . . . 5 TopOn TopOn TopOn
5 simpl3 1011 . . . . 5 TopOn TopOn
6 neiflim 20981 . . . . . 6 TopOn
7 cnpflf2.3 . . . . . . 7
87oveq2i 6314 . . . . . 6
96, 8syl6eleqr 2522 . . . . 5 TopOn
104, 5, 9syl2anc 666 . . . 4 TopOn TopOn
11 simpr 463 . . . 4 TopOn TopOn
12 cnpflfi 21006 . . . 4
1310, 11, 12syl2anc 666 . . 3 TopOn TopOn
143, 13jca 535 . 2 TopOn TopOn
15 simpl1 1009 . . . . . . . . . . . 12 TopOn TopOn TopOn
16 topontop 19933 . . . . . . . . . . . 12 TopOn
1715, 16syl 17 . . . . . . . . . . 11 TopOn TopOn
18 simpl3 1011 . . . . . . . . . . . 12 TopOn TopOn
19 toponuni 19934 . . . . . . . . . . . . 13 TopOn
2015, 19syl 17 . . . . . . . . . . . 12 TopOn TopOn
2118, 20eleqtrd 2513 . . . . . . . . . . 11 TopOn TopOn
227eleq2i 2501 . . . . . . . . . . . 12
23 eqid 2423 . . . . . . . . . . . . 13
2423isneip 20113 . . . . . . . . . . . 12
2522, 24syl5bb 261 . . . . . . . . . . 11
2617, 21, 25syl2anc 666 . . . . . . . . . 10 TopOn TopOn
27 imass2 5221 . . . . . . . . . . . . . . 15
28 sstr2 3472 . . . . . . . . . . . . . . . 16
2928com12 33 . . . . . . . . . . . . . . 15
3027, 29syl5 34 . . . . . . . . . . . . . 14
3130anim2d 568 . . . . . . . . . . . . 13
3231reximdv 2900 . . . . . . . . . . . 12
3332com12 33 . . . . . . . . . . 11
3433adantl 468 . . . . . . . . . 10
3526, 34syl6bi 232 . . . . . . . . 9 TopOn TopOn
3635rexlimdv 2916 . . . . . . . 8 TopOn TopOn
3736imim2d 55 . . . . . . 7 TopOn TopOn
3837ralimdv 2836 . . . . . 6 TopOn TopOn
39 simpr 463 . . . . . 6 TopOn TopOn
4038, 39jctild 546 . . . . 5 TopOn TopOn
4140adantld 469 . . . 4 TopOn TopOn
42 simpl2 1010 . . . . 5 TopOn TopOn TopOn
4318snssd 4143 . . . . . . 7 TopOn TopOn
44 snnzg 4115 . . . . . . . 8
4518, 44syl 17 . . . . . . 7 TopOn TopOn
46 neifil 20887 . . . . . . 7 TopOn
4715, 43, 45, 46syl3anc 1265 . . . . . 6 TopOn TopOn
487, 47syl5eqel 2515 . . . . 5 TopOn TopOn
49 isflf 21000 . . . . 5 TopOn
5042, 48, 39, 49syl3anc 1265 . . . 4 TopOn TopOn
51 iscnp 20245 . . . . 5 TopOn TopOn
5251adantr 467 . . . 4 TopOn TopOn
5341, 50, 523imtr4d 272 . . 3 TopOn TopOn
5453impr 624 . 2 TopOn TopOn
5514, 54impbida 841 1 TopOn TopOn
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   w3a 983   wceq 1438   wcel 1869   wne 2619  wral 2776  wrex 2777   wss 3437  c0 3762  csn 3997  cuni 4217  cima 4854  wf 5595  cfv 5599  (class class class)co 6303  ctop 19909  TopOnctopon 19910  cnei 20105   ccnp 20233  cfil 20852   cflim 20941   cflf 20942 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-rep 4534  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-op 4004  df-uni 4218  df-iun 4299  df-br 4422  df-opab 4481  df-mpt 4482  df-id 4766  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-ov 6306  df-oprab 6307  df-mpt2 6308  df-1st 6805  df-2nd 6806  df-map 7480  df-fbas 18960  df-fg 18961  df-top 19913  df-topon 19915  df-ntr 20027  df-nei 20106  df-cnp 20236  df-fil 20853  df-fm 20945  df-flim 20946  df-flf 20947 This theorem is referenced by:  cnpflf  21008
 Copyright terms: Public domain W3C validator