Theorem 0subm

Description: The zero submonoid of an arbitrary monoid. (Contributed by AV, 17-Feb-2024)

	Ref	Expression
Hypothesis	0subm.z	|- .0. = ( 0g ` G )
Assertion	0subm	|- ( G e. Mnd -> { .0. } e. ( SubMnd ` G ) )

Proof

Step	Hyp	Ref	Expression
1		0subm.z	|- .0. = ( 0g ` G )
2		eqid	|- ( Base ` G ) = ( Base ` G )
3	2 1	mndidcl	|- ( G e. Mnd -> .0. e. ( Base ` G ) )
4	3	snssd	|- ( G e. Mnd -> { .0. } C_ ( Base ` G ) )
5	1	fvexi	|- .0. e. _V
6	5	snid	|- .0. e. { .0. }
7	6	a1i	|- ( G e. Mnd -> .0. e. { .0. } )
8		velsn	|- ( a e. { .0. } <-> a = .0. )
9		velsn	|- ( b e. { .0. } <-> b = .0. )
10	8 9	anbi12i	|- ( ( a e. { .0. } /\ b e. { .0. } ) <-> ( a = .0. /\ b = .0. ) )
11		eqid	|- ( +g ` G ) = ( +g ` G )
12	2 11 1	mndlid	|- ( ( G e. Mnd /\ .0. e. ( Base ` G ) ) -> ( .0. ( +g ` G ) .0. ) = .0. )
13	3 12	mpdan	|- ( G e. Mnd -> ( .0. ( +g ` G ) .0. ) = .0. )
14		ovex	|- ( .0. ( +g ` G ) .0. ) e. _V
15	14	elsn	|- ( ( .0. ( +g ` G ) .0. ) e. { .0. } <-> ( .0. ( +g ` G ) .0. ) = .0. )
16	13 15	sylibr	|- ( G e. Mnd -> ( .0. ( +g ` G ) .0. ) e. { .0. } )
17		oveq12	|- ( ( a = .0. /\ b = .0. ) -> ( a ( +g ` G ) b ) = ( .0. ( +g ` G ) .0. ) )
18	17	eleq1d	|- ( ( a = .0. /\ b = .0. ) -> ( ( a ( +g ` G ) b ) e. { .0. } <-> ( .0. ( +g ` G ) .0. ) e. { .0. } ) )
19	16 18	syl5ibrcom	|- ( G e. Mnd -> ( ( a = .0. /\ b = .0. ) -> ( a ( +g ` G ) b ) e. { .0. } ) )
20	10 19	biimtrid	|- ( G e. Mnd -> ( ( a e. { .0. } /\ b e. { .0. } ) -> ( a ( +g ` G ) b ) e. { .0. } ) )
21	20	ralrimivv	|- ( G e. Mnd -> A. a e. { .0. } A. b e. { .0. } ( a ( +g ` G ) b ) e. { .0. } )
22	2 1 11	issubm	|- ( G e. Mnd -> ( { .0. } e. ( SubMnd ` G ) <-> ( { .0. } C_ ( Base ` G ) /\ .0. e. { .0. } /\ A. a e. { .0. } A. b e. { .0. } ( a ( +g ` G ) b ) e. { .0. } ) ) )
23	4 7 21 22	mpbir3and	|- ( G e. Mnd -> { .0. } e. ( SubMnd ` G ) )