Theorem gexcl

Description: The exponent of a group is a nonnegative integer. (Contributed by Mario Carneiro, 23-Apr-2016)

	Ref	Expression
Hypotheses	gexcl.1	$$⊢X={\mathrm{Base}}_G$$
	gexcl.2	$$⊢E=\mathrm{gEx}\left(G\right)$$
Assertion	gexcl	$$⊢G\in V\to E\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		gexcl.1	$$⊢X={\mathrm{Base}}_G$$
2		gexcl.2	$$⊢E=\mathrm{gEx}\left(G\right)$$
3		eqid	$$⊢{\cdot }_G={\cdot }_G$$
4		eqid	$$⊢0_G=0_G$$
5		eqid	$$⊢\left\{y\in \mathbb{N}|\forall x\in Xy{\cdot }_{G}x=0_G\right\}=\left\{y\in \mathbb{N}|\forall x\in Xy{\cdot }_{G}x=0_G\right\}$$
6	1 3 4 2 5	gexlem1	$$⊢G\in V\to \left(\left(E=0\wedge \left\{y\in \mathbb{N}|\forall x\in Xy{\cdot }_{G}x=0_G\right\}=\varnothing \right)\vee E\in \left\{y\in \mathbb{N}|\forall x\in Xy{\cdot }_{G}x=0_G\right\}\right)$$
7		simpl	$$⊢\left(E=0\wedge \left\{y\in \mathbb{N}|\forall x\in Xy{\cdot }_{G}x=0_G\right\}=\varnothing \right)\to E=0$$
8		elrabi	$$⊢E\in \left\{y\in \mathbb{N}|\forall x\in Xy{\cdot }_{G}x=0_G\right\}\to E\in \mathbb{N}$$
9	7 8	orim12i	$$⊢\left(\left(E=0\wedge \left\{y\in \mathbb{N}|\forall x\in Xy{\cdot }_{G}x=0_G\right\}=\varnothing \right)\vee E\in \left\{y\in \mathbb{N}|\forall x\in Xy{\cdot }_{G}x=0_G\right\}\right)\to \left(E=0\vee E\in \mathbb{N}\right)$$
10	6 9	syl	$$⊢G\in V\to \left(E=0\vee E\in \mathbb{N}\right)$$
11	10	orcomd	$$⊢G\in V\to \left(E\in \mathbb{N}\vee E=0\right)$$
12		elnn0	$$⊢E\in {\mathbb{N}}_0\leftrightarrow \left(E\in \mathbb{N}\vee E=0\right)$$
13	11 12	sylibr	$$⊢G\in V\to E\in {\mathbb{N}}_0$$