Theorem abln0

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

	Ref	Expression
Assertion	abln0	$$⊢\mathrm{Abel}\ne \varnothing$$

Proof

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