| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (Base‘𝑚) = (Base‘𝑀)) |
| 2 | 1 | pweqd 4617 |
. . . . 5
⊢ (𝑚 = 𝑀 → 𝒫 (Base‘𝑚) = 𝒫 (Base‘𝑀)) |
| 3 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (0g‘𝑚) = (0g‘𝑀)) |
| 4 | 3 | eleq1d 2826 |
. . . . . 6
⊢ (𝑚 = 𝑀 → ((0g‘𝑚) ∈ 𝑡 ↔ (0g‘𝑀) ∈ 𝑡)) |
| 5 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑚 = 𝑀 → (+g‘𝑚) = (+g‘𝑀)) |
| 6 | 5 | oveqd 7448 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → (𝑥(+g‘𝑚)𝑦) = (𝑥(+g‘𝑀)𝑦)) |
| 7 | 6 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → ((𝑥(+g‘𝑚)𝑦) ∈ 𝑡 ↔ (𝑥(+g‘𝑀)𝑦) ∈ 𝑡)) |
| 8 | 7 | 2ralbidv 3221 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑚)𝑦) ∈ 𝑡 ↔ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑀)𝑦) ∈ 𝑡)) |
| 9 | 4, 8 | anbi12d 632 |
. . . . 5
⊢ (𝑚 = 𝑀 → (((0g‘𝑚) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑚)𝑦) ∈ 𝑡) ↔ ((0g‘𝑀) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑀)𝑦) ∈ 𝑡))) |
| 10 | 2, 9 | rabeqbidv 3455 |
. . . 4
⊢ (𝑚 = 𝑀 → {𝑡 ∈ 𝒫 (Base‘𝑚) ∣
((0g‘𝑚)
∈ 𝑡 ∧
∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑚)𝑦) ∈ 𝑡)} = {𝑡 ∈ 𝒫 (Base‘𝑀) ∣
((0g‘𝑀)
∈ 𝑡 ∧
∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑀)𝑦) ∈ 𝑡)}) |
| 11 | | df-submnd 18797 |
. . . 4
⊢ SubMnd =
(𝑚 ∈ Mnd ↦
{𝑡 ∈ 𝒫
(Base‘𝑚) ∣
((0g‘𝑚)
∈ 𝑡 ∧
∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑚)𝑦) ∈ 𝑡)}) |
| 12 | | fvex 6919 |
. . . . . 6
⊢
(Base‘𝑀)
∈ V |
| 13 | 12 | pwex 5380 |
. . . . 5
⊢ 𝒫
(Base‘𝑀) ∈
V |
| 14 | 13 | rabex 5339 |
. . . 4
⊢ {𝑡 ∈ 𝒫
(Base‘𝑀) ∣
((0g‘𝑀)
∈ 𝑡 ∧
∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑀)𝑦) ∈ 𝑡)} ∈ V |
| 15 | 10, 11, 14 | fvmpt 7016 |
. . 3
⊢ (𝑀 ∈ Mnd →
(SubMnd‘𝑀) = {𝑡 ∈ 𝒫
(Base‘𝑀) ∣
((0g‘𝑀)
∈ 𝑡 ∧
∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑀)𝑦) ∈ 𝑡)}) |
| 16 | 15 | eleq2d 2827 |
. 2
⊢ (𝑀 ∈ Mnd → (𝑆 ∈ (SubMnd‘𝑀) ↔ 𝑆 ∈ {𝑡 ∈ 𝒫 (Base‘𝑀) ∣
((0g‘𝑀)
∈ 𝑡 ∧
∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑀)𝑦) ∈ 𝑡)})) |
| 17 | | eleq2 2830 |
. . . . 5
⊢ (𝑡 = 𝑆 → ((0g‘𝑀) ∈ 𝑡 ↔ (0g‘𝑀) ∈ 𝑆)) |
| 18 | | eleq2 2830 |
. . . . . . 7
⊢ (𝑡 = 𝑆 → ((𝑥(+g‘𝑀)𝑦) ∈ 𝑡 ↔ (𝑥(+g‘𝑀)𝑦) ∈ 𝑆)) |
| 19 | 18 | raleqbi1dv 3338 |
. . . . . 6
⊢ (𝑡 = 𝑆 → (∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑀)𝑦) ∈ 𝑡 ↔ ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆)) |
| 20 | 19 | raleqbi1dv 3338 |
. . . . 5
⊢ (𝑡 = 𝑆 → (∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑀)𝑦) ∈ 𝑡 ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆)) |
| 21 | 17, 20 | anbi12d 632 |
. . . 4
⊢ (𝑡 = 𝑆 → (((0g‘𝑀) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑀)𝑦) ∈ 𝑡) ↔ ((0g‘𝑀) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆))) |
| 22 | 21 | elrab 3692 |
. . 3
⊢ (𝑆 ∈ {𝑡 ∈ 𝒫 (Base‘𝑀) ∣
((0g‘𝑀)
∈ 𝑡 ∧
∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑀)𝑦) ∈ 𝑡)} ↔ (𝑆 ∈ 𝒫 (Base‘𝑀) ∧
((0g‘𝑀)
∈ 𝑆 ∧
∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆))) |
| 23 | | issubm.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑀) |
| 24 | 23 | sseq2i 4013 |
. . . . 5
⊢ (𝑆 ⊆ 𝐵 ↔ 𝑆 ⊆ (Base‘𝑀)) |
| 25 | | issubm.z |
. . . . . . 7
⊢ 0 =
(0g‘𝑀) |
| 26 | 25 | eleq1i 2832 |
. . . . . 6
⊢ ( 0 ∈ 𝑆 ↔
(0g‘𝑀)
∈ 𝑆) |
| 27 | | issubm.p |
. . . . . . . . 9
⊢ + =
(+g‘𝑀) |
| 28 | 27 | oveqi 7444 |
. . . . . . . 8
⊢ (𝑥 + 𝑦) = (𝑥(+g‘𝑀)𝑦) |
| 29 | 28 | eleq1i 2832 |
. . . . . . 7
⊢ ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) |
| 30 | 29 | 2ralbii 3128 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆) |
| 31 | 26, 30 | anbi12i 628 |
. . . . 5
⊢ (( 0 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) ↔ ((0g‘𝑀) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆)) |
| 32 | 24, 31 | anbi12i 628 |
. . . 4
⊢ ((𝑆 ⊆ 𝐵 ∧ ( 0 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)) ↔ (𝑆 ⊆ (Base‘𝑀) ∧ ((0g‘𝑀) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆))) |
| 33 | | 3anass 1095 |
. . . 4
⊢ ((𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) ↔ (𝑆 ⊆ 𝐵 ∧ ( 0 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆))) |
| 34 | 12 | elpw2 5334 |
. . . . 5
⊢ (𝑆 ∈ 𝒫
(Base‘𝑀) ↔ 𝑆 ⊆ (Base‘𝑀)) |
| 35 | 34 | anbi1i 624 |
. . . 4
⊢ ((𝑆 ∈ 𝒫
(Base‘𝑀) ∧
((0g‘𝑀)
∈ 𝑆 ∧
∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆)) ↔ (𝑆 ⊆ (Base‘𝑀) ∧ ((0g‘𝑀) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆))) |
| 36 | 32, 33, 35 | 3bitr4ri 304 |
. . 3
⊢ ((𝑆 ∈ 𝒫
(Base‘𝑀) ∧
((0g‘𝑀)
∈ 𝑆 ∧
∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑀)𝑦) ∈ 𝑆)) ↔ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)) |
| 37 | 22, 36 | bitri 275 |
. 2
⊢ (𝑆 ∈ {𝑡 ∈ 𝒫 (Base‘𝑀) ∣
((0g‘𝑀)
∈ 𝑡 ∧
∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑀)𝑦) ∈ 𝑡)} ↔ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)) |
| 38 | 16, 37 | bitrdi 287 |
1
⊢ (𝑀 ∈ Mnd → (𝑆 ∈ (SubMnd‘𝑀) ↔ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆))) |