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

Theorem cnconst2 12461
 Description: A constant function is continuous. (Contributed by Mario Carneiro, 19-Mar-2015.)
Assertion
Ref Expression
cnconst2 TopOn TopOn

Proof of Theorem cnconst2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fconst6g 5330 . . 3
213ad2ant3 1005 . 2 TopOn TopOn
32adantr 274 . . . 4 TopOn TopOn
4 simpll3 1023 . . . . . . . 8 TopOn TopOn
5 simplr 520 . . . . . . . 8 TopOn TopOn
6 fvconst2g 5643 . . . . . . . 8
74, 5, 6syl2anc 409 . . . . . . 7 TopOn TopOn
87eleq1d 2209 . . . . . 6 TopOn TopOn
9 simpll1 1021 . . . . . . . . 9 TopOn TopOn TopOn
10 toponmax 12251 . . . . . . . . 9 TopOn
119, 10syl 14 . . . . . . . 8 TopOn TopOn
12 simplr 520 . . . . . . . 8 TopOn TopOn
13 df-ima 4561 . . . . . . . . 9
14 ssid 3123 . . . . . . . . . . . . 13
15 xpssres 4863 . . . . . . . . . . . . 13
1614, 15ax-mp 5 . . . . . . . . . . . 12
1716rneqi 4776 . . . . . . . . . . 11
18 rnxpss 4979 . . . . . . . . . . 11
1917, 18eqsstri 3135 . . . . . . . . . 10
20 simprr 522 . . . . . . . . . . 11 TopOn TopOn
2120snssd 3674 . . . . . . . . . 10 TopOn TopOn
2219, 21sstrid 3114 . . . . . . . . 9 TopOn TopOn
2313, 22eqsstrid 3149 . . . . . . . 8 TopOn TopOn
24 eleq2 2204 . . . . . . . . . 10
25 imaeq2 4886 . . . . . . . . . . 11
2625sseq1d 3132 . . . . . . . . . 10
2724, 26anbi12d 465 . . . . . . . . 9
2827rspcev 2794 . . . . . . . 8
2911, 12, 23, 28syl12anc 1215 . . . . . . 7 TopOn TopOn
3029expr 373 . . . . . 6 TopOn TopOn
318, 30sylbid 149 . . . . 5 TopOn TopOn
3231ralrimiva 2509 . . . 4 TopOn TopOn
33 simpl1 985 . . . . 5 TopOn TopOn TopOn
34 simpl2 986 . . . . 5 TopOn TopOn TopOn
35 simpr 109 . . . . 5 TopOn TopOn
36 iscnp 12427 . . . . 5 TopOn TopOn
3733, 34, 35, 36syl3anc 1217 . . . 4 TopOn TopOn
383, 32, 37mpbir2and 929 . . 3 TopOn TopOn
3938ralrimiva 2509 . 2 TopOn TopOn
40 cncnp 12458 . . 3 TopOn TopOn
41403adant3 1002 . 2 TopOn TopOn
422, 39, 41mpbir2and 929 1 TopOn TopOn
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104   w3a 963   wceq 1332   wcel 1481  wral 2417  wrex 2418   wss 3077  csn 3533   cxp 4546   crn 4549   cres 4550  cima 4551  wf 5128  cfv 5132  (class class class)co 5783  TopOnctopon 12236   ccn 12413   ccnp 12414 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 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4052  ax-sep 4055  ax-pow 4107  ax-pr 4140  ax-un 4364  ax-setind 4461 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2692  df-sbc 2915  df-csb 3009  df-dif 3079  df-un 3081  df-in 3083  df-ss 3090  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-iun 3824  df-br 3939  df-opab 3999  df-mpt 4000  df-id 4224  df-xp 4554  df-rel 4555  df-cnv 4556  df-co 4557  df-dm 4558  df-rn 4559  df-res 4560  df-ima 4561  df-iota 5097  df-fun 5134  df-fn 5135  df-f 5136  df-f1 5137  df-fo 5138  df-f1o 5139  df-fv 5140  df-ov 5786  df-oprab 5787  df-mpo 5788  df-1st 6047  df-2nd 6048  df-map 6553  df-topgen 12200  df-top 12224  df-topon 12237  df-cn 12416  df-cnp 12417 This theorem is referenced by:  cnconst  12462  cnmptc  12510
 Copyright terms: Public domain W3C validator