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 ) |