Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mndpluscn Structured version   Unicode version

Theorem mndpluscn 26494
 Description: A mapping that is both a homeomorphism and a monoid homomorphism preserves the "continuousness" of the operation. (Contributed by Thierry Arnoux, 25-Mar-2017.)
Hypotheses
Ref Expression
mndpluscn.f
mndpluscn.p
mndpluscn.t
mndpluscn.j TopOn
mndpluscn.k TopOn
mndpluscn.h
mndpluscn.o
Assertion
Ref Expression
mndpluscn
Distinct variable groups:   , ,   ,   ,   ,   ,,   ,
Allowed substitution hints:   (,)   (,)   (,)

Proof of Theorem mndpluscn
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mndpluscn.t . . . 4
2 ffn 5660 . . . 4
3 fnov 6301 . . . . 5
43biimpi 194 . . . 4
51, 2, 4mp2b 10 . . 3
6 mndpluscn.f . . . . . . . . 9
7 mndpluscn.j . . . . . . . . . . 11 TopOn
87toponunii 18662 . . . . . . . . . 10
9 mndpluscn.k . . . . . . . . . . 11 TopOn
109toponunii 18662 . . . . . . . . . 10
118, 10hmeof1o 19462 . . . . . . . . 9
126, 11ax-mp 5 . . . . . . . 8
13 f1ocnvdm 6091 . . . . . . . 8
1412, 13mpan 670 . . . . . . 7
15 f1ocnvdm 6091 . . . . . . . 8
1612, 15mpan 670 . . . . . . 7
1714, 16anim12i 566 . . . . . 6
18 mndpluscn.h . . . . . . 7
1918rgen2a 2893 . . . . . 6
20 oveq1 6200 . . . . . . . . 9
2120fveq2d 5796 . . . . . . . 8
22 fveq2 5792 . . . . . . . . 9
2322oveq1d 6208 . . . . . . . 8
2421, 23eqeq12d 2473 . . . . . . 7
25 oveq2 6201 . . . . . . . . 9
2625fveq2d 5796 . . . . . . . 8
27 fveq2 5792 . . . . . . . . 9
2827oveq2d 6209 . . . . . . . 8
2926, 28eqeq12d 2473 . . . . . . 7
3024, 29rspc2va 3180 . . . . . 6
3117, 19, 30sylancl 662 . . . . 5
32 f1ocnvfv2 6086 . . . . . . 7
3312, 32mpan 670 . . . . . 6
34 f1ocnvfv2 6086 . . . . . . 7
3512, 34mpan 670 . . . . . 6
3633, 35oveqan12d 6212 . . . . 5
3731, 36eqtr2d 2493 . . . 4
3837mpt2eq3ia 6253 . . 3
395, 38eqtri 2480 . 2
409a1i 11 . . . 4 TopOn
4140, 40cnmpt1st 19366 . . . . . 6
42 hmeocnvcn 19459 . . . . . . 7
436, 42mp1i 12 . . . . . 6
4440, 40, 41, 43cnmpt21f 19370 . . . . 5
4540, 40cnmpt2nd 19367 . . . . . 6
4640, 40, 45, 43cnmpt21f 19370 . . . . 5
47 mndpluscn.o . . . . . 6
4847a1i 11 . . . . 5
4940, 40, 44, 46, 48cnmpt22f 19373 . . . 4
50 hmeocn 19458 . . . . 5
516, 50mp1i 12 . . . 4
5240, 40, 49, 51cnmpt21f 19370 . . 3
5352trud 1379 . 2
5439, 53eqeltri 2535 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   wceq 1370   wtru 1371   wcel 1758  wral 2795   cxp 4939  ccnv 4940   wfn 5514  wf 5515  wf1o 5518  cfv 5519  (class class class)co 6193   cmpt2 6195  TopOnctopon 18624   ccn 18953   ctx 19258  chmeo 19451 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4514  ax-nul 4522  ax-pow 4571  ax-pr 4632  ax-un 6475 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3073  df-sbc 3288  df-csb 3390  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-pw 3963  df-sn 3979  df-pr 3981  df-op 3985  df-uni 4193  df-iun 4274  df-br 4394  df-opab 4452  df-mpt 4453  df-id 4737  df-xp 4947  df-rel 4948  df-cnv 4949  df-co 4950  df-dm 4951  df-rn 4952  df-res 4953  df-ima 4954  df-iota 5482  df-fun 5521  df-fn 5522  df-f 5523  df-f1 5524  df-fo 5525  df-f1o 5526  df-fv 5527  df-ov 6196  df-oprab 6197  df-mpt2 6198  df-1st 6680  df-2nd 6681  df-map 7319  df-topgen 14493  df-top 18628  df-bases 18630  df-topon 18631  df-cn 18956  df-tx 19260  df-hmeo 19453 This theorem is referenced by:  mhmhmeotmd  26495  xrge0pluscn  26508
 Copyright terms: Public domain W3C validator