Definition df-gex 17772

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

This definition is referenced by:  gexval  17816