Proof of Theorem issubmd
Step | Hyp | Ref
| Expression |
1 | | ssrab2 3687 |
. . 3
⊢ {𝑧 ∈ 𝐵 ∣ 𝜓} ⊆ 𝐵 |
2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → {𝑧 ∈ 𝐵 ∣ 𝜓} ⊆ 𝐵) |
3 | | issubmd.m |
. . . 4
⊢ (𝜑 → 𝑀 ∈ Mnd) |
4 | | issubmd.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑀) |
5 | | issubmd.z |
. . . . 5
⊢ 0 =
(0g‘𝑀) |
6 | 4, 5 | mndidcl 17308 |
. . . 4
⊢ (𝑀 ∈ Mnd → 0 ∈ 𝐵) |
7 | 3, 6 | syl 17 |
. . 3
⊢ (𝜑 → 0 ∈ 𝐵) |
8 | | issubmd.cz |
. . 3
⊢ (𝜑 → 𝜒) |
9 | | issubmd.ch |
. . . 4
⊢ (𝑧 = 0 → (𝜓 ↔ 𝜒)) |
10 | 9 | elrab 3363 |
. . 3
⊢ ( 0 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓} ↔ ( 0 ∈ 𝐵 ∧ 𝜒)) |
11 | 7, 8, 10 | sylanbrc 698 |
. 2
⊢ (𝜑 → 0 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓}) |
12 | | issubmd.th |
. . . . . 6
⊢ (𝑧 = 𝑥 → (𝜓 ↔ 𝜃)) |
13 | 12 | elrab 3363 |
. . . . 5
⊢ (𝑥 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓} ↔ (𝑥 ∈ 𝐵 ∧ 𝜃)) |
14 | | issubmd.ta |
. . . . . 6
⊢ (𝑧 = 𝑦 → (𝜓 ↔ 𝜏)) |
15 | 14 | elrab 3363 |
. . . . 5
⊢ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓} ↔ (𝑦 ∈ 𝐵 ∧ 𝜏)) |
16 | 13, 15 | anbi12i 733 |
. . . 4
⊢ ((𝑥 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓} ∧ 𝑦 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓}) ↔ ((𝑥 ∈ 𝐵 ∧ 𝜃) ∧ (𝑦 ∈ 𝐵 ∧ 𝜏))) |
17 | 3 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝜃) ∧ (𝑦 ∈ 𝐵 ∧ 𝜏))) → 𝑀 ∈ Mnd) |
18 | | simprll 802 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝜃) ∧ (𝑦 ∈ 𝐵 ∧ 𝜏))) → 𝑥 ∈ 𝐵) |
19 | | simprrl 804 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝜃) ∧ (𝑦 ∈ 𝐵 ∧ 𝜏))) → 𝑦 ∈ 𝐵) |
20 | | issubmd.p |
. . . . . . 7
⊢ + =
(+g‘𝑀) |
21 | 4, 20 | mndcl 17301 |
. . . . . 6
⊢ ((𝑀 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) |
22 | 17, 18, 19, 21 | syl3anc 1326 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝜃) ∧ (𝑦 ∈ 𝐵 ∧ 𝜏))) → (𝑥 + 𝑦) ∈ 𝐵) |
23 | | an4 865 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐵 ∧ 𝜃) ∧ (𝑦 ∈ 𝐵 ∧ 𝜏)) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝜃 ∧ 𝜏))) |
24 | | issubmd.cp |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝜃 ∧ 𝜏))) → 𝜂) |
25 | 23, 24 | sylan2b 492 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝜃) ∧ (𝑦 ∈ 𝐵 ∧ 𝜏))) → 𝜂) |
26 | | issubmd.et |
. . . . . 6
⊢ (𝑧 = (𝑥 + 𝑦) → (𝜓 ↔ 𝜂)) |
27 | 26 | elrab 3363 |
. . . . 5
⊢ ((𝑥 + 𝑦) ∈ {𝑧 ∈ 𝐵 ∣ 𝜓} ↔ ((𝑥 + 𝑦) ∈ 𝐵 ∧ 𝜂)) |
28 | 22, 25, 27 | sylanbrc 698 |
. . . 4
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝜃) ∧ (𝑦 ∈ 𝐵 ∧ 𝜏))) → (𝑥 + 𝑦) ∈ {𝑧 ∈ 𝐵 ∣ 𝜓}) |
29 | 16, 28 | sylan2b 492 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓} ∧ 𝑦 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓})) → (𝑥 + 𝑦) ∈ {𝑧 ∈ 𝐵 ∣ 𝜓}) |
30 | 29 | ralrimivva 2971 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓}∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓} (𝑥 + 𝑦) ∈ {𝑧 ∈ 𝐵 ∣ 𝜓}) |
31 | 4, 5, 20 | issubm 17347 |
. . 3
⊢ (𝑀 ∈ Mnd → ({𝑧 ∈ 𝐵 ∣ 𝜓} ∈ (SubMnd‘𝑀) ↔ ({𝑧 ∈ 𝐵 ∣ 𝜓} ⊆ 𝐵 ∧ 0 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓} ∧ ∀𝑥 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓}∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓} (𝑥 + 𝑦) ∈ {𝑧 ∈ 𝐵 ∣ 𝜓}))) |
32 | 3, 31 | syl 17 |
. 2
⊢ (𝜑 → ({𝑧 ∈ 𝐵 ∣ 𝜓} ∈ (SubMnd‘𝑀) ↔ ({𝑧 ∈ 𝐵 ∣ 𝜓} ⊆ 𝐵 ∧ 0 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓} ∧ ∀𝑥 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓}∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ 𝜓} (𝑥 + 𝑦) ∈ {𝑧 ∈ 𝐵 ∣ 𝜓}))) |
33 | 2, 11, 30, 32 | mpbir3and 1245 |
1
⊢ (𝜑 → {𝑧 ∈ 𝐵 ∣ 𝜓} ∈ (SubMnd‘𝑀)) |