Step | Hyp | Ref
| Expression |
1 | | df-nbgra 25949 |
. 2
⊢
Neighbors = (𝑔 ∈ V,
𝑘 ∈ (1st
‘𝑔) ↦ {𝑛 ∈ (1st
‘𝑔) ∣ {𝑘, 𝑛} ∈ ran (2nd ‘𝑔)}) |
2 | | opex 4859 |
. . . 4
⊢
〈𝑉, 𝐸〉 ∈ V |
3 | 2 | a1i 11 |
. . 3
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → 〈𝑉, 𝐸〉 ∈ V) |
4 | | op1stg 7071 |
. . . . . . . 8
⊢ ((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) → (1st ‘〈𝑉, 𝐸〉) = 𝑉) |
5 | 4 | eqcomd 2616 |
. . . . . . 7
⊢ ((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) → 𝑉 = (1st ‘〈𝑉, 𝐸〉)) |
6 | 5 | eleq2d 2673 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) → (𝑁 ∈ 𝑉 ↔ 𝑁 ∈ (1st ‘〈𝑉, 𝐸〉))) |
7 | 6 | biimpa 500 |
. . . . 5
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → 𝑁 ∈ (1st ‘〈𝑉, 𝐸〉)) |
8 | 7 | adantr 480 |
. . . 4
⊢ ((((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) ∧ 𝑔 = 〈𝑉, 𝐸〉) → 𝑁 ∈ (1st ‘〈𝑉, 𝐸〉)) |
9 | | fveq2 6103 |
. . . . 5
⊢ (𝑔 = 〈𝑉, 𝐸〉 → (1st ‘𝑔) = (1st
‘〈𝑉, 𝐸〉)) |
10 | 9 | adantl 481 |
. . . 4
⊢ ((((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) ∧ 𝑔 = 〈𝑉, 𝐸〉) → (1st ‘𝑔) = (1st
‘〈𝑉, 𝐸〉)) |
11 | 8, 10 | eleqtrrd 2691 |
. . 3
⊢ ((((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) ∧ 𝑔 = 〈𝑉, 𝐸〉) → 𝑁 ∈ (1st ‘𝑔)) |
12 | | fvex 6113 |
. . . 4
⊢
(1st ‘𝑔) ∈ V |
13 | | rabexg 4739 |
. . . 4
⊢
((1st ‘𝑔) ∈ V → {𝑛 ∈ (1st ‘𝑔) ∣ {𝑘, 𝑛} ∈ ran (2nd ‘𝑔)} ∈ V) |
14 | 12, 13 | mp1i 13 |
. . 3
⊢ ((((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) ∧ (𝑔 = 〈𝑉, 𝐸〉 ∧ 𝑘 = 𝑁)) → {𝑛 ∈ (1st ‘𝑔) ∣ {𝑘, 𝑛} ∈ ran (2nd ‘𝑔)} ∈ V) |
15 | 9, 4 | sylan9eq 2664 |
. . . . . . . . 9
⊢ ((𝑔 = 〈𝑉, 𝐸〉 ∧ (𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍)) → (1st ‘𝑔) = 𝑉) |
16 | 15 | ex 449 |
. . . . . . . 8
⊢ (𝑔 = 〈𝑉, 𝐸〉 → ((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) → (1st ‘𝑔) = 𝑉)) |
17 | 16 | adantr 480 |
. . . . . . 7
⊢ ((𝑔 = 〈𝑉, 𝐸〉 ∧ 𝑘 = 𝑁) → ((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) → (1st ‘𝑔) = 𝑉)) |
18 | 17 | com12 32 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) → ((𝑔 = 〈𝑉, 𝐸〉 ∧ 𝑘 = 𝑁) → (1st ‘𝑔) = 𝑉)) |
19 | 18 | adantr 480 |
. . . . 5
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → ((𝑔 = 〈𝑉, 𝐸〉 ∧ 𝑘 = 𝑁) → (1st ‘𝑔) = 𝑉)) |
20 | 19 | imp 444 |
. . . 4
⊢ ((((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) ∧ (𝑔 = 〈𝑉, 𝐸〉 ∧ 𝑘 = 𝑁)) → (1st ‘𝑔) = 𝑉) |
21 | | preq1 4212 |
. . . . . . 7
⊢ (𝑘 = 𝑁 → {𝑘, 𝑛} = {𝑁, 𝑛}) |
22 | 21 | adantl 481 |
. . . . . 6
⊢ ((𝑔 = 〈𝑉, 𝐸〉 ∧ 𝑘 = 𝑁) → {𝑘, 𝑛} = {𝑁, 𝑛}) |
23 | 22 | adantl 481 |
. . . . 5
⊢ ((((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) ∧ (𝑔 = 〈𝑉, 𝐸〉 ∧ 𝑘 = 𝑁)) → {𝑘, 𝑛} = {𝑁, 𝑛}) |
24 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑔 = 〈𝑉, 𝐸〉 → (2nd ‘𝑔) = (2nd
‘〈𝑉, 𝐸〉)) |
25 | | op2ndg 7072 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) → (2nd ‘〈𝑉, 𝐸〉) = 𝐸) |
26 | 24, 25 | sylan9eq 2664 |
. . . . . . . . . . 11
⊢ ((𝑔 = 〈𝑉, 𝐸〉 ∧ (𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍)) → (2nd ‘𝑔) = 𝐸) |
27 | 26 | ex 449 |
. . . . . . . . . 10
⊢ (𝑔 = 〈𝑉, 𝐸〉 → ((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) → (2nd ‘𝑔) = 𝐸)) |
28 | 27 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑔 = 〈𝑉, 𝐸〉 ∧ 𝑘 = 𝑁) → ((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) → (2nd ‘𝑔) = 𝐸)) |
29 | 28 | com12 32 |
. . . . . . . 8
⊢ ((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) → ((𝑔 = 〈𝑉, 𝐸〉 ∧ 𝑘 = 𝑁) → (2nd ‘𝑔) = 𝐸)) |
30 | 29 | adantr 480 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → ((𝑔 = 〈𝑉, 𝐸〉 ∧ 𝑘 = 𝑁) → (2nd ‘𝑔) = 𝐸)) |
31 | 30 | imp 444 |
. . . . . 6
⊢ ((((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) ∧ (𝑔 = 〈𝑉, 𝐸〉 ∧ 𝑘 = 𝑁)) → (2nd ‘𝑔) = 𝐸) |
32 | 31 | rneqd 5274 |
. . . . 5
⊢ ((((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) ∧ (𝑔 = 〈𝑉, 𝐸〉 ∧ 𝑘 = 𝑁)) → ran (2nd ‘𝑔) = ran 𝐸) |
33 | 23, 32 | eleq12d 2682 |
. . . 4
⊢ ((((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) ∧ (𝑔 = 〈𝑉, 𝐸〉 ∧ 𝑘 = 𝑁)) → ({𝑘, 𝑛} ∈ ran (2nd ‘𝑔) ↔ {𝑁, 𝑛} ∈ ran 𝐸)) |
34 | 20, 33 | rabeqbidv 3168 |
. . 3
⊢ ((((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) ∧ (𝑔 = 〈𝑉, 𝐸〉 ∧ 𝑘 = 𝑁)) → {𝑛 ∈ (1st ‘𝑔) ∣ {𝑘, 𝑛} ∈ ran (2nd ‘𝑔)} = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸}) |
35 | 3, 11, 14, 34 | ovmpt2dv2 6692 |
. 2
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → ( Neighbors = (𝑔 ∈ V, 𝑘 ∈ (1st ‘𝑔) ↦ {𝑛 ∈ (1st ‘𝑔) ∣ {𝑘, 𝑛} ∈ ran (2nd ‘𝑔)}) → (〈𝑉, 𝐸〉 Neighbors 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸})) |
36 | 1, 35 | mpi 20 |
1
⊢ (((𝑉 ∈ 𝑌 ∧ 𝐸 ∈ 𝑍) ∧ 𝑁 ∈ 𝑉) → (〈𝑉, 𝐸〉 Neighbors 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ ran 𝐸}) |