Definition df-gex 19571

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 19567	. 2 class gEx
2		vg	. . 3 setvar 𝑔
3		cvv 3488	. . 3 class V
4		vi	. . . 4 setvar 𝑖
5		vn	. . . . . . . . 9 setvar 𝑛
6	5	cv 1536	. . . . . . . 8 class 𝑛
7		vx	. . . . . . . . 9 setvar 𝑥
8	7	cv 1536	. . . . . . . 8 class 𝑥
9	2	cv 1536	. . . . . . . . 9 class 𝑔
10		cmg 19107	. . . . . . . . 9 class .g
11	9, 10	cfv 6573	. . . . . . . 8 class (.g‘𝑔)
12	6, 8, 11	co 7448	. . . . . . 7 class (𝑛(.g‘𝑔)𝑥)
13		c0g 17499	. . . . . . . 8 class 0g
14	9, 13	cfv 6573	. . . . . . 7 class (0g‘𝑔)
15	12, 14	wceq 1537	. . . . . 6 wff (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)
16		cbs 17258	. . . . . . 7 class Base
17	9, 16	cfv 6573	. . . . . 6 class (Base‘𝑔)
18	15, 7, 17	wral 3067	. . . . 5 wff ∀𝑥 ∈ (Base‘𝑔)(𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)
19		cn 12293	. . . . 5 class ℕ
20	18, 5, 19	crab 3443	. . . 4 class {𝑛 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)}
21	4	cv 1536	. . . . . 6 class 𝑖
22		c0 4352	. . . . . 6 class ∅
23	21, 22	wceq 1537	. . . . 5 wff 𝑖 = ∅
24		cc0 11184	. . . . 5 class 0
25		cr 11183	. . . . . 6 class ℝ
26		clt 11324	. . . . . 6 class <
27	21, 25, 26	cinf 9510	. . . . 5 class inf(𝑖, ℝ, < )
28	23, 24, 27	cif 4548	. . . 4 class if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))
29	4, 20, 28	csb 3921	. . 3 class ⦋{𝑛 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))
30	2, 3, 29	cmpt 5249	. 2 class (𝑔 ∈ V ↦ ⦋{𝑛 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))
31	1, 30	wceq 1537	1 wff gEx = (𝑔 ∈ V ↦ ⦋{𝑛 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))

This definition is referenced by:  gexval  19620