Theorem odf

Description: Functionality of the group element order. (Contributed by Stefan O'Rear, 5-Sep-2015) (Proof shortened by AV, 5-Oct-2020)

	Ref	Expression
Hypotheses	odcl.1	$$⊢X={\mathrm{Base}}_G$$
	odcl.2	$$⊢O=\mathrm{od}\left(G\right)$$
Assertion	odf	$$⊢O:X⟶{\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		odcl.1	$$⊢X={\mathrm{Base}}_G$$
2		odcl.2	$$⊢O=\mathrm{od}\left(G\right)$$
3		c0ex	$$⊢0\in \mathrm{V}$$
4		ltso	$$⊢<\mathrm{Or}ℝ$$
5	4	infex	$$⊢inf\left(w,ℝ,<\right)\in \mathrm{V}$$
6	3 5	ifex	$$⊢if\left(w=\varnothing ,0,inf\left(w,ℝ,<\right)\right)\in \mathrm{V}$$
7	6	csbex	$$⊢⦋\left\{z\in \mathbb{N}|z{\cdot }_{G}y=0_G\right\}/w⦌if\left(w=\varnothing ,0,inf\left(w,ℝ,<\right)\right)\in \mathrm{V}$$
8		eqid	$$⊢{\cdot }_G={\cdot }_G$$
9		eqid	$$⊢0_G=0_G$$
10	1 8 9 2	odfval	$$⊢O=\left(y\in X⟼⦋\left\{z\in \mathbb{N}|z{\cdot }_{G}y=0_G\right\}/w⦌if\left(w=\varnothing ,0,inf\left(w,ℝ,<\right)\right)\right)$$
11	7 10	fnmpti	$$⊢OFnX$$
12	1 2	odcl	$$⊢x\in X\to O\left(x\right)\in {\mathbb{N}}_0$$
13	12	rgen	$$⊢\forall x\in XO\left(x\right)\in {\mathbb{N}}_0$$
14		ffnfv	$$⊢O:X⟶{\mathbb{N}}_0\leftrightarrow \left(OFnX\wedge \forall x\in XO\left(x\right)\in {\mathbb{N}}_0\right)$$
15	11 13 14	mpbir2an	$$⊢O:X⟶{\mathbb{N}}_0$$