Metamath Proof Explorer


Theorem pgpssslw

Description: Every P -subgroup is contained in a Sylow P -subgroup. (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Hypotheses pgpssslw.1
|- X = ( Base ` G )
pgpssslw.2
|- S = ( G |`s H )
pgpssslw.3
|- F = ( x e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } |-> ( # ` x ) )
Assertion pgpssslw
|- ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) -> E. k e. ( P pSyl G ) H C_ k )

Proof

Step Hyp Ref Expression
1 pgpssslw.1
 |-  X = ( Base ` G )
2 pgpssslw.2
 |-  S = ( G |`s H )
3 pgpssslw.3
 |-  F = ( x e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } |-> ( # ` x ) )
4 simp2
 |-  ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) -> X e. Fin )
5 elrabi
 |-  ( x e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } -> x e. ( SubGrp ` G ) )
6 1 subgss
 |-  ( x e. ( SubGrp ` G ) -> x C_ X )
7 5 6 syl
 |-  ( x e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } -> x C_ X )
8 ssfi
 |-  ( ( X e. Fin /\ x C_ X ) -> x e. Fin )
9 4 7 8 syl2an
 |-  ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ x e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } ) -> x e. Fin )
10 hashcl
 |-  ( x e. Fin -> ( # ` x ) e. NN0 )
11 9 10 syl
 |-  ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ x e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } ) -> ( # ` x ) e. NN0 )
12 11 nn0zd
 |-  ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ x e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } ) -> ( # ` x ) e. ZZ )
13 12 3 fmptd
 |-  ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) -> F : { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } --> ZZ )
14 13 frnd
 |-  ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) -> ran F C_ ZZ )
15 fvex
 |-  ( # ` x ) e. _V
16 15 3 fnmpti
 |-  F Fn { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) }
17 eqimss2
 |-  ( y = H -> H C_ y )
18 17 biantrud
 |-  ( y = H -> ( P pGrp ( G |`s y ) <-> ( P pGrp ( G |`s y ) /\ H C_ y ) ) )
19 oveq2
 |-  ( y = H -> ( G |`s y ) = ( G |`s H ) )
20 19 2 eqtr4di
 |-  ( y = H -> ( G |`s y ) = S )
21 20 breq2d
 |-  ( y = H -> ( P pGrp ( G |`s y ) <-> P pGrp S ) )
22 18 21 bitr3d
 |-  ( y = H -> ( ( P pGrp ( G |`s y ) /\ H C_ y ) <-> P pGrp S ) )
23 simp1
 |-  ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) -> H e. ( SubGrp ` G ) )
24 simp3
 |-  ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) -> P pGrp S )
25 22 23 24 elrabd
 |-  ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) -> H e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } )
26 fnfvelrn
 |-  ( ( F Fn { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } /\ H e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } ) -> ( F ` H ) e. ran F )
27 16 25 26 sylancr
 |-  ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) -> ( F ` H ) e. ran F )
28 27 ne0d
 |-  ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) -> ran F =/= (/) )
29 hashcl
 |-  ( X e. Fin -> ( # ` X ) e. NN0 )
30 4 29 syl
 |-  ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) -> ( # ` X ) e. NN0 )
31 30 nn0red
 |-  ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) -> ( # ` X ) e. RR )
32 fveq2
 |-  ( x = m -> ( # ` x ) = ( # ` m ) )
33 fvex
 |-  ( # ` m ) e. _V
34 32 3 33 fvmpt
 |-  ( m e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } -> ( F ` m ) = ( # ` m ) )
35 34 adantl
 |-  ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ m e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } ) -> ( F ` m ) = ( # ` m ) )
36 oveq2
 |-  ( y = m -> ( G |`s y ) = ( G |`s m ) )
37 36 breq2d
 |-  ( y = m -> ( P pGrp ( G |`s y ) <-> P pGrp ( G |`s m ) ) )
38 sseq2
 |-  ( y = m -> ( H C_ y <-> H C_ m ) )
39 37 38 anbi12d
 |-  ( y = m -> ( ( P pGrp ( G |`s y ) /\ H C_ y ) <-> ( P pGrp ( G |`s m ) /\ H C_ m ) ) )
40 39 elrab
 |-  ( m e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } <-> ( m e. ( SubGrp ` G ) /\ ( P pGrp ( G |`s m ) /\ H C_ m ) ) )
41 4 adantr
 |-  ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( m e. ( SubGrp ` G ) /\ ( P pGrp ( G |`s m ) /\ H C_ m ) ) ) -> X e. Fin )
42 1 subgss
 |-  ( m e. ( SubGrp ` G ) -> m C_ X )
43 42 ad2antrl
 |-  ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( m e. ( SubGrp ` G ) /\ ( P pGrp ( G |`s m ) /\ H C_ m ) ) ) -> m C_ X )
44 ssdomg
 |-  ( X e. Fin -> ( m C_ X -> m ~<_ X ) )
45 41 43 44 sylc
 |-  ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( m e. ( SubGrp ` G ) /\ ( P pGrp ( G |`s m ) /\ H C_ m ) ) ) -> m ~<_ X )
46 41 43 ssfid
 |-  ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( m e. ( SubGrp ` G ) /\ ( P pGrp ( G |`s m ) /\ H C_ m ) ) ) -> m e. Fin )
47 hashdom
 |-  ( ( m e. Fin /\ X e. Fin ) -> ( ( # ` m ) <_ ( # ` X ) <-> m ~<_ X ) )
48 46 41 47 syl2anc
 |-  ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( m e. ( SubGrp ` G ) /\ ( P pGrp ( G |`s m ) /\ H C_ m ) ) ) -> ( ( # ` m ) <_ ( # ` X ) <-> m ~<_ X ) )
49 45 48 mpbird
 |-  ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( m e. ( SubGrp ` G ) /\ ( P pGrp ( G |`s m ) /\ H C_ m ) ) ) -> ( # ` m ) <_ ( # ` X ) )
50 40 49 sylan2b
 |-  ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ m e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } ) -> ( # ` m ) <_ ( # ` X ) )
51 35 50 eqbrtrd
 |-  ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ m e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } ) -> ( F ` m ) <_ ( # ` X ) )
52 51 ralrimiva
 |-  ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) -> A. m e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } ( F ` m ) <_ ( # ` X ) )
53 breq1
 |-  ( w = ( F ` m ) -> ( w <_ ( # ` X ) <-> ( F ` m ) <_ ( # ` X ) ) )
54 53 ralrn
 |-  ( F Fn { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } -> ( A. w e. ran F w <_ ( # ` X ) <-> A. m e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } ( F ` m ) <_ ( # ` X ) ) )
55 16 54 ax-mp
 |-  ( A. w e. ran F w <_ ( # ` X ) <-> A. m e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } ( F ` m ) <_ ( # ` X ) )
56 52 55 sylibr
 |-  ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) -> A. w e. ran F w <_ ( # ` X ) )
57 brralrspcev
 |-  ( ( ( # ` X ) e. RR /\ A. w e. ran F w <_ ( # ` X ) ) -> E. z e. RR A. w e. ran F w <_ z )
58 31 56 57 syl2anc
 |-  ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) -> E. z e. RR A. w e. ran F w <_ z )
59 suprzcl
 |-  ( ( ran F C_ ZZ /\ ran F =/= (/) /\ E. z e. RR A. w e. ran F w <_ z ) -> sup ( ran F , RR , < ) e. ran F )
60 14 28 58 59 syl3anc
 |-  ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) -> sup ( ran F , RR , < ) e. ran F )
61 fvelrnb
 |-  ( F Fn { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } -> ( sup ( ran F , RR , < ) e. ran F <-> E. k e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } ( F ` k ) = sup ( ran F , RR , < ) ) )
62 16 61 ax-mp
 |-  ( sup ( ran F , RR , < ) e. ran F <-> E. k e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } ( F ` k ) = sup ( ran F , RR , < ) )
63 60 62 sylib
 |-  ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) -> E. k e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } ( F ` k ) = sup ( ran F , RR , < ) )
64 oveq2
 |-  ( y = k -> ( G |`s y ) = ( G |`s k ) )
65 64 breq2d
 |-  ( y = k -> ( P pGrp ( G |`s y ) <-> P pGrp ( G |`s k ) ) )
66 sseq2
 |-  ( y = k -> ( H C_ y <-> H C_ k ) )
67 65 66 anbi12d
 |-  ( y = k -> ( ( P pGrp ( G |`s y ) /\ H C_ y ) <-> ( P pGrp ( G |`s k ) /\ H C_ k ) ) )
68 67 rexrab
 |-  ( E. k e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } ( F ` k ) = sup ( ran F , RR , < ) <-> E. k e. ( SubGrp ` G ) ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) )
69 63 68 sylib
 |-  ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) -> E. k e. ( SubGrp ` G ) ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) )
70 simpl3
 |-  ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) -> P pGrp S )
71 pgpprm
 |-  ( P pGrp S -> P e. Prime )
72 70 71 syl
 |-  ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) -> P e. Prime )
73 simprl
 |-  ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) -> k e. ( SubGrp ` G ) )
74 zssre
 |-  ZZ C_ RR
75 14 74 sstrdi
 |-  ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) -> ran F C_ RR )
76 75 ad2antrr
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> ran F C_ RR )
77 28 ad2antrr
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> ran F =/= (/) )
78 58 ad2antrr
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> E. z e. RR A. w e. ran F w <_ z )
79 simprl
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> m e. ( SubGrp ` G ) )
80 simprrr
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> P pGrp ( G |`s m ) )
81 simprrl
 |-  ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) -> ( P pGrp ( G |`s k ) /\ H C_ k ) )
82 81 adantr
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> ( P pGrp ( G |`s k ) /\ H C_ k ) )
83 82 simprd
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> H C_ k )
84 simprrl
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> k C_ m )
85 83 84 sstrd
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> H C_ m )
86 80 85 jca
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> ( P pGrp ( G |`s m ) /\ H C_ m ) )
87 39 79 86 elrabd
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> m e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } )
88 87 34 syl
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> ( F ` m ) = ( # ` m ) )
89 fnfvelrn
 |-  ( ( F Fn { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } /\ m e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } ) -> ( F ` m ) e. ran F )
90 16 87 89 sylancr
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> ( F ` m ) e. ran F )
91 88 90 eqeltrrd
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> ( # ` m ) e. ran F )
92 76 77 78 91 suprubd
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> ( # ` m ) <_ sup ( ran F , RR , < ) )
93 simprrr
 |-  ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) -> ( F ` k ) = sup ( ran F , RR , < ) )
94 93 adantr
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> ( F ` k ) = sup ( ran F , RR , < ) )
95 73 adantr
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> k e. ( SubGrp ` G ) )
96 67 95 82 elrabd
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> k e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } )
97 fveq2
 |-  ( x = k -> ( # ` x ) = ( # ` k ) )
98 fvex
 |-  ( # ` k ) e. _V
99 97 3 98 fvmpt
 |-  ( k e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ H C_ y ) } -> ( F ` k ) = ( # ` k ) )
100 96 99 syl
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> ( F ` k ) = ( # ` k ) )
101 94 100 eqtr3d
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> sup ( ran F , RR , < ) = ( # ` k ) )
102 92 101 breqtrd
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> ( # ` m ) <_ ( # ` k ) )
103 simpll2
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> X e. Fin )
104 42 ad2antrl
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> m C_ X )
105 103 104 ssfid
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> m e. Fin )
106 105 84 ssfid
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> k e. Fin )
107 hashcl
 |-  ( m e. Fin -> ( # ` m ) e. NN0 )
108 hashcl
 |-  ( k e. Fin -> ( # ` k ) e. NN0 )
109 nn0re
 |-  ( ( # ` m ) e. NN0 -> ( # ` m ) e. RR )
110 nn0re
 |-  ( ( # ` k ) e. NN0 -> ( # ` k ) e. RR )
111 lenlt
 |-  ( ( ( # ` m ) e. RR /\ ( # ` k ) e. RR ) -> ( ( # ` m ) <_ ( # ` k ) <-> -. ( # ` k ) < ( # ` m ) ) )
112 109 110 111 syl2an
 |-  ( ( ( # ` m ) e. NN0 /\ ( # ` k ) e. NN0 ) -> ( ( # ` m ) <_ ( # ` k ) <-> -. ( # ` k ) < ( # ` m ) ) )
113 107 108 112 syl2an
 |-  ( ( m e. Fin /\ k e. Fin ) -> ( ( # ` m ) <_ ( # ` k ) <-> -. ( # ` k ) < ( # ` m ) ) )
114 105 106 113 syl2anc
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> ( ( # ` m ) <_ ( # ` k ) <-> -. ( # ` k ) < ( # ` m ) ) )
115 102 114 mpbid
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> -. ( # ` k ) < ( # ` m ) )
116 php3
 |-  ( ( m e. Fin /\ k C. m ) -> k ~< m )
117 116 ex
 |-  ( m e. Fin -> ( k C. m -> k ~< m ) )
118 105 117 syl
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> ( k C. m -> k ~< m ) )
119 hashsdom
 |-  ( ( k e. Fin /\ m e. Fin ) -> ( ( # ` k ) < ( # ` m ) <-> k ~< m ) )
120 106 105 119 syl2anc
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> ( ( # ` k ) < ( # ` m ) <-> k ~< m ) )
121 118 120 sylibrd
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> ( k C. m -> ( # ` k ) < ( # ` m ) ) )
122 115 121 mtod
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> -. k C. m )
123 sspss
 |-  ( k C_ m <-> ( k C. m \/ k = m ) )
124 84 123 sylib
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> ( k C. m \/ k = m ) )
125 124 ord
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> ( -. k C. m -> k = m ) )
126 122 125 mpd
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ ( m e. ( SubGrp ` G ) /\ ( k C_ m /\ P pGrp ( G |`s m ) ) ) ) -> k = m )
127 126 expr
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ m e. ( SubGrp ` G ) ) -> ( ( k C_ m /\ P pGrp ( G |`s m ) ) -> k = m ) )
128 81 simpld
 |-  ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) -> P pGrp ( G |`s k ) )
129 128 adantr
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ m e. ( SubGrp ` G ) ) -> P pGrp ( G |`s k ) )
130 oveq2
 |-  ( k = m -> ( G |`s k ) = ( G |`s m ) )
131 130 breq2d
 |-  ( k = m -> ( P pGrp ( G |`s k ) <-> P pGrp ( G |`s m ) ) )
132 eqimss
 |-  ( k = m -> k C_ m )
133 132 biantrurd
 |-  ( k = m -> ( P pGrp ( G |`s m ) <-> ( k C_ m /\ P pGrp ( G |`s m ) ) ) )
134 131 133 bitrd
 |-  ( k = m -> ( P pGrp ( G |`s k ) <-> ( k C_ m /\ P pGrp ( G |`s m ) ) ) )
135 129 134 syl5ibcom
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ m e. ( SubGrp ` G ) ) -> ( k = m -> ( k C_ m /\ P pGrp ( G |`s m ) ) ) )
136 127 135 impbid
 |-  ( ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) /\ m e. ( SubGrp ` G ) ) -> ( ( k C_ m /\ P pGrp ( G |`s m ) ) <-> k = m ) )
137 136 ralrimiva
 |-  ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) -> A. m e. ( SubGrp ` G ) ( ( k C_ m /\ P pGrp ( G |`s m ) ) <-> k = m ) )
138 isslw
 |-  ( k e. ( P pSyl G ) <-> ( P e. Prime /\ k e. ( SubGrp ` G ) /\ A. m e. ( SubGrp ` G ) ( ( k C_ m /\ P pGrp ( G |`s m ) ) <-> k = m ) ) )
139 72 73 137 138 syl3anbrc
 |-  ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) -> k e. ( P pSyl G ) )
140 81 simprd
 |-  ( ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) /\ ( k e. ( SubGrp ` G ) /\ ( ( P pGrp ( G |`s k ) /\ H C_ k ) /\ ( F ` k ) = sup ( ran F , RR , < ) ) ) ) -> H C_ k )
141 69 139 140 reximssdv
 |-  ( ( H e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) -> E. k e. ( P pSyl G ) H C_ k )