Definition df-eqlg 26638

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 26637	. 2 class eqltrG
2		vg	. . 3 setvar 𝑔
3		cvv 3486	. . 3 class V
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1536	. . . . 5 class 𝑥
6		c1 10524	. . . . . . 7 class 1
7	6, 5	cfv 6341	. . . . . 6 class (𝑥‘1)
8		c2 11679	. . . . . . 7 class 2
9	8, 5	cfv 6341	. . . . . 6 class (𝑥‘2)
10		cc0 10523	. . . . . . 7 class 0
11	10, 5	cfv 6341	. . . . . 6 class (𝑥‘0)
12	7, 9, 11	cs3 14189	. . . . 5 class ⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩
13	2	cv 1536	. . . . . 6 class 𝑔
14		ccgrg 26282	. . . . . 6 class cgrG
15	13, 14	cfv 6341	. . . . 5 class (cgrG‘𝑔)
16	5, 12, 15	wbr 5052	. . . 4 wff 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩
17		cbs 16466	. . . . . 6 class Base
18	13, 17	cfv 6341	. . . . 5 class (Base‘𝑔)
19		c3 11680	. . . . . 6 class 3
20		cfzo 13023	. . . . . 6 class ..^
21	10, 19, 20	co 7142	. . . . 5 class (0..^3)
22		cmap 8392	. . . . 5 class ↑m
23	18, 21, 22	co 7142	. . . 4 class ((Base‘𝑔) ↑m (0..^3))
24	16, 4, 23	crab 3142	. . 3 class {𝑥 ∈ ((Base‘𝑔) ↑m (0..^3)) ∣ 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩}
25	2, 3, 24	cmpt 5132	. 2 class (𝑔 ∈ V ↦ {𝑥 ∈ ((Base‘𝑔) ↑m (0..^3)) ∣ 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩})
26	1, 25	wceq 1537	1 wff eqltrG = (𝑔 ∈ V ↦ {𝑥 ∈ ((Base‘𝑔) ↑m (0..^3)) ∣ 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩})

This definition is referenced by:  iseqlg  26639