Definition df-eqlg 27208

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 27207	. 2 class eqltrG
2		vg	. . 3 setvar 𝑔
3		cvv 3430	. . 3 class V
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1540	. . . . 5 class 𝑥
6		c1 10856	. . . . . . 7 class 1
7	6, 5	cfv 6430	. . . . . 6 class (𝑥‘1)
8		c2 12011	. . . . . . 7 class 2
9	8, 5	cfv 6430	. . . . . 6 class (𝑥‘2)
10		cc0 10855	. . . . . . 7 class 0
11	10, 5	cfv 6430	. . . . . 6 class (𝑥‘0)
12	7, 9, 11	cs3 14536	. . . . 5 class ⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩
13	2	cv 1540	. . . . . 6 class 𝑔
14		ccgrg 26852	. . . . . 6 class cgrG
15	13, 14	cfv 6430	. . . . 5 class (cgrG‘𝑔)
16	5, 12, 15	wbr 5078	. . . 4 wff 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩
17		cbs 16893	. . . . . 6 class Base
18	13, 17	cfv 6430	. . . . 5 class (Base‘𝑔)
19		c3 12012	. . . . . 6 class 3
20		cfzo 13364	. . . . . 6 class ..^
21	10, 19, 20	co 7268	. . . . 5 class (0..^3)
22		cmap 8589	. . . . 5 class ↑m
23	18, 21, 22	co 7268	. . . 4 class ((Base‘𝑔) ↑m (0..^3))
24	16, 4, 23	crab 3069	. . 3 class {𝑥 ∈ ((Base‘𝑔) ↑m (0..^3)) ∣ 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩}
25	2, 3, 24	cmpt 5161	. 2 class (𝑔 ∈ V ↦ {𝑥 ∈ ((Base‘𝑔) ↑m (0..^3)) ∣ 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩})
26	1, 25	wceq 1541	1 wff eqltrG = (𝑔 ∈ V ↦ {𝑥 ∈ ((Base‘𝑔) ↑m (0..^3)) ∣ 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩})

This definition is referenced by:  iseqlg  27209