Definition df-od 19772

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 19768	. 2 class od
2		vg	. . 3 setvar 𝑔
3		cvv 3454	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5	2	cv 1569	. . . . 5 class 𝑔
6		cbs 17416	. . . . 5 class Base
7	5, 6	cfv 6558	. . . 4 class (Base‘𝑔)
8		vi	. . . . 5 setvar 𝑖
9		vn	. . . . . . . . 9 setvar 𝑛
10	9	cv 1569	. . . . . . . 8 class 𝑛
11	4	cv 1569	. . . . . . . 8 class 𝑥
12		cmg 19306	. . . . . . . . 9 class .g
13	5, 12	cfv 6558	. . . . . . . 8 class (.g‘𝑔)
14	10, 11, 13	co 7443	. . . . . . 7 class (𝑛(.g‘𝑔)𝑥)
15		c0g 17639	. . . . . . . 8 class 0g
16	5, 15	cfv 6558	. . . . . . 7 class (0g‘𝑔)
17	14, 16	wceq 1570	. . . . . 6 wff (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)
18		cn 12362	. . . . . 6 class ℕ
19	17, 9, 18	crab 3416	. . . . 5 class {𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)}
20	8	cv 1569	. . . . . . 7 class 𝑖
21		c0 4281	. . . . . . 7 class ∅
22	20, 21	wceq 1570	. . . . . 6 wff 𝑖 = ∅
23		cc0 11227	. . . . . 6 class 0
24		cr 11226	. . . . . . 7 class ℝ
25		clt 11370	. . . . . . 7 class <
26	20, 24, 25	cinf 9460	. . . . . 6 class inf(𝑖, ℝ, < )
27	22, 23, 26	cif 4485	. . . . 5 class if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))
28	8, 19, 27	csb 3851	. . . 4 class ⦋{𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))
29	4, 7, 28	cmpt 5189	. . 3 class (𝑥 ∈ (Base‘𝑔) ↦ ⦋{𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))
30	2, 3, 29	cmpt 5189	. 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ ⦋{𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))))
31	1, 30	wceq 1570	1 wff od = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ ⦋{𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))))

This definition is used by:  odfval  19776  odfvalALT  19777