Step | Hyp | Ref
| Expression |
1 | | ccgra 27791 |
. 2
class
cgrA |
2 | | vg |
. . 3
setvar 𝑔 |
3 | | cvv 3448 |
. . 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 11058 |
. . . . . . . . . . 11
class
0 |
9 | | c3 12216 |
. . . . . . . . . . 11
class
3 |
10 | | cfzo 13574 |
. . . . . . . . . . 11
class
..^ |
11 | 8, 9, 10 | co 7362 |
. . . . . . . . . 10
class
(0..^3) |
12 | | cmap 8772 |
. . . . . . . . . 10
class
↑m |
13 | 7, 11, 12 | co 7362 |
. . . . . . . . 9
class (𝑝 ↑m
(0..^3)) |
14 | 5, 13 | wcel 2107 |
. . . . . . . 8
wff 𝑎 ∈ (𝑝 ↑m (0..^3)) |
15 | | vb |
. . . . . . . . . 10
setvar 𝑏 |
16 | 15 | cv 1541 |
. . . . . . . . 9
class 𝑏 |
17 | 16, 13 | wcel 2107 |
. . . . . . . 8
wff 𝑏 ∈ (𝑝 ↑m (0..^3)) |
18 | 14, 17 | wa 397 |
. . . . . . 7
wff (𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m
(0..^3))) |
19 | | vx |
. . . . . . . . . . . . 13
setvar 𝑥 |
20 | 19 | cv 1541 |
. . . . . . . . . . . 12
class 𝑥 |
21 | | c1 11059 |
. . . . . . . . . . . . 13
class
1 |
22 | 21, 16 | cfv 6501 |
. . . . . . . . . . . 12
class (𝑏‘1) |
23 | | vy |
. . . . . . . . . . . . 13
setvar 𝑦 |
24 | 23 | cv 1541 |
. . . . . . . . . . . 12
class 𝑦 |
25 | 20, 22, 24 | cs3 14738 |
. . . . . . . . . . 11
class
⟨“𝑥(𝑏‘1)𝑦”⟩ |
26 | 2 | cv 1541 |
. . . . . . . . . . . 12
class 𝑔 |
27 | | ccgrg 27494 |
. . . . . . . . . . . 12
class
cgrG |
28 | 26, 27 | cfv 6501 |
. . . . . . . . . . 11
class
(cgrG‘𝑔) |
29 | 5, 25, 28 | wbr 5110 |
. . . . . . . . . 10
wff 𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ |
30 | 8, 16 | cfv 6501 |
. . . . . . . . . . 11
class (𝑏‘0) |
31 | | vk |
. . . . . . . . . . . . 13
setvar 𝑘 |
32 | 31 | cv 1541 |
. . . . . . . . . . . 12
class 𝑘 |
33 | 22, 32 | cfv 6501 |
. . . . . . . . . . 11
class (𝑘‘(𝑏‘1)) |
34 | 20, 30, 33 | wbr 5110 |
. . . . . . . . . 10
wff 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) |
35 | | c2 12215 |
. . . . . . . . . . . 12
class
2 |
36 | 35, 16 | cfv 6501 |
. . . . . . . . . . 11
class (𝑏‘2) |
37 | 24, 36, 33 | wbr 5110 |
. . . . . . . . . 10
wff 𝑦(𝑘‘(𝑏‘1))(𝑏‘2) |
38 | 29, 34, 37 | w3a 1088 |
. . . . . . . . 9
wff (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)) |
39 | 38, 23, 7 | wrex 3074 |
. . . . . . . 8
wff
∃𝑦 ∈
𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)) |
40 | 39, 19, 7 | wrex 3074 |
. . . . . . 7
wff
∃𝑥 ∈
𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)) |
41 | 18, 40 | wa 397 |
. . . . . 6
wff ((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2))) |
42 | | chlg 27584 |
. . . . . . 7
class
hlG |
43 | 26, 42 | cfv 6501 |
. . . . . 6
class
(hlG‘𝑔) |
44 | 41, 31, 43 | wsbc 3744 |
. . . . 5
wff
[(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2))) |
45 | | cbs 17090 |
. . . . . 6
class
Base |
46 | 26, 45 | cfv 6501 |
. . . . 5
class
(Base‘𝑔) |
47 | 44, 6, 46 | wsbc 3744 |
. . . 4
wff
[(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2))) |
48 | 47, 4, 15 | copab 5172 |
. . 3
class
{⟨𝑎, 𝑏⟩ ∣
[(Base‘𝑔) /
𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)⟨“𝑥(𝑏‘1)𝑦”⟩ ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))} |
49 | 2, 3, 48 | cmpt 5193 |
. 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)))}) |