Detailed syntax breakdown of Definition df-eqlg
Step | Hyp | Ref
| Expression |
1 | | ceqlg 26653 |
. 2
class
eqltrG |
2 | | vg |
. . 3
setvar 𝑔 |
3 | | cvv 3496 |
. . 3
class
V |
4 | | vx |
. . . . . 6
setvar 𝑥 |
5 | 4 | cv 1536 |
. . . . 5
class 𝑥 |
6 | | c1 10540 |
. . . . . . 7
class
1 |
7 | 6, 5 | cfv 6357 |
. . . . . 6
class (𝑥‘1) |
8 | | c2 11695 |
. . . . . . 7
class
2 |
9 | 8, 5 | cfv 6357 |
. . . . . 6
class (𝑥‘2) |
10 | | cc0 10539 |
. . . . . . 7
class
0 |
11 | 10, 5 | cfv 6357 |
. . . . . 6
class (𝑥‘0) |
12 | 7, 9, 11 | cs3 14206 |
. . . . 5
class
〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉 |
13 | 2 | cv 1536 |
. . . . . 6
class 𝑔 |
14 | | ccgrg 26298 |
. . . . . 6
class
cgrG |
15 | 13, 14 | cfv 6357 |
. . . . 5
class
(cgrG‘𝑔) |
16 | 5, 12, 15 | wbr 5068 |
. . . 4
wff 𝑥(cgrG‘𝑔)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉 |
17 | | cbs 16485 |
. . . . . 6
class
Base |
18 | 13, 17 | cfv 6357 |
. . . . 5
class
(Base‘𝑔) |
19 | | c3 11696 |
. . . . . 6
class
3 |
20 | | cfzo 13036 |
. . . . . 6
class
..^ |
21 | 10, 19, 20 | co 7158 |
. . . . 5
class
(0..^3) |
22 | | cmap 8408 |
. . . . 5
class
↑m |
23 | 18, 21, 22 | co 7158 |
. . . 4
class
((Base‘𝑔)
↑m (0..^3)) |
24 | 16, 4, 23 | crab 3144 |
. . 3
class {𝑥 ∈ ((Base‘𝑔) ↑m (0..^3))
∣ 𝑥(cgrG‘𝑔)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉} |
25 | 2, 3, 24 | cmpt 5148 |
. 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)”〉}) |