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	$$⊢{\mathrm{Base}}_M=𝒫A$$
	pwmnd.p	$$⊢{+}_M=\left(x\in 𝒫A,y\in 𝒫A⟼x\cup y\right)$$
Assertion	pwmndid	$$⊢0_M=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		pwmnd.b	$$⊢{\mathrm{Base}}_M=𝒫A$$
2		pwmnd.p	$$⊢{+}_M=\left(x\in 𝒫A,y\in 𝒫A⟼x\cup y\right)$$
3		0elpw	$$⊢\varnothing \in 𝒫A$$
4	1	eqcomi	$$⊢𝒫A={\mathrm{Base}}_M$$
5		eqid	$$⊢0_M=0_M$$
6		eqid	$$⊢{+}_M={+}_M$$
7		id	$$⊢\varnothing \in 𝒫A\to \varnothing \in 𝒫A$$
8	1 2	pwmndgplus	$$⊢\left(\varnothing \in 𝒫A\wedge z\in 𝒫A\right)\to \varnothing {+}_{M}z=\varnothing \cup z$$
9		0un	$$⊢\varnothing \cup z=z$$
10	8 9	syl6eq	$$⊢\left(\varnothing \in 𝒫A\wedge z\in 𝒫A\right)\to \varnothing {+}_{M}z=z$$
11	1 2	pwmndgplus	$$⊢\left(z\in 𝒫A\wedge \varnothing \in 𝒫A\right)\to z{+}_M\varnothing =z\cup \varnothing$$
12	11	ancoms	$$⊢\left(\varnothing \in 𝒫A\wedge z\in 𝒫A\right)\to z{+}_M\varnothing =z\cup \varnothing$$
13		un0	$$⊢z\cup \varnothing =z$$
14	12 13	syl6eq	$$⊢\left(\varnothing \in 𝒫A\wedge z\in 𝒫A\right)\to z{+}_M\varnothing =z$$
15	4 5 6 7 10 14	ismgmid2	$$⊢\varnothing \in 𝒫A\to \varnothing =0_M$$
16	15	eqcomd	$$⊢\varnothing \in 𝒫A\to 0_M=\varnothing$$
17	3 16	ax-mp	$$⊢0_M=\varnothing$$