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

Theorem cnpflf2 18015
 Description: is continous 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 17297 . . . . 5 TopOn TopOn
213expa 1153 . . . 4 TopOn TopOn
323adantl3 1115 . . 3 TopOn TopOn
4 simpl1 960 . . . . 5 TopOn TopOn TopOn
5 simpl3 962 . . . . 5 TopOn TopOn
6 neiflim 17989 . . . . . 6 TopOn
7 cnpflf2.3 . . . . . . 7
87oveq2i 6078 . . . . . 6
96, 8syl6eleqr 2521 . . . . 5 TopOn
104, 5, 9syl2anc 643 . . . 4 TopOn TopOn
11 simpr 448 . . . 4 TopOn TopOn
12 cnpflfi 18014 . . . 4
1310, 11, 12syl2anc 643 . . 3 TopOn TopOn
143, 13jca 519 . 2 TopOn TopOn
15 simpl1 960 . . . . . . . . . . . 12 TopOn TopOn TopOn
16 topontop 16974 . . . . . . . . . . . 12 TopOn
1715, 16syl 16 . . . . . . . . . . 11 TopOn TopOn
18 simpl3 962 . . . . . . . . . . . 12 TopOn TopOn
19 toponuni 16975 . . . . . . . . . . . . 13 TopOn
2015, 19syl 16 . . . . . . . . . . . 12 TopOn TopOn
2118, 20eleqtrd 2506 . . . . . . . . . . 11 TopOn TopOn
227eleq2i 2494 . . . . . . . . . . . 12
23 eqid 2430 . . . . . . . . . . . . 13
2423isneip 17152 . . . . . . . . . . . 12
2522, 24syl5bb 249 . . . . . . . . . . 11
2617, 21, 25syl2anc 643 . . . . . . . . . 10 TopOn TopOn
27 imass2 5226 . . . . . . . . . . . . . . 15
28 sstr2 3342 . . . . . . . . . . . . . . . 16
2928com12 29 . . . . . . . . . . . . . . 15
3027, 29syl5 30 . . . . . . . . . . . . . 14
3130anim2d 549 . . . . . . . . . . . . 13
3231reximdv 2804 . . . . . . . . . . . 12
3332com12 29 . . . . . . . . . . 11
3433adantl 453 . . . . . . . . . 10
3526, 34syl6bi 220 . . . . . . . . 9 TopOn TopOn
3635rexlimdv 2816 . . . . . . . 8 TopOn TopOn
3736imim2d 50 . . . . . . 7 TopOn TopOn
3837ralimdv 2772 . . . . . 6 TopOn TopOn
39 simpr 448 . . . . . 6 TopOn TopOn
4038, 39jctild 528 . . . . 5 TopOn TopOn
4140adantld 454 . . . 4 TopOn TopOn
42 simpl2 961 . . . . 5 TopOn TopOn TopOn
4318snssd 3930 . . . . . . 7 TopOn TopOn
44 snnzg 3908 . . . . . . . 8
4518, 44syl 16 . . . . . . 7 TopOn TopOn
46 neifil 17895 . . . . . . 7 TopOn
4715, 43, 45, 46syl3anc 1184 . . . . . 6 TopOn TopOn
487, 47syl5eqel 2514 . . . . 5 TopOn TopOn
49 isflf 18008 . . . . 5 TopOn
5042, 48, 39, 49syl3anc 1184 . . . 4 TopOn TopOn
51 iscnp 17284 . . . . 5 TopOn TopOn
5251adantr 452 . . . 4 TopOn TopOn
5341, 50, 523imtr4d 260 . . 3 TopOn TopOn
5453impr 603 . 2 TopOn TopOn
5514, 54impbida 806 1 TopOn TopOn
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   w3a 936   wceq 1652   wcel 1725   wne 2593  wral 2692  wrex 2693   wss 3307  c0 3615  csn 3801  cuni 4002  cima 4867  wf 5436  cfv 5440  (class class class)co 6067  ctop 16941  TopOnctopon 16942  cnei 17144   ccnp 17272  cfil 17860   cflim 17949   cflf 17950 This theorem is referenced by:  cnpflf  18016 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411  ax-rep 4307  ax-sep 4317  ax-nul 4325  ax-pow 4364  ax-pr 4390  ax-un 4687 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-ne 2595  df-nel 2596  df-ral 2697  df-rex 2698  df-reu 2699  df-rab 2701  df-v 2945  df-sbc 3149  df-csb 3239  df-dif 3310  df-un 3312  df-in 3314  df-ss 3321  df-nul 3616  df-if 3727  df-pw 3788  df-sn 3807  df-pr 3808  df-op 3810  df-uni 4003  df-iun 4082  df-br 4200  df-opab 4254  df-mpt 4255  df-id 4485  df-xp 4870  df-rel 4871  df-cnv 4872  df-co 4873  df-dm 4874  df-rn 4875  df-res 4876  df-ima 4877  df-iota 5404  df-fun 5442  df-fn 5443  df-f 5444  df-f1 5445  df-fo 5446  df-f1o 5447  df-fv 5448  df-ov 6070  df-oprab 6071  df-mpt2 6072  df-1st 6335  df-2nd 6336  df-map 7006  df-fbas 16682  df-fg 16683  df-top 16946  df-topon 16949  df-ntr 17067  df-nei 17145  df-cnp 17275  df-fil 17861  df-fm 17953  df-flim 17954  df-flf 17955
 Copyright terms: Public domain W3C validator