Metamath Proof Explorer


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
|- ( Base ` M ) = ~P A
pwmnd.p
|- ( +g ` M ) = ( x e. ~P A , y e. ~P A |-> ( x u. y ) )
Assertion pwmndgplus
|- ( ( X e. ~P A /\ Y e. ~P A ) -> ( X ( +g ` M ) Y ) = ( X u. Y ) )

Proof

Step Hyp Ref Expression
1 pwmnd.b
 |-  ( Base ` M ) = ~P A
2 pwmnd.p
 |-  ( +g ` M ) = ( x e. ~P A , y e. ~P A |-> ( x u. y ) )
3 2 a1i
 |-  ( ( X e. ~P A /\ Y e. ~P A ) -> ( +g ` M ) = ( x e. ~P A , y e. ~P A |-> ( x u. y ) ) )
4 uneq12
 |-  ( ( x = X /\ y = Y ) -> ( x u. y ) = ( X u. Y ) )
5 4 adantl
 |-  ( ( ( X e. ~P A /\ Y e. ~P A ) /\ ( x = X /\ y = Y ) ) -> ( x u. y ) = ( X u. Y ) )
6 simpl
 |-  ( ( X e. ~P A /\ Y e. ~P A ) -> X e. ~P A )
7 simpr
 |-  ( ( X e. ~P A /\ Y e. ~P A ) -> Y e. ~P A )
8 unexg
 |-  ( ( X e. ~P A /\ Y e. ~P A ) -> ( X u. Y ) e. _V )
9 3 5 6 7 8 ovmpod
 |-  ( ( X e. ~P A /\ Y e. ~P A ) -> ( X ( +g ` M ) Y ) = ( X u. Y ) )