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

Theorem isnsg 16839
 Description: Property of being a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
Hypotheses
Ref Expression
isnsg.1
isnsg.2
Assertion
Ref Expression
isnsg NrmSGrp SubGrp
Distinct variable groups:   ,,   , ,   ,,   ,,

Proof of Theorem isnsg
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nsg 16808 . . . 4 NrmSGrp SubGrp
21dmmptss 5330 . . 3 NrmSGrp
3 elfvdm 5889 . . 3 NrmSGrp NrmSGrp
42, 3sseldi 3429 . 2 NrmSGrp
5 subgrcl 16815 . . 3 SubGrp
65adantr 467 . 2 SubGrp
7 fveq2 5863 . . . . . 6 SubGrp SubGrp
8 fvex 5873 . . . . . . . 8
98a1i 11 . . . . . . 7
10 fveq2 5863 . . . . . . . 8
11 isnsg.1 . . . . . . . 8
1210, 11syl6eqr 2502 . . . . . . 7
13 fvex 5873 . . . . . . . . 9
1413a1i 11 . . . . . . . 8
15 simpl 459 . . . . . . . . . 10
1615fveq2d 5867 . . . . . . . . 9
17 isnsg.2 . . . . . . . . 9
1816, 17syl6eqr 2502 . . . . . . . 8
19 simplr 761 . . . . . . . . 9
20 simpr 463 . . . . . . . . . . . . 13
2120oveqd 6305 . . . . . . . . . . . 12
2221eleq1d 2512 . . . . . . . . . . 11
2320oveqd 6305 . . . . . . . . . . . 12
2423eleq1d 2512 . . . . . . . . . . 11
2522, 24bibi12d 323 . . . . . . . . . 10
2619, 25raleqbidv 3000 . . . . . . . . 9
2719, 26raleqbidv 3000 . . . . . . . 8
2814, 18, 27sbcied2 3304 . . . . . . 7
299, 12, 28sbcied2 3304 . . . . . 6
307, 29rabeqbidv 3039 . . . . 5 SubGrp SubGrp
31 fvex 5873 . . . . . 6 SubGrp
3231rabex 4553 . . . . 5 SubGrp
3330, 1, 32fvmpt 5946 . . . 4 NrmSGrp SubGrp
3433eleq2d 2513 . . 3 NrmSGrp SubGrp
35 eleq2 2517 . . . . . 6
36 eleq2 2517 . . . . . 6
3735, 36bibi12d 323 . . . . 5
38372ralbidv 2831 . . . 4
3938elrab 3195 . . 3 SubGrp SubGrp
4034, 39syl6bb 265 . 2 NrmSGrp SubGrp
414, 6, 40pm5.21nii 355 1 NrmSGrp SubGrp
 Colors of variables: wff setvar class Syntax hints:   wb 188   wa 371   wceq 1443   wcel 1886  wral 2736  crab 2740  cvv 3044  wsbc 3266   cdm 4833  cfv 5581  (class class class)co 6288  cbs 15114   cplusg 15183  cgrp 16662  SubGrpcsubg 16804  NrmSGrpcnsg 16805 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-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  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-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-sbc 3267  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-br 4402  df-opab 4461  df-mpt 4462  df-id 4748  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-iota 5545  df-fun 5583  df-fv 5589  df-ov 6291  df-subg 16807  df-nsg 16808 This theorem is referenced by:  isnsg2  16840  nsgbi  16841  nsgsubg  16842  isnsg4  16853  nmznsg  16854  ablnsg  17478  rzgrp  23496
 Copyright terms: Public domain W3C validator