Step | Hyp | Ref
| Expression |
1 | | eqid 2651 |
. . . . . 6
⊢
(Vtx‘𝑆) =
(Vtx‘𝑆) |
2 | 1 | nbgrssovtx 26302 |
. . . . 5
⊢ (𝑆 NeighbVtx 𝐾) ⊆ ((Vtx‘𝑆) ∖ {𝐾}) |
3 | | difpr 4366 |
. . . . . 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 26248 |
. . . . . . . . 9
⊢
(Vtx‘𝑆) =
(𝑉 ∖ {𝑁}) |
9 | 8 | eqcomi 2660 |
. . . . . . . 8
⊢ (𝑉 ∖ {𝑁}) = (Vtx‘𝑆) |
10 | 9 | a1i 11 |
. . . . . . 7
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) → (𝑉 ∖ {𝑁}) = (Vtx‘𝑆)) |
11 | 10 | difeq1d 3760 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) → ((𝑉 ∖ {𝑁}) ∖ {𝐾}) = ((Vtx‘𝑆) ∖ {𝐾})) |
12 | 3, 11 | syl5eq 2697 |
. . . . 5
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) → (𝑉 ∖ {𝑁, 𝐾}) = ((Vtx‘𝑆) ∖ {𝐾})) |
13 | 2, 12 | syl5sseqr 3687 |
. . . 4
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) → (𝑆 NeighbVtx 𝐾) ⊆ (𝑉 ∖ {𝑁, 𝐾})) |
14 | 13 | adantr 480 |
. . 3
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) → (𝑆 NeighbVtx 𝐾) ⊆ (𝑉 ∖ {𝑁, 𝐾})) |
15 | | simpl 472 |
. . . . . . . 8
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) → ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}))) |
16 | 15 | anim1i 591 |
. . . . . . 7
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑁 ∈
𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾})) → (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾}))) |
17 | | df-3an 1056 |
. . . . . . 7
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾})) ↔ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾}))) |
18 | 16, 17 | sylibr 224 |
. . . . . 6
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑁 ∈
𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾})) → ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾}))) |
19 | | dif32 3924 |
. . . . . . . . . . . . 13
⊢ ((𝑉 ∖ {𝑁}) ∖ {𝐾}) = ((𝑉 ∖ {𝐾}) ∖ {𝑁}) |
20 | 3, 19 | eqtri 2673 |
. . . . . . . . . . . 12
⊢ (𝑉 ∖ {𝑁, 𝐾}) = ((𝑉 ∖ {𝐾}) ∖ {𝑁}) |
21 | 20 | eleq2i 2722 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾}) ↔ 𝑛 ∈ ((𝑉 ∖ {𝐾}) ∖ {𝑁})) |
22 | | eldifsn 4350 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ((𝑉 ∖ {𝐾}) ∖ {𝑁}) ↔ (𝑛 ∈ (𝑉 ∖ {𝐾}) ∧ 𝑛 ≠ 𝑁)) |
23 | 21, 22 | bitri 264 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾}) ↔ (𝑛 ∈ (𝑉 ∖ {𝐾}) ∧ 𝑛 ≠ 𝑁)) |
24 | 23 | simplbi 475 |
. . . . . . . . 9
⊢ (𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾}) → 𝑛 ∈ (𝑉 ∖ {𝐾})) |
25 | | eleq2 2719 |
. . . . . . . . 9
⊢ ((𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾}) → (𝑛 ∈ (𝐺 NeighbVtx 𝐾) ↔ 𝑛 ∈ (𝑉 ∖ {𝐾}))) |
26 | 24, 25 | syl5ibr 236 |
. . . . . . . 8
⊢ ((𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾}) → (𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾}) → 𝑛 ∈ (𝐺 NeighbVtx 𝐾))) |
27 | 26 | adantl 481 |
. . . . . . 7
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) → (𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾}) → 𝑛 ∈ (𝐺 NeighbVtx 𝐾))) |
28 | 27 | imp 444 |
. . . . . 6
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑁 ∈
𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾})) → 𝑛 ∈ (𝐺 NeighbVtx 𝐾)) |
29 | 4, 5, 6, 7 | nbupgrres 26310 |
. . . . . 6
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾})) → (𝑛 ∈ (𝐺 NeighbVtx 𝐾) → 𝑛 ∈ (𝑆 NeighbVtx 𝐾))) |
30 | 18, 28, 29 | sylc 65 |
. . . . 5
⊢
(((((𝐺 ∈
UPGraph ∧ 𝑁 ∈
𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) ∧ 𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾})) → 𝑛 ∈ (𝑆 NeighbVtx 𝐾)) |
31 | 30 | ralrimiva 2995 |
. . . 4
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) → ∀𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾})𝑛 ∈ (𝑆 NeighbVtx 𝐾)) |
32 | | dfss3 3625 |
. . . 4
⊢ ((𝑉 ∖ {𝑁, 𝐾}) ⊆ (𝑆 NeighbVtx 𝐾) ↔ ∀𝑛 ∈ (𝑉 ∖ {𝑁, 𝐾})𝑛 ∈ (𝑆 NeighbVtx 𝐾)) |
33 | 31, 32 | sylibr 224 |
. . 3
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) → (𝑉 ∖ {𝑁, 𝐾}) ⊆ (𝑆 NeighbVtx 𝐾)) |
34 | 14, 33 | eqssd 3653 |
. 2
⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) ∧ (𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾})) → (𝑆 NeighbVtx 𝐾) = (𝑉 ∖ {𝑁, 𝐾})) |
35 | 34 | ex 449 |
1
⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) → ((𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾}) → (𝑆 NeighbVtx 𝐾) = (𝑉 ∖ {𝑁, 𝐾}))) |