Definition df-eqlg 29213

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 29212	. 2 class eqltrG
2		vg	. . 3 setvar 𝑔
3		cvv 3458	. . 3 class V
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1569	. . . . 5 class 𝑥
6		c1 11119	. . . . . . 7 class 1
7	6, 5	cfv 6543	. . . . . 6 class (𝑥‘1)
8		c2 12313	. . . . . . 7 class 2
9	8, 5	cfv 6543	. . . . . 6 class (𝑥‘2)
10		cc0 11118	. . . . . . 7 class 0
11	10, 5	cfv 6543	. . . . . 6 class (𝑥‘0)
12	7, 9, 11	cs3 14905	. . . . 5 class ⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩
13	2	cv 1569	. . . . . 6 class 𝑔
14		ccgrg 28809	. . . . . 6 class cgrG
15	13, 14	cfv 6543	. . . . 5 class (cgrG‘𝑔)
16	5, 12, 15	wbr 5114	. . . 4 wff 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩
17		cbs 17294	. . . . . 6 class Base
18	13, 17	cfv 6543	. . . . 5 class (Base‘𝑔)
19		c3 12314	. . . . . 6 class 3
20		cfzo 13701	. . . . . 6 class ..^
21	10, 19, 20	co 7423	. . . . 5 class (0..^3)
22		cmap 8833	. . . . 5 class ↑m
23	18, 21, 22	co 7423	. . . 4 class ((Base‘𝑔) ↑m (0..^3))
24	16, 4, 23	crab 3419	. . 3 class {𝑥 ∈ ((Base‘𝑔) ↑m (0..^3)) ∣ 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩}
25	2, 3, 24	cmpt 5197	. 2 class (𝑔 ∈ V ↦ {𝑥 ∈ ((Base‘𝑔) ↑m (0..^3)) ∣ 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩})
26	1, 25	wceq 1570	1 wff eqltrG = (𝑔 ∈ V ↦ {𝑥 ∈ ((Base‘𝑔) ↑m (0..^3)) ∣ 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩})

This definition is used by:  iseqlg  29214