Definition df-eqlg 28874

Description: Define the class of equilateral triangles. (Contributed by Thierry Arnoux, 27-Nov-2019.)

Assertion

Ref	Expression
df-eqlg	⊢ eqltrG = (𝑔 ∈ V ↦ {𝑥 ∈ ((Base‘𝑔) ↑m (0..^3)) ∣ 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩})

Distinct variable group:   𝑥,𝑔

Detailed syntax breakdown of Definition df-eqlg

Step	Hyp	Ref	Expression
1		ceqlg 28873	. 2 class eqltrG
2		vg	. . 3 setvar 𝑔
3		cvv 3480	. . 3 class V
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1539	. . . . 5 class 𝑥
6		c1 11156	. . . . . . 7 class 1
7	6, 5	cfv 6561	. . . . . 6 class (𝑥‘1)
8		c2 12321	. . . . . . 7 class 2
9	8, 5	cfv 6561	. . . . . 6 class (𝑥‘2)
10		cc0 11155	. . . . . . 7 class 0
11	10, 5	cfv 6561	. . . . . 6 class (𝑥‘0)
12	7, 9, 11	cs3 14881	. . . . 5 class ⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩
13	2	cv 1539	. . . . . 6 class 𝑔
14		ccgrg 28518	. . . . . 6 class cgrG
15	13, 14	cfv 6561	. . . . 5 class (cgrG‘𝑔)
16	5, 12, 15	wbr 5143	. . . 4 wff 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩
17		cbs 17247	. . . . . 6 class Base
18	13, 17	cfv 6561	. . . . 5 class (Base‘𝑔)
19		c3 12322	. . . . . 6 class 3
20		cfzo 13694	. . . . . 6 class ..^
21	10, 19, 20	co 7431	. . . . 5 class (0..^3)
22		cmap 8866	. . . . 5 class ↑m
23	18, 21, 22	co 7431	. . . 4 class ((Base‘𝑔) ↑m (0..^3))
24	16, 4, 23	crab 3436	. . 3 class {𝑥 ∈ ((Base‘𝑔) ↑m (0..^3)) ∣ 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩}
25	2, 3, 24	cmpt 5225	. 2 class (𝑔 ∈ V ↦ {𝑥 ∈ ((Base‘𝑔) ↑m (0..^3)) ∣ 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩})
26	1, 25	wceq 1540	1 wff eqltrG = (𝑔 ∈ V ↦ {𝑥 ∈ ((Base‘𝑔) ↑m (0..^3)) ∣ 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩})

This definition is referenced by:  iseqlg  28875