| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-clnbgr 47806 | . 2
⊢ 
ClNeighbVtx = (𝑔 ∈ V,
𝑣 ∈ (Vtx‘𝑔) ↦ ({𝑣} ∪ {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒})) | 
| 2 |  | clnbgrval.v | . . . 4
⊢ 𝑉 = (Vtx‘𝐺) | 
| 3 | 2 | 1vgrex 29019 | . . 3
⊢ (𝑁 ∈ 𝑉 → 𝐺 ∈ V) | 
| 4 |  | fveq2 6906 | . . . . . . 7
⊢ (𝐺 = 𝑔 → (Vtx‘𝐺) = (Vtx‘𝑔)) | 
| 5 | 4 | eqcoms 2745 | . . . . . 6
⊢ (𝑔 = 𝐺 → (Vtx‘𝐺) = (Vtx‘𝑔)) | 
| 6 | 2, 5 | eqtrid 2789 | . . . . 5
⊢ (𝑔 = 𝐺 → 𝑉 = (Vtx‘𝑔)) | 
| 7 | 6 | eleq2d 2827 | . . . 4
⊢ (𝑔 = 𝐺 → (𝑁 ∈ 𝑉 ↔ 𝑁 ∈ (Vtx‘𝑔))) | 
| 8 | 7 | biimpac 478 | . . 3
⊢ ((𝑁 ∈ 𝑉 ∧ 𝑔 = 𝐺) → 𝑁 ∈ (Vtx‘𝑔)) | 
| 9 |  | vsnex 5434 | . . . . 5
⊢ {𝑣} ∈ V | 
| 10 | 9 | a1i 11 | . . . 4
⊢ ((𝑁 ∈ 𝑉 ∧ (𝑔 = 𝐺 ∧ 𝑣 = 𝑁)) → {𝑣} ∈ V) | 
| 11 |  | fvex 6919 | . . . . 5
⊢
(Vtx‘𝑔) ∈
V | 
| 12 |  | rabexg 5337 | . . . . 5
⊢
((Vtx‘𝑔)
∈ V → {𝑛 ∈
(Vtx‘𝑔) ∣
∃𝑒 ∈
(Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒} ∈ V) | 
| 13 | 11, 12 | mp1i 13 | . . . 4
⊢ ((𝑁 ∈ 𝑉 ∧ (𝑔 = 𝐺 ∧ 𝑣 = 𝑁)) → {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒} ∈ V) | 
| 14 | 10, 13 | unexd 7774 | . . 3
⊢ ((𝑁 ∈ 𝑉 ∧ (𝑔 = 𝐺 ∧ 𝑣 = 𝑁)) → ({𝑣} ∪ {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒}) ∈ V) | 
| 15 |  | sneq 4636 | . . . . . 6
⊢ (𝑣 = 𝑁 → {𝑣} = {𝑁}) | 
| 16 | 15 | adantl 481 | . . . . 5
⊢ ((𝑔 = 𝐺 ∧ 𝑣 = 𝑁) → {𝑣} = {𝑁}) | 
| 17 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = (Vtx‘𝐺)) | 
| 18 | 17, 2 | eqtr4di 2795 | . . . . . . 7
⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = 𝑉) | 
| 19 | 18 | adantr 480 | . . . . . 6
⊢ ((𝑔 = 𝐺 ∧ 𝑣 = 𝑁) → (Vtx‘𝑔) = 𝑉) | 
| 20 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑔 = 𝐺 → (Edg‘𝑔) = (Edg‘𝐺)) | 
| 21 |  | clnbgrval.e | . . . . . . . . 9
⊢ 𝐸 = (Edg‘𝐺) | 
| 22 | 20, 21 | eqtr4di 2795 | . . . . . . . 8
⊢ (𝑔 = 𝐺 → (Edg‘𝑔) = 𝐸) | 
| 23 | 22 | adantr 480 | . . . . . . 7
⊢ ((𝑔 = 𝐺 ∧ 𝑣 = 𝑁) → (Edg‘𝑔) = 𝐸) | 
| 24 |  | preq1 4733 | . . . . . . . . 9
⊢ (𝑣 = 𝑁 → {𝑣, 𝑛} = {𝑁, 𝑛}) | 
| 25 | 24 | sseq1d 4015 | . . . . . . . 8
⊢ (𝑣 = 𝑁 → ({𝑣, 𝑛} ⊆ 𝑒 ↔ {𝑁, 𝑛} ⊆ 𝑒)) | 
| 26 | 25 | adantl 481 | . . . . . . 7
⊢ ((𝑔 = 𝐺 ∧ 𝑣 = 𝑁) → ({𝑣, 𝑛} ⊆ 𝑒 ↔ {𝑁, 𝑛} ⊆ 𝑒)) | 
| 27 | 23, 26 | rexeqbidv 3347 | . . . . . 6
⊢ ((𝑔 = 𝐺 ∧ 𝑣 = 𝑁) → (∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒 ↔ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒)) | 
| 28 | 19, 27 | rabeqbidv 3455 | . . . . 5
⊢ ((𝑔 = 𝐺 ∧ 𝑣 = 𝑁) → {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒} = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}) | 
| 29 | 16, 28 | uneq12d 4169 | . . . 4
⊢ ((𝑔 = 𝐺 ∧ 𝑣 = 𝑁) → ({𝑣} ∪ {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒}) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒})) | 
| 30 | 29 | adantl 481 | . . 3
⊢ ((𝑁 ∈ 𝑉 ∧ (𝑔 = 𝐺 ∧ 𝑣 = 𝑁)) → ({𝑣} ∪ {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒}) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒})) | 
| 31 | 3, 8, 14, 30 | ovmpodv2 7591 | . 2
⊢ (𝑁 ∈ 𝑉 → ( ClNeighbVtx = (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ ({𝑣} ∪ {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒})) → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}))) | 
| 32 | 1, 31 | mpi 20 | 1
⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒})) |