Definition df-od 17771

Description: Define the order of an element in a group. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by Stefan O'Rear, 4-Sep-2015.) (Revised by AV, 5-Oct-2020.)

Assertion

Ref	Expression
df-od	⊢ od = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ ⦋{𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))))

Distinct variable group:   𝑔,𝑖,𝑛,𝑥

Detailed syntax breakdown of Definition df-od

Step	Hyp	Ref	Expression
1		cod 17767	. 2 class od
2		vg	. . 3 setvar 𝑔
3		cvv 3173	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5	2	cv 1474	. . . . 5 class 𝑔
6		cbs 15695	. . . . 5 class Base
7	5, 6	cfv 5804	. . . 4 class (Base‘𝑔)
8		vi	. . . . 5 setvar 𝑖
9		vn	. . . . . . . . 9 setvar 𝑛
10	9	cv 1474	. . . . . . . 8 class 𝑛
11	4	cv 1474	. . . . . . . 8 class 𝑥
12		cmg 17363	. . . . . . . . 9 class .g
13	5, 12	cfv 5804	. . . . . . . 8 class (.g‘𝑔)
14	10, 11, 13	co 6549	. . . . . . 7 class (𝑛(.g‘𝑔)𝑥)
15		c0g 15923	. . . . . . . 8 class 0g
16	5, 15	cfv 5804	. . . . . . 7 class (0g‘𝑔)
17	14, 16	wceq 1475	. . . . . 6 wff (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)
18		cn 10897	. . . . . 6 class ℕ
19	17, 9, 18	crab 2900	. . . . 5 class {𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)}
20	8	cv 1474	. . . . . . 7 class 𝑖
21		c0 3874	. . . . . . 7 class ∅
22	20, 21	wceq 1475	. . . . . 6 wff 𝑖 = ∅
23		cc0 9815	. . . . . 6 class 0
24		cr 9814	. . . . . . 7 class ℝ
25		clt 9953	. . . . . . 7 class <
26	20, 24, 25	cinf 8230	. . . . . 6 class inf(𝑖, ℝ, < )
27	22, 23, 26	cif 4036	. . . . 5 class if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))
28	8, 19, 27	csb 3499	. . . 4 class ⦋{𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))
29	4, 7, 28	cmpt 4643	. . 3 class (𝑥 ∈ (Base‘𝑔) ↦ ⦋{𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))
30	2, 3, 29	cmpt 4643	. 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ ⦋{𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))))
31	1, 30	wceq 1475	1 wff od = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ ⦋{𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))))

This definition is referenced by:  odfval  17775