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

Theorem iscnp4 17332
 Description: The predicate " is a continuous function from topology to topology at point ." in terms of neighborhoods. (Contributed by FL, 18-Jul-2011.) (Revised by Mario Carneiro, 10-Sep-2015.)
Assertion
Ref Expression
iscnp4 TopOn TopOn
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,   ,,

Proof of Theorem iscnp4
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 cnpf2 17319 . . . . . 6 TopOn TopOn
213expa 1154 . . . . 5 TopOn TopOn
323adantl3 1116 . . . 4 TopOn TopOn
4 simplr 733 . . . . . . 7 TopOn TopOn
5 simpll2 998 . . . . . . . . 9 TopOn TopOn TopOn
6 topontop 16996 . . . . . . . . 9 TopOn
75, 6syl 16 . . . . . . . 8 TopOn TopOn
8 eqid 2438 . . . . . . . . . 10
98neii1 17175 . . . . . . . . 9
107, 9sylancom 650 . . . . . . . 8 TopOn TopOn
118ntropn 17118 . . . . . . . 8
127, 10, 11syl2anc 644 . . . . . . 7 TopOn TopOn
13 simpr 449 . . . . . . . . 9 TopOn TopOn
143adantr 453 . . . . . . . . . . . . 13 TopOn TopOn
15 simpll3 999 . . . . . . . . . . . . 13 TopOn TopOn
1614, 15ffvelrnd 5874 . . . . . . . . . . . 12 TopOn TopOn
17 toponuni 16997 . . . . . . . . . . . . 13 TopOn
185, 17syl 16 . . . . . . . . . . . 12 TopOn TopOn
1916, 18eleqtrd 2514 . . . . . . . . . . 11 TopOn TopOn
2019snssd 3945 . . . . . . . . . 10 TopOn TopOn
218neiint 17173 . . . . . . . . . 10
227, 20, 10, 21syl3anc 1185 . . . . . . . . 9 TopOn TopOn
2313, 22mpbid 203 . . . . . . . 8 TopOn TopOn
24 fvex 5745 . . . . . . . . 9
2524snss 3928 . . . . . . . 8
2623, 25sylibr 205 . . . . . . 7 TopOn TopOn
27 cnpimaex 17325 . . . . . . 7
284, 12, 26, 27syl3anc 1185 . . . . . 6 TopOn TopOn
29 simpl1 961 . . . . . . . . . . . 12 TopOn TopOn TopOn
3029ad2antrr 708 . . . . . . . . . . 11 TopOn TopOn TopOn
31 topontop 16996 . . . . . . . . . . 11 TopOn
3230, 31syl 16 . . . . . . . . . 10 TopOn TopOn
33 simprl 734 . . . . . . . . . 10 TopOn TopOn
34 simprrl 742 . . . . . . . . . 10 TopOn TopOn
35 opnneip 17188 . . . . . . . . . 10
3632, 33, 34, 35syl3anc 1185 . . . . . . . . 9 TopOn TopOn
37 simprrr 743 . . . . . . . . . 10 TopOn TopOn
388ntrss2 17126 . . . . . . . . . . . 12
397, 10, 38syl2anc 644 . . . . . . . . . . 11 TopOn TopOn
4039adantr 453 . . . . . . . . . 10 TopOn TopOn
4137, 40sstrd 3360 . . . . . . . . 9 TopOn TopOn
4236, 41jca 520 . . . . . . . 8 TopOn TopOn
4342ex 425 . . . . . . 7 TopOn TopOn
4443reximdv2 2817 . . . . . 6 TopOn TopOn
4528, 44mpd 15 . . . . 5 TopOn TopOn
4645ralrimiva 2791 . . . 4 TopOn TopOn
473, 46jca 520 . . 3 TopOn TopOn
4847ex 425 . 2 TopOn TopOn
49 simpll2 998 . . . . . . . . . . 11 TopOn TopOn TopOn
5049, 6syl 16 . . . . . . . . . 10 TopOn TopOn
51 simprl 734 . . . . . . . . . 10 TopOn TopOn
52 simprr 735 . . . . . . . . . 10 TopOn TopOn
53 opnneip 17188 . . . . . . . . . 10
5450, 51, 52, 53syl3anc 1185 . . . . . . . . 9 TopOn TopOn
55 simpl1 961 . . . . . . . . . . . . . 14 TopOn TopOn TopOn
5655ad2antrr 708 . . . . . . . . . . . . 13 TopOn TopOn TopOn
5756, 31syl 16 . . . . . . . . . . . 12 TopOn TopOn
58 simprl 734 . . . . . . . . . . . . 13 TopOn TopOn
59 eqid 2438 . . . . . . . . . . . . . 14
6059neii1 17175 . . . . . . . . . . . . 13
6157, 58, 60syl2anc 644 . . . . . . . . . . . 12 TopOn TopOn
6259ntropn 17118 . . . . . . . . . . . 12
6357, 61, 62syl2anc 644 . . . . . . . . . . 11 TopOn TopOn
64 simpll3 999 . . . . . . . . . . . . . . . . 17 TopOn TopOn
6564adantr 453 . . . . . . . . . . . . . . . 16 TopOn TopOn
66 toponuni 16997 . . . . . . . . . . . . . . . . 17 TopOn
6756, 66syl 16 . . . . . . . . . . . . . . . 16 TopOn TopOn
6865, 67eleqtrd 2514 . . . . . . . . . . . . . . 15 TopOn TopOn
6968snssd 3945 . . . . . . . . . . . . . 14 TopOn TopOn
7059neiint 17173 . . . . . . . . . . . . . 14
7157, 69, 61, 70syl3anc 1185 . . . . . . . . . . . . 13 TopOn TopOn
7258, 71mpbid 203 . . . . . . . . . . . 12 TopOn TopOn
73 snssg 3934 . . . . . . . . . . . . 13
7465, 73syl 16 . . . . . . . . . . . 12 TopOn TopOn
7572, 74mpbird 225 . . . . . . . . . . 11 TopOn TopOn
7659ntrss2 17126 . . . . . . . . . . . . . 14
7757, 61, 76syl2anc 644 . . . . . . . . . . . . 13 TopOn TopOn
78 imass2 5243 . . . . . . . . . . . . 13
7977, 78syl 16 . . . . . . . . . . . 12 TopOn TopOn
80 simprr 735 . . . . . . . . . . . 12 TopOn TopOn
8179, 80sstrd 3360 . . . . . . . . . . 11 TopOn TopOn
82 eleq2 2499 . . . . . . . . . . . . 13
83 imaeq2 5202 . . . . . . . . . . . . . 14
8483sseq1d 3377 . . . . . . . . . . . . 13
8582, 84anbi12d 693 . . . . . . . . . . . 12
8685rspcev 3054 . . . . . . . . . . 11
8763, 75, 81, 86syl12anc 1183 . . . . . . . . . 10 TopOn TopOn
8887rexlimdvaa 2833 . . . . . . . . 9 TopOn TopOn
8954, 88embantd 53 . . . . . . . 8 TopOn TopOn
9089ex 425 . . . . . . 7 TopOn TopOn
9190com23 75 . . . . . 6 TopOn TopOn
9291exp4a 591 . . . . 5 TopOn TopOn
9392ralimdv2 2788 . . . 4 TopOn TopOn
9493imdistanda 676 . . 3 TopOn TopOn
95 iscnp 17306 . . 3 TopOn TopOn
9694, 95sylibrd 227 . 2 TopOn TopOn
9748, 96impbid 185 1 TopOn TopOn
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wa 360   w3a 937   wceq 1653   wcel 1726  wral 2707  wrex 2708   wss 3322  csn 3816  cuni 4017  cima 4884  wf 5453  cfv 5457  (class class class)co 6084  ctop 16963  TopOnctopon 16964  cnt 17086  cnei 17166   ccnp 17294 This theorem is referenced by:  cnnei  17351 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4323  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-iun 4097  df-br 4216  df-opab 4270  df-mpt 4271  df-id 4501  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-1st 6352  df-2nd 6353  df-map 7023  df-top 16968  df-topon 16971  df-ntr 17089  df-nei 17167  df-cnp 17297
 Copyright terms: Public domain W3C validator