pwmndgplus

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

Step	Hyp	Ref	Expression
1		pwmnd.b	$⊢ {Base}_{M} = 𝒫 A$
2		pwmnd.p	$⊢ +_{M} = (x \in 𝒫 A, y \in 𝒫 A ⟼ x \cup y)$
3	2	a1i	$⊢ (X \in 𝒫 A \land Y \in 𝒫 A) \to +_{M} = (x \in 𝒫 A, y \in 𝒫 A ⟼ x \cup y)$
4		uneq12	$⊢ (x = X \land y = Y) \to x \cup y = X \cup Y$
5	4	adantl	$⊢ ((X \in 𝒫 A \land Y \in 𝒫 A) \land (x = X \land y = Y)) \to x \cup y = X \cup Y$
6		simpl	$⊢ (X \in 𝒫 A \land Y \in 𝒫 A) \to X \in 𝒫 A$
7		simpr	$⊢ (X \in 𝒫 A \land Y \in 𝒫 A) \to Y \in 𝒫 A$
8		unexg	$⊢ (X \in 𝒫 A \land Y \in 𝒫 A) \to X \cup Y \in V$
9	3 5 6 7 8	ovmpod	$⊢ (X \in 𝒫 A \land Y \in 𝒫 A) \to X +_{M} Y = X \cup Y$

Metamath Proof Explorer