Theorem pwmndgplus

Description: The operation of the monoid of the power set of a class A under union. (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	pwmndgplus	$$⊢\left(X\in 𝒫A\wedge Y\in 𝒫A\right)\to X{+}_{M}Y=X\cup Y$$

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	2	a1i	$$⊢\left(X\in 𝒫A\wedge Y\in 𝒫A\right)\to {+}_M=\left(x\in 𝒫A,y\in 𝒫A⟼x\cup y\right)$$
4		uneq12	$$⊢\left(x=X\wedge y=Y\right)\to x\cup y=X\cup Y$$
5	4	adantl	$$⊢\left(\left(X\in 𝒫A\wedge Y\in 𝒫A\right)\wedge \left(x=X\wedge y=Y\right)\right)\to x\cup y=X\cup Y$$
6		simpl	$$⊢\left(X\in 𝒫A\wedge Y\in 𝒫A\right)\to X\in 𝒫A$$
7		simpr	$$⊢\left(X\in 𝒫A\wedge Y\in 𝒫A\right)\to Y\in 𝒫A$$
8		unexg	$$⊢\left(X\in 𝒫A\wedge Y\in 𝒫A\right)\to X\cup Y\in \mathrm{V}$$
9	3 5 6 7 8	ovmpod	$$⊢\left(X\in 𝒫A\wedge Y\in 𝒫A\right)\to X{+}_{M}Y=X\cup Y$$