df-eqlg

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

		Ref	Expression
	Assertion	df-eqlg	$⊢ {Equilaterals}_{𝒢} = (g \in V ⟼ \{x \in ({Base}_{g}^{(0 ..^3)}) \| x \sim_{𝒢} (g) ⟨“ x (1) x (2) x (0) ”⟩\})$

Step	Hyp	Ref	Expression
0		ceqlg	$class {Equilaterals}_{𝒢}$
1		vg	$setvar g$
2		cvv	$class V$
3		vx	$setvar x$
4		cbs	$class Base$
5	1	cv	$setvar g$
6	5 4	cfv	$class {Base}_{g}$
7		cmap	$class ↑_{𝑚}$
8		cc0	$class 0$
9		cfzo	$class ..^$
10		c3	$class 3$
11	8 10 9	co	$class (0 ..^3)$
12	6 11 7	co	$class ({Base}_{g}^{(0 ..^3)})$
13	3	cv	$setvar x$
14		ccgrg	$class \sim_{𝒢}$
15	5 14	cfv	$class \sim_{𝒢} (g)$
16		c1	$class 1$
17	16 13	cfv	$class x (1)$
18		c2	$class 2$
19	18 13	cfv	$class x (2)$
20	8 13	cfv	$class x (0)$
21	17 19 20	cs3	$class ⟨“ x (1) x (2) x (0) ”⟩$
22	13 21 15	wbr	$wff x \sim_{𝒢} (g) ⟨“ x (1) x (2) x (0) ”⟩$
23	22 3 12	crab	$class \{x \in ({Base}_{g}^{(0 ..^3)}) \| x \sim_{𝒢} (g) ⟨“ x (1) x (2) x (0) ”⟩\}$
24	1 2 23	cmpt	$class (g \in V ⟼ \{x \in ({Base}_{g}^{(0 ..^3)}) \| x \sim_{𝒢} (g) ⟨“ x (1) x (2) x (0) ”⟩\})$
25	0 24	wceq	$wff {Equilaterals}_{𝒢} = (g \in V ⟼ \{x \in ({Base}_{g}^{(0 ..^3)}) \| x \sim_{𝒢} (g) ⟨“ x (1) x (2) x (0) ”⟩\})$

Metamath Proof Explorer