Step | Hyp | Ref
| Expression |
1 | | df-clnbgr 47693 |
. 2
⊢
ClNeighbVtx = (𝑔 ∈ V,
𝑣 ∈ (Vtx‘𝑔) ↦ ({𝑣} ∪ {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒})) |
2 | | clnbgrval.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
3 | 2 | 1vgrex 29037 |
. . 3
⊢ (𝑁 ∈ 𝑉 → 𝐺 ∈ V) |
4 | | fveq2 6920 |
. . . . . . 7
⊢ (𝐺 = 𝑔 → (Vtx‘𝐺) = (Vtx‘𝑔)) |
5 | 4 | eqcoms 2748 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (Vtx‘𝐺) = (Vtx‘𝑔)) |
6 | 2, 5 | eqtrid 2792 |
. . . . 5
⊢ (𝑔 = 𝐺 → 𝑉 = (Vtx‘𝑔)) |
7 | 6 | eleq2d 2830 |
. . . 4
⊢ (𝑔 = 𝐺 → (𝑁 ∈ 𝑉 ↔ 𝑁 ∈ (Vtx‘𝑔))) |
8 | 7 | biimpac 478 |
. . 3
⊢ ((𝑁 ∈ 𝑉 ∧ 𝑔 = 𝐺) → 𝑁 ∈ (Vtx‘𝑔)) |
9 | | vsnex 5449 |
. . . . 5
⊢ {𝑣} ∈ V |
10 | 9 | a1i 11 |
. . . 4
⊢ ((𝑁 ∈ 𝑉 ∧ (𝑔 = 𝐺 ∧ 𝑣 = 𝑁)) → {𝑣} ∈ V) |
11 | | fvex 6933 |
. . . . 5
⊢
(Vtx‘𝑔) ∈
V |
12 | | rabexg 5355 |
. . . . 5
⊢
((Vtx‘𝑔)
∈ V → {𝑛 ∈
(Vtx‘𝑔) ∣
∃𝑒 ∈
(Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒} ∈ V) |
13 | 11, 12 | mp1i 13 |
. . . 4
⊢ ((𝑁 ∈ 𝑉 ∧ (𝑔 = 𝐺 ∧ 𝑣 = 𝑁)) → {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒} ∈ V) |
14 | 10, 13 | unexd 7789 |
. . 3
⊢ ((𝑁 ∈ 𝑉 ∧ (𝑔 = 𝐺 ∧ 𝑣 = 𝑁)) → ({𝑣} ∪ {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒}) ∈ V) |
15 | | sneq 4658 |
. . . . . 6
⊢ (𝑣 = 𝑁 → {𝑣} = {𝑁}) |
16 | 15 | adantl 481 |
. . . . 5
⊢ ((𝑔 = 𝐺 ∧ 𝑣 = 𝑁) → {𝑣} = {𝑁}) |
17 | | fveq2 6920 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = (Vtx‘𝐺)) |
18 | 17, 2 | eqtr4di 2798 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = 𝑉) |
19 | 18 | adantr 480 |
. . . . . 6
⊢ ((𝑔 = 𝐺 ∧ 𝑣 = 𝑁) → (Vtx‘𝑔) = 𝑉) |
20 | | fveq2 6920 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (Edg‘𝑔) = (Edg‘𝐺)) |
21 | | clnbgrval.e |
. . . . . . . . 9
⊢ 𝐸 = (Edg‘𝐺) |
22 | 20, 21 | eqtr4di 2798 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (Edg‘𝑔) = 𝐸) |
23 | 22 | adantr 480 |
. . . . . . 7
⊢ ((𝑔 = 𝐺 ∧ 𝑣 = 𝑁) → (Edg‘𝑔) = 𝐸) |
24 | | preq1 4758 |
. . . . . . . . 9
⊢ (𝑣 = 𝑁 → {𝑣, 𝑛} = {𝑁, 𝑛}) |
25 | 24 | sseq1d 4040 |
. . . . . . . 8
⊢ (𝑣 = 𝑁 → ({𝑣, 𝑛} ⊆ 𝑒 ↔ {𝑁, 𝑛} ⊆ 𝑒)) |
26 | 25 | adantl 481 |
. . . . . . 7
⊢ ((𝑔 = 𝐺 ∧ 𝑣 = 𝑁) → ({𝑣, 𝑛} ⊆ 𝑒 ↔ {𝑁, 𝑛} ⊆ 𝑒)) |
27 | 23, 26 | rexeqbidv 3355 |
. . . . . 6
⊢ ((𝑔 = 𝐺 ∧ 𝑣 = 𝑁) → (∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒 ↔ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒)) |
28 | 19, 27 | rabeqbidv 3462 |
. . . . 5
⊢ ((𝑔 = 𝐺 ∧ 𝑣 = 𝑁) → {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒} = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}) |
29 | 16, 28 | uneq12d 4192 |
. . . 4
⊢ ((𝑔 = 𝐺 ∧ 𝑣 = 𝑁) → ({𝑣} ∪ {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒}) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒})) |
30 | 29 | adantl 481 |
. . 3
⊢ ((𝑁 ∈ 𝑉 ∧ (𝑔 = 𝐺 ∧ 𝑣 = 𝑁)) → ({𝑣} ∪ {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒}) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒})) |
31 | 3, 8, 14, 30 | ovmpodv2 7608 |
. 2
⊢ (𝑁 ∈ 𝑉 → ( ClNeighbVtx = (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ ({𝑣} ∪ {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒})) → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}))) |
32 | 1, 31 | mpi 20 |
1
⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒})) |