This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )