Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-eqlg Structured version   Visualization version   GIF version

Definition df-eqlg 26654
 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
StepHypRef Expression
1 ceqlg 26653 . 2 class eqltrG
2 vg . . 3 setvar 𝑔
3 cvv 3496 . . 3 class V
4 vx . . . . . 6 setvar 𝑥
54cv 1536 . . . . 5 class 𝑥
6 c1 10540 . . . . . . 7 class 1
76, 5cfv 6357 . . . . . 6 class (𝑥‘1)
8 c2 11695 . . . . . . 7 class 2
98, 5cfv 6357 . . . . . 6 class (𝑥‘2)
10 cc0 10539 . . . . . . 7 class 0
1110, 5cfv 6357 . . . . . 6 class (𝑥‘0)
127, 9, 11cs3 14206 . . . . 5 class ⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩
132cv 1536 . . . . . 6 class 𝑔
14 ccgrg 26298 . . . . . 6 class cgrG
1513, 14cfv 6357 . . . . 5 class (cgrG‘𝑔)
165, 12, 15wbr 5068 . . . 4 wff 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩
17 cbs 16485 . . . . . 6 class Base
1813, 17cfv 6357 . . . . 5 class (Base‘𝑔)
19 c3 11696 . . . . . 6 class 3
20 cfzo 13036 . . . . . 6 class ..^
2110, 19, 20co 7158 . . . . 5 class (0..^3)
22 cmap 8408 . . . . 5 class m
2318, 21, 22co 7158 . . . 4 class ((Base‘𝑔) ↑m (0..^3))
2416, 4, 23crab 3144 . . 3 class {𝑥 ∈ ((Base‘𝑔) ↑m (0..^3)) ∣ 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩}
252, 3, 24cmpt 5148 . 2 class (𝑔 ∈ V ↦ {𝑥 ∈ ((Base‘𝑔) ↑m (0..^3)) ∣ 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩})
261, 25wceq 1537 1 wff eqltrG = (𝑔 ∈ V ↦ {𝑥 ∈ ((Base‘𝑔) ↑m (0..^3)) ∣ 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩})
 Colors of variables: wff setvar class This definition is referenced by:  iseqlg  26655
 Copyright terms: Public domain W3C validator