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

Proof

Step	Hyp	Ref	Expression
1		pwmnd.b	⊢ ( Base ‘ 𝑀 ) = 𝒫 𝐴
2		pwmnd.p	⊢ ( +g ‘ 𝑀 ) = ( 𝑥 ∈ 𝒫 𝐴 , 𝑦 ∈ 𝒫 𝐴 ↦ ( 𝑥 ∪ 𝑦 ) )
3		0elpw	⊢ ∅ ∈ 𝒫 𝐴
4	1	eqcomi	⊢ 𝒫 𝐴 = ( Base ‘ 𝑀 )
5		eqid	⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
6		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
7		id	⊢ ( ∅ ∈ 𝒫 𝐴 → ∅ ∈ 𝒫 𝐴 )
8	1 2	pwmndgplus	⊢ ( ( ∅ ∈ 𝒫 𝐴 ∧ 𝑧 ∈ 𝒫 𝐴 ) → ( ∅ ( +g ‘ 𝑀 ) 𝑧 ) = ( ∅ ∪ 𝑧 ) )
9		0un	⊢ ( ∅ ∪ 𝑧 ) = 𝑧
10	8 9	eqtrdi	⊢ ( ( ∅ ∈ 𝒫 𝐴 ∧ 𝑧 ∈ 𝒫 𝐴 ) → ( ∅ ( +g ‘ 𝑀 ) 𝑧 ) = 𝑧 )
11	1 2	pwmndgplus	⊢ ( ( 𝑧 ∈ 𝒫 𝐴 ∧ ∅ ∈ 𝒫 𝐴 ) → ( 𝑧 ( +g ‘ 𝑀 ) ∅ ) = ( 𝑧 ∪ ∅ ) )
12	11	ancoms	⊢ ( ( ∅ ∈ 𝒫 𝐴 ∧ 𝑧 ∈ 𝒫 𝐴 ) → ( 𝑧 ( +g ‘ 𝑀 ) ∅ ) = ( 𝑧 ∪ ∅ ) )
13		un0	⊢ ( 𝑧 ∪ ∅ ) = 𝑧
14	12 13	eqtrdi	⊢ ( ( ∅ ∈ 𝒫 𝐴 ∧ 𝑧 ∈ 𝒫 𝐴 ) → ( 𝑧 ( +g ‘ 𝑀 ) ∅ ) = 𝑧 )
15	4 5 6 7 10 14	ismgmid2	⊢ ( ∅ ∈ 𝒫 𝐴 → ∅ = ( 0g ‘ 𝑀 ) )
16	15	eqcomd	⊢ ( ∅ ∈ 𝒫 𝐴 → ( 0g ‘ 𝑀 ) = ∅ )
17	3 16	ax-mp	⊢ ( 0g ‘ 𝑀 ) = ∅