Step |
Hyp |
Ref |
Expression |
1 |
|
pgpssslw.1 |
⊢ 𝑋 = ( Base ‘ 𝐺 ) |
2 |
|
pgpssslw.2 |
⊢ 𝑆 = ( 𝐺 ↾s 𝐻 ) |
3 |
|
pgpssslw.3 |
⊢ 𝐹 = ( 𝑥 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } ↦ ( ♯ ‘ 𝑥 ) ) |
4 |
|
simp2 |
⊢ ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → 𝑋 ∈ Fin ) |
5 |
|
elrabi |
⊢ ( 𝑥 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } → 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) |
6 |
1
|
subgss |
⊢ ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) → 𝑥 ⊆ 𝑋 ) |
7 |
5 6
|
syl |
⊢ ( 𝑥 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } → 𝑥 ⊆ 𝑋 ) |
8 |
|
ssfi |
⊢ ( ( 𝑋 ∈ Fin ∧ 𝑥 ⊆ 𝑋 ) → 𝑥 ∈ Fin ) |
9 |
4 7 8
|
syl2an |
⊢ ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ 𝑥 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } ) → 𝑥 ∈ Fin ) |
10 |
|
hashcl |
⊢ ( 𝑥 ∈ Fin → ( ♯ ‘ 𝑥 ) ∈ ℕ0 ) |
11 |
9 10
|
syl |
⊢ ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ 𝑥 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } ) → ( ♯ ‘ 𝑥 ) ∈ ℕ0 ) |
12 |
11
|
nn0zd |
⊢ ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ 𝑥 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } ) → ( ♯ ‘ 𝑥 ) ∈ ℤ ) |
13 |
12 3
|
fmptd |
⊢ ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → 𝐹 : { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } ⟶ ℤ ) |
14 |
13
|
frnd |
⊢ ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ran 𝐹 ⊆ ℤ ) |
15 |
|
fvex |
⊢ ( ♯ ‘ 𝑥 ) ∈ V |
16 |
15 3
|
fnmpti |
⊢ 𝐹 Fn { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } |
17 |
|
eqimss2 |
⊢ ( 𝑦 = 𝐻 → 𝐻 ⊆ 𝑦 ) |
18 |
17
|
biantrud |
⊢ ( 𝑦 = 𝐻 → ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ↔ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) ) ) |
19 |
|
oveq2 |
⊢ ( 𝑦 = 𝐻 → ( 𝐺 ↾s 𝑦 ) = ( 𝐺 ↾s 𝐻 ) ) |
20 |
19 2
|
eqtr4di |
⊢ ( 𝑦 = 𝐻 → ( 𝐺 ↾s 𝑦 ) = 𝑆 ) |
21 |
20
|
breq2d |
⊢ ( 𝑦 = 𝐻 → ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ↔ 𝑃 pGrp 𝑆 ) ) |
22 |
18 21
|
bitr3d |
⊢ ( 𝑦 = 𝐻 → ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) ↔ 𝑃 pGrp 𝑆 ) ) |
23 |
|
simp1 |
⊢ ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) |
24 |
|
simp3 |
⊢ ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → 𝑃 pGrp 𝑆 ) |
25 |
22 23 24
|
elrabd |
⊢ ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → 𝐻 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } ) |
26 |
|
fnfvelrn |
⊢ ( ( 𝐹 Fn { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } ∧ 𝐻 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } ) → ( 𝐹 ‘ 𝐻 ) ∈ ran 𝐹 ) |
27 |
16 25 26
|
sylancr |
⊢ ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ( 𝐹 ‘ 𝐻 ) ∈ ran 𝐹 ) |
28 |
27
|
ne0d |
⊢ ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ran 𝐹 ≠ ∅ ) |
29 |
|
hashcl |
⊢ ( 𝑋 ∈ Fin → ( ♯ ‘ 𝑋 ) ∈ ℕ0 ) |
30 |
4 29
|
syl |
⊢ ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ( ♯ ‘ 𝑋 ) ∈ ℕ0 ) |
31 |
30
|
nn0red |
⊢ ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ( ♯ ‘ 𝑋 ) ∈ ℝ ) |
32 |
|
fveq2 |
⊢ ( 𝑥 = 𝑚 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑚 ) ) |
33 |
|
fvex |
⊢ ( ♯ ‘ 𝑚 ) ∈ V |
34 |
32 3 33
|
fvmpt |
⊢ ( 𝑚 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } → ( 𝐹 ‘ 𝑚 ) = ( ♯ ‘ 𝑚 ) ) |
35 |
34
|
adantl |
⊢ ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ 𝑚 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } ) → ( 𝐹 ‘ 𝑚 ) = ( ♯ ‘ 𝑚 ) ) |
36 |
|
oveq2 |
⊢ ( 𝑦 = 𝑚 → ( 𝐺 ↾s 𝑦 ) = ( 𝐺 ↾s 𝑚 ) ) |
37 |
36
|
breq2d |
⊢ ( 𝑦 = 𝑚 → ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ↔ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) |
38 |
|
sseq2 |
⊢ ( 𝑦 = 𝑚 → ( 𝐻 ⊆ 𝑦 ↔ 𝐻 ⊆ 𝑚 ) ) |
39 |
37 38
|
anbi12d |
⊢ ( 𝑦 = 𝑚 → ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) ↔ ( 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ∧ 𝐻 ⊆ 𝑚 ) ) ) |
40 |
39
|
elrab |
⊢ ( 𝑚 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } ↔ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ∧ 𝐻 ⊆ 𝑚 ) ) ) |
41 |
4
|
adantr |
⊢ ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ∧ 𝐻 ⊆ 𝑚 ) ) ) → 𝑋 ∈ Fin ) |
42 |
1
|
subgss |
⊢ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) → 𝑚 ⊆ 𝑋 ) |
43 |
42
|
ad2antrl |
⊢ ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ∧ 𝐻 ⊆ 𝑚 ) ) ) → 𝑚 ⊆ 𝑋 ) |
44 |
|
ssdomg |
⊢ ( 𝑋 ∈ Fin → ( 𝑚 ⊆ 𝑋 → 𝑚 ≼ 𝑋 ) ) |
45 |
41 43 44
|
sylc |
⊢ ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ∧ 𝐻 ⊆ 𝑚 ) ) ) → 𝑚 ≼ 𝑋 ) |
46 |
41 43
|
ssfid |
⊢ ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ∧ 𝐻 ⊆ 𝑚 ) ) ) → 𝑚 ∈ Fin ) |
47 |
|
hashdom |
⊢ ( ( 𝑚 ∈ Fin ∧ 𝑋 ∈ Fin ) → ( ( ♯ ‘ 𝑚 ) ≤ ( ♯ ‘ 𝑋 ) ↔ 𝑚 ≼ 𝑋 ) ) |
48 |
46 41 47
|
syl2anc |
⊢ ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ∧ 𝐻 ⊆ 𝑚 ) ) ) → ( ( ♯ ‘ 𝑚 ) ≤ ( ♯ ‘ 𝑋 ) ↔ 𝑚 ≼ 𝑋 ) ) |
49 |
45 48
|
mpbird |
⊢ ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ∧ 𝐻 ⊆ 𝑚 ) ) ) → ( ♯ ‘ 𝑚 ) ≤ ( ♯ ‘ 𝑋 ) ) |
50 |
40 49
|
sylan2b |
⊢ ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ 𝑚 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } ) → ( ♯ ‘ 𝑚 ) ≤ ( ♯ ‘ 𝑋 ) ) |
51 |
35 50
|
eqbrtrd |
⊢ ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ 𝑚 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } ) → ( 𝐹 ‘ 𝑚 ) ≤ ( ♯ ‘ 𝑋 ) ) |
52 |
51
|
ralrimiva |
⊢ ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ∀ 𝑚 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } ( 𝐹 ‘ 𝑚 ) ≤ ( ♯ ‘ 𝑋 ) ) |
53 |
|
breq1 |
⊢ ( 𝑤 = ( 𝐹 ‘ 𝑚 ) → ( 𝑤 ≤ ( ♯ ‘ 𝑋 ) ↔ ( 𝐹 ‘ 𝑚 ) ≤ ( ♯ ‘ 𝑋 ) ) ) |
54 |
53
|
ralrn |
⊢ ( 𝐹 Fn { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } → ( ∀ 𝑤 ∈ ran 𝐹 𝑤 ≤ ( ♯ ‘ 𝑋 ) ↔ ∀ 𝑚 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } ( 𝐹 ‘ 𝑚 ) ≤ ( ♯ ‘ 𝑋 ) ) ) |
55 |
16 54
|
ax-mp |
⊢ ( ∀ 𝑤 ∈ ran 𝐹 𝑤 ≤ ( ♯ ‘ 𝑋 ) ↔ ∀ 𝑚 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } ( 𝐹 ‘ 𝑚 ) ≤ ( ♯ ‘ 𝑋 ) ) |
56 |
52 55
|
sylibr |
⊢ ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ∀ 𝑤 ∈ ran 𝐹 𝑤 ≤ ( ♯ ‘ 𝑋 ) ) |
57 |
|
brralrspcev |
⊢ ( ( ( ♯ ‘ 𝑋 ) ∈ ℝ ∧ ∀ 𝑤 ∈ ran 𝐹 𝑤 ≤ ( ♯ ‘ 𝑋 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ran 𝐹 𝑤 ≤ 𝑧 ) |
58 |
31 56 57
|
syl2anc |
⊢ ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ran 𝐹 𝑤 ≤ 𝑧 ) |
59 |
|
suprzcl |
⊢ ( ( ran 𝐹 ⊆ ℤ ∧ ran 𝐹 ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ran 𝐹 𝑤 ≤ 𝑧 ) → sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 ) |
60 |
14 28 58 59
|
syl3anc |
⊢ ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 ) |
61 |
|
fvelrnb |
⊢ ( 𝐹 Fn { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } → ( sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 ↔ ∃ 𝑘 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) |
62 |
16 61
|
ax-mp |
⊢ ( sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 ↔ ∃ 𝑘 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) |
63 |
60 62
|
sylib |
⊢ ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ∃ 𝑘 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) |
64 |
|
oveq2 |
⊢ ( 𝑦 = 𝑘 → ( 𝐺 ↾s 𝑦 ) = ( 𝐺 ↾s 𝑘 ) ) |
65 |
64
|
breq2d |
⊢ ( 𝑦 = 𝑘 → ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ↔ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ) |
66 |
|
sseq2 |
⊢ ( 𝑦 = 𝑘 → ( 𝐻 ⊆ 𝑦 ↔ 𝐻 ⊆ 𝑘 ) ) |
67 |
65 66
|
anbi12d |
⊢ ( 𝑦 = 𝑘 → ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) ↔ ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ) ) |
68 |
67
|
rexrab |
⊢ ( ∃ 𝑘 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ↔ ∃ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) |
69 |
63 68
|
sylib |
⊢ ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ∃ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) |
70 |
|
simpl3 |
⊢ ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) → 𝑃 pGrp 𝑆 ) |
71 |
|
pgpprm |
⊢ ( 𝑃 pGrp 𝑆 → 𝑃 ∈ ℙ ) |
72 |
70 71
|
syl |
⊢ ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) → 𝑃 ∈ ℙ ) |
73 |
|
simprl |
⊢ ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) → 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ) |
74 |
|
zssre |
⊢ ℤ ⊆ ℝ |
75 |
14 74
|
sstrdi |
⊢ ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ran 𝐹 ⊆ ℝ ) |
76 |
75
|
ad2antrr |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → ran 𝐹 ⊆ ℝ ) |
77 |
28
|
ad2antrr |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → ran 𝐹 ≠ ∅ ) |
78 |
58
|
ad2antrr |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ ran 𝐹 𝑤 ≤ 𝑧 ) |
79 |
|
simprl |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ) |
80 |
|
simprrr |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) |
81 |
|
simprrl |
⊢ ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) → ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ) |
82 |
81
|
adantr |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ) |
83 |
82
|
simprd |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → 𝐻 ⊆ 𝑘 ) |
84 |
|
simprrl |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → 𝑘 ⊆ 𝑚 ) |
85 |
83 84
|
sstrd |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → 𝐻 ⊆ 𝑚 ) |
86 |
80 85
|
jca |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → ( 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ∧ 𝐻 ⊆ 𝑚 ) ) |
87 |
39 79 86
|
elrabd |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → 𝑚 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } ) |
88 |
87 34
|
syl |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → ( 𝐹 ‘ 𝑚 ) = ( ♯ ‘ 𝑚 ) ) |
89 |
|
fnfvelrn |
⊢ ( ( 𝐹 Fn { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } ∧ 𝑚 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } ) → ( 𝐹 ‘ 𝑚 ) ∈ ran 𝐹 ) |
90 |
16 87 89
|
sylancr |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → ( 𝐹 ‘ 𝑚 ) ∈ ran 𝐹 ) |
91 |
88 90
|
eqeltrrd |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → ( ♯ ‘ 𝑚 ) ∈ ran 𝐹 ) |
92 |
76 77 78 91
|
suprubd |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → ( ♯ ‘ 𝑚 ) ≤ sup ( ran 𝐹 , ℝ , < ) ) |
93 |
|
simprrr |
⊢ ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) → ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) |
94 |
93
|
adantr |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) |
95 |
73
|
adantr |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ) |
96 |
67 95 82
|
elrabd |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → 𝑘 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } ) |
97 |
|
fveq2 |
⊢ ( 𝑥 = 𝑘 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑘 ) ) |
98 |
|
fvex |
⊢ ( ♯ ‘ 𝑘 ) ∈ V |
99 |
97 3 98
|
fvmpt |
⊢ ( 𝑘 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ 𝐻 ⊆ 𝑦 ) } → ( 𝐹 ‘ 𝑘 ) = ( ♯ ‘ 𝑘 ) ) |
100 |
96 99
|
syl |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → ( 𝐹 ‘ 𝑘 ) = ( ♯ ‘ 𝑘 ) ) |
101 |
94 100
|
eqtr3d |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → sup ( ran 𝐹 , ℝ , < ) = ( ♯ ‘ 𝑘 ) ) |
102 |
92 101
|
breqtrd |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → ( ♯ ‘ 𝑚 ) ≤ ( ♯ ‘ 𝑘 ) ) |
103 |
|
simpll2 |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → 𝑋 ∈ Fin ) |
104 |
42
|
ad2antrl |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → 𝑚 ⊆ 𝑋 ) |
105 |
103 104
|
ssfid |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → 𝑚 ∈ Fin ) |
106 |
105 84
|
ssfid |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → 𝑘 ∈ Fin ) |
107 |
|
hashcl |
⊢ ( 𝑚 ∈ Fin → ( ♯ ‘ 𝑚 ) ∈ ℕ0 ) |
108 |
|
hashcl |
⊢ ( 𝑘 ∈ Fin → ( ♯ ‘ 𝑘 ) ∈ ℕ0 ) |
109 |
|
nn0re |
⊢ ( ( ♯ ‘ 𝑚 ) ∈ ℕ0 → ( ♯ ‘ 𝑚 ) ∈ ℝ ) |
110 |
|
nn0re |
⊢ ( ( ♯ ‘ 𝑘 ) ∈ ℕ0 → ( ♯ ‘ 𝑘 ) ∈ ℝ ) |
111 |
|
lenlt |
⊢ ( ( ( ♯ ‘ 𝑚 ) ∈ ℝ ∧ ( ♯ ‘ 𝑘 ) ∈ ℝ ) → ( ( ♯ ‘ 𝑚 ) ≤ ( ♯ ‘ 𝑘 ) ↔ ¬ ( ♯ ‘ 𝑘 ) < ( ♯ ‘ 𝑚 ) ) ) |
112 |
109 110 111
|
syl2an |
⊢ ( ( ( ♯ ‘ 𝑚 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑘 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝑚 ) ≤ ( ♯ ‘ 𝑘 ) ↔ ¬ ( ♯ ‘ 𝑘 ) < ( ♯ ‘ 𝑚 ) ) ) |
113 |
107 108 112
|
syl2an |
⊢ ( ( 𝑚 ∈ Fin ∧ 𝑘 ∈ Fin ) → ( ( ♯ ‘ 𝑚 ) ≤ ( ♯ ‘ 𝑘 ) ↔ ¬ ( ♯ ‘ 𝑘 ) < ( ♯ ‘ 𝑚 ) ) ) |
114 |
105 106 113
|
syl2anc |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → ( ( ♯ ‘ 𝑚 ) ≤ ( ♯ ‘ 𝑘 ) ↔ ¬ ( ♯ ‘ 𝑘 ) < ( ♯ ‘ 𝑚 ) ) ) |
115 |
102 114
|
mpbid |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → ¬ ( ♯ ‘ 𝑘 ) < ( ♯ ‘ 𝑚 ) ) |
116 |
|
php3 |
⊢ ( ( 𝑚 ∈ Fin ∧ 𝑘 ⊊ 𝑚 ) → 𝑘 ≺ 𝑚 ) |
117 |
116
|
ex |
⊢ ( 𝑚 ∈ Fin → ( 𝑘 ⊊ 𝑚 → 𝑘 ≺ 𝑚 ) ) |
118 |
105 117
|
syl |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → ( 𝑘 ⊊ 𝑚 → 𝑘 ≺ 𝑚 ) ) |
119 |
|
hashsdom |
⊢ ( ( 𝑘 ∈ Fin ∧ 𝑚 ∈ Fin ) → ( ( ♯ ‘ 𝑘 ) < ( ♯ ‘ 𝑚 ) ↔ 𝑘 ≺ 𝑚 ) ) |
120 |
106 105 119
|
syl2anc |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → ( ( ♯ ‘ 𝑘 ) < ( ♯ ‘ 𝑚 ) ↔ 𝑘 ≺ 𝑚 ) ) |
121 |
118 120
|
sylibrd |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → ( 𝑘 ⊊ 𝑚 → ( ♯ ‘ 𝑘 ) < ( ♯ ‘ 𝑚 ) ) ) |
122 |
115 121
|
mtod |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → ¬ 𝑘 ⊊ 𝑚 ) |
123 |
|
sspss |
⊢ ( 𝑘 ⊆ 𝑚 ↔ ( 𝑘 ⊊ 𝑚 ∨ 𝑘 = 𝑚 ) ) |
124 |
84 123
|
sylib |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → ( 𝑘 ⊊ 𝑚 ∨ 𝑘 = 𝑚 ) ) |
125 |
124
|
ord |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → ( ¬ 𝑘 ⊊ 𝑚 → 𝑘 = 𝑚 ) ) |
126 |
122 125
|
mpd |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ ( 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) → 𝑘 = 𝑚 ) |
127 |
126
|
expr |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) → 𝑘 = 𝑚 ) ) |
128 |
81
|
simpld |
⊢ ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) → 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) |
129 |
128
|
adantr |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) |
130 |
|
oveq2 |
⊢ ( 𝑘 = 𝑚 → ( 𝐺 ↾s 𝑘 ) = ( 𝐺 ↾s 𝑚 ) ) |
131 |
130
|
breq2d |
⊢ ( 𝑘 = 𝑚 → ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ↔ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) |
132 |
|
eqimss |
⊢ ( 𝑘 = 𝑚 → 𝑘 ⊆ 𝑚 ) |
133 |
132
|
biantrurd |
⊢ ( 𝑘 = 𝑚 → ( 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ↔ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) |
134 |
131 133
|
bitrd |
⊢ ( 𝑘 = 𝑚 → ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ↔ ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) |
135 |
129 134
|
syl5ibcom |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑘 = 𝑚 → ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ) ) |
136 |
127 135
|
impbid |
⊢ ( ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) ∧ 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ↔ 𝑘 = 𝑚 ) ) |
137 |
136
|
ralrimiva |
⊢ ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) → ∀ 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ↔ 𝑘 = 𝑚 ) ) |
138 |
|
isslw |
⊢ ( 𝑘 ∈ ( 𝑃 pSyl 𝐺 ) ↔ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑚 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑘 ⊆ 𝑚 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑚 ) ) ↔ 𝑘 = 𝑚 ) ) ) |
139 |
72 73 137 138
|
syl3anbrc |
⊢ ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) → 𝑘 ∈ ( 𝑃 pSyl 𝐺 ) ) |
140 |
81
|
simprd |
⊢ ( ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ∧ 𝐻 ⊆ 𝑘 ) ∧ ( 𝐹 ‘ 𝑘 ) = sup ( ran 𝐹 , ℝ , < ) ) ) ) → 𝐻 ⊆ 𝑘 ) |
141 |
69 139 140
|
reximssdv |
⊢ ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆 ) → ∃ 𝑘 ∈ ( 𝑃 pSyl 𝐺 ) 𝐻 ⊆ 𝑘 ) |