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

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 ) )