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	$$⊢{\mathrm{Base}}_M=𝒫A$$
	pwmnd.p	$$⊢{+}_M=\left(x\in 𝒫A,y\in 𝒫A⟼x\cup y\right)$$
Assertion	pwmnd	$$⊢M\in \mathrm{Mnd}$$

Proof

Step	Hyp	Ref	Expression
1		pwmnd.b	$$⊢{\mathrm{Base}}_M=𝒫A$$
2		pwmnd.p	$$⊢{+}_M=\left(x\in 𝒫A,y\in 𝒫A⟼x\cup y\right)$$
3	1	eleq2i	$$⊢a\in {\mathrm{Base}}_M\leftrightarrow a\in 𝒫A$$
4	1	eleq2i	$$⊢b\in {\mathrm{Base}}_M\leftrightarrow b\in 𝒫A$$
5		pwuncl	$$⊢\left(a\in 𝒫A\wedge b\in 𝒫A\right)\to a\cup b\in 𝒫A$$
6	1 2	pwmndgplus	$$⊢\left(a\in 𝒫A\wedge b\in 𝒫A\right)\to a{+}_{M}b=a\cup b$$
7	1	a1i	$$⊢\left(a\in 𝒫A\wedge b\in 𝒫A\right)\to {\mathrm{Base}}_M=𝒫A$$
8	5 6 7	3eltr4d	$$⊢\left(a\in 𝒫A\wedge b\in 𝒫A\right)\to a{+}_{M}b\in {\mathrm{Base}}_M$$
9	1	eleq2i	$$⊢c\in {\mathrm{Base}}_M\leftrightarrow c\in 𝒫A$$
10		unass	$$⊢\left(a\cup b\right)\cup c=a\cup \left(b\cup c\right)$$
11	6	adantr	$$⊢\left(\left(a\in 𝒫A\wedge b\in 𝒫A\right)\wedge c\in 𝒫A\right)\to a{+}_{M}b=a\cup b$$
12	11	oveq1d	$$⊢\left(\left(a\in 𝒫A\wedge b\in 𝒫A\right)\wedge c\in 𝒫A\right)\to \left(a{+}_{M}b\right){+}_{M}c=\left(a\cup b\right){+}_{M}c$$
13	1 2	pwmndgplus	$$⊢\left(a\cup b\in 𝒫A\wedge c\in 𝒫A\right)\to \left(a\cup b\right){+}_{M}c=\left(a\cup b\right)\cup c$$
14	5 13	sylan	$$⊢\left(\left(a\in 𝒫A\wedge b\in 𝒫A\right)\wedge c\in 𝒫A\right)\to \left(a\cup b\right){+}_{M}c=\left(a\cup b\right)\cup c$$
15	12 14	eqtrd	$$⊢\left(\left(a\in 𝒫A\wedge b\in 𝒫A\right)\wedge c\in 𝒫A\right)\to \left(a{+}_{M}b\right){+}_{M}c=\left(a\cup b\right)\cup c$$
16	1 2	pwmndgplus	$$⊢\left(b\in 𝒫A\wedge c\in 𝒫A\right)\to b{+}_{M}c=b\cup c$$
17	16	adantll	$$⊢\left(\left(a\in 𝒫A\wedge b\in 𝒫A\right)\wedge c\in 𝒫A\right)\to b{+}_{M}c=b\cup c$$
18	17	oveq2d	$$⊢\left(\left(a\in 𝒫A\wedge b\in 𝒫A\right)\wedge c\in 𝒫A\right)\to a{+}_M\left(b{+}_{M}c\right)=a{+}_M\left(b\cup c\right)$$
19		simpll	$$⊢\left(\left(a\in 𝒫A\wedge b\in 𝒫A\right)\wedge c\in 𝒫A\right)\to a\in 𝒫A$$
20		pwuncl	$$⊢\left(b\in 𝒫A\wedge c\in 𝒫A\right)\to b\cup c\in 𝒫A$$
21	20	adantll	$$⊢\left(\left(a\in 𝒫A\wedge b\in 𝒫A\right)\wedge c\in 𝒫A\right)\to b\cup c\in 𝒫A$$
22	19 21	jca	$$⊢\left(\left(a\in 𝒫A\wedge b\in 𝒫A\right)\wedge c\in 𝒫A\right)\to \left(a\in 𝒫A\wedge b\cup c\in 𝒫A\right)$$
23	1 2	pwmndgplus	$$⊢\left(a\in 𝒫A\wedge b\cup c\in 𝒫A\right)\to a{+}_M\left(b\cup c\right)=a\cup \left(b\cup c\right)$$
24	22 23	syl	$$⊢\left(\left(a\in 𝒫A\wedge b\in 𝒫A\right)\wedge c\in 𝒫A\right)\to a{+}_M\left(b\cup c\right)=a\cup \left(b\cup c\right)$$
25	18 24	eqtrd	$$⊢\left(\left(a\in 𝒫A\wedge b\in 𝒫A\right)\wedge c\in 𝒫A\right)\to a{+}_M\left(b{+}_{M}c\right)=a\cup \left(b\cup c\right)$$
26	10 15 25	3eqtr4a	$$⊢\left(\left(a\in 𝒫A\wedge b\in 𝒫A\right)\wedge c\in 𝒫A\right)\to \left(a{+}_{M}b\right){+}_{M}c=a{+}_M\left(b{+}_{M}c\right)$$
27	26	ex	$$⊢\left(a\in 𝒫A\wedge b\in 𝒫A\right)\to \left(c\in 𝒫A\to \left(a{+}_{M}b\right){+}_{M}c=a{+}_M\left(b{+}_{M}c\right)\right)$$
28	9 27	biimtrid	$$⊢\left(a\in 𝒫A\wedge b\in 𝒫A\right)\to \left(c\in {\mathrm{Base}}_M\to \left(a{+}_{M}b\right){+}_{M}c=a{+}_M\left(b{+}_{M}c\right)\right)$$
29	28	ralrimiv	$$⊢\left(a\in 𝒫A\wedge b\in 𝒫A\right)\to \forall c\in {\mathrm{Base}}_M\left(a{+}_{M}b\right){+}_{M}c=a{+}_M\left(b{+}_{M}c\right)$$
30	8 29	jca	$$⊢\left(a\in 𝒫A\wedge b\in 𝒫A\right)\to \left(a{+}_{M}b\in {\mathrm{Base}}_M\wedge \forall c\in {\mathrm{Base}}_M\left(a{+}_{M}b\right){+}_{M}c=a{+}_M\left(b{+}_{M}c\right)\right)$$
31	3 4 30	syl2anb	$$⊢\left(a\in {\mathrm{Base}}_M\wedge b\in {\mathrm{Base}}_M\right)\to \left(a{+}_{M}b\in {\mathrm{Base}}_M\wedge \forall c\in {\mathrm{Base}}_M\left(a{+}_{M}b\right){+}_{M}c=a{+}_M\left(b{+}_{M}c\right)\right)$$
32	31	rgen2	$$⊢\forall a\in {\mathrm{Base}}_M\forall b\in {\mathrm{Base}}_M\left(a{+}_{M}b\in {\mathrm{Base}}_M\wedge \forall c\in {\mathrm{Base}}_M\left(a{+}_{M}b\right){+}_{M}c=a{+}_M\left(b{+}_{M}c\right)\right)$$
33		0ex	$$⊢\varnothing \in \mathrm{V}$$
34		eleq1	$$⊢e=\varnothing \to \left(e\in {\mathrm{Base}}_M\leftrightarrow \varnothing \in {\mathrm{Base}}_M\right)$$
35		oveq1	$$⊢e=\varnothing \to e{+}_{M}a=\varnothing {+}_{M}a$$
36	35	eqeq1d	$$⊢e=\varnothing \to \left(e{+}_{M}a=a\leftrightarrow \varnothing {+}_{M}a=a\right)$$
37		oveq2	$$⊢e=\varnothing \to a{+}_{M}e=a{+}_M\varnothing$$
38	37	eqeq1d	$$⊢e=\varnothing \to \left(a{+}_{M}e=a\leftrightarrow a{+}_M\varnothing =a\right)$$
39	36 38	anbi12d	$$⊢e=\varnothing \to \left(\left(e{+}_{M}a=a\wedge a{+}_{M}e=a\right)\leftrightarrow \left(\varnothing {+}_{M}a=a\wedge a{+}_M\varnothing =a\right)\right)$$
40	39	ralbidv	$$⊢e=\varnothing \to \left(\forall a\in {\mathrm{Base}}_M\left(e{+}_{M}a=a\wedge a{+}_{M}e=a\right)\leftrightarrow \forall a\in {\mathrm{Base}}_M\left(\varnothing {+}_{M}a=a\wedge a{+}_M\varnothing =a\right)\right)$$
41	34 40	anbi12d	$$⊢e=\varnothing \to \left(\left(e\in {\mathrm{Base}}_M\wedge \forall a\in {\mathrm{Base}}_M\left(e{+}_{M}a=a\wedge a{+}_{M}e=a\right)\right)\leftrightarrow \left(\varnothing \in {\mathrm{Base}}_M\wedge \forall a\in {\mathrm{Base}}_M\left(\varnothing {+}_{M}a=a\wedge a{+}_M\varnothing =a\right)\right)\right)$$
42		0elpw	$$⊢\varnothing \in 𝒫A$$
43	42 1	eleqtrri	$$⊢\varnothing \in {\mathrm{Base}}_M$$
44	1 2	pwmndgplus	$$⊢\left(\varnothing \in 𝒫A\wedge a\in 𝒫A\right)\to \varnothing {+}_{M}a=\varnothing \cup a$$
45		0un	$$⊢\varnothing \cup a=a$$
46	44 45	eqtrdi	$$⊢\left(\varnothing \in 𝒫A\wedge a\in 𝒫A\right)\to \varnothing {+}_{M}a=a$$
47	1 2	pwmndgplus	$$⊢\left(a\in 𝒫A\wedge \varnothing \in 𝒫A\right)\to a{+}_M\varnothing =a\cup \varnothing$$
48	47	ancoms	$$⊢\left(\varnothing \in 𝒫A\wedge a\in 𝒫A\right)\to a{+}_M\varnothing =a\cup \varnothing$$
49		un0	$$⊢a\cup \varnothing =a$$
50	48 49	eqtrdi	$$⊢\left(\varnothing \in 𝒫A\wedge a\in 𝒫A\right)\to a{+}_M\varnothing =a$$
51	46 50	jca	$$⊢\left(\varnothing \in 𝒫A\wedge a\in 𝒫A\right)\to \left(\varnothing {+}_{M}a=a\wedge a{+}_M\varnothing =a\right)$$
52	42 51	mpan	$$⊢a\in 𝒫A\to \left(\varnothing {+}_{M}a=a\wedge a{+}_M\varnothing =a\right)$$
53	3 52	sylbi	$$⊢a\in {\mathrm{Base}}_M\to \left(\varnothing {+}_{M}a=a\wedge a{+}_M\varnothing =a\right)$$
54	53	rgen	$$⊢\forall a\in {\mathrm{Base}}_M\left(\varnothing {+}_{M}a=a\wedge a{+}_M\varnothing =a\right)$$
55	43 54	pm3.2i	$$⊢\left(\varnothing \in {\mathrm{Base}}_M\wedge \forall a\in {\mathrm{Base}}_M\left(\varnothing {+}_{M}a=a\wedge a{+}_M\varnothing =a\right)\right)$$
56	33 41 55	ceqsexv2d	$$⊢\exists e\left(e\in {\mathrm{Base}}_M\wedge \forall a\in {\mathrm{Base}}_M\left(e{+}_{M}a=a\wedge a{+}_{M}e=a\right)\right)$$
57		df-rex	$$⊢\exists e\in {\mathrm{Base}}_M\forall a\in {\mathrm{Base}}_M\left(e{+}_{M}a=a\wedge a{+}_{M}e=a\right)\leftrightarrow \exists e\left(e\in {\mathrm{Base}}_M\wedge \forall a\in {\mathrm{Base}}_M\left(e{+}_{M}a=a\wedge a{+}_{M}e=a\right)\right)$$
58	56 57	mpbir	$$⊢\exists e\in {\mathrm{Base}}_M\forall a\in {\mathrm{Base}}_M\left(e{+}_{M}a=a\wedge a{+}_{M}e=a\right)$$
59	32 58	pm3.2i	$$⊢\left(\forall a\in {\mathrm{Base}}_M\forall b\in {\mathrm{Base}}_M\left(a{+}_{M}b\in {\mathrm{Base}}_M\wedge \forall c\in {\mathrm{Base}}_M\left(a{+}_{M}b\right){+}_{M}c=a{+}_M\left(b{+}_{M}c\right)\right)\wedge \exists e\in {\mathrm{Base}}_M\forall a\in {\mathrm{Base}}_M\left(e{+}_{M}a=a\wedge a{+}_{M}e=a\right)\right)$$
60		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
61		eqid	$$⊢{+}_M={+}_M$$
62	60 61	ismnd	$$⊢M\in \mathrm{Mnd}\leftrightarrow \left(\forall a\in {\mathrm{Base}}_M\forall b\in {\mathrm{Base}}_M\left(a{+}_{M}b\in {\mathrm{Base}}_M\wedge \forall c\in {\mathrm{Base}}_M\left(a{+}_{M}b\right){+}_{M}c=a{+}_M\left(b{+}_{M}c\right)\right)\wedge \exists e\in {\mathrm{Base}}_M\forall a\in {\mathrm{Base}}_M\left(e{+}_{M}a=a\wedge a{+}_{M}e=a\right)\right)$$
63	59 62	mpbir	$$⊢M\in \mathrm{Mnd}$$