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

Theorem clssubg 21116
 Description: The closure of a subgroup in a topological group is a subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.)
Hypothesis
Ref Expression
subgntr.h
Assertion
Ref Expression
clssubg SubGrp SubGrp

Proof of Theorem clssubg
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 subgntr.h . . . . . . 7
2 eqid 2450 . . . . . . 7
31, 2tgptopon 21090 . . . . . 6 TopOn
43adantr 467 . . . . 5 SubGrp TopOn
5 topontop 19934 . . . . 5 TopOn
64, 5syl 17 . . . 4 SubGrp
72subgss 16811 . . . . . 6 SubGrp
87adantl 468 . . . . 5 SubGrp
9 toponuni 19935 . . . . . 6 TopOn
104, 9syl 17 . . . . 5 SubGrp
118, 10sseqtrd 3467 . . . 4 SubGrp
12 eqid 2450 . . . . 5
1312clsss3 20067 . . . 4
146, 11, 13syl2anc 666 . . 3 SubGrp
1514, 10sseqtr4d 3468 . 2 SubGrp
1612sscls 20064 . . . 4
176, 11, 16syl2anc 666 . . 3 SubGrp
18 eqid 2450 . . . . . 6
1918subg0cl 16818 . . . . 5 SubGrp
2019adantl 468 . . . 4 SubGrp
21 ne0i 3736 . . . 4
2220, 21syl 17 . . 3 SubGrp
23 ssn0 3766 . . 3
2417, 22, 23syl2anc 666 . 2 SubGrp
25 df-ov 6291 . . . 4
26 opelxpi 4865 . . . . . . 7
27 txcls 20612 . . . . . . . . . 10 TopOn TopOn
284, 4, 8, 8, 27syl22anc 1268 . . . . . . . . 9 SubGrp
29 txtopon 20599 . . . . . . . . . . . . 13 TopOn TopOn TopOn
304, 4, 29syl2anc 666 . . . . . . . . . . . 12 SubGrp TopOn
31 topontop 19934 . . . . . . . . . . . 12 TopOn
3230, 31syl 17 . . . . . . . . . . 11 SubGrp
33 cnvimass 5187 . . . . . . . . . . . . 13
34 tgpgrp 21086 . . . . . . . . . . . . . . . 16
3534adantr 467 . . . . . . . . . . . . . . 15 SubGrp
36 eqid 2450 . . . . . . . . . . . . . . . 16
372, 36grpsubf 16726 . . . . . . . . . . . . . . 15
3835, 37syl 17 . . . . . . . . . . . . . 14 SubGrp
39 fdm 5731 . . . . . . . . . . . . . 14
4038, 39syl 17 . . . . . . . . . . . . 13 SubGrp
4133, 40syl5sseq 3479 . . . . . . . . . . . 12 SubGrp
42 toponuni 19935 . . . . . . . . . . . . 13 TopOn
4330, 42syl 17 . . . . . . . . . . . 12 SubGrp
4441, 43sseqtrd 3467 . . . . . . . . . . 11 SubGrp
4536subgsubcl 16821 . . . . . . . . . . . . . . . 16 SubGrp
46453expb 1208 . . . . . . . . . . . . . . 15 SubGrp
4746ralrimivva 2808 . . . . . . . . . . . . . 14 SubGrp
48 fveq2 5863 . . . . . . . . . . . . . . . . 17
4948, 25syl6eqr 2502 . . . . . . . . . . . . . . . 16
5049eleq1d 2512 . . . . . . . . . . . . . . 15
5150ralxp 4975 . . . . . . . . . . . . . 14
5247, 51sylibr 216 . . . . . . . . . . . . 13 SubGrp
5352adantl 468 . . . . . . . . . . . 12 SubGrp
54 ffun 5729 . . . . . . . . . . . . . 14
5538, 54syl 17 . . . . . . . . . . . . 13 SubGrp
56 xpss12 4939 . . . . . . . . . . . . . . 15
578, 8, 56syl2anc 666 . . . . . . . . . . . . . 14 SubGrp
5857, 40sseqtr4d 3468 . . . . . . . . . . . . 13 SubGrp
59 funimass5 5997 . . . . . . . . . . . . 13
6055, 58, 59syl2anc 666 . . . . . . . . . . . 12 SubGrp
6153, 60mpbird 236 . . . . . . . . . . 11 SubGrp
62 eqid 2450 . . . . . . . . . . . 12
6362clsss 20062 . . . . . . . . . . 11
6432, 44, 61, 63syl3anc 1267 . . . . . . . . . 10 SubGrp
651, 36tgpsubcn 21098 . . . . . . . . . . . 12
6665adantr 467 . . . . . . . . . . 11 SubGrp
6712cncls2i 20279 . . . . . . . . . . 11
6866, 11, 67syl2anc 666 . . . . . . . . . 10 SubGrp
6964, 68sstrd 3441 . . . . . . . . 9 SubGrp
7028, 69eqsstr3d 3466 . . . . . . . 8 SubGrp
7170sselda 3431 . . . . . . 7 SubGrp
7226, 71sylan2 477 . . . . . 6 SubGrp
7334ad2antrr 731 . . . . . . 7 SubGrp
74 ffn 5726 . . . . . . 7
75 elpreima 6000 . . . . . . 7
7673, 37, 74, 754syl 19 . . . . . 6 SubGrp
7772, 76mpbid 214 . . . . 5 SubGrp
7877simprd 465 . . . 4 SubGrp
7925, 78syl5eqel 2532 . . 3 SubGrp
8079ralrimivva 2808 . 2 SubGrp
812, 36issubg4 16829 . . 3 SubGrp
8235, 81syl 17 . 2 SubGrp SubGrp
8315, 24, 80, 82mpbir3and 1190 1 SubGrp SubGrp
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   w3a 984   wceq 1443   wcel 1886   wne 2621  wral 2736   wss 3403  c0 3730  cop 3973  cuni 4197   cxp 4831  ccnv 4832   cdm 4833  cima 4836   wfun 5575   wfn 5576  wf 5577  cfv 5581  (class class class)co 6288  cbs 15114  ctopn 15313  c0g 15331  cgrp 16662  csg 16664  SubGrpcsubg 16804  ctop 19910  TopOnctopon 19911  ccl 20026   ccn 20233   ctx 20568  ctgp 21079 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-cnex 9592  ax-resscn 9593  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-mulcom 9600  ax-addass 9601  ax-mulass 9602  ax-distr 9603  ax-i2m1 9604  ax-1ne0 9605  ax-1rid 9606  ax-rnegex 9607  ax-rrecex 9608  ax-cnre 9609  ax-pre-lttri 9610  ax-pre-lttrn 9611  ax-pre-ltadd 9612  ax-pre-mulgt0 9613 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-int 4234  df-iun 4279  df-iin 4280  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-om 6690  df-1st 6790  df-2nd 6791  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-er 7360  df-map 7471  df-en 7567  df-dom 7568  df-sdom 7569  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-sub 9859  df-neg 9860  df-nn 10607  df-2 10665  df-ndx 15117  df-slot 15118  df-base 15119  df-sets 15120  df-ress 15121  df-plusg 15196  df-0g 15333  df-topgen 15335  df-plusf 16480  df-mgm 16481  df-sgrp 16520  df-mnd 16530  df-grp 16666  df-minusg 16667  df-sbg 16668  df-subg 16807  df-top 19914  df-bases 19915  df-topon 19916  df-topsp 19917  df-cld 20027  df-ntr 20028  df-cls 20029  df-cn 20236  df-tx 20570  df-tmd 21080  df-tgp 21081 This theorem is referenced by:  clsnsg  21117  tgptsmscls  21157
 Copyright terms: Public domain W3C validator