abln0

Description: Abelian groups (and therefore also groups and monoids) exist. (Contributed by AV, 29-Apr-2019)

		Ref	Expression
	Assertion	abln0	$⊢ Abel \neq \emptyset$

Step	Hyp	Ref	Expression
1		vex	$⊢ i \in V$
2		eqid	$⊢ \{⟨{Base}_{ndx}, \{i\}⟩, ⟨+_{ndx}, \{⟨⟨i, i⟩, i⟩\}⟩\} = \{⟨{Base}_{ndx}, \{i\}⟩, ⟨+_{ndx}, \{⟨⟨i, i⟩, i⟩\}⟩\}$
3	2	abl1	$⊢ i \in V \to \{⟨{Base}_{ndx}, \{i\}⟩, ⟨+_{ndx}, \{⟨⟨i, i⟩, i⟩\}⟩\} \in Abel$
4		ne0i	$⊢ \{⟨{Base}_{ndx}, \{i\}⟩, ⟨+_{ndx}, \{⟨⟨i, i⟩, i⟩\}⟩\} \in Abel \to Abel \neq \emptyset$
5	1 3 4	mp2b	$⊢ Abel \neq \emptyset$

Metamath Proof Explorer