Definition df-gex 19705

Description: Define the exponent of a group. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by Stefan O'Rear, 4-Sep-2015.) (Revised by AV, 26-Sep-2020.)

Assertion

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

Distinct variable group:   𝑔,𝑖,𝑛,𝑥

Detailed syntax breakdown of Definition df-gex

Step	Hyp	Ref	Expression
1		cgex 19701	. 2 class gEx
2		vg	. . 3 setvar 𝑔
3		cvv 3450	. . 3 class V
4		vi	. . . 4 setvar 𝑖
5		vn	. . . . . . . . 9 setvar 𝑛
6	5	cv 1569	. . . . . . . 8 class 𝑛
7		vx	. . . . . . . . 9 setvar 𝑥
8	7	cv 1569	. . . . . . . 8 class 𝑥
9	2	cv 1569	. . . . . . . . 9 class 𝑔
10		cmg 19239	. . . . . . . . 9 class .g
11	9, 10	cfv 6527	. . . . . . . 8 class (.g‘𝑔)
12	6, 8, 11	co 7408	. . . . . . 7 class (𝑛(.g‘𝑔)𝑥)
13		c0g 17572	. . . . . . . 8 class 0g
14	9, 13	cfv 6527	. . . . . . 7 class (0g‘𝑔)
15	12, 14	wceq 1570	. . . . . 6 wff (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)
16		cbs 17349	. . . . . . 7 class Base
17	9, 16	cfv 6527	. . . . . 6 class (Base‘𝑔)
18	15, 7, 17	wral 3076	. . . . 5 wff ∀𝑥 ∈ (Base‘𝑔)(𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)
19		cn 12305	. . . . 5 class ℕ
20	18, 5, 19	crab 3412	. . . 4 class {𝑛 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)}
21	4	cv 1569	. . . . . 6 class 𝑖
22		c0 4278	. . . . . 6 class ∅
23	21, 22	wceq 1570	. . . . 5 wff 𝑖 = ∅
24		cc0 11172	. . . . 5 class 0
25		cr 11171	. . . . . 6 class ℝ
26		clt 11315	. . . . . 6 class <
27	21, 25, 26	cinf 9411	. . . . 5 class inf(𝑖, ℝ, < )
28	23, 24, 27	cif 4481	. . . 4 class if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))
29	4, 20, 28	csb 3846	. . 3 class ⦋{𝑛 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))
30	2, 3, 29	cmpt 5185	. 2 class (𝑔 ∈ V ↦ ⦋{𝑛 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))
31	1, 30	wceq 1570	1 wff gEx = (𝑔 ∈ V ↦ ⦋{𝑛 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))

This definition is used by:  gexval  19754