Definition df-od 19474

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 19470	. 2 class od
2		vg	. . 3 setvar 𝑔
3		cvv 3469	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5	2	cv 1533	. . . . 5 class 𝑔
6		cbs 17171	. . . . 5 class Base
7	5, 6	cfv 6542	. . . 4 class (Base‘𝑔)
8		vi	. . . . 5 setvar 𝑖
9		vn	. . . . . . . . 9 setvar 𝑛
10	9	cv 1533	. . . . . . . 8 class 𝑛
11	4	cv 1533	. . . . . . . 8 class 𝑥
12		cmg 19014	. . . . . . . . 9 class .g
13	5, 12	cfv 6542	. . . . . . . 8 class (.g‘𝑔)
14	10, 11, 13	co 7414	. . . . . . 7 class (𝑛(.g‘𝑔)𝑥)
15		c0g 17412	. . . . . . . 8 class 0g
16	5, 15	cfv 6542	. . . . . . 7 class (0g‘𝑔)
17	14, 16	wceq 1534	. . . . . 6 wff (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)
18		cn 12234	. . . . . 6 class ℕ
19	17, 9, 18	crab 3427	. . . . 5 class {𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)}
20	8	cv 1533	. . . . . . 7 class 𝑖
21		c0 4318	. . . . . . 7 class ∅
22	20, 21	wceq 1534	. . . . . 6 wff 𝑖 = ∅
23		cc0 11130	. . . . . 6 class 0
24		cr 11129	. . . . . . 7 class ℝ
25		clt 11270	. . . . . . 7 class <
26	20, 24, 25	cinf 9456	. . . . . 6 class inf(𝑖, ℝ, < )
27	22, 23, 26	cif 4524	. . . . 5 class if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))
28	8, 19, 27	csb 3889	. . . 4 class ⦋{𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))
29	4, 7, 28	cmpt 5225	. . 3 class (𝑥 ∈ (Base‘𝑔) ↦ ⦋{𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))
30	2, 3, 29	cmpt 5225	. 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ ⦋{𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))))
31	1, 30	wceq 1534	1 wff od = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ ⦋{𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))))

This definition is referenced by:  odfval  19478  odfvalALT  19479