Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  iscnp4 Unicode version

Theorem iscnp4 12413
 Description: The predicate "the class 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 12402 . . . . . 6 TopOn TopOn
213expa 1181 . . . . 5 TopOn TopOn
323adantl3 1139 . . . 4 TopOn TopOn
4 simpll1 1020 . . . . . . 7 TopOn TopOn TopOn
5 simpll2 1021 . . . . . . 7 TopOn TopOn TopOn
6 simpll3 1022 . . . . . . 7 TopOn TopOn
7 simplr 519 . . . . . . 7 TopOn TopOn
8 topontop 12207 . . . . . . . . 9 TopOn
95, 8syl 14 . . . . . . . 8 TopOn TopOn
10 eqid 2139 . . . . . . . . . 10
1110neii1 12342 . . . . . . . . 9
129, 11sylancom 416 . . . . . . . 8 TopOn TopOn
1310ntropn 12312 . . . . . . . 8
149, 12, 13syl2anc 408 . . . . . . 7 TopOn TopOn
15 simpr 109 . . . . . . . . 9 TopOn TopOn
163adantr 274 . . . . . . . . . . . . 13 TopOn TopOn
1716, 6ffvelrnd 5559 . . . . . . . . . . . 12 TopOn TopOn
18 toponuni 12208 . . . . . . . . . . . . 13 TopOn
195, 18syl 14 . . . . . . . . . . . 12 TopOn TopOn
2017, 19eleqtrd 2218 . . . . . . . . . . 11 TopOn TopOn
2120snssd 3668 . . . . . . . . . 10 TopOn TopOn
2210neiint 12340 . . . . . . . . . 10
239, 21, 12, 22syl3anc 1216 . . . . . . . . 9 TopOn TopOn
2415, 23mpbid 146 . . . . . . . 8 TopOn TopOn
25 fvexg 5443 . . . . . . . . . 10
267, 6, 25syl2anc 408 . . . . . . . . 9 TopOn TopOn
27 snssg 3659 . . . . . . . . 9
2826, 27syl 14 . . . . . . . 8 TopOn TopOn
2924, 28mpbird 166 . . . . . . 7 TopOn TopOn
30 icnpimaex 12406 . . . . . . 7 TopOn TopOn
314, 5, 6, 7, 14, 29, 30syl33anc 1231 . . . . . 6 TopOn TopOn
32 simpl1 984 . . . . . . . . 9 TopOn TopOn TopOn
3332ad2antrr 479 . . . . . . . 8 TopOn TopOn TopOn
34 topontop 12207 . . . . . . . 8 TopOn
3533, 34syl 14 . . . . . . 7 TopOn TopOn
36 simprl 520 . . . . . . 7 TopOn TopOn
37 simprrl 528 . . . . . . 7 TopOn TopOn
38 opnneip 12354 . . . . . . 7
3935, 36, 37, 38syl3anc 1216 . . . . . 6 TopOn TopOn
40 simprrr 529 . . . . . . 7 TopOn TopOn
4110ntrss2 12316 . . . . . . . . 9
429, 12, 41syl2anc 408 . . . . . . . 8 TopOn TopOn
4342adantr 274 . . . . . . 7 TopOn TopOn
4440, 43sstrd 3107 . . . . . 6 TopOn TopOn
4531, 39, 44reximssdv 2536 . . . . 5 TopOn TopOn
4645ralrimiva 2505 . . . 4 TopOn TopOn
473, 46jca 304 . . 3 TopOn TopOn
4847ex 114 . 2 TopOn TopOn
49 simpll2 1021 . . . . . . . . . . 11 TopOn TopOn TopOn
5049, 8syl 14 . . . . . . . . . 10 TopOn TopOn
51 simprl 520 . . . . . . . . . 10 TopOn TopOn
52 simprr 521 . . . . . . . . . 10 TopOn TopOn
53 opnneip 12354 . . . . . . . . . 10
5450, 51, 52, 53syl3anc 1216 . . . . . . . . 9 TopOn TopOn
55 simpl1 984 . . . . . . . . . . . . . 14 TopOn TopOn TopOn
5655ad2antrr 479 . . . . . . . . . . . . 13 TopOn TopOn TopOn
5756, 34syl 14 . . . . . . . . . . . 12 TopOn TopOn
58 simprl 520 . . . . . . . . . . . . 13 TopOn TopOn
59 eqid 2139 . . . . . . . . . . . . . 14
6059neii1 12342 . . . . . . . . . . . . 13
6157, 58, 60syl2anc 408 . . . . . . . . . . . 12 TopOn TopOn
6259ntropn 12312 . . . . . . . . . . . 12
6357, 61, 62syl2anc 408 . . . . . . . . . . 11 TopOn TopOn
64 simpll3 1022 . . . . . . . . . . . . . . . . 17 TopOn TopOn
6564adantr 274 . . . . . . . . . . . . . . . 16 TopOn TopOn
66 toponuni 12208 . . . . . . . . . . . . . . . . 17 TopOn
6756, 66syl 14 . . . . . . . . . . . . . . . 16 TopOn TopOn
6865, 67eleqtrd 2218 . . . . . . . . . . . . . . 15 TopOn TopOn
6968snssd 3668 . . . . . . . . . . . . . 14 TopOn TopOn
7059neiint 12340 . . . . . . . . . . . . . 14
7157, 69, 61, 70syl3anc 1216 . . . . . . . . . . . . 13 TopOn TopOn
7258, 71mpbid 146 . . . . . . . . . . . 12 TopOn TopOn
73 snssg 3659 . . . . . . . . . . . . 13
7465, 73syl 14 . . . . . . . . . . . 12 TopOn TopOn
7572, 74mpbird 166 . . . . . . . . . . 11 TopOn TopOn
7659ntrss2 12316 . . . . . . . . . . . . . 14
7757, 61, 76syl2anc 408 . . . . . . . . . . . . 13 TopOn TopOn
78 imass2 4918 . . . . . . . . . . . . 13
7977, 78syl 14 . . . . . . . . . . . 12 TopOn TopOn
80 simprr 521 . . . . . . . . . . . 12 TopOn TopOn
8179, 80sstrd 3107 . . . . . . . . . . 11 TopOn TopOn
82 eleq2 2203 . . . . . . . . . . . . 13
83 imaeq2 4880 . . . . . . . . . . . . . 14
8483sseq1d 3126 . . . . . . . . . . . . 13
8582, 84anbi12d 464 . . . . . . . . . . . 12
8685rspcev 2789 . . . . . . . . . . 11
8763, 75, 81, 86syl12anc 1214 . . . . . . . . . 10 TopOn TopOn
8887rexlimdvaa 2550 . . . . . . . . 9 TopOn TopOn
8954, 88embantd 56 . . . . . . . 8 TopOn TopOn
9089ex 114 . . . . . . 7 TopOn TopOn
9190com23 78 . . . . . 6 TopOn TopOn
9291exp4a 363 . . . . 5 TopOn TopOn
9392ralimdv2 2502 . . . 4 TopOn TopOn
9493imdistanda 444 . . 3 TopOn TopOn
95 iscnp 12394 . . 3 TopOn TopOn
9694, 95sylibrd 168 . 2 TopOn TopOn
9748, 96impbid 128 1 TopOn TopOn
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104   w3a 962   wceq 1331   wcel 1480  wral 2416  wrex 2417  cvv 2686   wss 3071  csn 3527  cuni 3739  cima 4545  wf 5122  cfv 5126  (class class class)co 5777  ctop 12190  TopOnctopon 12203  cnt 12288  cnei 12333   ccnp 12381 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4046  ax-sep 4049  ax-pow 4101  ax-pr 4134  ax-un 4358  ax-setind 4455 This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3740  df-iun 3818  df-br 3933  df-opab 3993  df-mpt 3994  df-id 4218  df-xp 4548  df-rel 4549  df-cnv 4550  df-co 4551  df-dm 4552  df-rn 4553  df-res 4554  df-ima 4555  df-iota 5091  df-fun 5128  df-fn 5129  df-f 5130  df-f1 5131  df-fo 5132  df-f1o 5133  df-fv 5134  df-ov 5780  df-oprab 5781  df-mpo 5782  df-1st 6041  df-2nd 6042  df-map 6547  df-top 12191  df-topon 12204  df-ntr 12291  df-nei 12334  df-cnp 12384 This theorem is referenced by:  cnnei  12427
 Copyright terms: Public domain W3C validator