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