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 ‘ 𝑀 ) = 𝒫 𝐴
pwmnd.p ⊢ ( +g ‘ 𝑀 ) = ( 𝑥 ∈ 𝒫 𝐴 , 𝑦 ∈ 𝒫 𝐴 ↦ ( 𝑥 ∪ 𝑦 ) )
Assertion pwmnd 𝑀 ∈ Mnd

Proof

Step Hyp Ref Expression
1 pwmnd.b ⊢ ( Base ‘ 𝑀 ) = 𝒫 𝐴
2 pwmnd.p ⊢ ( +g ‘ 𝑀 ) = ( 𝑥 ∈ 𝒫 𝐴 , 𝑦 ∈ 𝒫 𝐴 ↦ ( 𝑥 ∪ 𝑦 ) )
3 1 eleq2i ⊢ ( 𝑎 ∈ ( Base ‘ 𝑀 ) ↔ 𝑎 ∈ 𝒫 𝐴 )
4 1 eleq2i ⊢ ( 𝑏 ∈ ( Base ‘ 𝑀 ) ↔ 𝑏 ∈ 𝒫 𝐴 )
5 pwuncl ⊢ ( ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) → ( 𝑎 ∪ 𝑏 ) ∈ 𝒫 𝐴 )
6 1 2 pwmndgplus ⊢ ( ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) = ( 𝑎 ∪ 𝑏 ) )
7 1 a1i ⊢ ( ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) → ( Base ‘ 𝑀 ) = 𝒫 𝐴 )
8 5 6 7 3eltr4d ⊢ ( ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ ( Base ‘ 𝑀 ) )
9 1 eleq2i ⊢ ( 𝑐 ∈ ( Base ‘ 𝑀 ) ↔ 𝑐 ∈ 𝒫 𝐴 )
10 unass ⊢ ( ( 𝑎 ∪ 𝑏 ) ∪ 𝑐 ) = ( 𝑎 ∪ ( 𝑏 ∪ 𝑐 ) )
11 6 adantr ⊢ ( ( ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ∧ 𝑐 ∈ 𝒫 𝐴 ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) = ( 𝑎 ∪ 𝑏 ) )
12 11 oveq1d ⊢ ( ( ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ∧ 𝑐 ∈ 𝒫 𝐴 ) → ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( ( 𝑎 ∪ 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) )
13 1 2 pwmndgplus ⊢ ( ( ( 𝑎 ∪ 𝑏 ) ∈ 𝒫 𝐴 ∧ 𝑐 ∈ 𝒫 𝐴 ) → ( ( 𝑎 ∪ 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( ( 𝑎 ∪ 𝑏 ) ∪ 𝑐 ) )
14 5 13 sylan ⊢ ( ( ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ∧ 𝑐 ∈ 𝒫 𝐴 ) → ( ( 𝑎 ∪ 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( ( 𝑎 ∪ 𝑏 ) ∪ 𝑐 ) )
15 12 14 eqtrd ⊢ ( ( ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ∧ 𝑐 ∈ 𝒫 𝐴 ) → ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( ( 𝑎 ∪ 𝑏 ) ∪ 𝑐 ) )
16 1 2 pwmndgplus ⊢ ( ( 𝑏 ∈ 𝒫 𝐴 ∧ 𝑐 ∈ 𝒫 𝐴 ) → ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝑏 ∪ 𝑐 ) )
17 16 adantll ⊢ ( ( ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ∧ 𝑐 ∈ 𝒫 𝐴 ) → ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝑏 ∪ 𝑐 ) )
18 17 oveq2d ⊢ ( ( ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ∧ 𝑐 ∈ 𝒫 𝐴 ) → ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) = ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ∪ 𝑐 ) ) )
19 simpll ⊢ ( ( ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ∧ 𝑐 ∈ 𝒫 𝐴 ) → 𝑎 ∈ 𝒫 𝐴 )
20 pwuncl ⊢ ( ( 𝑏 ∈ 𝒫 𝐴 ∧ 𝑐 ∈ 𝒫 𝐴 ) → ( 𝑏 ∪ 𝑐 ) ∈ 𝒫 𝐴 )
21 20 adantll ⊢ ( ( ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ∧ 𝑐 ∈ 𝒫 𝐴 ) → ( 𝑏 ∪ 𝑐 ) ∈ 𝒫 𝐴 )
22 19 21 jca ⊢ ( ( ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ∧ 𝑐 ∈ 𝒫 𝐴 ) → ( 𝑎 ∈ 𝒫 𝐴 ∧ ( 𝑏 ∪ 𝑐 ) ∈ 𝒫 𝐴 ) )
23 1 2 pwmndgplus ⊢ ( ( 𝑎 ∈ 𝒫 𝐴 ∧ ( 𝑏 ∪ 𝑐 ) ∈ 𝒫 𝐴 ) → ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ∪ 𝑐 ) ) = ( 𝑎 ∪ ( 𝑏 ∪ 𝑐 ) ) )
24 22 23 syl ⊢ ( ( ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ∧ 𝑐 ∈ 𝒫 𝐴 ) → ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ∪ 𝑐 ) ) = ( 𝑎 ∪ ( 𝑏 ∪ 𝑐 ) ) )
25 18 24 eqtrd ⊢ ( ( ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ∧ 𝑐 ∈ 𝒫 𝐴 ) → ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) = ( 𝑎 ∪ ( 𝑏 ∪ 𝑐 ) ) )
26 10 15 25 3eqtr4a ⊢ ( ( ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ∧ 𝑐 ∈ 𝒫 𝐴 ) → ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) )
27 26 ex ⊢ ( ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) → ( 𝑐 ∈ 𝒫 𝐴 → ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ) )
28 9 27 biimtrid ⊢ ( ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) → ( 𝑐 ∈ ( Base ‘ 𝑀 ) → ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ) )
29 28 ralrimiv ⊢ ( ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) → ∀ 𝑐 ∈ ( Base ‘ 𝑀 ) ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) )
30 8 29 jca ⊢ ( ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) → ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ ( Base ‘ 𝑀 ) ∧ ∀ 𝑐 ∈ ( Base ‘ 𝑀 ) ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ) )
31 3 4 30 syl2anb ⊢ ( ( 𝑎 ∈ ( Base ‘ 𝑀 ) ∧ 𝑏 ∈ ( Base ‘ 𝑀 ) ) → ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ ( Base ‘ 𝑀 ) ∧ ∀ 𝑐 ∈ ( Base ‘ 𝑀 ) ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ) )
32 31 rgen2 ⊢ ∀ 𝑎 ∈ ( Base ‘ 𝑀 ) ∀ 𝑏 ∈ ( Base ‘ 𝑀 ) ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ ( Base ‘ 𝑀 ) ∧ ∀ 𝑐 ∈ ( Base ‘ 𝑀 ) ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) )
33 0ex ⊢ ∅ ∈ V
34 eleq1 ⊢ ( 𝑒 = ∅ → ( 𝑒 ∈ ( Base ‘ 𝑀 ) ↔ ∅ ∈ ( Base ‘ 𝑀 ) ) )
35 oveq1 ⊢ ( 𝑒 = ∅ → ( 𝑒 ( +g ‘ 𝑀 ) 𝑎 ) = ( ∅ ( +g ‘ 𝑀 ) 𝑎 ) )
36 35 eqeq1d ⊢ ( 𝑒 = ∅ → ( ( 𝑒 ( +g ‘ 𝑀 ) 𝑎 ) = 𝑎 ↔ ( ∅ ( +g ‘ 𝑀 ) 𝑎 ) = 𝑎 ) )
37 oveq2 ⊢ ( 𝑒 = ∅ → ( 𝑎 ( +g ‘ 𝑀 ) 𝑒 ) = ( 𝑎 ( +g ‘ 𝑀 ) ∅ ) )
38 37 eqeq1d ⊢ ( 𝑒 = ∅ → ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑒 ) = 𝑎 ↔ ( 𝑎 ( +g ‘ 𝑀 ) ∅ ) = 𝑎 ) )
39 36 38 anbi12d ⊢ ( 𝑒 = ∅ → ( ( ( 𝑒 ( +g ‘ 𝑀 ) 𝑎 ) = 𝑎 ∧ ( 𝑎 ( +g ‘ 𝑀 ) 𝑒 ) = 𝑎 ) ↔ ( ( ∅ ( +g ‘ 𝑀 ) 𝑎 ) = 𝑎 ∧ ( 𝑎 ( +g ‘ 𝑀 ) ∅ ) = 𝑎 ) ) )
40 39 ralbidv ⊢ ( 𝑒 = ∅ → ( ∀ 𝑎 ∈ ( Base ‘ 𝑀 ) ( ( 𝑒 ( +g ‘ 𝑀 ) 𝑎 ) = 𝑎 ∧ ( 𝑎 ( +g ‘ 𝑀 ) 𝑒 ) = 𝑎 ) ↔ ∀ 𝑎 ∈ ( Base ‘ 𝑀 ) ( ( ∅ ( +g ‘ 𝑀 ) 𝑎 ) = 𝑎 ∧ ( 𝑎 ( +g ‘ 𝑀 ) ∅ ) = 𝑎 ) ) )
41 34 40 anbi12d ⊢ ( 𝑒 = ∅ → ( ( 𝑒 ∈ ( Base ‘ 𝑀 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑀 ) ( ( 𝑒 ( +g ‘ 𝑀 ) 𝑎 ) = 𝑎 ∧ ( 𝑎 ( +g ‘ 𝑀 ) 𝑒 ) = 𝑎 ) ) ↔ ( ∅ ∈ ( Base ‘ 𝑀 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑀 ) ( ( ∅ ( +g ‘ 𝑀 ) 𝑎 ) = 𝑎 ∧ ( 𝑎 ( +g ‘ 𝑀 ) ∅ ) = 𝑎 ) ) ) )
42 0elpw ⊢ ∅ ∈ 𝒫 𝐴
43 42 1 eleqtrri ⊢ ∅ ∈ ( Base ‘ 𝑀 )
44 1 2 pwmndgplus ⊢ ( ( ∅ ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐴 ) → ( ∅ ( +g ‘ 𝑀 ) 𝑎 ) = ( ∅ ∪ 𝑎 ) )
45 0un ⊢ ( ∅ ∪ 𝑎 ) = 𝑎
46 44 45 eqtrdi ⊢ ( ( ∅ ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐴 ) → ( ∅ ( +g ‘ 𝑀 ) 𝑎 ) = 𝑎 )
47 1 2 pwmndgplus ⊢ ( ( 𝑎 ∈ 𝒫 𝐴 ∧ ∅ ∈ 𝒫 𝐴 ) → ( 𝑎 ( +g ‘ 𝑀 ) ∅ ) = ( 𝑎 ∪ ∅ ) )
48 47 ancoms ⊢ ( ( ∅ ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐴 ) → ( 𝑎 ( +g ‘ 𝑀 ) ∅ ) = ( 𝑎 ∪ ∅ ) )
49 un0 ⊢ ( 𝑎 ∪ ∅ ) = 𝑎
50 48 49 eqtrdi ⊢ ( ( ∅ ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐴 ) → ( 𝑎 ( +g ‘ 𝑀 ) ∅ ) = 𝑎 )
51 46 50 jca ⊢ ( ( ∅ ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐴 ) → ( ( ∅ ( +g ‘ 𝑀 ) 𝑎 ) = 𝑎 ∧ ( 𝑎 ( +g ‘ 𝑀 ) ∅ ) = 𝑎 ) )
52 42 51 mpan ⊢ ( 𝑎 ∈ 𝒫 𝐴 → ( ( ∅ ( +g ‘ 𝑀 ) 𝑎 ) = 𝑎 ∧ ( 𝑎 ( +g ‘ 𝑀 ) ∅ ) = 𝑎 ) )
53 3 52 sylbi ⊢ ( 𝑎 ∈ ( Base ‘ 𝑀 ) → ( ( ∅ ( +g ‘ 𝑀 ) 𝑎 ) = 𝑎 ∧ ( 𝑎 ( +g ‘ 𝑀 ) ∅ ) = 𝑎 ) )
54 53 rgen ⊢ ∀ 𝑎 ∈ ( Base ‘ 𝑀 ) ( ( ∅ ( +g ‘ 𝑀 ) 𝑎 ) = 𝑎 ∧ ( 𝑎 ( +g ‘ 𝑀 ) ∅ ) = 𝑎 )
55 43 54 pm3.2i ⊢ ( ∅ ∈ ( Base ‘ 𝑀 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑀 ) ( ( ∅ ( +g ‘ 𝑀 ) 𝑎 ) = 𝑎 ∧ ( 𝑎 ( +g ‘ 𝑀 ) ∅ ) = 𝑎 ) )
56 33 41 55 ceqsexv2d ⊢ ∃ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑀 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑀 ) ( ( 𝑒 ( +g ‘ 𝑀 ) 𝑎 ) = 𝑎 ∧ ( 𝑎 ( +g ‘ 𝑀 ) 𝑒 ) = 𝑎 ) )
57 df-rex ⊢ ( ∃ 𝑒 ∈ ( Base ‘ 𝑀 ) ∀ 𝑎 ∈ ( Base ‘ 𝑀 ) ( ( 𝑒 ( +g ‘ 𝑀 ) 𝑎 ) = 𝑎 ∧ ( 𝑎 ( +g ‘ 𝑀 ) 𝑒 ) = 𝑎 ) ↔ ∃ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑀 ) ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑀 ) ( ( 𝑒 ( +g ‘ 𝑀 ) 𝑎 ) = 𝑎 ∧ ( 𝑎 ( +g ‘ 𝑀 ) 𝑒 ) = 𝑎 ) ) )
58 56 57 mpbir ⊢ ∃ 𝑒 ∈ ( Base ‘ 𝑀 ) ∀ 𝑎 ∈ ( Base ‘ 𝑀 ) ( ( 𝑒 ( +g ‘ 𝑀 ) 𝑎 ) = 𝑎 ∧ ( 𝑎 ( +g ‘ 𝑀 ) 𝑒 ) = 𝑎 )
59 32 58 pm3.2i ⊢ ( ∀ 𝑎 ∈ ( Base ‘ 𝑀 ) ∀ 𝑏 ∈ ( Base ‘ 𝑀 ) ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ ( Base ‘ 𝑀 ) ∧ ∀ 𝑐 ∈ ( Base ‘ 𝑀 ) ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ) ∧ ∃ 𝑒 ∈ ( Base ‘ 𝑀 ) ∀ 𝑎 ∈ ( Base ‘ 𝑀 ) ( ( 𝑒 ( +g ‘ 𝑀 ) 𝑎 ) = 𝑎 ∧ ( 𝑎 ( +g ‘ 𝑀 ) 𝑒 ) = 𝑎 ) )
60 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
61 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
62 60 61 ismnd ⊢ ( 𝑀 ∈ Mnd ↔ ( ∀ 𝑎 ∈ ( Base ‘ 𝑀 ) ∀ 𝑏 ∈ ( Base ‘ 𝑀 ) ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ ( Base ‘ 𝑀 ) ∧ ∀ 𝑐 ∈ ( Base ‘ 𝑀 ) ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ) ∧ ∃ 𝑒 ∈ ( Base ‘ 𝑀 ) ∀ 𝑎 ∈ ( Base ‘ 𝑀 ) ( ( 𝑒 ( +g ‘ 𝑀 ) 𝑎 ) = 𝑎 ∧ ( 𝑎 ( +g ‘ 𝑀 ) 𝑒 ) = 𝑎 ) ) )
63 59 62 mpbir ⊢ 𝑀 ∈ Mnd