| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-nbgr 29350 | . 2
⊢ 
NeighbVtx = (𝑔 ∈ V,
𝑘 ∈ (Vtx‘𝑔) ↦ {𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑘}) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑘, 𝑛} ⊆ 𝑒}) | 
| 2 |  | nbgrval.v | . . . 4
⊢ 𝑉 = (Vtx‘𝐺) | 
| 3 | 2 | 1vgrex 29019 | . . 3
⊢ (𝑁 ∈ 𝑉 → 𝐺 ∈ V) | 
| 4 |  | fveq2 6906 | . . . . . 6
⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = (Vtx‘𝐺)) | 
| 5 | 2, 4 | eqtr4id 2796 | . . . . 5
⊢ (𝑔 = 𝐺 → 𝑉 = (Vtx‘𝑔)) | 
| 6 | 5 | eleq2d 2827 | . . . 4
⊢ (𝑔 = 𝐺 → (𝑁 ∈ 𝑉 ↔ 𝑁 ∈ (Vtx‘𝑔))) | 
| 7 | 6 | biimpac 478 | . . 3
⊢ ((𝑁 ∈ 𝑉 ∧ 𝑔 = 𝐺) → 𝑁 ∈ (Vtx‘𝑔)) | 
| 8 |  | fvex 6919 | . . . . 5
⊢
(Vtx‘𝑔) ∈
V | 
| 9 | 8 | difexi 5330 | . . . 4
⊢
((Vtx‘𝑔)
∖ {𝑘}) ∈
V | 
| 10 |  | rabexg 5337 | . . . 4
⊢
(((Vtx‘𝑔)
∖ {𝑘}) ∈ V
→ {𝑛 ∈
((Vtx‘𝑔) ∖
{𝑘}) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑘, 𝑛} ⊆ 𝑒} ∈ V) | 
| 11 | 9, 10 | mp1i 13 | . . 3
⊢ ((𝑁 ∈ 𝑉 ∧ (𝑔 = 𝐺 ∧ 𝑘 = 𝑁)) → {𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑘}) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑘, 𝑛} ⊆ 𝑒} ∈ V) | 
| 12 | 4, 2 | eqtr4di 2795 | . . . . . . 7
⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = 𝑉) | 
| 13 | 12 | adantr 480 | . . . . . 6
⊢ ((𝑔 = 𝐺 ∧ 𝑘 = 𝑁) → (Vtx‘𝑔) = 𝑉) | 
| 14 |  | sneq 4636 | . . . . . . 7
⊢ (𝑘 = 𝑁 → {𝑘} = {𝑁}) | 
| 15 | 14 | adantl 481 | . . . . . 6
⊢ ((𝑔 = 𝐺 ∧ 𝑘 = 𝑁) → {𝑘} = {𝑁}) | 
| 16 | 13, 15 | difeq12d 4127 | . . . . 5
⊢ ((𝑔 = 𝐺 ∧ 𝑘 = 𝑁) → ((Vtx‘𝑔) ∖ {𝑘}) = (𝑉 ∖ {𝑁})) | 
| 17 | 16 | adantl 481 | . . . 4
⊢ ((𝑁 ∈ 𝑉 ∧ (𝑔 = 𝐺 ∧ 𝑘 = 𝑁)) → ((Vtx‘𝑔) ∖ {𝑘}) = (𝑉 ∖ {𝑁})) | 
| 18 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑔 = 𝐺 → (Edg‘𝑔) = (Edg‘𝐺)) | 
| 19 |  | nbgrval.e | . . . . . . . 8
⊢ 𝐸 = (Edg‘𝐺) | 
| 20 | 18, 19 | eqtr4di 2795 | . . . . . . 7
⊢ (𝑔 = 𝐺 → (Edg‘𝑔) = 𝐸) | 
| 21 | 20 | adantr 480 | . . . . . 6
⊢ ((𝑔 = 𝐺 ∧ 𝑘 = 𝑁) → (Edg‘𝑔) = 𝐸) | 
| 22 | 21 | adantl 481 | . . . . 5
⊢ ((𝑁 ∈ 𝑉 ∧ (𝑔 = 𝐺 ∧ 𝑘 = 𝑁)) → (Edg‘𝑔) = 𝐸) | 
| 23 |  | preq1 4733 | . . . . . . . 8
⊢ (𝑘 = 𝑁 → {𝑘, 𝑛} = {𝑁, 𝑛}) | 
| 24 | 23 | sseq1d 4015 | . . . . . . 7
⊢ (𝑘 = 𝑁 → ({𝑘, 𝑛} ⊆ 𝑒 ↔ {𝑁, 𝑛} ⊆ 𝑒)) | 
| 25 | 24 | adantl 481 | . . . . . 6
⊢ ((𝑔 = 𝐺 ∧ 𝑘 = 𝑁) → ({𝑘, 𝑛} ⊆ 𝑒 ↔ {𝑁, 𝑛} ⊆ 𝑒)) | 
| 26 | 25 | adantl 481 | . . . . 5
⊢ ((𝑁 ∈ 𝑉 ∧ (𝑔 = 𝐺 ∧ 𝑘 = 𝑁)) → ({𝑘, 𝑛} ⊆ 𝑒 ↔ {𝑁, 𝑛} ⊆ 𝑒)) | 
| 27 | 22, 26 | rexeqbidv 3347 | . . . 4
⊢ ((𝑁 ∈ 𝑉 ∧ (𝑔 = 𝐺 ∧ 𝑘 = 𝑁)) → (∃𝑒 ∈ (Edg‘𝑔){𝑘, 𝑛} ⊆ 𝑒 ↔ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒)) | 
| 28 | 17, 27 | rabeqbidv 3455 | . . 3
⊢ ((𝑁 ∈ 𝑉 ∧ (𝑔 = 𝐺 ∧ 𝑘 = 𝑁)) → {𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑘}) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑘, 𝑛} ⊆ 𝑒} = {𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}) | 
| 29 | 3, 7, 11, 28 | ovmpodv2 7591 | . 2
⊢ (𝑁 ∈ 𝑉 → ( NeighbVtx = (𝑔 ∈ V, 𝑘 ∈ (Vtx‘𝑔) ↦ {𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑘}) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑘, 𝑛} ⊆ 𝑒}) → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒})) | 
| 30 | 1, 29 | mpi 20 | 1
⊢ (𝑁 ∈ 𝑉 → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}) |