Metamath Proof Explorer

Theorem pwmnd

Description: The power set of a class A is a monoid 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 pwmnd 
|- M e. Mnd

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 1 eleq2i 
 |-  ( a e. ( Base ` M ) <-> a e. ~P A )
4 1 eleq2i 
 |-  ( b e. ( Base ` M ) <-> b e. ~P A )
5 pwuncl 
 |-  ( ( a e. ~P A /\ b e. ~P A ) -> ( a u. b ) e. ~P A )
6 1 2 pwmndgplus 
 |-  ( ( a e. ~P A /\ b e. ~P A ) -> ( a ( +g ` M ) b ) = ( a u. b ) )
7 1 a1i 
 |-  ( ( a e. ~P A /\ b e. ~P A ) -> ( Base ` M ) = ~P A )
8 5 6 7 3eltr4d 
 |-  ( ( a e. ~P A /\ b e. ~P A ) -> ( a ( +g ` M ) b ) e. ( Base ` M ) )
9 1 eleq2i 
 |-  ( c e. ( Base ` M ) <-> c e. ~P A )
10 unass 
 |-  ( ( a u. b ) u. c ) = ( a u. ( b u. c ) )
11 6 adantr 
 |-  ( ( ( a e. ~P A /\ b e. ~P A ) /\ c e. ~P A ) -> ( a ( +g ` M ) b ) = ( a u. b ) )
12 11 oveq1d 
 |-  ( ( ( a e. ~P A /\ b e. ~P A ) /\ c e. ~P A ) -> ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( ( a u. b ) ( +g ` M ) c ) )
13 1 2 pwmndgplus 
 |-  ( ( ( a u. b ) e. ~P A /\ c e. ~P A ) -> ( ( a u. b ) ( +g ` M ) c ) = ( ( a u. b ) u. c ) )
14 5 13 sylan 
 |-  ( ( ( a e. ~P A /\ b e. ~P A ) /\ c e. ~P A ) -> ( ( a u. b ) ( +g ` M ) c ) = ( ( a u. b ) u. c ) )
15 12 14 eqtrd 
 |-  ( ( ( a e. ~P A /\ b e. ~P A ) /\ c e. ~P A ) -> ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( ( a u. b ) u. c ) )
16 1 2 pwmndgplus 
 |-  ( ( b e. ~P A /\ c e. ~P A ) -> ( b ( +g ` M ) c ) = ( b u. c ) )
17 16 adantll 
 |-  ( ( ( a e. ~P A /\ b e. ~P A ) /\ c e. ~P A ) -> ( b ( +g ` M ) c ) = ( b u. c ) )
18 17 oveq2d 
 |-  ( ( ( a e. ~P A /\ b e. ~P A ) /\ c e. ~P A ) -> ( a ( +g ` M ) ( b ( +g ` M ) c ) ) = ( a ( +g ` M ) ( b u. c ) ) )
19 simpll 
 |-  ( ( ( a e. ~P A /\ b e. ~P A ) /\ c e. ~P A ) -> a e. ~P A )
20 pwuncl 
 |-  ( ( b e. ~P A /\ c e. ~P A ) -> ( b u. c ) e. ~P A )
21 20 adantll 
 |-  ( ( ( a e. ~P A /\ b e. ~P A ) /\ c e. ~P A ) -> ( b u. c ) e. ~P A )
22 19 21 jca 
 |-  ( ( ( a e. ~P A /\ b e. ~P A ) /\ c e. ~P A ) -> ( a e. ~P A /\ ( b u. c ) e. ~P A ) )
23 1 2 pwmndgplus 
 |-  ( ( a e. ~P A /\ ( b u. c ) e. ~P A ) -> ( a ( +g ` M ) ( b u. c ) ) = ( a u. ( b u. c ) ) )
24 22 23 syl 
 |-  ( ( ( a e. ~P A /\ b e. ~P A ) /\ c e. ~P A ) -> ( a ( +g ` M ) ( b u. c ) ) = ( a u. ( b u. c ) ) )
25 18 24 eqtrd 
 |-  ( ( ( a e. ~P A /\ b e. ~P A ) /\ c e. ~P A ) -> ( a ( +g ` M ) ( b ( +g ` M ) c ) ) = ( a u. ( b u. c ) ) )
26 10 15 25 3eqtr4a 
 |-  ( ( ( a e. ~P A /\ b e. ~P A ) /\ c e. ~P A ) -> ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( a ( +g ` M ) ( b ( +g ` M ) c ) ) )
27 26 ex 
 |-  ( ( a e. ~P A /\ b e. ~P A ) -> ( c e. ~P A -> ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( a ( +g ` M ) ( b ( +g ` M ) c ) ) ) )
28 9 27 biimtrid 
 |-  ( ( a e. ~P A /\ b e. ~P A ) -> ( c e. ( Base ` M ) -> ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( a ( +g ` M ) ( b ( +g ` M ) c ) ) ) )
29 28 ralrimiv 
 |-  ( ( a e. ~P A /\ b e. ~P A ) -> A. c e. ( Base ` M ) ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( a ( +g ` M ) ( b ( +g ` M ) c ) ) )
30 8 29 jca 
 |-  ( ( a e. ~P A /\ b e. ~P A ) -> ( ( a ( +g ` M ) b ) e. ( Base ` M ) /\ A. c e. ( Base ` M ) ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( a ( +g ` M ) ( b ( +g ` M ) c ) ) ) )
31 3 4 30 syl2anb 
 |-  ( ( a e. ( Base ` M ) /\ b e. ( Base ` M ) ) -> ( ( a ( +g ` M ) b ) e. ( Base ` M ) /\ A. c e. ( Base ` M ) ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( a ( +g ` M ) ( b ( +g ` M ) c ) ) ) )
32 31 rgen2 
 |-  A. a e. ( Base ` M ) A. b e. ( Base ` M ) ( ( a ( +g ` M ) b ) e. ( Base ` M ) /\ A. c e. ( Base ` M ) ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( a ( +g ` M ) ( b ( +g ` M ) c ) ) )
33 0ex 
 |-  (/) e. _V
34 eleq1 
 |-  ( e = (/) -> ( e e. ( Base ` M ) <-> (/) e. ( Base ` M ) ) )
35 oveq1 
 |-  ( e = (/) -> ( e ( +g ` M ) a ) = ( (/) ( +g ` M ) a ) )
36 35 eqeq1d 
 |-  ( e = (/) -> ( ( e ( +g ` M ) a ) = a <-> ( (/) ( +g ` M ) a ) = a ) )
37 oveq2 
 |-  ( e = (/) -> ( a ( +g ` M ) e ) = ( a ( +g ` M ) (/) ) )
38 37 eqeq1d 
 |-  ( e = (/) -> ( ( a ( +g ` M ) e ) = a <-> ( a ( +g ` M ) (/) ) = a ) )
39 36 38 anbi12d 
 |-  ( e = (/) -> ( ( ( e ( +g ` M ) a ) = a /\ ( a ( +g ` M ) e ) = a ) <-> ( ( (/) ( +g ` M ) a ) = a /\ ( a ( +g ` M ) (/) ) = a ) ) )
40 39 ralbidv 
 |-  ( e = (/) -> ( A. a e. ( Base ` M ) ( ( e ( +g ` M ) a ) = a /\ ( a ( +g ` M ) e ) = a ) <-> A. a e. ( Base ` M ) ( ( (/) ( +g ` M ) a ) = a /\ ( a ( +g ` M ) (/) ) = a ) ) )
41 34 40 anbi12d 
 |-  ( e = (/) -> ( ( e e. ( Base ` M ) /\ A. a e. ( Base ` M ) ( ( e ( +g ` M ) a ) = a /\ ( a ( +g ` M ) e ) = a ) ) <-> ( (/) e. ( Base ` M ) /\ A. a e. ( Base ` M ) ( ( (/) ( +g ` M ) a ) = a /\ ( a ( +g ` M ) (/) ) = a ) ) ) )
42 0elpw 
 |-  (/) e. ~P A
43 42 1 eleqtrri 
 |-  (/) e. ( Base ` M )
44 1 2 pwmndgplus 
 |-  ( ( (/) e. ~P A /\ a e. ~P A ) -> ( (/) ( +g ` M ) a ) = ( (/) u. a ) )
45 0un 
 |-  ( (/) u. a ) = a
46 44 45 eqtrdi 
 |-  ( ( (/) e. ~P A /\ a e. ~P A ) -> ( (/) ( +g ` M ) a ) = a )
47 1 2 pwmndgplus 
 |-  ( ( a e. ~P A /\ (/) e. ~P A ) -> ( a ( +g ` M ) (/) ) = ( a u. (/) ) )
48 47 ancoms 
 |-  ( ( (/) e. ~P A /\ a e. ~P A ) -> ( a ( +g ` M ) (/) ) = ( a u. (/) ) )
49 un0 
 |-  ( a u. (/) ) = a
50 48 49 eqtrdi 
 |-  ( ( (/) e. ~P A /\ a e. ~P A ) -> ( a ( +g ` M ) (/) ) = a )
51 46 50 jca 
 |-  ( ( (/) e. ~P A /\ a e. ~P A ) -> ( ( (/) ( +g ` M ) a ) = a /\ ( a ( +g ` M ) (/) ) = a ) )
52 42 51 mpan 
 |-  ( a e. ~P A -> ( ( (/) ( +g ` M ) a ) = a /\ ( a ( +g ` M ) (/) ) = a ) )
53 3 52 sylbi 
 |-  ( a e. ( Base ` M ) -> ( ( (/) ( +g ` M ) a ) = a /\ ( a ( +g ` M ) (/) ) = a ) )
54 53 rgen 
 |-  A. a e. ( Base ` M ) ( ( (/) ( +g ` M ) a ) = a /\ ( a ( +g ` M ) (/) ) = a )
55 43 54 pm3.2i 
 |-  ( (/) e. ( Base ` M ) /\ A. a e. ( Base ` M ) ( ( (/) ( +g ` M ) a ) = a /\ ( a ( +g ` M ) (/) ) = a ) )
56 33 41 55 ceqsexv2d 
 |-  E. e ( e e. ( Base ` M ) /\ A. a e. ( Base ` M ) ( ( e ( +g ` M ) a ) = a /\ ( a ( +g ` M ) e ) = a ) )
57 df-rex 
 |-  ( E. e e. ( Base ` M ) A. a e. ( Base ` M ) ( ( e ( +g ` M ) a ) = a /\ ( a ( +g ` M ) e ) = a ) <-> E. e ( e e. ( Base ` M ) /\ A. a e. ( Base ` M ) ( ( e ( +g ` M ) a ) = a /\ ( a ( +g ` M ) e ) = a ) ) )
58 56 57 mpbir 
 |-  E. e e. ( Base ` M ) A. a e. ( Base ` M ) ( ( e ( +g ` M ) a ) = a /\ ( a ( +g ` M ) e ) = a )
59 32 58 pm3.2i 
 |-  ( A. a e. ( Base ` M ) A. b e. ( Base ` M ) ( ( a ( +g ` M ) b ) e. ( Base ` M ) /\ A. c e. ( Base ` M ) ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( a ( +g ` M ) ( b ( +g ` M ) c ) ) ) /\ E. e e. ( Base ` M ) A. a e. ( Base ` M ) ( ( e ( +g ` M ) a ) = a /\ ( a ( +g ` M ) e ) = a ) )
60 eqid 
 |-  ( Base ` M ) = ( Base ` M )
61 eqid 
 |-  ( +g ` M ) = ( +g ` M )
62 60 61 ismnd 
 |-  ( M e. Mnd <-> ( A. a e. ( Base ` M ) A. b e. ( Base ` M ) ( ( a ( +g ` M ) b ) e. ( Base ` M ) /\ A. c e. ( Base ` M ) ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( a ( +g ` M ) ( b ( +g ` M ) c ) ) ) /\ E. e e. ( Base ` M ) A. a e. ( Base ` M ) ( ( e ( +g ` M ) a ) = a /\ ( a ( +g ` M ) e ) = a ) ) )
63 59 62 mpbir 
 |-  M e. Mnd