Step |
Hyp |
Ref |
Expression |
1 |
|
slwispgp.1 |
|- S = ( G |`s K ) |
2 |
|
simp3 |
|- ( ( H e. ( P pSyl G ) /\ K e. ( SubGrp ` G ) /\ H C. K ) -> H C. K ) |
3 |
2
|
pssned |
|- ( ( H e. ( P pSyl G ) /\ K e. ( SubGrp ` G ) /\ H C. K ) -> H =/= K ) |
4 |
2
|
pssssd |
|- ( ( H e. ( P pSyl G ) /\ K e. ( SubGrp ` G ) /\ H C. K ) -> H C_ K ) |
5 |
4
|
biantrurd |
|- ( ( H e. ( P pSyl G ) /\ K e. ( SubGrp ` G ) /\ H C. K ) -> ( P pGrp S <-> ( H C_ K /\ P pGrp S ) ) ) |
6 |
1
|
slwispgp |
|- ( ( H e. ( P pSyl G ) /\ K e. ( SubGrp ` G ) ) -> ( ( H C_ K /\ P pGrp S ) <-> H = K ) ) |
7 |
6
|
3adant3 |
|- ( ( H e. ( P pSyl G ) /\ K e. ( SubGrp ` G ) /\ H C. K ) -> ( ( H C_ K /\ P pGrp S ) <-> H = K ) ) |
8 |
5 7
|
bitrd |
|- ( ( H e. ( P pSyl G ) /\ K e. ( SubGrp ` G ) /\ H C. K ) -> ( P pGrp S <-> H = K ) ) |
9 |
8
|
necon3bbid |
|- ( ( H e. ( P pSyl G ) /\ K e. ( SubGrp ` G ) /\ H C. K ) -> ( -. P pGrp S <-> H =/= K ) ) |
10 |
3 9
|
mpbird |
|- ( ( H e. ( P pSyl G ) /\ K e. ( SubGrp ` G ) /\ H C. K ) -> -. P pGrp S ) |