Step | Hyp | Ref
| Expression |
1 | | pwmnd.b |
. . . . . 6
⊢
(Base‘𝑀) =
𝒫 𝐴 |
2 | 1 | eleq2i 2825 |
. . . . 5
⊢ (𝑎 ∈ (Base‘𝑀) ↔ 𝑎 ∈ 𝒫 𝐴) |
3 | 1 | eleq2i 2825 |
. . . . 5
⊢ (𝑏 ∈ (Base‘𝑀) ↔ 𝑏 ∈ 𝒫 𝐴) |
4 | | pwuncl 7514 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) → (𝑎 ∪ 𝑏) ∈ 𝒫 𝐴) |
5 | | pwmnd.p |
. . . . . . . 8
⊢
(+g‘𝑀) = (𝑥 ∈ 𝒫 𝐴, 𝑦 ∈ 𝒫 𝐴 ↦ (𝑥 ∪ 𝑦)) |
6 | 1, 5 | pwmndgplus 18219 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) → (𝑎(+g‘𝑀)𝑏) = (𝑎 ∪ 𝑏)) |
7 | 1 | a1i 11 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) → (Base‘𝑀) = 𝒫 𝐴) |
8 | 4, 6, 7 | 3eltr4d 2849 |
. . . . . 6
⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) → (𝑎(+g‘𝑀)𝑏) ∈ (Base‘𝑀)) |
9 | 1 | eleq2i 2825 |
. . . . . . . 8
⊢ (𝑐 ∈ (Base‘𝑀) ↔ 𝑐 ∈ 𝒫 𝐴) |
10 | | unass 4057 |
. . . . . . . . . 10
⊢ ((𝑎 ∪ 𝑏) ∪ 𝑐) = (𝑎 ∪ (𝑏 ∪ 𝑐)) |
11 | 6 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) ∧ 𝑐 ∈ 𝒫 𝐴) → (𝑎(+g‘𝑀)𝑏) = (𝑎 ∪ 𝑏)) |
12 | 11 | oveq1d 7188 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) ∧ 𝑐 ∈ 𝒫 𝐴) → ((𝑎(+g‘𝑀)𝑏)(+g‘𝑀)𝑐) = ((𝑎 ∪ 𝑏)(+g‘𝑀)𝑐)) |
13 | 1, 5 | pwmndgplus 18219 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∪ 𝑏) ∈ 𝒫 𝐴 ∧ 𝑐 ∈ 𝒫 𝐴) → ((𝑎 ∪ 𝑏)(+g‘𝑀)𝑐) = ((𝑎 ∪ 𝑏) ∪ 𝑐)) |
14 | 4, 13 | sylan 583 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) ∧ 𝑐 ∈ 𝒫 𝐴) → ((𝑎 ∪ 𝑏)(+g‘𝑀)𝑐) = ((𝑎 ∪ 𝑏) ∪ 𝑐)) |
15 | 12, 14 | eqtrd 2774 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) ∧ 𝑐 ∈ 𝒫 𝐴) → ((𝑎(+g‘𝑀)𝑏)(+g‘𝑀)𝑐) = ((𝑎 ∪ 𝑏) ∪ 𝑐)) |
16 | 1, 5 | pwmndgplus 18219 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ 𝒫 𝐴 ∧ 𝑐 ∈ 𝒫 𝐴) → (𝑏(+g‘𝑀)𝑐) = (𝑏 ∪ 𝑐)) |
17 | 16 | adantll 714 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) ∧ 𝑐 ∈ 𝒫 𝐴) → (𝑏(+g‘𝑀)𝑐) = (𝑏 ∪ 𝑐)) |
18 | 17 | oveq2d 7189 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) ∧ 𝑐 ∈ 𝒫 𝐴) → (𝑎(+g‘𝑀)(𝑏(+g‘𝑀)𝑐)) = (𝑎(+g‘𝑀)(𝑏 ∪ 𝑐))) |
19 | | simpll 767 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) ∧ 𝑐 ∈ 𝒫 𝐴) → 𝑎 ∈ 𝒫 𝐴) |
20 | | pwuncl 7514 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ 𝒫 𝐴 ∧ 𝑐 ∈ 𝒫 𝐴) → (𝑏 ∪ 𝑐) ∈ 𝒫 𝐴) |
21 | 20 | adantll 714 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) ∧ 𝑐 ∈ 𝒫 𝐴) → (𝑏 ∪ 𝑐) ∈ 𝒫 𝐴) |
22 | 19, 21 | jca 515 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) ∧ 𝑐 ∈ 𝒫 𝐴) → (𝑎 ∈ 𝒫 𝐴 ∧ (𝑏 ∪ 𝑐) ∈ 𝒫 𝐴)) |
23 | 1, 5 | pwmndgplus 18219 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ (𝑏 ∪ 𝑐) ∈ 𝒫 𝐴) → (𝑎(+g‘𝑀)(𝑏 ∪ 𝑐)) = (𝑎 ∪ (𝑏 ∪ 𝑐))) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) ∧ 𝑐 ∈ 𝒫 𝐴) → (𝑎(+g‘𝑀)(𝑏 ∪ 𝑐)) = (𝑎 ∪ (𝑏 ∪ 𝑐))) |
25 | 18, 24 | eqtrd 2774 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) ∧ 𝑐 ∈ 𝒫 𝐴) → (𝑎(+g‘𝑀)(𝑏(+g‘𝑀)𝑐)) = (𝑎 ∪ (𝑏 ∪ 𝑐))) |
26 | 10, 15, 25 | 3eqtr4a 2800 |
. . . . . . . . 9
⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) ∧ 𝑐 ∈ 𝒫 𝐴) → ((𝑎(+g‘𝑀)𝑏)(+g‘𝑀)𝑐) = (𝑎(+g‘𝑀)(𝑏(+g‘𝑀)𝑐))) |
27 | 26 | ex 416 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) → (𝑐 ∈ 𝒫 𝐴 → ((𝑎(+g‘𝑀)𝑏)(+g‘𝑀)𝑐) = (𝑎(+g‘𝑀)(𝑏(+g‘𝑀)𝑐)))) |
28 | 9, 27 | syl5bi 245 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) → (𝑐 ∈ (Base‘𝑀) → ((𝑎(+g‘𝑀)𝑏)(+g‘𝑀)𝑐) = (𝑎(+g‘𝑀)(𝑏(+g‘𝑀)𝑐)))) |
29 | 28 | ralrimiv 3096 |
. . . . . 6
⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) → ∀𝑐 ∈ (Base‘𝑀)((𝑎(+g‘𝑀)𝑏)(+g‘𝑀)𝑐) = (𝑎(+g‘𝑀)(𝑏(+g‘𝑀)𝑐))) |
30 | 8, 29 | jca 515 |
. . . . 5
⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) → ((𝑎(+g‘𝑀)𝑏) ∈ (Base‘𝑀) ∧ ∀𝑐 ∈ (Base‘𝑀)((𝑎(+g‘𝑀)𝑏)(+g‘𝑀)𝑐) = (𝑎(+g‘𝑀)(𝑏(+g‘𝑀)𝑐)))) |
31 | 2, 3, 30 | syl2anb 601 |
. . . 4
⊢ ((𝑎 ∈ (Base‘𝑀) ∧ 𝑏 ∈ (Base‘𝑀)) → ((𝑎(+g‘𝑀)𝑏) ∈ (Base‘𝑀) ∧ ∀𝑐 ∈ (Base‘𝑀)((𝑎(+g‘𝑀)𝑏)(+g‘𝑀)𝑐) = (𝑎(+g‘𝑀)(𝑏(+g‘𝑀)𝑐)))) |
32 | 31 | rgen2 3116 |
. . 3
⊢
∀𝑎 ∈
(Base‘𝑀)∀𝑏 ∈ (Base‘𝑀)((𝑎(+g‘𝑀)𝑏) ∈ (Base‘𝑀) ∧ ∀𝑐 ∈ (Base‘𝑀)((𝑎(+g‘𝑀)𝑏)(+g‘𝑀)𝑐) = (𝑎(+g‘𝑀)(𝑏(+g‘𝑀)𝑐))) |
33 | | 0ex 5176 |
. . . . 5
⊢ ∅
∈ V |
34 | | eleq1 2821 |
. . . . . 6
⊢ (𝑒 = ∅ → (𝑒 ∈ (Base‘𝑀) ↔ ∅ ∈
(Base‘𝑀))) |
35 | | oveq1 7180 |
. . . . . . . . 9
⊢ (𝑒 = ∅ → (𝑒(+g‘𝑀)𝑎) = (∅(+g‘𝑀)𝑎)) |
36 | 35 | eqeq1d 2741 |
. . . . . . . 8
⊢ (𝑒 = ∅ → ((𝑒(+g‘𝑀)𝑎) = 𝑎 ↔ (∅(+g‘𝑀)𝑎) = 𝑎)) |
37 | | oveq2 7181 |
. . . . . . . . 9
⊢ (𝑒 = ∅ → (𝑎(+g‘𝑀)𝑒) = (𝑎(+g‘𝑀)∅)) |
38 | 37 | eqeq1d 2741 |
. . . . . . . 8
⊢ (𝑒 = ∅ → ((𝑎(+g‘𝑀)𝑒) = 𝑎 ↔ (𝑎(+g‘𝑀)∅) = 𝑎)) |
39 | 36, 38 | anbi12d 634 |
. . . . . . 7
⊢ (𝑒 = ∅ → (((𝑒(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)𝑒) = 𝑎) ↔ ((∅(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)∅) = 𝑎))) |
40 | 39 | ralbidv 3110 |
. . . . . 6
⊢ (𝑒 = ∅ → (∀𝑎 ∈ (Base‘𝑀)((𝑒(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)𝑒) = 𝑎) ↔ ∀𝑎 ∈ (Base‘𝑀)((∅(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)∅) = 𝑎))) |
41 | 34, 40 | anbi12d 634 |
. . . . 5
⊢ (𝑒 = ∅ → ((𝑒 ∈ (Base‘𝑀) ∧ ∀𝑎 ∈ (Base‘𝑀)((𝑒(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)𝑒) = 𝑎)) ↔ (∅ ∈ (Base‘𝑀) ∧ ∀𝑎 ∈ (Base‘𝑀)((∅(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)∅) = 𝑎)))) |
42 | | 0elpw 5223 |
. . . . . . 7
⊢ ∅
∈ 𝒫 𝐴 |
43 | 42, 1 | eleqtrri 2833 |
. . . . . 6
⊢ ∅
∈ (Base‘𝑀) |
44 | 1, 5 | pwmndgplus 18219 |
. . . . . . . . . . 11
⊢ ((∅
∈ 𝒫 𝐴 ∧
𝑎 ∈ 𝒫 𝐴) →
(∅(+g‘𝑀)𝑎) = (∅ ∪ 𝑎)) |
45 | | 0un 4282 |
. . . . . . . . . . 11
⊢ (∅
∪ 𝑎) = 𝑎 |
46 | 44, 45 | eqtrdi 2790 |
. . . . . . . . . 10
⊢ ((∅
∈ 𝒫 𝐴 ∧
𝑎 ∈ 𝒫 𝐴) →
(∅(+g‘𝑀)𝑎) = 𝑎) |
47 | 1, 5 | pwmndgplus 18219 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ ∅ ∈ 𝒫
𝐴) → (𝑎(+g‘𝑀)∅) = (𝑎 ∪ ∅)) |
48 | 47 | ancoms 462 |
. . . . . . . . . . 11
⊢ ((∅
∈ 𝒫 𝐴 ∧
𝑎 ∈ 𝒫 𝐴) → (𝑎(+g‘𝑀)∅) = (𝑎 ∪ ∅)) |
49 | | un0 4280 |
. . . . . . . . . . 11
⊢ (𝑎 ∪ ∅) = 𝑎 |
50 | 48, 49 | eqtrdi 2790 |
. . . . . . . . . 10
⊢ ((∅
∈ 𝒫 𝐴 ∧
𝑎 ∈ 𝒫 𝐴) → (𝑎(+g‘𝑀)∅) = 𝑎) |
51 | 46, 50 | jca 515 |
. . . . . . . . 9
⊢ ((∅
∈ 𝒫 𝐴 ∧
𝑎 ∈ 𝒫 𝐴) →
((∅(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)∅) = 𝑎)) |
52 | 42, 51 | mpan 690 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝒫 𝐴 →
((∅(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)∅) = 𝑎)) |
53 | 2, 52 | sylbi 220 |
. . . . . . 7
⊢ (𝑎 ∈ (Base‘𝑀) →
((∅(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)∅) = 𝑎)) |
54 | 53 | rgen 3064 |
. . . . . 6
⊢
∀𝑎 ∈
(Base‘𝑀)((∅(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)∅) = 𝑎) |
55 | 43, 54 | pm3.2i 474 |
. . . . 5
⊢ (∅
∈ (Base‘𝑀) ∧
∀𝑎 ∈
(Base‘𝑀)((∅(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)∅) = 𝑎)) |
56 | 33, 41, 55 | ceqsexv2d 3447 |
. . . 4
⊢
∃𝑒(𝑒 ∈ (Base‘𝑀) ∧ ∀𝑎 ∈ (Base‘𝑀)((𝑒(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)𝑒) = 𝑎)) |
57 | | df-rex 3060 |
. . . 4
⊢
(∃𝑒 ∈
(Base‘𝑀)∀𝑎 ∈ (Base‘𝑀)((𝑒(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)𝑒) = 𝑎) ↔ ∃𝑒(𝑒 ∈ (Base‘𝑀) ∧ ∀𝑎 ∈ (Base‘𝑀)((𝑒(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)𝑒) = 𝑎))) |
58 | 56, 57 | mpbir 234 |
. . 3
⊢
∃𝑒 ∈
(Base‘𝑀)∀𝑎 ∈ (Base‘𝑀)((𝑒(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)𝑒) = 𝑎) |
59 | 32, 58 | pm3.2i 474 |
. 2
⊢
(∀𝑎 ∈
(Base‘𝑀)∀𝑏 ∈ (Base‘𝑀)((𝑎(+g‘𝑀)𝑏) ∈ (Base‘𝑀) ∧ ∀𝑐 ∈ (Base‘𝑀)((𝑎(+g‘𝑀)𝑏)(+g‘𝑀)𝑐) = (𝑎(+g‘𝑀)(𝑏(+g‘𝑀)𝑐))) ∧ ∃𝑒 ∈ (Base‘𝑀)∀𝑎 ∈ (Base‘𝑀)((𝑒(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)𝑒) = 𝑎)) |
60 | | eqid 2739 |
. . 3
⊢
(Base‘𝑀) =
(Base‘𝑀) |
61 | | eqid 2739 |
. . 3
⊢
(+g‘𝑀) = (+g‘𝑀) |
62 | 60, 61 | ismnd 18033 |
. 2
⊢ (𝑀 ∈ Mnd ↔
(∀𝑎 ∈
(Base‘𝑀)∀𝑏 ∈ (Base‘𝑀)((𝑎(+g‘𝑀)𝑏) ∈ (Base‘𝑀) ∧ ∀𝑐 ∈ (Base‘𝑀)((𝑎(+g‘𝑀)𝑏)(+g‘𝑀)𝑐) = (𝑎(+g‘𝑀)(𝑏(+g‘𝑀)𝑐))) ∧ ∃𝑒 ∈ (Base‘𝑀)∀𝑎 ∈ (Base‘𝑀)((𝑒(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)𝑒) = 𝑎))) |
63 | 59, 62 | mpbir 234 |
1
⊢ 𝑀 ∈ Mnd |