Detailed syntax breakdown of Definition df-cgra
Step | Hyp | Ref
| Expression |
1 | | ccgra 27166 |
. 2
class
cgrA |
2 | | vg |
. . 3
setvar 𝑔 |
3 | | cvv 3431 |
. . 3
class
V |
4 | | va |
. . . . . . . . . 10
setvar 𝑎 |
5 | 4 | cv 1541 |
. . . . . . . . 9
class 𝑎 |
6 | | vp |
. . . . . . . . . . 11
setvar 𝑝 |
7 | 6 | cv 1541 |
. . . . . . . . . 10
class 𝑝 |
8 | | cc0 10872 |
. . . . . . . . . . 11
class
0 |
9 | | c3 12029 |
. . . . . . . . . . 11
class
3 |
10 | | cfzo 13381 |
. . . . . . . . . . 11
class
..^ |
11 | 8, 9, 10 | co 7271 |
. . . . . . . . . 10
class
(0..^3) |
12 | | cmap 8598 |
. . . . . . . . . 10
class
↑m |
13 | 7, 11, 12 | co 7271 |
. . . . . . . . 9
class (𝑝 ↑m
(0..^3)) |
14 | 5, 13 | wcel 2110 |
. . . . . . . 8
wff 𝑎 ∈ (𝑝 ↑m (0..^3)) |
15 | | vb |
. . . . . . . . . 10
setvar 𝑏 |
16 | 15 | cv 1541 |
. . . . . . . . 9
class 𝑏 |
17 | 16, 13 | wcel 2110 |
. . . . . . . 8
wff 𝑏 ∈ (𝑝 ↑m (0..^3)) |
18 | 14, 17 | wa 396 |
. . . . . . 7
wff (𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m
(0..^3))) |
19 | | vx |
. . . . . . . . . . . . 13
setvar 𝑥 |
20 | 19 | cv 1541 |
. . . . . . . . . . . 12
class 𝑥 |
21 | | c1 10873 |
. . . . . . . . . . . . 13
class
1 |
22 | 21, 16 | cfv 6432 |
. . . . . . . . . . . 12
class (𝑏‘1) |
23 | | vy |
. . . . . . . . . . . . 13
setvar 𝑦 |
24 | 23 | cv 1541 |
. . . . . . . . . . . 12
class 𝑦 |
25 | 20, 22, 24 | cs3 14553 |
. . . . . . . . . . 11
class
〈“𝑥(𝑏‘1)𝑦”〉 |
26 | 2 | cv 1541 |
. . . . . . . . . . . 12
class 𝑔 |
27 | | ccgrg 26869 |
. . . . . . . . . . . 12
class
cgrG |
28 | 26, 27 | cfv 6432 |
. . . . . . . . . . 11
class
(cgrG‘𝑔) |
29 | 5, 25, 28 | wbr 5079 |
. . . . . . . . . 10
wff 𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 |
30 | 8, 16 | cfv 6432 |
. . . . . . . . . . 11
class (𝑏‘0) |
31 | | vk |
. . . . . . . . . . . . 13
setvar 𝑘 |
32 | 31 | cv 1541 |
. . . . . . . . . . . 12
class 𝑘 |
33 | 22, 32 | cfv 6432 |
. . . . . . . . . . 11
class (𝑘‘(𝑏‘1)) |
34 | 20, 30, 33 | wbr 5079 |
. . . . . . . . . 10
wff 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) |
35 | | c2 12028 |
. . . . . . . . . . . 12
class
2 |
36 | 35, 16 | cfv 6432 |
. . . . . . . . . . 11
class (𝑏‘2) |
37 | 24, 36, 33 | wbr 5079 |
. . . . . . . . . 10
wff 𝑦(𝑘‘(𝑏‘1))(𝑏‘2) |
38 | 29, 34, 37 | w3a 1086 |
. . . . . . . . 9
wff (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)) |
39 | 38, 23, 7 | wrex 3067 |
. . . . . . . 8
wff
∃𝑦 ∈
𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)) |
40 | 39, 19, 7 | wrex 3067 |
. . . . . . 7
wff
∃𝑥 ∈
𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)) |
41 | 18, 40 | wa 396 |
. . . . . 6
wff ((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2))) |
42 | | chlg 26959 |
. . . . . . 7
class
hlG |
43 | 26, 42 | cfv 6432 |
. . . . . 6
class
(hlG‘𝑔) |
44 | 41, 31, 43 | wsbc 3720 |
. . . . 5
wff
[(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2))) |
45 | | cbs 16910 |
. . . . . 6
class
Base |
46 | 26, 45 | cfv 6432 |
. . . . 5
class
(Base‘𝑔) |
47 | 44, 6, 46 | wsbc 3720 |
. . . 4
wff
[(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2))) |
48 | 47, 4, 15 | copab 5141 |
. . 3
class
{〈𝑎, 𝑏〉 ∣
[(Base‘𝑔) /
𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))} |
49 | 2, 3, 48 | cmpt 5162 |
. 2
class (𝑔 ∈ V ↦ {〈𝑎, 𝑏〉 ∣ [(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))}) |
50 | 1, 49 | wceq 1542 |
1
wff cgrA =
(𝑔 ∈ V ↦
{〈𝑎, 𝑏〉 ∣
[(Base‘𝑔) /
𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))}) |