| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . . 6
⊢
(Vtx‘𝑆) =
(Vtx‘𝑆) |
| 2 | 1 | nbgrssovtx 29378 |
. . . . 5
⊢ (𝑆 NeighbVtx 𝐾) ⊆ ((Vtx‘𝑆) ∖ {𝐾}) |
| 3 | | difpr 4803 |
. . . . . 6
⊢ (𝑉 ∖ {𝑁, 𝐾}) = ((𝑉 ∖ {𝑁}) ∖ {𝐾}) |
| 4 | | nbupgruvtxres.v |
. . . . . . . . . 10
⊢ 𝑉 = (Vtx‘𝐺) |
| 5 | | nbupgruvtxres.e |
. . . . . . . . . 10
⊢ 𝐸 = (Edg‘𝐺) |
| 6 | | nbupgruvtxres.f |
. . . . . . . . . 10
⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} |
| 7 | | nbupgruvtxres.s |
. . . . . . . . . 10
⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 |
| 8 | 4, 5, 6, 7 | upgrres1lem2 29328 |
. . . . . . . . 9
⊢
(Vtx‘𝑆) =
(𝑉 ∖ {𝑁}) |
| 9 | 8 | eqcomi 2746 |
. . . . . . . 8
⊢ (𝑉 ∖ {𝑁}) = (Vtx‘𝑆) |
| 10 | 9 | a1i 11 |
. . . . . . 7
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) → (𝑉 ∖ {𝑁}) = (Vtx‘𝑆)) |
| 11 | 10 | difeq1d 4125 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) → ((𝑉 ∖ {𝑁}) ∖ {𝐾}) = ((Vtx‘𝑆) ∖ {𝐾})) |
| 12 | 3, 11 | eqtrid 2789 |
. . . . 5
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) → (𝑉 ∖ {𝑁, 𝐾}) = ((Vtx‘𝑆) ∖ {𝐾})) |
| 13 | 2, 12 | sseqtrrid 4027 |
. . . 4
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) → (𝑆 NeighbVtx 𝐾) ⊆ (𝑉 ∖ {𝑁, 𝐾})) |
| 14 | 13 | adantr 480 |
. . 3
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) → (𝑆 NeighbVtx 𝐾) ⊆ (𝑉 ∖ {𝑁, 𝐾})) |
| 15 | | simpl 482 |
. . . . . 6
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) → ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}))) |
| 16 | 15 | anim1i 615 |
. . . . 5
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑁 ∈
𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾})) → (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾}))) |
| 17 | | df-3an 1089 |
. . . . 5
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾})) ↔ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾}))) |
| 18 | 16, 17 | sylibr 234 |
. . . 4
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑁 ∈
𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾})) → ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾}))) |
| 19 | | dif32 4302 |
. . . . . . . . . . 11
⊢ ((𝑉 ∖ {𝑁}) ∖ {𝐾}) = ((𝑉 ∖ {𝐾}) ∖ {𝑁}) |
| 20 | 3, 19 | eqtri 2765 |
. . . . . . . . . 10
⊢ (𝑉 ∖ {𝑁, 𝐾}) = ((𝑉 ∖ {𝐾}) ∖ {𝑁}) |
| 21 | 20 | eleq2i 2833 |
. . . . . . . . 9
⊢ (𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾}) ↔ 𝑛 ∈ ((𝑉 ∖ {𝐾}) ∖ {𝑁})) |
| 22 | | eldifsn 4786 |
. . . . . . . . 9
⊢ (𝑛 ∈ ((𝑉 ∖ {𝐾}) ∖ {𝑁}) ↔ (𝑛 ∈ (𝑉 ∖ {𝐾}) ∧ 𝑛 ≠ 𝑁)) |
| 23 | 21, 22 | bitri 275 |
. . . . . . . 8
⊢ (𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾}) ↔ (𝑛 ∈ (𝑉 ∖ {𝐾}) ∧ 𝑛 ≠ 𝑁)) |
| 24 | 23 | simplbi 497 |
. . . . . . 7
⊢ (𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾}) → 𝑛 ∈ (𝑉 ∖ {𝐾})) |
| 25 | | eleq2 2830 |
. . . . . . 7
⊢ ((𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾}) → (𝑛 ∈ (𝐺 NeighbVtx 𝐾) ↔ 𝑛 ∈ (𝑉 ∖ {𝐾}))) |
| 26 | 24, 25 | imbitrrid 246 |
. . . . . 6
⊢ ((𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾}) → (𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾}) → 𝑛 ∈ (𝐺 NeighbVtx 𝐾))) |
| 27 | 26 | adantl 481 |
. . . . 5
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) → (𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾}) → 𝑛 ∈ (𝐺 NeighbVtx 𝐾))) |
| 28 | 27 | imp 406 |
. . . 4
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑁 ∈
𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾})) → 𝑛 ∈ (𝐺 NeighbVtx 𝐾)) |
| 29 | 4, 5, 6, 7 | nbupgrres 29381 |
. . . 4
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾})) → (𝑛 ∈ (𝐺 NeighbVtx 𝐾) → 𝑛 ∈ (𝑆 NeighbVtx 𝐾))) |
| 30 | 18, 28, 29 | sylc 65 |
. . 3
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑁 ∈
𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾})) → 𝑛 ∈ (𝑆 NeighbVtx 𝐾)) |
| 31 | 14, 30 | eqelssd 4005 |
. 2
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) → (𝑆 NeighbVtx 𝐾) = (𝑉 ∖ {𝑁, 𝐾})) |
| 32 | 31 | ex 412 |
1
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) → ((𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾}) → (𝑆 NeighbVtx 𝐾) = (𝑉 ∖ {𝑁, 𝐾}))) |