Step | Hyp | Ref
| Expression |
1 | | cnbgra 25712 |
. 2
class
Neighbors |
2 | | vg |
. . 3
setvar 𝑔 |
3 | | vk |
. . 3
setvar 𝑘 |
4 | | cvv 3172 |
. . 3
class
V |
5 | 2 | cv 1473 |
. . . 4
class 𝑔 |
6 | | c1st 7034 |
. . . 4
class
1^{st} |
7 | 5, 6 | cfv 5790 |
. . 3
class
(1^{st} ‘𝑔) |
8 | 3 | cv 1473 |
. . . . . 6
class 𝑘 |
9 | | vn |
. . . . . . 7
setvar 𝑛 |
10 | 9 | cv 1473 |
. . . . . 6
class 𝑛 |
11 | 8, 10 | cpr 4126 |
. . . . 5
class {𝑘, 𝑛} |
12 | | c2nd 7035 |
. . . . . . 7
class
2^{nd} |
13 | 5, 12 | cfv 5790 |
. . . . . 6
class
(2^{nd} ‘𝑔) |
14 | 13 | crn 5029 |
. . . . 5
class ran
(2^{nd} ‘𝑔) |
15 | 11, 14 | wcel 1976 |
. . . 4
wff {𝑘, 𝑛} ∈ ran (2^{nd} ‘𝑔) |
16 | 15, 9, 7 | crab 2899 |
. . 3
class {𝑛 ∈ (1^{st}
‘𝑔) ∣ {𝑘, 𝑛} ∈ ran (2^{nd} ‘𝑔)} |
17 | 2, 3, 4, 7, 16 | cmpt2 6529 |
. 2
class (𝑔 ∈ V, 𝑘 ∈ (1^{st} ‘𝑔) ↦ {𝑛 ∈ (1^{st} ‘𝑔) ∣ {𝑘, 𝑛} ∈ ran (2^{nd} ‘𝑔)}) |
18 | 1, 17 | wceq 1474 |
1
wff Neighbors
= (𝑔 ∈ V, 𝑘 ∈ (1^{st}
‘𝑔) ↦ {𝑛 ∈ (1^{st}
‘𝑔) ∣ {𝑘, 𝑛} ∈ ran (2^{nd} ‘𝑔)}) |