| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | submacs.b | . . . . . 6
⊢ 𝐵 = (Base‘𝐺) | 
| 2 |  | eqid 2737 | . . . . . 6
⊢
(0g‘𝐺) = (0g‘𝐺) | 
| 3 |  | eqid 2737 | . . . . . 6
⊢
(+g‘𝐺) = (+g‘𝐺) | 
| 4 | 1, 2, 3 | issubm 18816 | . . . . 5
⊢ (𝐺 ∈ Mnd → (𝑠 ∈ (SubMnd‘𝐺) ↔ (𝑠 ⊆ 𝐵 ∧ (0g‘𝐺) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝐺)𝑦) ∈ 𝑠))) | 
| 5 |  | velpw 4605 | . . . . . . 7
⊢ (𝑠 ∈ 𝒫 𝐵 ↔ 𝑠 ⊆ 𝐵) | 
| 6 | 5 | anbi1i 624 | . . . . . 6
⊢ ((𝑠 ∈ 𝒫 𝐵 ∧
((0g‘𝐺)
∈ 𝑠 ∧
∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝐺)𝑦) ∈ 𝑠)) ↔ (𝑠 ⊆ 𝐵 ∧ ((0g‘𝐺) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝐺)𝑦) ∈ 𝑠))) | 
| 7 |  | 3anass 1095 | . . . . . 6
⊢ ((𝑠 ⊆ 𝐵 ∧ (0g‘𝐺) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝐺)𝑦) ∈ 𝑠) ↔ (𝑠 ⊆ 𝐵 ∧ ((0g‘𝐺) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝐺)𝑦) ∈ 𝑠))) | 
| 8 | 6, 7 | bitr4i 278 | . . . . 5
⊢ ((𝑠 ∈ 𝒫 𝐵 ∧
((0g‘𝐺)
∈ 𝑠 ∧
∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝐺)𝑦) ∈ 𝑠)) ↔ (𝑠 ⊆ 𝐵 ∧ (0g‘𝐺) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝐺)𝑦) ∈ 𝑠)) | 
| 9 | 4, 8 | bitr4di 289 | . . . 4
⊢ (𝐺 ∈ Mnd → (𝑠 ∈ (SubMnd‘𝐺) ↔ (𝑠 ∈ 𝒫 𝐵 ∧ ((0g‘𝐺) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝐺)𝑦) ∈ 𝑠)))) | 
| 10 | 9 | eqabdv 2875 | . . 3
⊢ (𝐺 ∈ Mnd →
(SubMnd‘𝐺) = {𝑠 ∣ (𝑠 ∈ 𝒫 𝐵 ∧ ((0g‘𝐺) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝐺)𝑦) ∈ 𝑠))}) | 
| 11 |  | df-rab 3437 | . . 3
⊢ {𝑠 ∈ 𝒫 𝐵 ∣
((0g‘𝐺)
∈ 𝑠 ∧
∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝐺)𝑦) ∈ 𝑠)} = {𝑠 ∣ (𝑠 ∈ 𝒫 𝐵 ∧ ((0g‘𝐺) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝐺)𝑦) ∈ 𝑠))} | 
| 12 | 10, 11 | eqtr4di 2795 | . 2
⊢ (𝐺 ∈ Mnd →
(SubMnd‘𝐺) = {𝑠 ∈ 𝒫 𝐵 ∣
((0g‘𝐺)
∈ 𝑠 ∧
∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝐺)𝑦) ∈ 𝑠)}) | 
| 13 |  | inrab 4316 | . . 3
⊢ ({𝑠 ∈ 𝒫 𝐵 ∣
(0g‘𝐺)
∈ 𝑠} ∩ {𝑠 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝐺)𝑦) ∈ 𝑠}) = {𝑠 ∈ 𝒫 𝐵 ∣ ((0g‘𝐺) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝐺)𝑦) ∈ 𝑠)} | 
| 14 | 1 | fvexi 6920 | . . . . 5
⊢ 𝐵 ∈ V | 
| 15 |  | mreacs 17701 | . . . . 5
⊢ (𝐵 ∈ V →
(ACS‘𝐵) ∈
(Moore‘𝒫 𝐵)) | 
| 16 | 14, 15 | mp1i 13 | . . . 4
⊢ (𝐺 ∈ Mnd →
(ACS‘𝐵) ∈
(Moore‘𝒫 𝐵)) | 
| 17 | 1, 2 | mndidcl 18762 | . . . . 5
⊢ (𝐺 ∈ Mnd →
(0g‘𝐺)
∈ 𝐵) | 
| 18 |  | acsfn0 17703 | . . . . 5
⊢ ((𝐵 ∈ V ∧
(0g‘𝐺)
∈ 𝐵) → {𝑠 ∈ 𝒫 𝐵 ∣
(0g‘𝐺)
∈ 𝑠} ∈
(ACS‘𝐵)) | 
| 19 | 14, 17, 18 | sylancr 587 | . . . 4
⊢ (𝐺 ∈ Mnd → {𝑠 ∈ 𝒫 𝐵 ∣
(0g‘𝐺)
∈ 𝑠} ∈
(ACS‘𝐵)) | 
| 20 | 1, 3 | mndcl 18755 | . . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(+g‘𝐺)𝑦) ∈ 𝐵) | 
| 21 | 20 | 3expb 1121 | . . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐺)𝑦) ∈ 𝐵) | 
| 22 | 21 | ralrimivva 3202 | . . . . 5
⊢ (𝐺 ∈ Mnd → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥(+g‘𝐺)𝑦) ∈ 𝐵) | 
| 23 |  | acsfn2 17706 | . . . . 5
⊢ ((𝐵 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥(+g‘𝐺)𝑦) ∈ 𝐵) → {𝑠 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝐺)𝑦) ∈ 𝑠} ∈ (ACS‘𝐵)) | 
| 24 | 14, 22, 23 | sylancr 587 | . . . 4
⊢ (𝐺 ∈ Mnd → {𝑠 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝐺)𝑦) ∈ 𝑠} ∈ (ACS‘𝐵)) | 
| 25 |  | mreincl 17642 | . . . 4
⊢
(((ACS‘𝐵)
∈ (Moore‘𝒫 𝐵) ∧ {𝑠 ∈ 𝒫 𝐵 ∣ (0g‘𝐺) ∈ 𝑠} ∈ (ACS‘𝐵) ∧ {𝑠 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝐺)𝑦) ∈ 𝑠} ∈ (ACS‘𝐵)) → ({𝑠 ∈ 𝒫 𝐵 ∣ (0g‘𝐺) ∈ 𝑠} ∩ {𝑠 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝐺)𝑦) ∈ 𝑠}) ∈ (ACS‘𝐵)) | 
| 26 | 16, 19, 24, 25 | syl3anc 1373 | . . 3
⊢ (𝐺 ∈ Mnd → ({𝑠 ∈ 𝒫 𝐵 ∣
(0g‘𝐺)
∈ 𝑠} ∩ {𝑠 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝐺)𝑦) ∈ 𝑠}) ∈ (ACS‘𝐵)) | 
| 27 | 13, 26 | eqeltrrid 2846 | . 2
⊢ (𝐺 ∈ Mnd → {𝑠 ∈ 𝒫 𝐵 ∣
((0g‘𝐺)
∈ 𝑠 ∧
∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝐺)𝑦) ∈ 𝑠)} ∈ (ACS‘𝐵)) | 
| 28 | 12, 27 | eqeltrd 2841 | 1
⊢ (𝐺 ∈ Mnd →
(SubMnd‘𝐺) ∈
(ACS‘𝐵)) |