| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | vex 3484 | . . . . . 6
⊢ 𝑤 ∈ V | 
| 2 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → 𝐴 ∈ 𝑍) | 
| 3 |  | elecg 8789 | . . . . . 6
⊢ ((𝑤 ∈ V ∧ 𝐴 ∈ 𝑍) → (𝑤 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝑤)) | 
| 4 | 1, 2, 3 | sylancr 587 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → (𝑤 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝑤)) | 
| 5 |  | sylow2a.r | . . . . . . . 8
⊢  ∼ =
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} | 
| 6 | 5 | gaorb 19325 | . . . . . . 7
⊢ (𝐴 ∼ 𝑤 ↔ (𝐴 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ∧ ∃𝑘 ∈ 𝑋 (𝑘 ⊕ 𝐴) = 𝑤)) | 
| 7 | 6 | simp3bi 1148 | . . . . . 6
⊢ (𝐴 ∼ 𝑤 → ∃𝑘 ∈ 𝑋 (𝑘 ⊕ 𝐴) = 𝑤) | 
| 8 |  | oveq2 7439 | . . . . . . . . . . . . . 14
⊢ (𝑢 = 𝐴 → (ℎ ⊕ 𝑢) = (ℎ ⊕ 𝐴)) | 
| 9 |  | id 22 | . . . . . . . . . . . . . 14
⊢ (𝑢 = 𝐴 → 𝑢 = 𝐴) | 
| 10 | 8, 9 | eqeq12d 2753 | . . . . . . . . . . . . 13
⊢ (𝑢 = 𝐴 → ((ℎ ⊕ 𝑢) = 𝑢 ↔ (ℎ ⊕ 𝐴) = 𝐴)) | 
| 11 | 10 | ralbidv 3178 | . . . . . . . . . . . 12
⊢ (𝑢 = 𝐴 → (∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑢) = 𝑢 ↔ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝐴) = 𝐴)) | 
| 12 |  | sylow2a.z | . . . . . . . . . . . 12
⊢ 𝑍 = {𝑢 ∈ 𝑌 ∣ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑢) = 𝑢} | 
| 13 | 11, 12 | elrab2 3695 | . . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑍 ↔ (𝐴 ∈ 𝑌 ∧ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝐴) = 𝐴)) | 
| 14 | 2, 13 | sylib 218 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → (𝐴 ∈ 𝑌 ∧ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝐴) = 𝐴)) | 
| 15 | 14 | simprd 495 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝐴) = 𝐴) | 
| 16 |  | oveq1 7438 | . . . . . . . . . . 11
⊢ (ℎ = 𝑘 → (ℎ ⊕ 𝐴) = (𝑘 ⊕ 𝐴)) | 
| 17 | 16 | eqeq1d 2739 | . . . . . . . . . 10
⊢ (ℎ = 𝑘 → ((ℎ ⊕ 𝐴) = 𝐴 ↔ (𝑘 ⊕ 𝐴) = 𝐴)) | 
| 18 | 17 | rspccva 3621 | . . . . . . . . 9
⊢
((∀ℎ ∈
𝑋 (ℎ ⊕ 𝐴) = 𝐴 ∧ 𝑘 ∈ 𝑋) → (𝑘 ⊕ 𝐴) = 𝐴) | 
| 19 | 15, 18 | sylan 580 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → (𝑘 ⊕ 𝐴) = 𝐴) | 
| 20 |  | eqeq1 2741 | . . . . . . . 8
⊢ ((𝑘 ⊕ 𝐴) = 𝑤 → ((𝑘 ⊕ 𝐴) = 𝐴 ↔ 𝑤 = 𝐴)) | 
| 21 | 19, 20 | syl5ibcom 245 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → ((𝑘 ⊕ 𝐴) = 𝑤 → 𝑤 = 𝐴)) | 
| 22 | 21 | rexlimdva 3155 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → (∃𝑘 ∈ 𝑋 (𝑘 ⊕ 𝐴) = 𝑤 → 𝑤 = 𝐴)) | 
| 23 | 7, 22 | syl5 34 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → (𝐴 ∼ 𝑤 → 𝑤 = 𝐴)) | 
| 24 | 4, 23 | sylbid 240 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → (𝑤 ∈ [𝐴] ∼ → 𝑤 = 𝐴)) | 
| 25 |  | velsn 4642 | . . . 4
⊢ (𝑤 ∈ {𝐴} ↔ 𝑤 = 𝐴) | 
| 26 | 24, 25 | imbitrrdi 252 | . . 3
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → (𝑤 ∈ [𝐴] ∼ → 𝑤 ∈ {𝐴})) | 
| 27 | 26 | ssrdv 3989 | . 2
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → [𝐴] ∼ ⊆ {𝐴}) | 
| 28 |  | sylow2a.m | . . . . . . 7
⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct 𝑌)) | 
| 29 |  | sylow2a.x | . . . . . . . 8
⊢ 𝑋 = (Base‘𝐺) | 
| 30 | 5, 29 | gaorber 19326 | . . . . . . 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 8765 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → 𝐴 ∼ 𝐴) | 
| 35 |  | elecg 8789 | . . . . 5
⊢ ((𝐴 ∈ 𝑍 ∧ 𝐴 ∈ 𝑍) → (𝐴 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝐴)) | 
| 36 | 2, 35 | sylancom 588 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → (𝐴 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝐴)) | 
| 37 | 34, 36 | mpbird 257 | . . 3
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → 𝐴 ∈ [𝐴] ∼ ) | 
| 38 | 37 | snssd 4809 | . 2
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → {𝐴} ⊆ [𝐴] ∼ ) | 
| 39 | 27, 38 | eqssd 4001 | 1
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → [𝐴] ∼ = {𝐴}) |