Theorem abln0

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

	Ref	Expression
Assertion	abln0	|- Abel =/= (/)

Proof

Step	Hyp	Ref	Expression
1		vex	|- i e. _V
2		eqid	|- { <. ( Base ` ndx ) , { i } >. , <. ( +g ` ndx ) , { <. <. i , i >. , i >. } >. } = { <. ( Base ` ndx ) , { i } >. , <. ( +g ` ndx ) , { <. <. i , i >. , i >. } >. }
3	2	abl1	|- ( i e. _V -> { <. ( Base ` ndx ) , { i } >. , <. ( +g ` ndx ) , { <. <. i , i >. , i >. } >. } e. Abel )
4		ne0i	|- ( { <. ( Base ` ndx ) , { i } >. , <. ( +g ` ndx ) , { <. <. i , i >. , i >. } >. } e. Abel -> Abel =/= (/) )
5	1 3 4	mp2b	|- Abel =/= (/)