Metamath Proof Explorer

Theorem pwmndid

Description: The identity of the monoid of the power set of a class A under union is the empty set. (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 pwmndid 
|- ( 0g ` M ) = (/)

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 0elpw 
 |-  (/) e. ~P A
4 1 eqcomi 
 |-  ~P A = ( Base ` M )
5 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
6 eqid 
 |-  ( +g ` M ) = ( +g ` M )
7 id 
 |-  ( (/) e. ~P A -> (/) e. ~P A )
8 1 2 pwmndgplus 
 |-  ( ( (/) e. ~P A /\ z e. ~P A ) -> ( (/) ( +g ` M ) z ) = ( (/) u. z ) )
9 0un 
 |-  ( (/) u. z ) = z
10 8 9 eqtrdi 
 |-  ( ( (/) e. ~P A /\ z e. ~P A ) -> ( (/) ( +g ` M ) z ) = z )
11 1 2 pwmndgplus 
 |-  ( ( z e. ~P A /\ (/) e. ~P A ) -> ( z ( +g ` M ) (/) ) = ( z u. (/) ) )
12 11 ancoms 
 |-  ( ( (/) e. ~P A /\ z e. ~P A ) -> ( z ( +g ` M ) (/) ) = ( z u. (/) ) )
13 un0 
 |-  ( z u. (/) ) = z
14 12 13 eqtrdi 
 |-  ( ( (/) e. ~P A /\ z e. ~P A ) -> ( z ( +g ` M ) (/) ) = z )
15 4 5 6 7 10 14 ismgmid2 
 |-  ( (/) e. ~P A -> (/) = ( 0g ` M ) )
16 15 eqcomd 
 |-  ( (/) e. ~P A -> ( 0g ` M ) = (/) )
17 3 16 ax-mp 
 |-  ( 0g ` M ) = (/)