mnd1id

Description: The singleton element of atrivial monoid is its identity element. (Contributed by AV, 23-Jan-2020)

		Ref	Expression
	Hypothesis	mnd1.m	$⊢ M = \{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}$
	Assertion	mnd1id	$⊢ I \in V \to 0_{M} = I$

Proof

Step	Hyp	Ref	Expression
1		mnd1.m	$⊢ M = \{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}$
2		snex	$⊢ \{I\} \in V$
3	1	grpbase	$⊢ \{I\} \in V \to \{I\} = {Base}_{M}$
4	2 3	ax-mp	$⊢ \{I\} = {Base}_{M}$
5		eqid	$⊢ 0_{M} = 0_{M}$
6		snex	$⊢ \{⟨⟨I, I⟩, I⟩\} \in V$
7	1	grpplusg	$⊢ \{⟨⟨I, I⟩, I⟩\} \in V \to \{⟨⟨I, I⟩, I⟩\} = +_{M}$
8	6 7	ax-mp	$⊢ \{⟨⟨I, I⟩, I⟩\} = +_{M}$
9		snidg	$⊢ I \in V \to I \in \{I\}$
10		velsn	$⊢ a \in \{I\} \leftrightarrow a = I$
11		df-ov	$⊢ I \{⟨⟨I, I⟩, I⟩\} I = \{⟨⟨I, I⟩, I⟩\} (⟨I, I⟩)$
12		opex	$⊢ ⟨I, I⟩ \in V$
13		fvsng	$⊢ (⟨I, I⟩ \in V \land I \in V) \to \{⟨⟨I, I⟩, I⟩\} (⟨I, I⟩) = I$
14	12 13	mpan	$⊢ I \in V \to \{⟨⟨I, I⟩, I⟩\} (⟨I, I⟩) = I$
15	11 14	eqtrid	$⊢ I \in V \to I \{⟨⟨I, I⟩, I⟩\} I = I$
16		oveq2	$⊢ a = I \to I \{⟨⟨I, I⟩, I⟩\} a = I \{⟨⟨I, I⟩, I⟩\} I$
17		id	$⊢ a = I \to a = I$
18	16 17	eqeq12d	$⊢ a = I \to (I \{⟨⟨I, I⟩, I⟩\} a = a \leftrightarrow I \{⟨⟨I, I⟩, I⟩\} I = I)$
19	15 18	syl5ibrcom	$⊢ I \in V \to (a = I \to I \{⟨⟨I, I⟩, I⟩\} a = a)$
20	10 19	biimtrid	$⊢ I \in V \to (a \in \{I\} \to I \{⟨⟨I, I⟩, I⟩\} a = a)$
21	20	imp	$⊢ (I \in V \land a \in \{I\}) \to I \{⟨⟨I, I⟩, I⟩\} a = a$
22		oveq1	$⊢ a = I \to a \{⟨⟨I, I⟩, I⟩\} I = I \{⟨⟨I, I⟩, I⟩\} I$
23	22 17	eqeq12d	$⊢ a = I \to (a \{⟨⟨I, I⟩, I⟩\} I = a \leftrightarrow I \{⟨⟨I, I⟩, I⟩\} I = I)$
24	15 23	syl5ibrcom	$⊢ I \in V \to (a = I \to a \{⟨⟨I, I⟩, I⟩\} I = a)$
25	10 24	biimtrid	$⊢ I \in V \to (a \in \{I\} \to a \{⟨⟨I, I⟩, I⟩\} I = a)$
26	25	imp	$⊢ (I \in V \land a \in \{I\}) \to a \{⟨⟨I, I⟩, I⟩\} I = a$
27	4 5 8 9 21 26	ismgmid2	$⊢ I \in V \to I = 0_{M}$
28	27	eqcomd	$⊢ I \in V \to 0_{M} = I$

Metamath Proof Explorer

Theorem mnd1id

Proof