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

Theorem pgpssslw 17265
 Description: Every -subgroup is contained in a Sylow -subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.)
Hypotheses
Ref Expression
pgpssslw.1
pgpssslw.2 s
pgpssslw.3 SubGrp pGrp s
Assertion
Ref Expression
pgpssslw SubGrp pGrp pSyl
Distinct variable groups:   ,,,   ,,,   ,,,   ,,   ,   ,,,
Allowed substitution hints:   (,)   ()

Proof of Theorem pgpssslw
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp2 1006 . . . . . . . . . 10 SubGrp pGrp
2 elrabi 3225 . . . . . . . . . . 11 SubGrp pGrp s SubGrp
3 pgpssslw.1 . . . . . . . . . . . 12
43subgss 16817 . . . . . . . . . . 11 SubGrp
52, 4syl 17 . . . . . . . . . 10 SubGrp pGrp s
6 ssfi 7801 . . . . . . . . . 10
71, 5, 6syl2an 479 . . . . . . . . 9 SubGrp pGrp SubGrp pGrp s
8 hashcl 12544 . . . . . . . . 9
97, 8syl 17 . . . . . . . 8 SubGrp pGrp SubGrp pGrp s
109nn0zd 11045 . . . . . . 7 SubGrp pGrp SubGrp pGrp s
11 pgpssslw.3 . . . . . . 7 SubGrp pGrp s
1210, 11fmptd 6061 . . . . . 6 SubGrp pGrp SubGrp pGrp s
13 frn 5752 . . . . . 6 SubGrp pGrp s
1412, 13syl 17 . . . . 5 SubGrp pGrp
15 fvex 5891 . . . . . . . 8
1615, 11fnmpti 5724 . . . . . . 7 SubGrp pGrp s
17 simp1 1005 . . . . . . . 8 SubGrp pGrp SubGrp
18 simp3 1007 . . . . . . . 8 SubGrp pGrp pGrp
19 eqimss2 3517 . . . . . . . . . . 11
2019biantrud 509 . . . . . . . . . 10 pGrp s pGrp s
21 oveq2 6313 . . . . . . . . . . . 12 s s
22 pgpssslw.2 . . . . . . . . . . . 12 s
2321, 22syl6eqr 2481 . . . . . . . . . . 11 s
2423breq2d 4435 . . . . . . . . . 10 pGrp s pGrp
2520, 24bitr3d 258 . . . . . . . . 9 pGrp s pGrp
2625elrab 3228 . . . . . . . 8 SubGrp pGrp s SubGrp pGrp
2717, 18, 26sylanbrc 668 . . . . . . 7 SubGrp pGrp SubGrp pGrp s
28 fnfvelrn 6034 . . . . . . 7 SubGrp pGrp s SubGrp pGrp s
2916, 27, 28sylancr 667 . . . . . 6 SubGrp pGrp
30 ne0i 3767 . . . . . 6
3129, 30syl 17 . . . . 5 SubGrp pGrp
32 hashcl 12544 . . . . . . . 8
331, 32syl 17 . . . . . . 7 SubGrp pGrp
3433nn0red 10933 . . . . . 6 SubGrp pGrp
35 fveq2 5881 . . . . . . . . . . 11
36 fvex 5891 . . . . . . . . . . 11
3735, 11, 36fvmpt 5964 . . . . . . . . . 10 SubGrp pGrp s
3837adantl 467 . . . . . . . . 9 SubGrp pGrp SubGrp pGrp s
39 oveq2 6313 . . . . . . . . . . . . 13 s s
4039breq2d 4435 . . . . . . . . . . . 12 pGrp s pGrp s
41 sseq2 3486 . . . . . . . . . . . 12
4240, 41anbi12d 715 . . . . . . . . . . 11 pGrp s pGrp s
4342elrab 3228 . . . . . . . . . 10 SubGrp pGrp s SubGrp pGrp s
441adantr 466 . . . . . . . . . . . 12 SubGrp pGrp SubGrp pGrp s
453subgss 16817 . . . . . . . . . . . . 13 SubGrp
4645ad2antrl 732 . . . . . . . . . . . 12 SubGrp pGrp SubGrp pGrp s
47 ssdomg 7625 . . . . . . . . . . . 12
4844, 46, 47sylc 62 . . . . . . . . . . 11 SubGrp pGrp SubGrp pGrp s
49 ssfi 7801 . . . . . . . . . . . . 13
5044, 46, 49syl2anc 665 . . . . . . . . . . . 12 SubGrp pGrp SubGrp pGrp s
51 hashdom 12564 . . . . . . . . . . . 12
5250, 44, 51syl2anc 665 . . . . . . . . . . 11 SubGrp pGrp SubGrp pGrp s
5348, 52mpbird 235 . . . . . . . . . 10 SubGrp pGrp SubGrp pGrp s
5443, 53sylan2b 477 . . . . . . . . 9 SubGrp pGrp SubGrp pGrp s
5538, 54eqbrtrd 4444 . . . . . . . 8 SubGrp pGrp SubGrp pGrp s
5655ralrimiva 2836 . . . . . . 7 SubGrp pGrp SubGrp pGrp s
57 breq1 4426 . . . . . . . . 9
5857ralrn 6040 . . . . . . . 8 SubGrp pGrp s SubGrp pGrp s
5916, 58ax-mp 5 . . . . . . 7 SubGrp pGrp s
6056, 59sylibr 215 . . . . . 6 SubGrp pGrp
61 breq2 4427 . . . . . . . 8
6261ralbidv 2861 . . . . . . 7
6362rspcev 3182 . . . . . 6
6434, 60, 63syl2anc 665 . . . . 5 SubGrp pGrp
65 suprzcl 11022 . . . . 5
6614, 31, 64, 65syl3anc 1264 . . . 4 SubGrp pGrp
67 fvelrnb 5928 . . . . 5 SubGrp pGrp s SubGrp pGrp s
6816, 67ax-mp 5 . . . 4 SubGrp pGrp s
6966, 68sylib 199 . . 3 SubGrp pGrp SubGrp pGrp s
70 oveq2 6313 . . . . . 6 s s
7170breq2d 4435 . . . . 5 pGrp s pGrp s
72 sseq2 3486 . . . . 5
7371, 72anbi12d 715 . . . 4 pGrp s pGrp s
7473rexrab 3234 . . 3 SubGrp pGrp s SubGrp pGrp s
7569, 74sylib 199 . 2 SubGrp pGrp SubGrp pGrp s
76 simpl3 1010 . . . . . . 7 SubGrp pGrp SubGrp pGrp s pGrp
77 pgpprm 17244 . . . . . . 7 pGrp
7876, 77syl 17 . . . . . 6 SubGrp pGrp SubGrp pGrp s
79 simprl 762 . . . . . 6 SubGrp pGrp SubGrp pGrp s SubGrp
80 zssre 10951 . . . . . . . . . . . . . . . 16
8114, 80syl6ss 3476 . . . . . . . . . . . . . . 15 SubGrp pGrp
8281ad2antrr 730 . . . . . . . . . . . . . 14 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
8331ad2antrr 730 . . . . . . . . . . . . . 14 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
8464ad2antrr 730 . . . . . . . . . . . . . 14 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
85 simprl 762 . . . . . . . . . . . . . . . . 17 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s SubGrp
86 simprrr 773 . . . . . . . . . . . . . . . . . 18 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s pGrp s
87 simprrl 772 . . . . . . . . . . . . . . . . . . . . 21 SubGrp pGrp SubGrp pGrp s pGrp s
8887adantr 466 . . . . . . . . . . . . . . . . . . . 20 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s pGrp s
8988simprd 464 . . . . . . . . . . . . . . . . . . 19 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
90 simprrl 772 . . . . . . . . . . . . . . . . . . 19 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
9189, 90sstrd 3474 . . . . . . . . . . . . . . . . . 18 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
9286, 91jca 534 . . . . . . . . . . . . . . . . 17 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s pGrp s
9385, 92, 43sylanbrc 668 . . . . . . . . . . . . . . . 16 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s SubGrp pGrp s
9493, 37syl 17 . . . . . . . . . . . . . . 15 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
95 fnfvelrn 6034 . . . . . . . . . . . . . . . 16 SubGrp pGrp s SubGrp pGrp s
9616, 93, 95sylancr 667 . . . . . . . . . . . . . . 15 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
9794, 96eqeltrrd 2508 . . . . . . . . . . . . . 14 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
98 suprub 10577 . . . . . . . . . . . . . 14
9982, 83, 84, 97, 98syl31anc 1267 . . . . . . . . . . . . 13 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
100 simprrr 773 . . . . . . . . . . . . . . 15 SubGrp pGrp SubGrp pGrp s
101100adantr 466 . . . . . . . . . . . . . 14 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
10279adantr 466 . . . . . . . . . . . . . . . 16 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s SubGrp
10373elrab 3228 . . . . . . . . . . . . . . . 16 SubGrp pGrp s SubGrp pGrp s
104102, 88, 103sylanbrc 668 . . . . . . . . . . . . . . 15 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s SubGrp pGrp s
105 fveq2 5881 . . . . . . . . . . . . . . . 16
106 fvex 5891 . . . . . . . . . . . . . . . 16
107105, 11, 106fvmpt 5964 . . . . . . . . . . . . . . 15 SubGrp pGrp s
108104, 107syl 17 . . . . . . . . . . . . . 14 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
109101, 108eqtr3d 2465 . . . . . . . . . . . . 13 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
11099, 109breqtrd 4448 . . . . . . . . . . . 12 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
111 simpll2 1045 . . . . . . . . . . . . . 14 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
11245ad2antrl 732 . . . . . . . . . . . . . 14 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
113111, 112, 49syl2anc 665 . . . . . . . . . . . . 13 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
114 ssfi 7801 . . . . . . . . . . . . . 14
115113, 90, 114syl2anc 665 . . . . . . . . . . . . 13 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
116 hashcl 12544 . . . . . . . . . . . . . 14
117 hashcl 12544 . . . . . . . . . . . . . 14
118 nn0re 10885 . . . . . . . . . . . . . . 15
119 nn0re 10885 . . . . . . . . . . . . . . 15
120 lenlt 9719 . . . . . . . . . . . . . . 15
121118, 119, 120syl2an 479 . . . . . . . . . . . . . 14
122116, 117, 121syl2an 479 . . . . . . . . . . . . 13
123113, 115, 122syl2anc 665 . . . . . . . . . . . 12 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
124110, 123mpbid 213 . . . . . . . . . . 11 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
125 php3 7767 . . . . . . . . . . . . . 14
126125ex 435 . . . . . . . . . . . . 13
127113, 126syl 17 . . . . . . . . . . . 12 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
128 hashsdom 12566 . . . . . . . . . . . . 13
129115, 113, 128syl2anc 665 . . . . . . . . . . . 12 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
130127, 129sylibrd 237 . . . . . . . . . . 11 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
131124, 130mtod 180 . . . . . . . . . 10 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
132 sspss 3564 . . . . . . . . . . . 12
13390, 132sylib 199 . . . . . . . . . . 11 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
134133ord 378 . . . . . . . . . 10 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
135131, 134mpd 15 . . . . . . . . 9 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
136135expr 618 . . . . . . . 8 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
13787simpld 460 . . . . . . . . . 10 SubGrp pGrp SubGrp pGrp s pGrp s
138137adantr 466 . . . . . . . . 9 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
139 oveq2 6313 . . . . . . . . . . 11 s s
140139breq2d 4435 . . . . . . . . . 10 pGrp s pGrp s
141 eqimss 3516 . . . . . . . . . . 11
142141biantrurd 510 . . . . . . . . . 10 pGrp s pGrp s
143140, 142bitrd 256 . . . . . . . . 9 pGrp s pGrp s
144138, 143syl5ibcom 223 . . . . . . . 8 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
145136, 144impbid 193 . . . . . . 7 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
146145ralrimiva 2836 . . . . . 6 SubGrp pGrp SubGrp pGrp s SubGrp pGrp s
147 isslw 17259 . . . . . 6 pSyl SubGrp SubGrp pGrp s
14878, 79, 146, 147syl3anbrc 1189 . . . . 5 SubGrp pGrp SubGrp pGrp s pSyl
14987simprd 464 . . . . 5 SubGrp pGrp SubGrp pGrp s
150148, 149jca 534 . . . 4 SubGrp pGrp SubGrp pGrp s pSyl
151150ex 435 . . 3 SubGrp pGrp SubGrp pGrp s pSyl
152151reximdv2 2893 . 2 SubGrp pGrp SubGrp pGrp s pSyl
15375, 152mpd 15 1 SubGrp pGrp pSyl
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wo 369   wa 370   w3a 982   wceq 1437   wcel 1872   wne 2614  wral 2771  wrex 2772  crab 2775   wss 3436   wpss 3437  c0 3761   class class class wbr 4423   cmpt 4482   crn 4854   wfn 5596  wf 5597  cfv 5601  (class class class)co 6305   cdom 7578   csdm 7579  cfn 7580  csup 7963  cr 9545   clt 9682   cle 9683  cn0 10876  cz 10944  chash 12521  cprime 14621  cbs 15120   ↾s cress 15121  SubGrpcsubg 16810   pGrp cpgp 17168   pSyl cslw 17170 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-cnex 9602  ax-resscn 9603  ax-1cn 9604  ax-icn 9605  ax-addcl 9606  ax-addrcl 9607  ax-mulcl 9608  ax-mulrcl 9609  ax-mulcom 9610  ax-addass 9611  ax-mulass 9612  ax-distr 9613  ax-i2m1 9614  ax-1ne0 9615  ax-1rid 9616  ax-rnegex 9617  ax-rrecex 9618  ax-cnre 9619  ax-pre-lttri 9620  ax-pre-lttrn 9621  ax-pre-ltadd 9622  ax-pre-mulgt0 9623  ax-pre-sup 9624 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rmo 2779  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-int 4256  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-1st 6807  df-2nd 6808  df-wrecs 7039  df-recs 7101  df-rdg 7139  df-1o 7193  df-oadd 7197  df-er 7374  df-en 7581  df-dom 7582  df-sdom 7583  df-fin 7584  df-sup 7965  df-card 8381  df-pnf 9684  df-mnf 9685  df-xr 9686  df-ltxr 9687  df-le 9688  df-sub 9869  df-neg 9870  df-nn 10617  df-n0 10877  df-z 10945  df-uz 11167  df-fz 11792  df-hash 12522  df-subg 16813  df-pgp 17175  df-slw 17177 This theorem is referenced by:  slwn0  17266
 Copyright terms: Public domain W3C validator