Step | Hyp | Ref
| Expression |
1 | | df-nbgra 25949 |
. . 3
⊢
Neighbors = (𝑥 ∈ V,
𝑦 ∈ (1st
‘𝑥) ↦ {𝑛 ∈ (1st
‘𝑥) ∣ {𝑦, 𝑛} ∈ ran (2nd ‘𝑥)}) |
2 | 1 | mpt2xopoveq 7232 |
. 2
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → (〈𝑉, 𝐸〉 Neighbors 𝑁) = {𝑛 ∈ 𝑉 ∣ [〈𝑉, 𝐸〉 / 𝑥][𝑁 / 𝑦]{𝑦, 𝑛} ∈ ran (2nd ‘𝑥)}) |
3 | | sbcel1g 3939 |
. . . . . 6
⊢ (𝑁 ∈ 𝑉 → ([𝑁 / 𝑦]{𝑦, 𝑛} ∈ ran (2nd ‘𝑥) ↔ ⦋𝑁 / 𝑦⦌{𝑦, 𝑛} ∈ ran (2nd ‘𝑥))) |
4 | 3 | adantl 481 |
. . . . 5
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → ([𝑁 / 𝑦]{𝑦, 𝑛} ∈ ran (2nd ‘𝑥) ↔ ⦋𝑁 / 𝑦⦌{𝑦, 𝑛} ∈ ran (2nd ‘𝑥))) |
5 | 4 | sbcbidv 3457 |
. . . 4
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → ([〈𝑉, 𝐸〉 / 𝑥][𝑁 / 𝑦]{𝑦, 𝑛} ∈ ran (2nd ‘𝑥) ↔ [〈𝑉, 𝐸〉 / 𝑥]⦋𝑁 / 𝑦⦌{𝑦, 𝑛} ∈ ran (2nd ‘𝑥))) |
6 | | sbcel2 3941 |
. . . . 5
⊢
([〈𝑉,
𝐸〉 / 𝑥]⦋𝑁 / 𝑦⦌{𝑦, 𝑛} ∈ ran (2nd ‘𝑥) ↔ ⦋𝑁 / 𝑦⦌{𝑦, 𝑛} ∈ ⦋〈𝑉, 𝐸〉 / 𝑥⦌ran (2nd
‘𝑥)) |
7 | 6 | a1i 11 |
. . . 4
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → ([〈𝑉, 𝐸〉 / 𝑥]⦋𝑁 / 𝑦⦌{𝑦, 𝑛} ∈ ran (2nd ‘𝑥) ↔ ⦋𝑁 / 𝑦⦌{𝑦, 𝑛} ∈ ⦋〈𝑉, 𝐸〉 / 𝑥⦌ran (2nd
‘𝑥))) |
8 | | df-pr 4128 |
. . . . . . . 8
⊢ {𝑦, 𝑛} = ({𝑦} ∪ {𝑛}) |
9 | 8 | a1i 11 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → {𝑦, 𝑛} = ({𝑦} ∪ {𝑛})) |
10 | 9 | csbeq2dv 3944 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → ⦋𝑁 / 𝑦⦌{𝑦, 𝑛} = ⦋𝑁 / 𝑦⦌({𝑦} ∪ {𝑛})) |
11 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑦({𝑁} ∪ {𝑛}) |
12 | 11 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ 𝑉 → Ⅎ𝑦({𝑁} ∪ {𝑛})) |
13 | | sneq 4135 |
. . . . . . . . 9
⊢ (𝑦 = 𝑁 → {𝑦} = {𝑁}) |
14 | 13 | uneq1d 3728 |
. . . . . . . 8
⊢ (𝑦 = 𝑁 → ({𝑦} ∪ {𝑛}) = ({𝑁} ∪ {𝑛})) |
15 | 12, 14 | csbiegf 3523 |
. . . . . . 7
⊢ (𝑁 ∈ 𝑉 → ⦋𝑁 / 𝑦⦌({𝑦} ∪ {𝑛}) = ({𝑁} ∪ {𝑛})) |
16 | 15 | adantl 481 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → ⦋𝑁 / 𝑦⦌({𝑦} ∪ {𝑛}) = ({𝑁} ∪ {𝑛})) |
17 | | df-pr 4128 |
. . . . . . . 8
⊢ {𝑁, 𝑛} = ({𝑁} ∪ {𝑛}) |
18 | 17 | eqcomi 2619 |
. . . . . . 7
⊢ ({𝑁} ∪ {𝑛}) = {𝑁, 𝑛} |
19 | 18 | a1i 11 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → ({𝑁} ∪ {𝑛}) = {𝑁, 𝑛}) |
20 | 10, 16, 19 | 3eqtrd 2648 |
. . . . 5
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → ⦋𝑁 / 𝑦⦌{𝑦, 𝑛} = {𝑁, 𝑛}) |
21 | | csbrn 5514 |
. . . . . . 7
⊢
⦋〈𝑉, 𝐸〉 / 𝑥⦌ran (2nd
‘𝑥) = ran
⦋〈𝑉,
𝐸〉 / 𝑥⦌(2nd
‘𝑥) |
22 | 21 | a1i 11 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → ⦋〈𝑉, 𝐸〉 / 𝑥⦌ran (2nd
‘𝑥) = ran
⦋〈𝑉,
𝐸〉 / 𝑥⦌(2nd
‘𝑥)) |
23 | | opex 4859 |
. . . . . . . . 9
⊢
〈𝑉, 𝐸〉 ∈ V |
24 | | csbfv2g 6142 |
. . . . . . . . 9
⊢
(〈𝑉, 𝐸〉 ∈ V →
⦋〈𝑉,
𝐸〉 / 𝑥⦌(2nd
‘𝑥) = (2nd
‘⦋〈𝑉, 𝐸〉 / 𝑥⦌𝑥)) |
25 | 23, 24 | mp1i 13 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → ⦋〈𝑉, 𝐸〉 / 𝑥⦌(2nd ‘𝑥) = (2nd
‘⦋〈𝑉, 𝐸〉 / 𝑥⦌𝑥)) |
26 | | csbvarg 3955 |
. . . . . . . . . 10
⊢
(〈𝑉, 𝐸〉 ∈ V →
⦋〈𝑉,
𝐸〉 / 𝑥⦌𝑥 = 〈𝑉, 𝐸〉) |
27 | 23, 26 | mp1i 13 |
. . . . . . . . 9
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → ⦋〈𝑉, 𝐸〉 / 𝑥⦌𝑥 = 〈𝑉, 𝐸〉) |
28 | 27 | fveq2d 6107 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → (2nd
‘⦋〈𝑉, 𝐸〉 / 𝑥⦌𝑥) = (2nd ‘〈𝑉, 𝐸〉)) |
29 | | op2ndg 7072 |
. . . . . . . . 9
⊢ ((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) → (2nd ‘〈𝑉, 𝐸〉) = 𝐸) |
30 | 29 | adantr 480 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → (2nd ‘〈𝑉, 𝐸〉) = 𝐸) |
31 | 25, 28, 30 | 3eqtrd 2648 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → ⦋〈𝑉, 𝐸〉 / 𝑥⦌(2nd ‘𝑥) = 𝐸) |
32 | 31 | rneqd 5274 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → ran ⦋〈𝑉, 𝐸〉 / 𝑥⦌(2nd ‘𝑥) = ran 𝐸) |
33 | 22, 32 | eqtrd 2644 |
. . . . 5
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → ⦋〈𝑉, 𝐸〉 / 𝑥⦌ran (2nd
‘𝑥) = ran 𝐸) |
34 | 20, 33 | eleq12d 2682 |
. . . 4
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → (⦋𝑁 / 𝑦⦌{𝑦, 𝑛} ∈ ⦋〈𝑉, 𝐸〉 / 𝑥⦌ran (2nd
‘𝑥) ↔ {𝑁, 𝑛} ∈ ran 𝐸)) |
35 | 5, 7, 34 | 3bitrd 293 |
. . 3
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → ([〈𝑉, 𝐸〉 / 𝑥][𝑁 / 𝑦]{𝑦, 𝑛} ∈ ran (2nd ‘𝑥) ↔ {𝑁, 𝑛} ∈ ran 𝐸)) |
36 | 35 | rabbidv 3164 |
. 2
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → {𝑛 ∈ 𝑉 ∣ [〈𝑉, 𝐸〉 / 𝑥][𝑁 / 𝑦]{𝑦, 𝑛} ∈ ran (2nd ‘𝑥)} = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸}) |
37 | 2, 36 | eqtrd 2644 |
1
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → (〈𝑉, 𝐸〉 Neighbors 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸}) |