This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pwmndid

Description: The identity of the monoid of the power set of a class A under union is the empty set. (Contributed by AV, 27-Feb-2024)

Ref Expression
Hypotheses pwmnd.b ⊢ Base M = 𝒫 A
pwmnd.p ⊢ + M = x ∈ 𝒫 A , y ∈ 𝒫 A ⟼ x ∪ y
Assertion pwmndid ⊢ 0 M = ∅

Proof

Step Hyp Ref Expression
1 pwmnd.b ⊢ Base M = 𝒫 A
2 pwmnd.p ⊢ + M = x ∈ 𝒫 A , y ∈ 𝒫 A ⟼ x ∪ y
3 0elpw ⊢ ∅ ∈ 𝒫 A
4 1 eqcomi ⊢ 𝒫 A = Base M
5 eqid ⊢ 0 M = 0 M
6 eqid ⊢ + M = + M
7 id ⊢ ∅ ∈ 𝒫 A → ∅ ∈ 𝒫 A
8 1 2 pwmndgplus ⊢ ∅ ∈ 𝒫 A ∧ z ∈ 𝒫 A → ∅ + M z = ∅ ∪ z
9 0un ⊢ ∅ ∪ z = z
10 8 9 eqtrdi ⊢ ∅ ∈ 𝒫 A ∧ z ∈ 𝒫 A → ∅ + M z = z
11 1 2 pwmndgplus ⊢ z ∈ 𝒫 A ∧ ∅ ∈ 𝒫 A → z + M ∅ = z ∪ ∅
12 11 ancoms ⊢ ∅ ∈ 𝒫 A ∧ z ∈ 𝒫 A → z + M ∅ = z ∪ ∅
13 un0 ⊢ z ∪ ∅ = z
14 12 13 eqtrdi ⊢ ∅ ∈ 𝒫 A ∧ z ∈ 𝒫 A → z + M ∅ = z
15 4 5 6 7 10 14 ismgmid2 ⊢ ∅ ∈ 𝒫 A → ∅ = 0 M
16 15 eqcomd ⊢ ∅ ∈ 𝒫 A → 0 M = ∅
17 3 16 ax-mp ⊢ 0 M = ∅