| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pwmnd.b | . . . . . 6
⊢
(Base‘𝑀) =
𝒫 𝐴 | 
| 2 | 1 | eleq2i 2833 | . . . . 5
⊢ (𝑎 ∈ (Base‘𝑀) ↔ 𝑎 ∈ 𝒫 𝐴) | 
| 3 | 1 | eleq2i 2833 | . . . . 5
⊢ (𝑏 ∈ (Base‘𝑀) ↔ 𝑏 ∈ 𝒫 𝐴) | 
| 4 |  | pwuncl 7790 | . . . . . . 7
⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) → (𝑎 ∪ 𝑏) ∈ 𝒫 𝐴) | 
| 5 |  | pwmnd.p | . . . . . . . 8
⊢
(+g‘𝑀) = (𝑥 ∈ 𝒫 𝐴, 𝑦 ∈ 𝒫 𝐴 ↦ (𝑥 ∪ 𝑦)) | 
| 6 | 1, 5 | pwmndgplus 18948 | . . . . . . 7
⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) → (𝑎(+g‘𝑀)𝑏) = (𝑎 ∪ 𝑏)) | 
| 7 | 1 | a1i 11 | . . . . . . 7
⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) → (Base‘𝑀) = 𝒫 𝐴) | 
| 8 | 4, 6, 7 | 3eltr4d 2856 | . . . . . 6
⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) → (𝑎(+g‘𝑀)𝑏) ∈ (Base‘𝑀)) | 
| 9 | 1 | eleq2i 2833 | . . . . . . . 8
⊢ (𝑐 ∈ (Base‘𝑀) ↔ 𝑐 ∈ 𝒫 𝐴) | 
| 10 |  | unass 4172 | . . . . . . . . . 10
⊢ ((𝑎 ∪ 𝑏) ∪ 𝑐) = (𝑎 ∪ (𝑏 ∪ 𝑐)) | 
| 11 | 6 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) ∧ 𝑐 ∈ 𝒫 𝐴) → (𝑎(+g‘𝑀)𝑏) = (𝑎 ∪ 𝑏)) | 
| 12 | 11 | oveq1d 7446 | . . . . . . . . . . 11
⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) ∧ 𝑐 ∈ 𝒫 𝐴) → ((𝑎(+g‘𝑀)𝑏)(+g‘𝑀)𝑐) = ((𝑎 ∪ 𝑏)(+g‘𝑀)𝑐)) | 
| 13 | 1, 5 | pwmndgplus 18948 | . . . . . . . . . . . 12
⊢ (((𝑎 ∪ 𝑏) ∈ 𝒫 𝐴 ∧ 𝑐 ∈ 𝒫 𝐴) → ((𝑎 ∪ 𝑏)(+g‘𝑀)𝑐) = ((𝑎 ∪ 𝑏) ∪ 𝑐)) | 
| 14 | 4, 13 | sylan 580 | . . . . . . . . . . 11
⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) ∧ 𝑐 ∈ 𝒫 𝐴) → ((𝑎 ∪ 𝑏)(+g‘𝑀)𝑐) = ((𝑎 ∪ 𝑏) ∪ 𝑐)) | 
| 15 | 12, 14 | eqtrd 2777 | . . . . . . . . . 10
⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) ∧ 𝑐 ∈ 𝒫 𝐴) → ((𝑎(+g‘𝑀)𝑏)(+g‘𝑀)𝑐) = ((𝑎 ∪ 𝑏) ∪ 𝑐)) | 
| 16 | 1, 5 | pwmndgplus 18948 | . . . . . . . . . . . . 13
⊢ ((𝑏 ∈ 𝒫 𝐴 ∧ 𝑐 ∈ 𝒫 𝐴) → (𝑏(+g‘𝑀)𝑐) = (𝑏 ∪ 𝑐)) | 
| 17 | 16 | adantll 714 | . . . . . . . . . . . 12
⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) ∧ 𝑐 ∈ 𝒫 𝐴) → (𝑏(+g‘𝑀)𝑐) = (𝑏 ∪ 𝑐)) | 
| 18 | 17 | oveq2d 7447 | . . . . . . . . . . 11
⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) ∧ 𝑐 ∈ 𝒫 𝐴) → (𝑎(+g‘𝑀)(𝑏(+g‘𝑀)𝑐)) = (𝑎(+g‘𝑀)(𝑏 ∪ 𝑐))) | 
| 19 |  | simpll 767 | . . . . . . . . . . . . 13
⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) ∧ 𝑐 ∈ 𝒫 𝐴) → 𝑎 ∈ 𝒫 𝐴) | 
| 20 |  | pwuncl 7790 | . . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ 𝒫 𝐴 ∧ 𝑐 ∈ 𝒫 𝐴) → (𝑏 ∪ 𝑐) ∈ 𝒫 𝐴) | 
| 21 | 20 | adantll 714 | . . . . . . . . . . . . 13
⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) ∧ 𝑐 ∈ 𝒫 𝐴) → (𝑏 ∪ 𝑐) ∈ 𝒫 𝐴) | 
| 22 | 19, 21 | jca 511 | . . . . . . . . . . . 12
⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) ∧ 𝑐 ∈ 𝒫 𝐴) → (𝑎 ∈ 𝒫 𝐴 ∧ (𝑏 ∪ 𝑐) ∈ 𝒫 𝐴)) | 
| 23 | 1, 5 | pwmndgplus 18948 | . . . . . . . . . . . 12
⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ (𝑏 ∪ 𝑐) ∈ 𝒫 𝐴) → (𝑎(+g‘𝑀)(𝑏 ∪ 𝑐)) = (𝑎 ∪ (𝑏 ∪ 𝑐))) | 
| 24 | 22, 23 | syl 17 | . . . . . . . . . . 11
⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) ∧ 𝑐 ∈ 𝒫 𝐴) → (𝑎(+g‘𝑀)(𝑏 ∪ 𝑐)) = (𝑎 ∪ (𝑏 ∪ 𝑐))) | 
| 25 | 18, 24 | eqtrd 2777 | . . . . . . . . . 10
⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) ∧ 𝑐 ∈ 𝒫 𝐴) → (𝑎(+g‘𝑀)(𝑏(+g‘𝑀)𝑐)) = (𝑎 ∪ (𝑏 ∪ 𝑐))) | 
| 26 | 10, 15, 25 | 3eqtr4a 2803 | . . . . . . . . 9
⊢ (((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) ∧ 𝑐 ∈ 𝒫 𝐴) → ((𝑎(+g‘𝑀)𝑏)(+g‘𝑀)𝑐) = (𝑎(+g‘𝑀)(𝑏(+g‘𝑀)𝑐))) | 
| 27 | 26 | ex 412 | . . . . . . . 8
⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) → (𝑐 ∈ 𝒫 𝐴 → ((𝑎(+g‘𝑀)𝑏)(+g‘𝑀)𝑐) = (𝑎(+g‘𝑀)(𝑏(+g‘𝑀)𝑐)))) | 
| 28 | 9, 27 | biimtrid 242 | . . . . . . 7
⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) → (𝑐 ∈ (Base‘𝑀) → ((𝑎(+g‘𝑀)𝑏)(+g‘𝑀)𝑐) = (𝑎(+g‘𝑀)(𝑏(+g‘𝑀)𝑐)))) | 
| 29 | 28 | ralrimiv 3145 | . . . . . 6
⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) → ∀𝑐 ∈ (Base‘𝑀)((𝑎(+g‘𝑀)𝑏)(+g‘𝑀)𝑐) = (𝑎(+g‘𝑀)(𝑏(+g‘𝑀)𝑐))) | 
| 30 | 8, 29 | jca 511 | . . . . 5
⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴) → ((𝑎(+g‘𝑀)𝑏) ∈ (Base‘𝑀) ∧ ∀𝑐 ∈ (Base‘𝑀)((𝑎(+g‘𝑀)𝑏)(+g‘𝑀)𝑐) = (𝑎(+g‘𝑀)(𝑏(+g‘𝑀)𝑐)))) | 
| 31 | 2, 3, 30 | syl2anb 598 | . . . 4
⊢ ((𝑎 ∈ (Base‘𝑀) ∧ 𝑏 ∈ (Base‘𝑀)) → ((𝑎(+g‘𝑀)𝑏) ∈ (Base‘𝑀) ∧ ∀𝑐 ∈ (Base‘𝑀)((𝑎(+g‘𝑀)𝑏)(+g‘𝑀)𝑐) = (𝑎(+g‘𝑀)(𝑏(+g‘𝑀)𝑐)))) | 
| 32 | 31 | rgen2 3199 | . . 3
⊢
∀𝑎 ∈
(Base‘𝑀)∀𝑏 ∈ (Base‘𝑀)((𝑎(+g‘𝑀)𝑏) ∈ (Base‘𝑀) ∧ ∀𝑐 ∈ (Base‘𝑀)((𝑎(+g‘𝑀)𝑏)(+g‘𝑀)𝑐) = (𝑎(+g‘𝑀)(𝑏(+g‘𝑀)𝑐))) | 
| 33 |  | 0ex 5307 | . . . . 5
⊢ ∅
∈ V | 
| 34 |  | eleq1 2829 | . . . . . 6
⊢ (𝑒 = ∅ → (𝑒 ∈ (Base‘𝑀) ↔ ∅ ∈
(Base‘𝑀))) | 
| 35 |  | oveq1 7438 | . . . . . . . . 9
⊢ (𝑒 = ∅ → (𝑒(+g‘𝑀)𝑎) = (∅(+g‘𝑀)𝑎)) | 
| 36 | 35 | eqeq1d 2739 | . . . . . . . 8
⊢ (𝑒 = ∅ → ((𝑒(+g‘𝑀)𝑎) = 𝑎 ↔ (∅(+g‘𝑀)𝑎) = 𝑎)) | 
| 37 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑒 = ∅ → (𝑎(+g‘𝑀)𝑒) = (𝑎(+g‘𝑀)∅)) | 
| 38 | 37 | eqeq1d 2739 | . . . . . . . 8
⊢ (𝑒 = ∅ → ((𝑎(+g‘𝑀)𝑒) = 𝑎 ↔ (𝑎(+g‘𝑀)∅) = 𝑎)) | 
| 39 | 36, 38 | anbi12d 632 | . . . . . . 7
⊢ (𝑒 = ∅ → (((𝑒(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)𝑒) = 𝑎) ↔ ((∅(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)∅) = 𝑎))) | 
| 40 | 39 | ralbidv 3178 | . . . . . 6
⊢ (𝑒 = ∅ → (∀𝑎 ∈ (Base‘𝑀)((𝑒(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)𝑒) = 𝑎) ↔ ∀𝑎 ∈ (Base‘𝑀)((∅(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)∅) = 𝑎))) | 
| 41 | 34, 40 | anbi12d 632 | . . . . 5
⊢ (𝑒 = ∅ → ((𝑒 ∈ (Base‘𝑀) ∧ ∀𝑎 ∈ (Base‘𝑀)((𝑒(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)𝑒) = 𝑎)) ↔ (∅ ∈ (Base‘𝑀) ∧ ∀𝑎 ∈ (Base‘𝑀)((∅(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)∅) = 𝑎)))) | 
| 42 |  | 0elpw 5356 | . . . . . . 7
⊢ ∅
∈ 𝒫 𝐴 | 
| 43 | 42, 1 | eleqtrri 2840 | . . . . . 6
⊢ ∅
∈ (Base‘𝑀) | 
| 44 | 1, 5 | pwmndgplus 18948 | . . . . . . . . . . 11
⊢ ((∅
∈ 𝒫 𝐴 ∧
𝑎 ∈ 𝒫 𝐴) →
(∅(+g‘𝑀)𝑎) = (∅ ∪ 𝑎)) | 
| 45 |  | 0un 4396 | . . . . . . . . . . 11
⊢ (∅
∪ 𝑎) = 𝑎 | 
| 46 | 44, 45 | eqtrdi 2793 | . . . . . . . . . 10
⊢ ((∅
∈ 𝒫 𝐴 ∧
𝑎 ∈ 𝒫 𝐴) →
(∅(+g‘𝑀)𝑎) = 𝑎) | 
| 47 | 1, 5 | pwmndgplus 18948 | . . . . . . . . . . . 12
⊢ ((𝑎 ∈ 𝒫 𝐴 ∧ ∅ ∈ 𝒫
𝐴) → (𝑎(+g‘𝑀)∅) = (𝑎 ∪ ∅)) | 
| 48 | 47 | ancoms 458 | . . . . . . . . . . 11
⊢ ((∅
∈ 𝒫 𝐴 ∧
𝑎 ∈ 𝒫 𝐴) → (𝑎(+g‘𝑀)∅) = (𝑎 ∪ ∅)) | 
| 49 |  | un0 4394 | . . . . . . . . . . 11
⊢ (𝑎 ∪ ∅) = 𝑎 | 
| 50 | 48, 49 | eqtrdi 2793 | . . . . . . . . . 10
⊢ ((∅
∈ 𝒫 𝐴 ∧
𝑎 ∈ 𝒫 𝐴) → (𝑎(+g‘𝑀)∅) = 𝑎) | 
| 51 | 46, 50 | jca 511 | . . . . . . . . 9
⊢ ((∅
∈ 𝒫 𝐴 ∧
𝑎 ∈ 𝒫 𝐴) →
((∅(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)∅) = 𝑎)) | 
| 52 | 42, 51 | mpan 690 | . . . . . . . 8
⊢ (𝑎 ∈ 𝒫 𝐴 →
((∅(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)∅) = 𝑎)) | 
| 53 | 2, 52 | sylbi 217 | . . . . . . 7
⊢ (𝑎 ∈ (Base‘𝑀) →
((∅(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)∅) = 𝑎)) | 
| 54 | 53 | rgen 3063 | . . . . . 6
⊢
∀𝑎 ∈
(Base‘𝑀)((∅(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)∅) = 𝑎) | 
| 55 | 43, 54 | pm3.2i 470 | . . . . 5
⊢ (∅
∈ (Base‘𝑀) ∧
∀𝑎 ∈
(Base‘𝑀)((∅(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)∅) = 𝑎)) | 
| 56 | 33, 41, 55 | ceqsexv2d 3533 | . . . 4
⊢
∃𝑒(𝑒 ∈ (Base‘𝑀) ∧ ∀𝑎 ∈ (Base‘𝑀)((𝑒(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)𝑒) = 𝑎)) | 
| 57 |  | df-rex 3071 | . . . 4
⊢
(∃𝑒 ∈
(Base‘𝑀)∀𝑎 ∈ (Base‘𝑀)((𝑒(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)𝑒) = 𝑎) ↔ ∃𝑒(𝑒 ∈ (Base‘𝑀) ∧ ∀𝑎 ∈ (Base‘𝑀)((𝑒(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)𝑒) = 𝑎))) | 
| 58 | 56, 57 | mpbir 231 | . . 3
⊢
∃𝑒 ∈
(Base‘𝑀)∀𝑎 ∈ (Base‘𝑀)((𝑒(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)𝑒) = 𝑎) | 
| 59 | 32, 58 | pm3.2i 470 | . 2
⊢
(∀𝑎 ∈
(Base‘𝑀)∀𝑏 ∈ (Base‘𝑀)((𝑎(+g‘𝑀)𝑏) ∈ (Base‘𝑀) ∧ ∀𝑐 ∈ (Base‘𝑀)((𝑎(+g‘𝑀)𝑏)(+g‘𝑀)𝑐) = (𝑎(+g‘𝑀)(𝑏(+g‘𝑀)𝑐))) ∧ ∃𝑒 ∈ (Base‘𝑀)∀𝑎 ∈ (Base‘𝑀)((𝑒(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)𝑒) = 𝑎)) | 
| 60 |  | eqid 2737 | . . 3
⊢
(Base‘𝑀) =
(Base‘𝑀) | 
| 61 |  | eqid 2737 | . . 3
⊢
(+g‘𝑀) = (+g‘𝑀) | 
| 62 | 60, 61 | ismnd 18750 | . 2
⊢ (𝑀 ∈ Mnd ↔
(∀𝑎 ∈
(Base‘𝑀)∀𝑏 ∈ (Base‘𝑀)((𝑎(+g‘𝑀)𝑏) ∈ (Base‘𝑀) ∧ ∀𝑐 ∈ (Base‘𝑀)((𝑎(+g‘𝑀)𝑏)(+g‘𝑀)𝑐) = (𝑎(+g‘𝑀)(𝑏(+g‘𝑀)𝑐))) ∧ ∃𝑒 ∈ (Base‘𝑀)∀𝑎 ∈ (Base‘𝑀)((𝑒(+g‘𝑀)𝑎) = 𝑎 ∧ (𝑎(+g‘𝑀)𝑒) = 𝑎))) | 
| 63 | 59, 62 | mpbir 231 | 1
⊢ 𝑀 ∈ Mnd |