Step | Hyp | Ref
| Expression |
1 | | vex 3438 |
. . . . . 6
⊢ 𝑤 ∈ V |
2 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → 𝐴 ∈ 𝑍) |
3 | | elecg 8561 |
. . . . . 6
⊢ ((𝑤 ∈ V ∧ 𝐴 ∈ 𝑍) → (𝑤 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝑤)) |
4 | 1, 2, 3 | sylancr 586 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → (𝑤 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝑤)) |
5 | | sylow2a.r |
. . . . . . . 8
⊢ ∼ =
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} |
6 | 5 | gaorb 18941 |
. . . . . . 7
⊢ (𝐴 ∼ 𝑤 ↔ (𝐴 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ∧ ∃𝑘 ∈ 𝑋 (𝑘 ⊕ 𝐴) = 𝑤)) |
7 | 6 | simp3bi 1145 |
. . . . . 6
⊢ (𝐴 ∼ 𝑤 → ∃𝑘 ∈ 𝑋 (𝑘 ⊕ 𝐴) = 𝑤) |
8 | | oveq2 7303 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 𝐴 → (ℎ ⊕ 𝑢) = (ℎ ⊕ 𝐴)) |
9 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 𝐴 → 𝑢 = 𝐴) |
10 | 8, 9 | eqeq12d 2749 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝐴 → ((ℎ ⊕ 𝑢) = 𝑢 ↔ (ℎ ⊕ 𝐴) = 𝐴)) |
11 | 10 | ralbidv 3168 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝐴 → (∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑢) = 𝑢 ↔ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝐴) = 𝐴)) |
12 | | sylow2a.z |
. . . . . . . . . . . 12
⊢ 𝑍 = {𝑢 ∈ 𝑌 ∣ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑢) = 𝑢} |
13 | 11, 12 | elrab2 3629 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑍 ↔ (𝐴 ∈ 𝑌 ∧ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝐴) = 𝐴)) |
14 | 2, 13 | sylib 217 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → (𝐴 ∈ 𝑌 ∧ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝐴) = 𝐴)) |
15 | 14 | simprd 495 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝐴) = 𝐴) |
16 | | oveq1 7302 |
. . . . . . . . . . 11
⊢ (ℎ = 𝑘 → (ℎ ⊕ 𝐴) = (𝑘 ⊕ 𝐴)) |
17 | 16 | eqeq1d 2735 |
. . . . . . . . . 10
⊢ (ℎ = 𝑘 → ((ℎ ⊕ 𝐴) = 𝐴 ↔ (𝑘 ⊕ 𝐴) = 𝐴)) |
18 | 17 | rspccva 3562 |
. . . . . . . . 9
⊢
((∀ℎ ∈
𝑋 (ℎ ⊕ 𝐴) = 𝐴 ∧ 𝑘 ∈ 𝑋) → (𝑘 ⊕ 𝐴) = 𝐴) |
19 | 15, 18 | sylan 579 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → (𝑘 ⊕ 𝐴) = 𝐴) |
20 | | eqeq1 2737 |
. . . . . . . 8
⊢ ((𝑘 ⊕ 𝐴) = 𝑤 → ((𝑘 ⊕ 𝐴) = 𝐴 ↔ 𝑤 = 𝐴)) |
21 | 19, 20 | syl5ibcom 244 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → ((𝑘 ⊕ 𝐴) = 𝑤 → 𝑤 = 𝐴)) |
22 | 21 | rexlimdva 3146 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → (∃𝑘 ∈ 𝑋 (𝑘 ⊕ 𝐴) = 𝑤 → 𝑤 = 𝐴)) |
23 | 7, 22 | syl5 34 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → (𝐴 ∼ 𝑤 → 𝑤 = 𝐴)) |
24 | 4, 23 | sylbid 239 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → (𝑤 ∈ [𝐴] ∼ → 𝑤 = 𝐴)) |
25 | | velsn 4580 |
. . . 4
⊢ (𝑤 ∈ {𝐴} ↔ 𝑤 = 𝐴) |
26 | 24, 25 | syl6ibr 251 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → (𝑤 ∈ [𝐴] ∼ → 𝑤 ∈ {𝐴})) |
27 | 26 | ssrdv 3929 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → [𝐴] ∼ ⊆ {𝐴}) |
28 | | sylow2a.m |
. . . . . . 7
⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct 𝑌)) |
29 | | sylow2a.x |
. . . . . . . 8
⊢ 𝑋 = (Base‘𝐺) |
30 | 5, 29 | gaorber 18942 |
. . . . . . 7
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) → ∼ Er 𝑌) |
31 | 28, 30 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∼ Er 𝑌) |
32 | 31 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → ∼ Er 𝑌) |
33 | 14 | simpld 494 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → 𝐴 ∈ 𝑌) |
34 | 32, 33 | erref 8538 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → 𝐴 ∼ 𝐴) |
35 | | elecg 8561 |
. . . . 5
⊢ ((𝐴 ∈ 𝑍 ∧ 𝐴 ∈ 𝑍) → (𝐴 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝐴)) |
36 | 2, 35 | sylancom 587 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → (𝐴 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝐴)) |
37 | 34, 36 | mpbird 256 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → 𝐴 ∈ [𝐴] ∼ ) |
38 | 37 | snssd 4745 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → {𝐴} ⊆ [𝐴] ∼ ) |
39 | 27, 38 | eqssd 3940 |
1
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → [𝐴] ∼ = {𝐴}) |